diff --git a/client/Datatype.ml b/client/Datatype.ml
index 909b54615f03790043f25653f8164a07e0a3d7f6..d96d50bace05ab18bab302dce67cfaa4cd37d5d0 100644
--- a/client/Datatype.ml
+++ b/client/Datatype.ml
@@ -1,5 +1,5 @@
-(* tyconstr_id is the name of an datatype constructor.
- label_id is the name of a field label or data constructor. *)
+(* [tyconstr_id] is the name of an datatype constructor.
+ [label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@@ -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 9f5515807a18203b6904780b80882c51dcd2b611..8c87bcab12232ca4112161351a8f769f98a5d83c 100644
--- a/client/Datatype.mli
+++ b/client/Datatype.mli
@@ -1,5 +1,5 @@
-(* tyconstr_id is the name of an datatype constructor.
- label_id is the name of a field label or data constructor. *)
+(* [tyconstr_id] is the name of an datatype constructor.
+ [label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@@ -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 36c56fb25b52a93561e1ac4b91130ffa1a4f1566..c48ede5d6606d58ebcaec1235f7bcd8a5f95f3ea 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 18582366cdece785d5b924018aa1c7f217ee4ce4..d5079d2d7343f71887877792cb2a7b4576f24e86 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
@@ -439,9 +443,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 ->
@@ -483,6 +495,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 047252e8db109cba5535b5bf202aa6a5a87638c3..92324a968b714b08c7e55156cdc2d80c509bf200 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 1c54e8d015c191f0ed93a932d2a0f48370820391..936c16c3747c3a912dfc8b67981e85def521f6d1 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -124,6 +124,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
@@ -675,6 +683,7 @@ let test_suite =
test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
test_type_error "match variable bound twice" Datatype.Env.empty
match_variable_bound_twice;
+ 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;