From 2025ded107e8b7a6426d0cb40b9dfd26bee5f4cb Mon Sep 17 00:00:00 2001 From: Olivier <olivier.martinot@inria.fr> Date: Thu, 26 Jan 2023 14:15:41 +0100 Subject: [PATCH 1/2] [binding_pattern] add new bindings directly in the environment. --- client/DeBruijn.ml | 15 ---------- client/DeBruijn.mli | 5 ---- client/FTypeChecker.ml | 68 +++++++++++------------------------------- 3 files changed, 17 insertions(+), 71 deletions(-) diff --git a/client/DeBruijn.ml b/client/DeBruijn.ml index 6eb3c74..16a75ea 100644 --- a/client/DeBruijn.ml +++ b/client/DeBruijn.ml @@ -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 (* -------------------------------------------------------------------------- *) diff --git a/client/DeBruijn.mli b/client/DeBruijn.mli index 0c3e761..7b85c28 100644 --- a/client/DeBruijn.mli +++ b/client/DeBruijn.mli @@ -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 (* -------------------------------------------------------------------------- *) diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml index 6084e76..1858236 100644 --- a/client/FTypeChecker.ml +++ b/client/FTypeChecker.ml @@ -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 -- GitLab From 1083149b06152d3e6ef24c36a7838e9aca23004b Mon Sep 17 00:00:00 2001 From: Olivier <olivier.martinot@inria.fr> Date: Fri, 27 Jan 2023 14:53:33 +0100 Subject: [PATCH 2/2] Add tests for pattern-matching. --- client/test/TestF.ml | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/client/test/TestF.ml b/client/test/TestF.ml index 7a766df..1c54e8d 100644 --- a/client/test/TestF.ml +++ b/client/test/TestF.ml @@ -83,7 +83,7 @@ let let_prod = (app (var p) (tuple [])) (app (var f) (var x)) -(* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *) +(* Λαβ. λx:{α*β}. match x with (_, y) -> y end *) let match_with_prod = let alpha, beta = 1, 0 in tyabs alpha @@ @@ -93,6 +93,15 @@ let match_with_prod = (ptuple [ pwildcard ; pvar "y" ]) , var"y" ] +(* Λα. λx:{α*α}. match x with (y, y) -> y end *) +let match_variable_bound_twice = + let alpha = 0 in + tyabs alpha @@ + abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar alpha ]) @@ + match_ (F.TyVar alpha) (var "x") [ + (ptuple [ pvar "y" ; pvar "y" ]) , var"y" + ] + (* option *) let option_env = let option_typedecl = @@ -157,6 +166,25 @@ let match_none = (some_pattern , unit); ] +(* Λα. λx:α. + match (x,Some x) with + | (y, None) -> y + | (y,Some y) -> y + end + *) +let match_variable_bound_twice_under_tuple = + let alpha = 0 in + let none_label = Datatype.Label "None" in + let some_label = Datatype.Label "Some" in + let datatype = Datatype.Type "option", [ F.TyVar alpha ] in + tyabs alpha @@ + abs "x" (F.TyVar alpha) @@ + match_ (F.TyVar alpha) + (tuple [var "x"; variant some_label datatype (var "x")]) [ + (ptuple [ pvar "y" ; pvariant none_label datatype unit_pattern ]) , var"y" ; + (ptuple [ pvar "y" ; pvariant some_label datatype (pvar "y") ]) , var"y" + ] + (* ( refl_{} : Eq(∀α.{} , {}) ) *) let type_eq = let alpha = 0 in @@ -645,12 +673,17 @@ 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 "match variable bound twice" Datatype.Env.empty + match_variable_bound_twice; test_ok_from_ast "unit" option_env unit; test_ok_from_ast "none" option_env none; test_ok_from_ast "some" option_env some; test_ok_from_ast "match none" option_env match_none; + test_type_error "match deep variable bound twice" option_env + match_variable_bound_twice_under_tuple; test_type_error "type equality" Datatype.Env.empty type_eq; - test_ok_from_ast "introduce type equality" Datatype.Env.empty introduce_type_eq; + test_ok_from_ast "introduce type equality" Datatype.Env.empty + introduce_type_eq; test_ok_from_ast "symmetry" Datatype.Env.empty sym; test_ok_from_ast "transitivity" Datatype.Env.empty trans; test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall; -- GitLab