From c47ba76407c5c364fb91e1d43e8c3f3e9ca38ef9 Mon Sep 17 00:00:00 2001
From: Olivier <olivier.martinot@inria.fr>
Date: Fri, 27 Jan 2023 15:50:09 +0100
Subject: [PATCH] [FTypeChecker] More informative error message (and more
robust code) when typechecking variants.
---
client/Datatype.ml | 26 +++++++++++++-------------
client/Datatype.mli | 2 ++
client/FPrinter.ml | 13 +++++++++++--
client/FTypeChecker.ml | 21 +++++++++++++++++----
client/FTypeChecker.mli | 3 +++
client/test/TestF.ml | 9 +++++++++
6 files changed, 55 insertions(+), 19 deletions(-)
diff --git a/client/Datatype.ml b/client/Datatype.ml
index 5e3537f..d96d50b 100644
--- a/client/Datatype.ml
+++ b/client/Datatype.ml
@@ -46,6 +46,8 @@ module Env = struct
}
exception UnexpectedRecord
+ exception DeclarationNotFound of tyconstr_id
+ exception LabelNotFound of label_id
let empty = {
datatypes = TyConstrMap.empty;
@@ -64,19 +66,17 @@ module Env = struct
labels = add_labels e.labels tdescr.labels_descr;
}
- let find_label { labels ; _ } (Label l) =
- LabelMap.find (Label l) labels
-
- let find_decl { datatypes ; _ } (Type tid) =
- TyConstrMap.find (Type tid) datatypes
-
- let label_index { labels_descr ; _ } l =
- let combine i ldescr = (i, ldescr.label_name) in
- List.mapi combine labels_descr
- |> List.find (fun (_, l') -> l = l')
- |> fst
-
- let () = ignore label_index
+ let find_label { labels ; _ } label =
+ try
+ LabelMap.find label labels
+ with Not_found ->
+ raise (LabelNotFound label)
+
+ let find_decl { datatypes ; _ } tid =
+ try
+ TyConstrMap.find tid datatypes
+ with Not_found ->
+ raise (DeclarationNotFound tid)
let map (type b1 b2 t1 t2)
(f : (b1, t1) decl -> (b2, t2) decl)
diff --git a/client/Datatype.mli b/client/Datatype.mli
index 81a632a..8c87bca 100644
--- a/client/Datatype.mli
+++ b/client/Datatype.mli
@@ -34,6 +34,8 @@ module Env : sig
type ('b, 't) t
exception UnexpectedRecord
+ exception DeclarationNotFound of tyconstr_id
+ exception LabelNotFound of label_id
val empty: ('b, 't) t
val add_decl: ('b, 't) t -> ('b, 't) decl -> ('b, 't) t
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index 36c56fb..c48ede5 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -216,5 +216,14 @@ let print_type_error e =
str "Scope error." ++
str "The variable %s is bound twice in a pattern." x
| ContextNotAbsurd ->
- str "Type error." ++
- str "The type equations in the typing environment are not contradictory."
+ str "Type error." ++
+ str "The type equations in the typing environment are not contradictory."
+ | UnexpectedRecord ->
+ str "Type error." ++
+ str "A record was expected."
+ | DeclarationNotFound (Datatype.Type tid) ->
+ str "Scope error." ++
+ str "Unknown type declaration : %s." tid
+ | LabelNotFound (Datatype.Label lid) ->
+ str "Scope error." ++
+ str "Unknown variant constructor : %s." lid
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 6084e76..23c22b3 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -11,6 +11,10 @@ type type_error =
| UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
+ | UnexpectedRecord
+ | DeclarationNotFound of Datatype.tyconstr_id
+ | LabelNotFound of Datatype.label_id
+
and arity_requirement = Index of int | Total of int
@@ -469,9 +473,17 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
and typeof_variant datatype_env lbl (tid, tyargs) =
let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
- Datatype.Env.find_decl datatype_env tid in
+ try
+ Datatype.Env.find_decl datatype_env tid
+ with Datatype.Env.DeclarationNotFound _ ->
+ raise (TypeError (DeclarationNotFound tid))
+ in
let Datatype.{ arg_type; _ } =
- List.find (fun l -> l.Datatype.label_name = lbl) labels_descr in
+ try
+ List.find (fun l -> l.Datatype.label_name = lbl) labels_descr
+ with Datatype.Env.LabelNotFound _ ->
+ raise (TypeError (LabelNotFound lbl))
+ in
begin
match data_kind with
| Datatype.Variant ->
@@ -517,6 +529,7 @@ let typeof datatype_env t =
let typeof_result datatype_env u =
match typeof datatype_env u with
- | v -> Ok v
+ | v ->
+ Ok v
| exception TypeError e ->
- Error e
+ Error e
diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli
index 047252e..92324a9 100644
--- a/client/FTypeChecker.mli
+++ b/client/FTypeChecker.mli
@@ -13,6 +13,9 @@ type type_error =
| UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
+ | UnexpectedRecord
+ | DeclarationNotFound of Datatype.tyconstr_id
+ | LabelNotFound of Datatype.label_id
(* An arity-related requirement on a certain (sum or product) type
arising during type-checking:
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 7a766df..985baf9 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -115,6 +115,14 @@ let option_env =
in
Datatype.Env.add_decl Datatype.Env.empty option_typedecl
+(* We test this example in an empty datatype environment. It should raise
+ an error indicating that it did not find the label. *)
+let not_in_env =
+ let alpha = 0 in
+ let label = Datatype.Label "None" in
+ let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+ variant label datatype unit
+
(* None *)
let none =
let alpha = 0 in
@@ -645,6 +653,7 @@ let test_suite =
"test F ast",
[ test_ok_from_ast "let prod" Datatype.Env.empty let_prod;
test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
+ test_type_error "not in env" Datatype.Env.empty not_in_env;
test_ok_from_ast "unit" option_env unit;
test_ok_from_ast "none" option_env none;
test_ok_from_ast "some" option_env some;
--
GitLab