Merge branch 'master' into 'env-concat'

# Conflicts:
#   client/test/TestF.ml
This commit is contained in:
SCHERER Gabriel 2023-02-02 06:55:13 +00:00
commit 2ab5a617e7
6 changed files with 58 additions and 22 deletions

View File

@ -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_label { labels ; _ } label =
try
LabelMap.find label labels
with Not_found ->
raise (LabelNotFound label)
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_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)

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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:

View File

@ -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;