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.return (App(gen (), gen ())); (* try to generate applications... *)
-        M.delay (Utils.not_yet "Generator.untyped"); (* ... or fail *)
-      ]
+      M.sum (List.append
+        (List.map (fun v -> M.return (Var(v))) (TeVarSet.to_list env))
+        [
+          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

@@ -192,5 +192,5 @@ module Make(T : Utils.Functor) = struct
       (* 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: Do case" (env, p, fun () -> has_type)
+      Constraint.Do (T.map (fun z -> has_type env z w) p)
 end