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