Implementend Generator, does not work

src/Generator.ml

@@ -8,19 +8,33 @@ module Make(M : Utils.MonadPlus) = struct
   module TeVarSet = Untyped.Var.Set
   module TyVarSet = STLC.TyVar.Set
 
+let rec applyn n f acc =
+  if n <= 0 then acc else applyn (pred n) f (f acc)
 
 let untyped : Untyped.term =
   (* This definition is *not* a good solution,
      but it could give you a flavor of possible definitions. *)
-  let rec gen () : Untyped.term =
+  let rec gen (env: TeVarSet.t) : Untyped.term =
     let open Untyped in
+    let var1,var2,var3 = Var.fresh "z",[Var.fresh "t";Var.fresh "t"],[Var.fresh "t";Var.fresh "t";Var.fresh "t"] in
+    let nenv1,nenv2,nenv3 = TeVarSet.add var1 env,TeVarSet.add_seq (List.to_seq var2) env,TeVarSet.add_seq (List.to_seq var3) env in
     Do (M.delay @@ fun () ->
-      M.sum [
+      M.sum (List.append
-        M.return (App(gen (), gen ())); (* try to generate applications... *)
+        (List.map (fun v -> M.return (Var(v))) (TeVarSet.to_list env))
-        M.delay (Utils.not_yet "Generator.untyped"); (* ... or fail *)
+        [
-      ]
+          M.return (Abs(var1,gen nenv1));
+          M.return (App(gen env, gen env));
+          M.return (Let(var1,gen env, gen nenv1));
+          (*M.return (Annot(nvar,gen env, gen nenv));*)
+          M.return (Tuple([gen env;gen env]));
+          M.return (Tuple([gen env;gen env;gen env]));
+          M.return (LetTuple(var2,gen env,gen nenv2));
+          M.return (LetTuple(var3,gen env,gen nenv3));
+          M.delay (fun () -> M.fail); (* ... or fail *)
+        ]
+      )
     )
-  in gen ()
+  in gen TeVarSet.empty
 
 let constraint_ : (STLC.term, Infer.err) Constraint.t =
   let w = Constraint.Var.fresh "final_type" in
@@ -30,7 +44,7 @@ let constraint_ : (STLC.term, Infer.err) Constraint.t =
       untyped
       w))
 
-let typed ~depth =
+let typed ~depth : STLC.term M.t =
   (* This definition uses [constraint_] to generate well-typed terms.
      An informal description of a possible way to do this is described
      in the README, Section "Two or three effect instances", where
@@ -46,6 +60,22 @@ let typed ~depth =
      > can be reached by expanding `Do` nodes *at most* `depth` times, but
      > this typically gives a worse generator.)
   *)
-  Utils.not_yet "Generator.typed" depth
+  let extractor (con: (STLC.term, Infer.err) Constraint.t) : STLC.term M.t =
+    let _,env,ncon = Solver.eval ~log:false Unif.Env.empty con in
+    begin match ncon with
+    | NRet x -> M.return (x (fun v -> Decode.decode env v))
+    | NErr _ -> M.fail
+    | NDo _ -> M.fail
+    end in
+  let cstep (con: (STLC.term, Infer.err) Constraint.t) : (STLC.term, Infer.err) Constraint.t M.t =
+    let _,_,ncon = Solver.eval ~log:false Unif.Env.empty con in
+    begin match ncon with
+    (* The first case should never happen because the Do's expand indefinitely *)
+    | NRet x -> M.return (Constraint.Ret(x))
+    | NErr _ -> M.fail
+    | NDo d -> d
+    end
+  in
+  M.bind (applyn depth (fun acc -> M.bind acc cstep) (M.return constraint_)) extractor
 
-end
+end

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,10 +43,33 @@ 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 =
+  let rec bind : type a . STLC.ty -> (Constraint.variable -> (a, err) t) -> (a, err) t =
-    (* Feel free to postpone implementing this function
+    fun ty k ->
-       until you implement the Annot case below. *)
+    match ty with
-    Utils.not_yet "Infer.bind" (ty, k, fun () -> bind)
+    | 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,
+        Exist(bp,None,
+        Map(
+          Conj(
+            bind ta (fun x -> eq x ap),
+            Conj(
+              bind tb (fun x -> eq x bp),
+              Exist(w,Some (Structure.Arrow (ap,bp)),k w)
+            )
+          ),
+          fun ((),((),t)) -> t
+        )))
+    | Constr Prod l -> 
+        let w = Var.fresh "w" in
+        let arr = List.map (fun ty -> (ty,Var.fresh "t")) l in
+        List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr (
+          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)
+          ))
 
   (** This function generates a typing constraint from an untyped term:
       [has_type env t w] generates a constraint [C] which contains [w] as
@@ -89,34 +104,93 @@ 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,tau = Var.fresh "a", Var.fresh "τ" in
+      Exist(a,None,
+      Exist(tau,Some (Arrow(a,w)),
+        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,
-          Map(Conj(
+        Exist(b,None,
-            has_type newenv t b,
+          Map(
-            eq tau w
+            Conj(
-          ), fun t -> let (x,_) = p in x) (* term * unit -> term isomorphism *)
+              Conj(
-        )
+                has_type newenv t b,
+                Exist(tau,Some (Arrow (a,b)),eq tau w) 
+              ),
+              decode a
+            ),
+            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) ->
-      Utils.not_yet "Infer.has_type: Let case" (env, t, ty, bind, fun () -> has_type)
+        Map(
+          bind ty (fun ww -> Map(Conj(eq w ww,has_type env t ww),snd)),
+          fun tt -> STLC.Annot(tt,ty)
+        )
     | Untyped.Tuple ts ->
-      let (t1, t2) = assume_pair ts in
+      let ww = Var.fresh "w" in
-      Utils.not_yet "Infer.has_type: Let case" (env, t1, t2, fun () -> has_type)
+      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
+      let a = Var.fresh "a" in
-      Utils.not_yet "Infer.has_type: Let case" (env, x1, x2, t, u, fun () -> has_type)
+      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
          work on all the other cases is a good first step. *)
-      Utils.not_yet "Infer.has_type: Let case" (env, p, fun () -> has_type)
+      Constraint.Do (T.map (fun z -> has_type env z w) p)
 end

src/MSeq.ml

@@ -1,25 +1,24 @@
-type 'a t = MSeq_not_implemented_yet
+type 'a t = 'a Seq.t
 
 let map (f : 'a -> 'b) (s : 'a t) : 'b t =
-  Utils.not_yet "MSeq.map" (f, s)
+  Seq.map f s
 
 let return (x : 'a) : 'a t =
-  Utils.not_yet "MSeq.return" x
+  Seq.return x
 
 let bind (sa : 'a t) (f : 'a -> 'b t) : 'b t =
-  Utils.not_yet "MSeq.bind" (sa, f)
+  Seq.concat_map f sa
 
 let delay (f : unit -> 'a t) : 'a t =
-  Utils.not_yet "MSeq.delay" f
+  fun () -> f () () (* f is already «delayed» form *)
 
 let sum (li : 'a t list) : 'a t =
-  Utils.not_yet "MSeq.sum" li
+  Seq.concat (List.to_seq li)
 
-let fail : 'a t =
+let fail : 'a t = Seq.empty
-  MSeq_not_implemented_yet
 
 let one_of (vs : 'a array) : 'a t =
   Utils.not_yet "MSeq.one_of" vs
 
 let run (s : 'a t) : 'a Seq.t =
-  Utils.not_yet "MSeq.run" s
+  s

src/Solver.ml

@@ -37,9 +37,9 @@ module Make (T : Utils.Functor) = struct
     | NErr of 'e
     | NDo of ('a, 'e) Constraint.t T.t
 
-  let eval (type a e) ~log (env : env) (c0 : (a, e) Constraint.t)
+  let eval (type a e) ~log (env0 : env) (c0 : (a, e) Constraint.t)
     : log * env * (a, e) normal_constraint
-  =
+  = 
     let add_to_log, get_log =
       if log then make_logger c0
       else ignore, (fun _ -> [])
@@ -57,6 +57,52 @@ module Make (T : Utils.Functor) = struct
        (You can also tweak this code temporarily to print stuff on
        stderr right away if you need dirtier ways to debug.)
     *)
-    Utils.not_yet "Solver.eval" (env, c0, add_to_log, get_log)
+    let env = ref env0 in
-
+    let rec evalc : type aa ee. (aa,ee) Constraint.t -> (aa, ee) normal_constraint = 
+      function
+      | Ret(a) -> NRet a
+      | Err(e) -> NErr e
+      | Map(c, f) -> 
+          begin match (evalc c) with
+          | NRet a -> NRet (fun ctx -> (f (a ctx)))
+          | NErr e -> NErr e
+          | NDo act -> NDo (T.map (fun c -> Constraint.Map(c,f)) act)
+          end
+      | MapErr(c, f) ->
+          begin match (evalc c) with
+          | NRet a -> NRet a
+          | NErr e -> NErr (f e)
+          | NDo act -> NDo (T.map (fun c -> Constraint.MapErr(c,f)) act)
+          end
+      | Conj(c,d) -> 
+          begin match (evalc c) with
+          | NRet a ->
+            begin match (evalc d) with
+            | NRet b -> NRet (fun ctx -> (a ctx,b ctx))
+            | NErr e -> NErr e
+            | NDo act2 -> NDo (T.map (fun d -> Constraint.Conj(c,d)) act2)
+            end
+          | NErr e -> NErr e
+          | NDo act1 -> NDo (T.map (fun c -> Constraint.Conj(c,d)) act1)
+          end
+      | Eq(x,y) -> 
+          begin match (Unif.unify (!env) x y) with
+          | Ok(a) -> 
+              env := a;
+              add_to_log (!env);
+              NRet (fun _ -> ()) (* We return unit *)
+            | Error(Clash(x,y)) -> 
+              let xt,yt = Decode.decode (!env) x, Decode.decode (!env) y in
+              NErr(Clash(xt,yt))
+            | Error(Cycle(x)) -> NErr (Cycle(x))
+          end
+      | Exist(x,s,c) -> 
+          env := Unif.Env.add x s !env;
+          add_to_log (!env);
+          evalc c
+      | Decode(v) -> NRet (fun _ -> Decode.decode (!env) v)
+      | Do(act) -> NDo act
+    in
+    let out = evalc c0 in
+    (get_log (), !env, out)
 end

src/Structure.ml

@@ -46,7 +46,11 @@ let map f = function
   | Prod ts -> Prod (List.map f ts)
 
 let merge f s1 s2 =
-    Utils.not_yet "Structure.merge" (f, s1, s2)
+    match (s1,s2) with
+    | Var(x),Var(y) -> if x=y then Some(Var(x)) else None
+    | Arrow(s,t),Arrow(u,v) -> Some(Arrow(f s u, f t v))
+    | Prod(t),Prod(u) -> Some(Prod(List.map2 f t u))
+    | _ -> None
 
 let global_tyvar : string -> TyVar.t =
   (* There are no binders for type variables, which are scoped

tests.t/trifun.test

@@ -0,0 +1 @@
+lambda f. lambda x. lambda y. f x y

tests.t/tuple-inversion.test

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