Implementend Generator, does not work

Reported-by: Mathis Bouverot-Dupuis

.gitignore

@@ -0,0 +1,2 @@
+_build/
+_opam/

README.md

@@ -118,6 +118,20 @@ $ eval $(opam env)
 
 To configure your favorite text editor, see the [Real World OCaml setup](http://dev.realworldocaml.org/install.html#editor-setup).
 
+#### Tip on GADTs in OCaml
+
+The type of constraints is a GADT, a Generalized (or Guarded)
+Algebraic Datatype. Writing functions that operate on these datatypes
+requires a bit more ceremony than everyday OCaml code, due to their
+inherent use of polymorphic recursion.
+
+If you are unfamiliar with function declarations that look like
+
+    let rec foo : type a e . (a, e) t -> ...
+
+then you should read the GADT chapter of the OCaml manual:
+  https://v2.ocaml.org/releases/5.1/htmlman/gadts-tutorial.html
+
 ### Using a different language
 
 We wrote useful support code in OCaml, so it is going to be much
@@ -359,7 +373,7 @@ you prefer).
 
 - `src/`: the bulk of the code, that place where we expect you to
    work. `src/*.{ml,mli}` are the more important modules that you will
-   have to modify or use directory. `src/support/*.{ml,mli}` has the
+   have to modify or use directly. `src/support/*.{ml,mli}` has the
    less interesting support code. (Again, feel free to modify the
    support code, but you do not need to.)
 

src/Decode.ml

@@ -1,3 +1,8 @@
+(* There is nothing that you have to implement in this file/module,
+   and no particular need to read its implementation. [Decode.mli]
+   explains its purpose. *)
+
+
 type env = Unif.Env.t
 
 type slot =

src/Decode.mli

@@ -0,0 +1,21 @@
+type env = Unif.Env.t
+
+(** Suppose the unification environment [env] contains the following equations:
+
+    ?w = ?w1 -> ?w2
+    ?w1 = int
+    ?w2 = bool
+    ?w3 = ?w1 -> ?w4
+    ?w4 : no structure
+
+    Then [decode env ?w] will return the type [int -> bool].
+
+    Notice on the other hand that [?w3] is of the form [?w1 -> ?w4]
+    for a still-undertermined variable [?w4]. Any type of the form
+    [int -> foo] might work, for any [foo], but further progress in
+    the inference process could end up in a solution incompatible with
+    any specific choice of [foo]. We decide to decode this into
+    a fresh (rigid) type variable (which is assumed distinct from
+    everything else, but nothing else): [?w3] decodes into [int -> α].
+*)
+val decode : env -> Constraint.variable -> STLC.ty

src/Generator.ml

@@ -8,13 +8,74 @@ 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 =
-  Do (M.delay (Utils.not_yet "Generator.untyped"))
+  (* This definition is *not* a good solution,
+     but it could give you a flavor of possible definitions. *)
+  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 (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 TeVarSet.empty
 
 let constraint_ : (STLC.term, Infer.err) Constraint.t =
-  Do (M.delay (Utils.not_yet "Generator.constraint_"))
+  let w = Constraint.Var.fresh "final_type" in
+  Constraint.(Exist (w, None,
+    Infer.has_type
+      Untyped.Var.Map.empty
+      untyped
+      w))
 
-let typed ~depth =
-  Utils.not_yet "Generator.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
+     the function is valled [gen]:
 
-end
+     > it is possible to define a function
+     >
+     >     val gen : depth:int -> ('a, 'e) constraint -> ('a, 'e) result M.t
+     >
+     > on top of `eval`, that returns all the results that can be reached by
+     > expanding `Do` nodes using `M.bind`, recursively, exactly `depth`
+     > times. (Another natural choice would be to generate all the terms that
+     > can be reached by expanding `Do` nodes *at most* `depth` times, but
+     > this typically gives a worse generator.)
+  *)
+  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

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 =
-    (* Feel free to postpone implementing this function
-       until you implement the Annot case below. *)
-    Utils.not_yet "Infer.bind" (ty, k, fun () -> bind)
+  let rec bind : type a . STLC.ty -> (Constraint.variable -> (a, err) t) -> (a, err) t =
+    fun ty k ->
+    match ty with
+    | 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
@@ -64,30 +79,118 @@ module Make(T : Utils.Functor) = struct
       For example, if [t] is the term [lambda x. x], then [has_type env t w]
       generates a constraint equivalent to [∃?v. ?w = (?v -> ?v)].
 
+      More precisely, one possible generated constraint would be:
+      {[
+        Exist(v, None,
+          Map(
+            Conj(
+              Exist (arr, Some (Arrow (v, v)), Eq (arr, w)),
+              MapErr(Decode v, fun e -> Cycle e)
+            ),
+            fun ((), ty) -> Abs (x, ty, Var x)
+        ))
+      ]}
+      but the actually generated constraint may be more complex/verbose.
+
       Precondition: when calling [has_type env t], [env] must map each
       term variable that is free in [t] to an inference variable.
   *)
   let rec has_type (env : env) (t : Untyped.term) (w : variable) : (STLC.term, err) t =
     match t with
     | Untyped.Var x ->
-      Utils.not_yet "Infer.has_type: Var case" (env, t, w, x)
+      (Option.fold 
+          ~none:(
+            let a = Var.fresh "x" in
+            Exist(a, None, Ret (fun _ -> STLC.Var(x)))
+          ) 
+          ~some:(
+            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)
-    | Untyped.Abs (x, t) ->
-      Utils.not_yet "Infer.has_type: Abs case" (env, x, t, 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(a,None,
+        Exist(b,None,
+          Map(
+            Conj(
+              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
-      Utils.not_yet "Infer.has_type: Let 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: Let 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
          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/MRand.ml

@@ -10,7 +10,7 @@ let bind (sa : 'a t) (f : 'a -> 'b t) : 'b t =
   Utils.not_yet "MRand.bind" (sa, f)
 
 let delay (f : unit -> 'a t) : 'a t =
-  Utils.not_yet "MRand.delay" (f ())
+  Utils.not_yet "MRand.delay" f
 
 let sum (li : 'a t list) : 'a t =
   Utils.not_yet "MRand.sum" li

src/MRand.mli

@@ -1 +1,13 @@
 include Utils.MonadPlus
+
+(**
+   We demand that [MRand.run e] returns an infinite sequence of solutions
+   sampled from [e], for example
+   {[
+     (let open MRand in sum [return 1; return 2; return 3])
+     |> MRand.run     (* infinite stream of random samples *)
+     |> Seq.take 10   (* take the first 10 elements *)
+     |> List.of_seq
+   ]}
+   could be the list [[1; 2; 1; 2; 1; 1; 1; 3; 3; 2]].
+*)

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 =
-  MSeq_not_implemented_yet
+let fail : 'a t = Seq.empty
 
 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/MSeq.mli

@@ -1 +1,13 @@
 include Utils.MonadPlus
+
+(**
+   We demand that [MSeq.run e] returns the finite list of solutions
+   for [e], for example
+   {[
+     (let open MSeq in sum [return 1; return 2; return 3])
+     |> MSeq.run    (* list of all solutions *)
+     |> List.of_seq
+   ]}
+   should be the list [[1; 2; 3]] -- or maybe the same elements in
+   some other order.
+*)

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

src/Unif.ml

@@ -1,6 +1,6 @@
 (* There is nothing that you have to implement in this file/module,
    and no particular need to read its implementation. On the other hand,
-   you want to understand the interface exposed in [Unif.mli] has it
+   you want to understand the interface exposed in [Unif.mli], as it
    is important to implement a constraint solver in Solver.ml. *)
 
 module UF = UnionFind.Make(UnionFind.StoreMap)

src/support/ConstraintSimplifier.ml

@@ -58,6 +58,7 @@ module Make(T : Utils.Functor) = struct
             VarSet.of_list [v1; v2], Eq (v1, v2)
         end
       | Exist (v, s, c) ->
+        let v = normalize v in
         let fvs, c = simpl (VarSet.add v bvs) c in
         if is_in_env v then (fvs, c)
         else if not (VarSet.mem v fvs) then (fvs, c)

src/support/Decode.mli

@@ -1,3 +0,0 @@
-type env = Unif.Env.t
-
-val decode : env -> Constraint.variable -> STLC.ty

tests.t/run.t

@@ -92,17 +92,8 @@ to the bin/dune content.)
   Input term:
     lambda x. x
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?x ?wt (?warr = ?x -> ?wt). ?final_type = ?warr ∧ decode ?x ∧ ?wt = ?x)
-      ∧ decode ?final_type
-  
-  Inferred type:
-    α -> α
-  
-  Elaborated term:
-    lambda (x : α). x
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 
 `id_int` is the monomorphic identity on the type `int`. Note
 that we have not implemented support for a built-in `int`
@@ -113,20 +104,8 @@ type, this is just an abstract/rigid type variable: `Constr
   Input term:
     lambda x. (x : int)
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?x ?wt (?warr = ?x -> ?wt).
-        ?final_type = ?warr
-        ∧ decode ?x
-        ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt))
-      ∧ decode ?final_type
-  
-  Inferred type:
-    int -> int
-  
-  Elaborated term:
-    lambda (x : int). x
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 
 ## Logging the constraint-solving process
 
@@ -138,59 +117,8 @@ the inference variables.
   Input term:
     lambda x. (x : int)
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?x ?wt (?warr = ?x -> ?wt).
-        ?final_type = ?warr
-        ∧ decode ?x
-        ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt))
-      ∧ decode ?final_type
-  
-  Constraint solving log:
-    ∃?final_type.
-      decode ?final_type
-      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
-        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?final_type.
-      decode ?final_type
-      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
-        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?final_type.
-      decode ?final_type
-      ∧ (∃?wt (?warr = ?x -> ?wt).
-        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?wt ?final_type.
-      decode ?final_type
-      ∧ (∃(?warr = ?x -> ?wt).
-        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?wt (?warr = ?x -> ?wt) ?final_type.
-      decode ?final_type
-      ∧ (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
-      ∧ decode ?x
-      ∧ ?final_type = ?warr
-    ∃?x ?wt (?final_type = ?x -> ?wt).
-      decode ?final_type ∧ (∃(?int = int). ?int = ?wt ∧ ?int = ?x) ∧ decode ?x
-    ∃?x ?wt (?int = int) (?final_type = ?x -> ?wt).
-      decode ?final_type ∧ ?int = ?wt ∧ ?int = ?x ∧ decode ?x
-    ∃?wt (?int = int) (?final_type = ?int -> ?wt).
-      decode ?final_type ∧ ?int = ?wt ∧ decode ?int
-    ∃(?int = int) (?final_type = ?int -> ?int).
-      decode ?final_type ∧ decode ?int
-  
-  Inferred type:
-    int -> int
-  
-  Elaborated term:
-    lambda (x : int). x
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 
 ## An erroneous program
 
@@ -198,20 +126,8 @@ the inference variables.
   Input term:
     (lambda x. (x : int)) (lambda y. y)
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?wu (?wt = ?wu -> ?final_type).
-        (∃?x ?wt/1 (?warr = ?x -> ?wt/1).
-          ?wt = ?warr ∧ decode ?x ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt/1))
-        ∧ (∃?y ?wt/2 (?warr/1 = ?y -> ?wt/2).
-          ?wu = ?warr/1 ∧ decode ?y ∧ ?wt/2 = ?y))
-      ∧ decode ?final_type
-  
-  Error:
-      int
-    incompatible with
-      β -> α
-  
+  Fatal error: exception Failure("Infer.has_type: App case: not implemented yet")
+  [2]
 
 ## Examples with products
 
@@ -219,60 +135,15 @@ the inference variables.
   Input term:
     lambda f. lambda x. lambda y. f (x, y)
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?f ?wt (?warr = ?f -> ?wt).
-        ?final_type = ?warr
-        ∧ decode ?f
-        ∧ (∃?x ?wt/1 (?warr/1 = ?x -> ?wt/1).
-          ?wt = ?warr/1
-          ∧ decode ?x
-          ∧ (∃?y ?wt/2 (?warr/2 = ?y -> ?wt/2).
-            ?wt/1 = ?warr/2
-            ∧ decode ?y
-            ∧ (∃?wu (?wt/3 = ?wu -> ?wt/2).
-              ?wt/3 = ?f
-              ∧ (∃?w1.
-                ?w1 = ?x
-                ∧ (∃?w2. ?w2 = ?y ∧ (∃(?wprod = {?w1 * ?w2}). ?wu = ?wprod)))))))
-      ∧ decode ?final_type
-  
-  Inferred type:
-    ({γ * β} -> α) -> γ -> β -> α
-  
-  Elaborated term:
-    lambda (f : {γ * β} -> α). lambda (x : γ). lambda (y : β). f (x, y)
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 
   $ minihell $FLAGS uncurry.test
   Input term:
     lambda f. lambda p. let (x, y) = p in f x y
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?f ?wt (?warr = ?f -> ?wt).
-        ?final_type = ?warr
-        ∧ decode ?f
-        ∧ (∃?p ?wt/1 (?warr/1 = ?p -> ?wt/1).
-          ?wt = ?warr/1
-          ∧ decode ?p
-          ∧ (∃?x ?y (?wt/2 = {?x * ?y}).
-            decode ?x
-            ∧ decode ?y
-            ∧ ?wt/2 = ?p
-            ∧ (∃?wu (?wt/3 = ?wu -> ?wt/1).
-              (∃?wu/1 (?wt/4 = ?wu/1 -> ?wt/3). ?wt/4 = ?f ∧ ?wu/1 = ?x)
-              ∧ ?wu = ?y))))
-      ∧ decode ?final_type
-  
-  Inferred type:
-    (β -> γ -> α) -> {β * γ} -> α
-  
-  Elaborated term:
-    lambda
-    (f : β -> γ -> α).
-      lambda (p : {β * γ}). let ((x : β), (y : γ)) = p in f x y
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 ## Cyclic types
 
 Unification can sometimes create cyclic types. We decide to reject
@@ -286,61 +157,8 @@ a lot of those.)
   Input term:
     lambda x. x x
   
-  Generated constraint:
-    ∃?final_type.
-      (∃?x ?wt (?warr = ?x -> ?wt).
-        ?final_type = ?warr
-        ∧ decode ?x
-        ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wt/1 = ?x ∧ ?wu = ?x))
-      ∧ decode ?final_type
-  
-  Constraint solving log:
-    ∃?final_type.
-      decode ?final_type
-      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
-        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?final_type.
-      decode ?final_type
-      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
-        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?final_type.
-      decode ?final_type
-      ∧ (∃?wt (?warr = ?x -> ?wt).
-        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?wt ?final_type.
-      decode ?final_type
-      ∧ (∃(?warr = ?x -> ?wt).
-        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-        ∧ decode ?x
-        ∧ ?final_type = ?warr)
-    ∃?x ?wt (?warr = ?x -> ?wt) ?final_type.
-      decode ?final_type
-      ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-      ∧ decode ?x
-      ∧ ?final_type = ?warr
-    ∃?x ?wt (?final_type = ?x -> ?wt).
-      decode ?final_type
-      ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-      ∧ decode ?x
-    ∃?x ?wu ?wt (?final_type = ?x -> ?wt).
-      decode ?final_type
-      ∧ (∃(?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
-      ∧ decode ?x
-    ∃?x ?wu ?wt (?wt/1 = ?wu -> ?wt) ?wt (?final_type = ?x -> ?wt).
-      decode ?final_type ∧ ?wu = ?x ∧ ?wt/1 = ?x ∧ decode ?x
-    ∃?wu ?wt (?wt/1 = ?wu -> ?wt) ?wt (?final_type = ?wt/1 -> ?wt).
-      decode ?final_type ∧ ⊥ ∧ decode ?wt/1
-  
-  Error:
-    cycle on constraint variable
-    ?wu
-  
+  Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
+  [2]
 ## Generator tests
 
 This gives example outputs for my implementation. It is completely
@@ -349,52 +167,15 @@ fine if your own implementation produces different (sensible) results.
 There are not many programs with depth 3, 4 and 5.
 
   $ minigen --exhaustive --depth 3 --count 100
-  lambda (x/4 : α). x/4
+  Fatal error: exception Failure("MSeq.delay: not implemented yet")
+  [2]
 
   $ minigen --exhaustive --depth 4 --count 100
-  lambda (v/14 : β/1). lambda (u/19 : α/1). u/19
-  
-  lambda (v/14 : α/1). lambda (u/19 : γ/1). v/14
+  Fatal error: exception Failure("MSeq.delay: not implemented yet")
+  [2]
 
 An example of random sampling output at higher depth.
 
   $ minigen --seed 42 --depth 6 --count 10
-  lambda (z/90 : β/21). (z/90, lambda (u/90 : α/21). u/90)
-  
-  lambda (v/3d4 : β/dc). (lambda (w/3d4 : β/dc). v/3d4) v/3d4
-  
-  lambda
-  (x/48b : {δ/110 * γ/110}).
-    let
-    ((y/48b : δ/110), (z/48b : γ/110))
-    =
-    x/48b
-    in lambda (u/48b : β/110). u/48b
-  
-  lambda
-  (w/568 : γ/144).
-    lambda
-    (x/569 : {β/144 * α/144}).
-      let ((y/569 : β/144), (z/569 : α/144)) = x/569 in z/569
-  
-  lambda
-  (y/58e : α/14c).
-    let (z/58e : δ/14b -> δ/14b) = lambda (u/58e : δ/14b). u/58e in y/58e
-  
-  (lambda (u/5f3 : γ/165). u/5f3, lambda (v/5f3 : β/165). v/5f3)
-  
-  (lambda (y/6b2 : α/187). y/6b2, lambda (z/6b2 : δ/186). z/6b2)
-  
-  lambda
-  (u/722 : {δ/19c * γ/19c}).
-    let
-    ((v/722 : δ/19c), (w/722 : γ/19c))
-    =
-    u/722
-    in lambda (x/723 : β/19c). v/722
-  
-  lambda
-  (x/7fd : β/1c0).
-    lambda (y/7fd : α/1c0). let (z/7fd : α/1c0) = y/7fd in x/7fd
-  
-  lambda (x/b58 : δ/283). (lambda (y/b58 : γ/283). y/b58, x/b58)
+  Fatal error: exception Failure("MRand.delay: not implemented yet")
+  [2]

tests.t/run.t.orig

@@ -0,0 +1,400 @@
+# TL;DR
+
+To run the tests, run
+
+```
+dune runtest
+```
+
+from the root of the project directory. If this outputs
+nothing, the testsuite passes. If this outputs a diff, it
+means that there is a mismatch between the recorded/reference
+output and the behavior of your program.
+
+To *promote* the tests outputs (that is, to modify the reference
+output to match the current behavior of your program), run
+
+```
+dune runtest
+dune promote
+```
+
+When you submit your project, please check that `dune runtest` does
+not produce a diff -- the recorded output should match your
+program. If some outputs are wrong / not what you would expect, please
+explain this in the present file.
+
+
+# Intro
+
+This file is a "dune cram test" as explained at
+> https://dune.readthedocs.io/en/stable/tests.html#cram-tests
+
+The idea is to write 2-indented command lines prefixed by
+a dollar sign. The tool will run the command and check that
+the output corresponds to the output recorded in the file.
+
+  $ echo example
+  example
+
+To run the tests, just run `dune runtest` at the root of the
+project. This will show you a diff between the observed
+output and the recorded output of the test -- we consider
+that the test 'passes' if the diff is empty.  
+In particular, if you run `dune runtest` and you see no
+output, this is good! It means there was no change in the
+test output.
+
+If you think that the new output is better than the previous
+output, run `dune promote`; dune will rewrite the recorded
+outputs to match the observed outputs. (You can also modify
+outputs by hand but this is more cumbersome.)
+
+It is totally okay to have some test outputs recorded in
+your repository that are known to be broken -- because there
+is a bug, or some feature is not documented yet. Feel free
+to use the free-form comments in run.t to mention explicitly
+that the output is broken. (But then please remember, as the
+output changes in the future, to also update your comments.)
+
+
+# The tests
+
+The tests below use the `minihell` program defined in
+../bin/minihell.ml, called on the *.test files stored in the
+present directory. If you want to add new tests, just add
+new test files and then new commands below to exercise them.
+
+`minihell` takes untyped programs as input and will
+type-check and elaborate them. It can show many things
+depending on the input flags passed. By default we ask
+`minihell` to repeat the source file (to make the recorded
+output here more pleasant to read) and to show the generated
+constraint. It will also show the result type and the
+elaborated term.
+
+  $ FLAGS="--show-source --show-constraint"
+
+Remark: You can call minihell from the command-line yourself
+by using either
+> dune exec bin/minihell.exe -- <arguments>
+or
+> dune exec minihell -- <arguments>
+(The latter short form, used in the tests below, is available thanks
+to the bin/dune content.)
+
+
+## Simple tests
+
+`id_poly` is just the polymorphic identity.
+
+  $ minihell $FLAGS id_poly.test
+  Input term:
+    lambda x. x
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?x ?wt (?warr = ?x -> ?wt). ?final_type = ?warr ∧ decode ?x ∧ ?wt = ?x)
+      ∧ decode ?final_type
+  
+  Inferred type:
+    α -> α
+  
+  Elaborated term:
+    lambda (x : α). x
+  
+
+`id_int` is the monomorphic identity on the type `int`. Note
+that we have not implemented support for a built-in `int`
+type, this is just an abstract/rigid type variable: `Constr
+(Var ...)` at type `STLC.ty`.
+
+  $ minihell $FLAGS id_int.test
+  Input term:
+    lambda x. (x : int)
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?x ?wt (?warr = ?x -> ?wt).
+        ?final_type = ?warr
+        ∧ decode ?x
+        ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt))
+      ∧ decode ?final_type
+  
+  Inferred type:
+    int -> int
+  
+  Elaborated term:
+    lambda (x : int). x
+  
+
+## Logging the constraint-solving process
+
+You can ask `minihell` to show how the constraint evolves as
+the solver progresses and accumulates more information on
+the inference variables.
+
+  $ minihell $FLAGS --log-solver id_int.test
+  Input term:
+    lambda x. (x : int)
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?x ?wt (?warr = ?x -> ?wt).
+        ?final_type = ?warr
+        ∧ decode ?x
+        ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt))
+      ∧ decode ?final_type
+  
+  Constraint solving log:
+    ∃?final_type.
+      decode ?final_type
+      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
+        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?final_type.
+      decode ?final_type
+      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
+        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?final_type.
+      decode ?final_type
+      ∧ (∃?wt (?warr = ?x -> ?wt).
+        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?wt ?final_type.
+      decode ?final_type
+      ∧ (∃(?warr = ?x -> ?wt).
+        (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?wt (?warr = ?x -> ?wt) ?final_type.
+      decode ?final_type
+      ∧ (∃(?int = int). ?int = ?wt ∧ ?int = ?x)
+      ∧ decode ?x
+      ∧ ?final_type = ?warr
+    ∃?x ?wt (?final_type = ?x -> ?wt).
+      decode ?final_type ∧ (∃(?int = int). ?int = ?wt ∧ ?int = ?x) ∧ decode ?x
+    ∃?x ?wt (?int = int) (?final_type = ?x -> ?wt).
+      decode ?final_type ∧ ?int = ?wt ∧ ?int = ?x ∧ decode ?x
+    ∃?wt (?int = int) (?final_type = ?int -> ?wt).
+      decode ?final_type ∧ ?int = ?wt ∧ decode ?int
+    ∃(?int = int) (?final_type = ?int -> ?int).
+      decode ?final_type ∧ decode ?int
+  
+  Inferred type:
+    int -> int
+  
+  Elaborated term:
+    lambda (x : int). x
+  
+
+## An erroneous program
+
+  $ minihell $FLAGS error.test
+  Input term:
+    (lambda x. (x : int)) (lambda y. y)
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?wu (?wt = ?wu -> ?final_type).
+        (∃?x ?wt/1 (?warr = ?x -> ?wt/1).
+          ?wt = ?warr ∧ decode ?x ∧ (∃(?int = int). ?int = ?x ∧ ?int = ?wt/1))
+        ∧ (∃?y ?wt/2 (?warr/1 = ?y -> ?wt/2).
+          ?wu = ?warr/1 ∧ decode ?y ∧ ?wt/2 = ?y))
+      ∧ decode ?final_type
+  
+  Error:
+      int
+    incompatible with
+      β -> α
+  
+
+## Examples with products
+
+  $ minihell $FLAGS curry.test
+  Input term:
+    lambda f. lambda x. lambda y. f (x, y)
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?f ?wt (?warr = ?f -> ?wt).
+        ?final_type = ?warr
+        ∧ decode ?f
+        ∧ (∃?x ?wt/1 (?warr/1 = ?x -> ?wt/1).
+          ?wt = ?warr/1
+          ∧ decode ?x
+          ∧ (∃?y ?wt/2 (?warr/2 = ?y -> ?wt/2).
+            ?wt/1 = ?warr/2
+            ∧ decode ?y
+            ∧ (∃?wu (?wt/3 = ?wu -> ?wt/2).
+              ?wt/3 = ?f
+              ∧ (∃?w1.
+                ?w1 = ?x
+                ∧ (∃?w2. ?w2 = ?y ∧ (∃(?wprod = {?w1 * ?w2}). ?wu = ?wprod)))))))
+      ∧ decode ?final_type
+  
+  Inferred type:
+    ({γ * β} -> α) -> γ -> β -> α
+  
+  Elaborated term:
+    lambda (f : {γ * β} -> α). lambda (x : γ). lambda (y : β). f (x, y)
+  
+
+  $ minihell $FLAGS uncurry.test
+  Input term:
+    lambda f. lambda p. let (x, y) = p in f x y
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?f ?wt (?warr = ?f -> ?wt).
+        ?final_type = ?warr
+        ∧ decode ?f
+        ∧ (∃?p ?wt/1 (?warr/1 = ?p -> ?wt/1).
+          ?wt = ?warr/1
+          ∧ decode ?p
+          ∧ (∃?x ?y (?wt/2 = {?x * ?y}).
+            decode ?x
+            ∧ decode ?y
+            ∧ ?wt/2 = ?p
+            ∧ (∃?wu (?wt/3 = ?wu -> ?wt/1).
+              (∃?wu/1 (?wt/4 = ?wu/1 -> ?wt/3). ?wt/4 = ?f ∧ ?wu/1 = ?x)
+              ∧ ?wu = ?y))))
+      ∧ decode ?final_type
+  
+  Inferred type:
+    (β -> γ -> α) -> {β * γ} -> α
+  
+  Elaborated term:
+    lambda
+    (f : β -> γ -> α).
+      lambda (p : {β * γ}). let ((x : β), (y : γ)) = p in f x y
+  
+## Cyclic types
+
+Unification can sometimes create cyclic types. We decide to reject
+these situations with an error. (We could also accept those as they
+preserve type-safety, but they have the issue, just like the
+OCaml -rectypes option, that they allow to write somewhat-nonsensical
+program, and our random term generator will be very good at finding
+a lot of those.)
+
+  $ minihell $FLAGS --log-solver selfapp.test
+  Input term:
+    lambda x. x x
+  
+  Generated constraint:
+    ∃?final_type.
+      (∃?x ?wt (?warr = ?x -> ?wt).
+        ?final_type = ?warr
+        ∧ decode ?x
+        ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wt/1 = ?x ∧ ?wu = ?x))
+      ∧ decode ?final_type
+  
+  Constraint solving log:
+    ∃?final_type.
+      decode ?final_type
+      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
+        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?final_type.
+      decode ?final_type
+      ∧ (∃?x ?wt (?warr = ?x -> ?wt).
+        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?final_type.
+      decode ?final_type
+      ∧ (∃?wt (?warr = ?x -> ?wt).
+        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?wt ?final_type.
+      decode ?final_type
+      ∧ (∃(?warr = ?x -> ?wt).
+        (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+        ∧ decode ?x
+        ∧ ?final_type = ?warr)
+    ∃?x ?wt (?warr = ?x -> ?wt) ?final_type.
+      decode ?final_type
+      ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+      ∧ decode ?x
+      ∧ ?final_type = ?warr
+    ∃?x ?wt (?final_type = ?x -> ?wt).
+      decode ?final_type
+      ∧ (∃?wu (?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+      ∧ decode ?x
+    ∃?x ?wu ?wt (?final_type = ?x -> ?wt).
+      decode ?final_type
+      ∧ (∃(?wt/1 = ?wu -> ?wt). ?wu = ?x ∧ ?wt/1 = ?x)
+      ∧ decode ?x
+    ∃?x ?wu ?wt (?wt/1 = ?wu -> ?wt) ?wt (?final_type = ?x -> ?wt).
+      decode ?final_type ∧ ?wu = ?x ∧ ?wt/1 = ?x ∧ decode ?x
+    ∃?wu ?wt (?wt/1 = ?wu -> ?wt) ?wt (?final_type = ?wt/1 -> ?wt).
+      decode ?final_type ∧ ⊥ ∧ decode ?wt/1
+  
+  Error:
+    cycle on constraint variable
+    ?wu
+  
+## Generator tests
+
+This gives example outputs for my implementation. It is completely
+fine if your own implementation produces different (sensible) results.
+
+There are not many programs with depth 3, 4 and 5.
+
+  $ minigen --exhaustive --depth 3 --count 100
+  lambda (x/4 : α). x/4
+
+  $ minigen --exhaustive --depth 4 --count 100
+  lambda (v/14 : β/1). lambda (u/19 : α/1). u/19
+  
+  lambda (v/14 : α/1). lambda (u/19 : γ/1). v/14
+
+An example of random sampling output at higher depth.
+
+  $ minigen --seed 42 --depth 6 --count 10
+  lambda (z/90 : β/21). (z/90, lambda (u/90 : α/21). u/90)
+  
+  lambda (v/3d4 : β/dc). (lambda (w/3d4 : β/dc). v/3d4) v/3d4
+  
+  lambda
+  (x/48b : {δ/110 * γ/110}).
+    let
+    ((y/48b : δ/110), (z/48b : γ/110))
+    =
+    x/48b
+    in lambda (u/48b : β/110). u/48b
+  
+  lambda
+  (w/568 : γ/144).
+    lambda
+    (x/569 : {β/144 * α/144}).
+      let ((y/569 : β/144), (z/569 : α/144)) = x/569 in z/569
+  
+  lambda
+  (y/58e : α/14c).
+    let (z/58e : δ/14b -> δ/14b) = lambda (u/58e : δ/14b). u/58e in y/58e
+  
+  (lambda (u/5f3 : γ/165). u/5f3, lambda (v/5f3 : β/165). v/5f3)
+  
+  (lambda (y/6b2 : α/187). y/6b2, lambda (z/6b2 : δ/186). z/6b2)
+  
+  lambda
+  (u/722 : {δ/19c * γ/19c}).
+    let
+    ((v/722 : δ/19c), (w/722 : γ/19c))
+    =
+    u/722
+    in lambda (x/723 : β/19c). v/722
+  
+  lambda
+  (x/7fd : β/1c0).
+    lambda (y/7fd : α/1c0). let (z/7fd : α/1c0) = y/7fd in x/7fd
+  
+  lambda (x/b58 : δ/283). (lambda (y/b58 : γ/283). y/b58, x/b58)

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)