[binding_pattern] add new bindings directly in the environment.
This commit is contained in:
parent
f3f73388db
commit
2025ded107
|
@ -79,21 +79,6 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
|
|||
let current = current + 1 in
|
||||
{ map; current }
|
||||
|
||||
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
|
||||
bindings of [env2] shadow any binding of the same variable in [env1]. *)
|
||||
|
||||
let concat env1 env2 =
|
||||
(* We need to shift the de Bruijn levels of [env2] (and its
|
||||
[current] value) by as many bindings as there are in [env1]. *)
|
||||
let shift _x in1 in2 =
|
||||
match in2 with
|
||||
| None -> in1
|
||||
| Some lvl -> Some (env1.current + lvl)
|
||||
in
|
||||
{
|
||||
current = env1.current + env2.current;
|
||||
map = M.merge shift env1.map env2.map;
|
||||
}
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -49,11 +49,6 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
|
|||
to [slide (bump env) x]. *)
|
||||
|
||||
val bump: env -> env
|
||||
|
||||
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
|
||||
bindings of [env2] shadow any binding of the same variable in [env1]. *)
|
||||
|
||||
val concat: env -> env -> env
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -117,6 +117,11 @@ let extend_with_tevar { types; names; equations } x ty =
|
|||
names = N2DB.slide names x;
|
||||
equations; }
|
||||
|
||||
let extend_with_tevar_no_dup ({ types; _ } as env) x ty =
|
||||
if TermVarMap.mem x types then
|
||||
raise (TypeError (TwoOccurencesOfSameVariable x));
|
||||
extend_with_tevar env x ty
|
||||
|
||||
let extend_with_tyvar { types; names; equations } =
|
||||
match equations with
|
||||
| Inconsistent ->
|
||||
|
@ -130,41 +135,6 @@ let extend_with_tyvar { types; names; equations } =
|
|||
let names = N2DB.bump names in
|
||||
{ types; names ; equations = Equations { store ; tyvars } }
|
||||
|
||||
let singleton x ty =
|
||||
extend_with_tevar empty x ty
|
||||
|
||||
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
|
||||
match (env1.equations, env2.equations) with
|
||||
| Inconsistent,_ | _, Inconsistent ->
|
||||
{ types; names; equations = Inconsistent }
|
||||
| Equations { store = store1; tyvars = tyvars1 },
|
||||
Equations { store = store2; tyvars = tyvars2 } ->
|
||||
assert (store1 == store2);
|
||||
let store = store1 in
|
||||
let tyvars = tyvars1 @ tyvars2 in
|
||||
{ types; names; equations = Equations { store; tyvars} }
|
||||
|
||||
let concat_disjoint env1 env2 =
|
||||
let exception Conflict of TermVarMap.key in
|
||||
try
|
||||
let combine x _ _ =
|
||||
raise (Conflict x) in
|
||||
let types = TermVarMap.union combine env1.types env2.types in
|
||||
let names = N2DB.concat env1.names env2.names in
|
||||
match (env1.equations, env2.equations) with
|
||||
| Inconsistent,_ | _, Inconsistent ->
|
||||
Ok { types; names; equations = Inconsistent }
|
||||
| Equations { store = store1; tyvars = tyvars1 },
|
||||
Equations { store = store2; tyvars = tyvars2 } ->
|
||||
assert (store1 == store2);
|
||||
let store = store1 in
|
||||
let tyvars = tyvars1 @ tyvars2 in
|
||||
Ok { types; names; equations = Equations { store; tyvars } }
|
||||
with Conflict x -> Error x
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Destructors. *)
|
||||
|
@ -483,34 +453,30 @@ and typeof_variant datatype_env lbl (tid, tyargs) =
|
|||
Type.subst ty 0 arg_type
|
||||
) tyargs type_params arg_type
|
||||
|
||||
and typeof_branch datatype_env env scrutinee_ty (pat, rhs) =
|
||||
let new_bindings = binding_pattern datatype_env env scrutinee_ty pat in
|
||||
let new_env = concat env new_bindings in
|
||||
and typeof_branch datatype_env env scrutinee_ty (pat, rhs) : debruijn_type =
|
||||
let new_env = binding_pattern datatype_env env scrutinee_ty pat in
|
||||
typeof datatype_env new_env rhs
|
||||
|
||||
and binding_pattern datatype_env env scrutinee_ty pat =
|
||||
let binding_pattern = binding_pattern datatype_env env in
|
||||
and binding_pattern datatype_env env scrutinee_ty pat : env =
|
||||
let binding_pattern = binding_pattern datatype_env in
|
||||
match pat with
|
||||
| PVar (_, x) ->
|
||||
singleton x scrutinee_ty
|
||||
extend_with_tevar_no_dup env x scrutinee_ty
|
||||
| PWildcard _ ->
|
||||
empty
|
||||
env
|
||||
| PAnnot (_, pat, ty) ->
|
||||
enforce_equal env scrutinee_ty ty;
|
||||
binding_pattern ty pat
|
||||
binding_pattern env ty pat
|
||||
| PTuple (_, ps) ->
|
||||
let tys = as_product scrutinee_ty in
|
||||
let envs = List.map2 binding_pattern tys ps in
|
||||
let f env1 env2 =
|
||||
match concat_disjoint env1 env2 with
|
||||
| Ok env -> env
|
||||
| Error x -> raise (TypeError (TwoOccurencesOfSameVariable x))
|
||||
in
|
||||
List.fold_left f empty envs
|
||||
if List.length ps <> List.length tys then
|
||||
raise
|
||||
(TypeError (ArityMismatch (Total (List.length ps), scrutinee_ty)));
|
||||
List.fold_left2 binding_pattern env tys ps
|
||||
| PVariant (_, lbl, dty, pat) ->
|
||||
let arg_type = typeof_variant datatype_env lbl dty in
|
||||
enforce_equal env scrutinee_ty (TyConstr dty);
|
||||
binding_pattern arg_type pat
|
||||
binding_pattern env arg_type pat
|
||||
|
||||
let typeof datatype_env t =
|
||||
typeof datatype_env empty t
|
||||
|
|
Loading…
Reference in New Issue