Added all type inference

src/Infer.ml

@@ -30,14 +30,6 @@ module Make(T : Utils.Functor) = struct
   let eq v1 v2 = Eq(v1, v2)
   let decode v = MapErr(Decode v, fun e -> Cycle e)
 
-  let assume_pair = function
-    | [v1; v2] -> (v1, v2)
-    | other ->
-      Printf.ksprintf failwith
-        "Error: this implementation currently only supports pairs,
-         not tuples of size %d."
-        (List.length other)
-
   (** This is a helper function to implement constraint generation for
       the [Annot] construct.
      
@@ -51,11 +43,12 @@ module Make(T : Utils.Functor) = struct
         [∃(?w1 = ?v2 -> ?v3). ∃(?w2 = ?v1 -> ?w1). k ?w2], or equivalently
         [∃?w3 ?w4. ?w3 = ?v1 -> ?w4 ∧ ?w4 = ?v2 -> ?v3 ∧ k ?w3].
   *)
-  let rec bind (ty : STLC.ty) (k : Constraint.variable -> ('a, 'e) t) : ('a, 'e) t =
-    (* Feel free to postpone implementing this function
-       until you implement the Annot case below. *)
+  let rec bind : type a . STLC.ty -> (Constraint.variable -> (a, err) t) -> (a, err) t =
+    fun ty k ->
     match ty with
-    | Constr Var x -> k x
+    | Constr Var x -> 
+      let w = Var.fresh "w" in
+      Exist(w,Some (Var x),k w)
     | Constr Arrow (ta,tb) ->
         let w,ap,bp = Var.fresh "w",Var.fresh "a",Var.fresh "b" in
         Exist(ap,None,
@@ -77,7 +70,6 @@ module Make(T : Utils.Functor) = struct
           List.fold_right (fun (tt,av) con -> Map(Conj(bind tt (fun x -> eq x av),con),fun ((),t) -> t)) arr (
             Exist(w,Some (Structure.Prod (List.map snd arr)),k w)
           ))
-    end
 
   (** This function generates a typing constraint from an untyped term:
       [has_type env t w] generates a constraint [C] which contains [w] as
@@ -112,36 +104,91 @@ module Make(T : Utils.Functor) = struct
             Exist(a, None, Ret (fun _ -> STLC.Var(x)))
           ) 
           ~some:(
-            fun envt -> Map(eq envt w, fun _ -> STLC.Var(x))
+            fun envt -> Map(eq envt w, fun () -> STLC.Var(x))
           ) 
           (Env.find_opt x env)
       )
     | Untyped.App (t, u) ->
-      Utils.not_yet "Infer.has_type: App case" (env, t, u, fun () -> has_type)
+      let a,b,tau = Var.fresh "a", Var.fresh "b", Var.fresh "τ" in
+      Exist(a,None,
+      Exist(b,None,
+      Exist(tau,Some (Arrow(a,b)),
+        Map(
+          Conj(has_type env t tau,has_type env u a),
+          fun (tt,uu) -> App(tt,uu)
+      ))))
     | Untyped.Abs (x, t) -> 
         let tau,a,b = Var.fresh "τ",Var.fresh "α", Var.fresh "β" in
         let newenv = Env.add x a env in
-        Exist(tau, Some (Arrow(a, b)),
+        Exist(a,None,
+        Exist(b,None,
           Map(
             Conj(
               Conj(
                 has_type newenv t b,
-                eq tau w 
+                Exist(tau,Some (Arrow (a,b)),eq tau w) 
               ),
-              decode tau
+              decode a
             ),
-            fun ((tt,()),ty) -> Abs(x, ty, tt))
-        )
+            fun ((tt,()),ty) -> STLC.Abs(x, ty, tt))
+        ))
     | Untyped.Let (x, t, u) ->
-      Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type)
+      let a,b = Var.fresh "α", Var.fresh "β" in
+        let newenv = Env.add x a env in
+        Exist(a,None,
+        Exist(b,None,
+          Map(
+            Conj(
+              Conj(
+                Conj(
+                  has_type env t a,
+                  has_type newenv u b
+                ),
+                eq w b
+              ),
+              decode a
+            ),
+            fun (((tt,uu),()),ta) -> STLC.Let(x,ta,tt,uu))
+        ))
     | Untyped.Annot (t, ty) ->
-        bind (fun w -> has_type env w) ty
+        Map(
+          bind ty (fun w -> has_type env t w),
+          fun tt -> STLC.Annot(tt,ty)
+        )
     | Untyped.Tuple ts ->
-      let (t1, t2) = assume_pair ts in
-      Utils.not_yet "Infer.has_type: Tuple case" (env, t1, t2, fun () -> has_type)
+      let ww = Var.fresh "w" in
+      let arr = List.map (fun tt -> (tt,Var.fresh "t")) ts in (*On crée une variable par indice du tuple*)
+      List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr ( (*On quantifie sur leur existence*)
+        Map(
+          (List.fold_right (fun (tt,av) con -> Map(Conj(has_type env tt av,con),fun (tt,tl) -> tt::tl)) arr ( (* Que chaque membre a le type attendu *)
+            Map(
+              Exist(ww,Some (Prod (List.map snd arr)),
+                eq w ww
+              ),
+              fun () -> []
+            )
+          )),
+          fun tl -> STLC.Tuple(tl)
+        )
+      )
     | Untyped.LetTuple (xs, t, u) ->
-      let (x1, x2) = assume_pair xs in
-      Utils.not_yet "Infer.has_type: LetTuple case" (env, x1, x2, t, u, fun () -> has_type)
+      let a = Var.fresh "a" in
+      let arr = List.map (fun x -> (x,Var.fresh "t")) xs in (*On crée une variable par variable du tuple*)
+      let newenv = List.fold_right (fun (x,ta) acc -> Env.add x ta acc) arr env in
+      List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr ( (*On quantifie sur leur existence*)
+        Map(
+          List.fold_right (fun (_,tx) acc -> Map(Conj(decode tx,acc),fun (ttx,(tta,ttb,ttl)) -> (tta,ttb,ttx::ttl))) arr (
+            Map(
+              Conj(
+                Exist(a,Some (Prod (List.map snd arr)),has_type env t a),
+                has_type newenv u w
+              ),
+              fun (tta,ttb) -> (tta,ttb,[])
+            )
+          ),
+          fun (tta,ttb,ttl) -> STLC.LetTuple(List.map2 (fun x y -> (x,y)) xs ttl,tta,ttb)
+        )
+      )
     | Do p ->
       (* Feel free to postone this until you start looking
          at random generation. Getting type inference to

tests.t/tuple-inversion.test

@@ -0,0 +1 @@
+lambda p. let (x,y,z) = p in (z,y,x)