Tried to implement Var and Abs has_type method ...

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,44 @@ module Make(M : Utils.MonadPlus) = struct
   module TeVarSet = Untyped.Var.Set
   module TyVarSet = STLC.TyVar.Set
 
+
 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 () : Untyped.term =
+    let open Untyped 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 *)
+      ]
+    )
+  in gen ()
 
 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 =
+  (* 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]:
+
+     > 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.)
+  *)
   Utils.not_yet "Generator.typed" depth
 
 end

src/Infer.ml

@@ -64,17 +64,46 @@ 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)
+    | 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)),
+          Map(Conj(
+            has_type newenv t b,
+            eq tau w
+          ), fun t -> let (x,_) = p in x) (* term * unit -> term isomorphism *)
+        )
     | Untyped.Let (x, t, u) ->
       Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type)
     | Untyped.Annot (t, ty) ->

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

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

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/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)