[FTypecheker] Inconsistent stores/tyvars are no longer stored in the env.

This commit is contained in:
Olivier 2023-01-22 15:54:10 +01:00
parent 96d629f80a
commit d558af66c4
1 changed files with 84 additions and 56 deletions

View File

@ -70,26 +70,31 @@ and structure =
instead of indices makes the equality test easier. *)
| SForallLevel of int
(* The global store of the union-find. *)
type store = structure option UF.store
(* A mapping from rigid variables to union-find vertices. *)
type tyvars = structure option UF.elem list
(* If the type equations introduced are inconsistent, then no need for
[store] and [tyvars] *)
type consistency =
| Consistent of store * tyvars
| Inconsistent
type env = {
(* A mapping of term variables to types. *)
types: debruijn_type TermVarMap.t;
(* A translation environment of TERM variables to TYPE indices. *)
names: N2DB.env;
(* The global store of the union-find. *)
store: structure option UF.store;
(* A mapping from rigid variables to union-find vertices. *)
tyvars: structure option UF.elem list;
(* Is set to false when an inconsistent equation is introduced in the
environment. It is useful while typechecking pattern-matching. *)
consistent: bool;
(* We keep trace of wheter or not the typing equations is consistent *)
uf_state: consistency
}
let empty = {
types = TermVarMap.empty;
names = N2DB.empty;
store = UF.new_store();
tyvars = [];
consistent = true;
uf_state = Consistent (UF.new_store(), []);
}
let lookup { types; names; _ } x =
@ -105,23 +110,26 @@ let lookup { types; names; _ } x =
(* must have been raised by [TermVarMap.find] *)
raise (TypeError (UnboundTermVariable x))
let extend_with_tevar { types; names; store; tyvars; consistent } x ty =
let extend_with_tevar { types; names; uf_state; } x ty =
(* Map the name [x] to [ty], and record when it was bound, without
incrementing the time. *)
{ types = TermVarMap.add x ty types;
names = N2DB.slide names x;
store;
tyvars;
consistent; }
uf_state; }
let extend_with_tyvar { types; names; store; tyvars; consistent } =
(* Create a fresh vertex for the new type variable *)
let v = UF.make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
let names = N2DB.bump names in
{ types; names ; store; tyvars; consistent }
let extend_with_tyvar { types; names; uf_state; } =
match uf_state with
| Inconsistent ->
(* TODO : verify that it is correct *)
{ types; names; uf_state; }
| Consistent (store, tyvars) ->
(* Create a fresh vertex for the new type variable *)
let v = UF.make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
let names = N2DB.bump names in
{ types; names ; uf_state = Consistent(store,tyvars); }
let singleton x ty =
extend_with_tevar empty x ty
@ -130,10 +138,15 @@ let concat env1 env2 =
let combine _ _ ty2 = Some ty2 in
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
{ types; names; store; tyvars; consistent }
match (env1.uf_state, env2.uf_state) with
| Inconsistent,_ | _, Inconsistent ->
{ types; names; uf_state = Inconsistent }
| Consistent (store1, tyvars1),
Consistent (store2, tyvars2) ->
assert (store1 == store2);
let store = store1 in
let tyvars = tyvars1 @ tyvars2 in
{ types; names; uf_state = Consistent (store, tyvars); }
let concat_disjoint env1 env2 =
let exception Conflict of TermVarMap.key in
@ -142,10 +155,15 @@ let concat_disjoint env1 env2 =
raise (Conflict x) in
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
Ok { types; names; store; tyvars; consistent }
match (env1.uf_state, env2.uf_state) with
| Inconsistent,_ | _, Inconsistent ->
Ok { types; names; uf_state = Inconsistent }
| Consistent (store1, tyvars1),
Consistent (store2, tyvars2) ->
assert (store1 == store2);
let store = store1 in
let tyvars = tyvars1 @ tyvars2 in
Ok { types; names; uf_state = Consistent (store, tyvars); }
with Conflict x -> Error x
(* -------------------------------------------------------------------------- *)
@ -312,14 +330,17 @@ let unify mode store v1 v2 =
unify mode store q v1 v2
let unify_types mode env ty1 ty2 =
not env.consistent ||
try
let v1 = translate ~inside_mu:false env.store env.tyvars ty1
and v2 = translate ~inside_mu:false env.store env.tyvars ty2 in
unify mode env.store v1 v2;
true
with Clash ->
false
match env.uf_state with
| Inconsistent ->
true
| Consistent (store, tyvars) ->
try
let v1 = translate ~inside_mu:false store tyvars ty1
and v2 = translate ~inside_mu:false store tyvars ty2 in
unify mode store v1 v2;
true
with Clash ->
false
(* -------------------------------------------------------------------------- *)
@ -394,27 +415,34 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
List.iter (fun ty2 -> equal env ty ty2) tys;
ty
| Absurd (_, ty) ->
if env.consistent then
raise (TypeError (ContextNotAbsurd))
else
ty
begin
match env.uf_state with
| Inconsistent ->
ty
| Consistent _ ->
raise (TypeError (ContextNotAbsurd))
end
| Refl (_, ty) ->
TyEq (ty, ty)
| Use (_, t, u) ->
let store_copy = UF.copy env.store in
let env = { env with store = store_copy } in
begin
match typeof env t with
| TyEq (ty1, ty2) ->
if consistent env ty1 ty2 then
(* typecheck [u] in a context containing equalities introduced by
the equality ty1 = ty2 *)
typeof env u
else
typeof { env with consistent = false } u
| ty ->
raise (TypeError (NotAnEqual ty))
end
match env.uf_state with
| Inconsistent ->
typeof env u
| Consistent (store, tyvars) ->
let store_copy = UF.copy store in
let env = { env with uf_state = Consistent (store_copy, tyvars) } in
begin
match typeof env t with
| TyEq (ty1, ty2) ->
if consistent env ty1 ty2 then
(* typecheck [u] in a context containing equalities introduced
by the equality ty1 = ty2 *)
typeof env u
else
typeof { env with uf_state = Inconsistent } u
| ty ->
raise (TypeError (NotAnEqual ty))
end
and typeof_variant datatype_env lbl (tid, tyargs) =
let Datatype.{ data_kind ; type_params ; labels_descr; _ } =