Print "unification" variables (existential variables scoped under par…

…ameters) as underscores in OCaml code annotations.

TODO.md

@@ -3,6 +3,4 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README.
 * TODO: perhaps `check_connected` could be simplified or even removed from abduction?
 * FIXME: repeating `newtype` and `newcons` definitions should be errors.
 * TODO: calibrate timeout parameters (number of iterations before forced exit from simple abduction, joint abduction etc.)
-* FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument.
-* FIXME: export the type of tuples to OCaml using asterisks instead of commas.
-* FIXME: either mute the "unification" type variables on let-in node annotations by printing them as `_`, or move them to the other side of `=` if that helps.
+* FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument.

examples/eval.ml.target

@@ -19,6 +19,6 @@ let rec eval : type a . (a term -> a) =
     | Plus (x, y) -> plus (eval x) (eval y)
     | If (b, t, e) -> if_then (eval b) (eval t) (eval e)
     | Pair (x, y) -> (eval x, eval y)
-    | Fst p -> let ((x, y): (a * 't47)) = eval p in x
-    | Snd p -> let ((x, y): ('t59 * a)) = eval p in y): a term -> a)
+    | Fst p -> let ((x, y): (a * _)) = eval p in x
+    | Snd p -> let ((x, y): (_ * a)) = eval p in y): a term -> a)
 

examples/mutual_recursion_eval.ml.target

@@ -0,0 +1,49 @@
+type num = int
+type _ term =
+  | IsZero : calc -> boolean term
+  | If : (*∀'a.*)boolean term * 'a term * 'a term -> 'a term
+  | Pair : (*∀'a, 'b.*)'a term * 'b term -> (('a * 'b)) term
+  | Fst : (*∀'a, 'b.*)(('a * 'b)) term -> 'a term
+  | Snd : (*∀'a, 'b.*)(('a * 'b)) term -> 'b term
+and calc =
+  | Lit : (*∀'k.*)(* k *) num -> calc
+  | Plus : calc * calc -> calc
+  | Mult : calc * calc -> calc
+  | Cond : boolean term * calc * calc -> calc
+and boolean
+
+external plus : ((* i *) num -> (* j *) num -> (* i + j *) num) = "plus"
+type ex1 =
+  | Ex1 : (*∀'k.*)(* k *) num -> ex1
+external mult : ((* i *) num -> (* j *) num -> ex1) = "mult"
+external is_zero : ((* i *) num -> boolean) = "is_zero"
+type ex2 =
+  | Ex2 : (*∀'k.*)(* k *) num -> ex2
+external cond : (boolean -> (* i *) num -> (* j *) num -> ex2) = "cond"
+external if_then : (boolean -> 'a -> 'a -> 'a) = "if_then"
+let snd (*: type a b . ((a * b) -> b)*) = (fun ((_, x)) -> x)
+type ex3 =
+  | Ex3 : (*∀'n.*)(* n *) num -> ex3
+let (calc, eval) (*: type a . ((calc -> ex3) * (a term -> a))*) =
+  let rec eval : type b . ((calc -> ex3) * (b term -> b)) =
+  let rec calc : (calc -> ex3) =
+  ((function Lit i -> let xcase = i in Ex3 xcase
+    | Plus (x, y) ->
+        let Ex3 rx = calc x in
+        let Ex3 ry = calc y in let xcase = plus rx ry in Ex3 xcase
+    | Mult (x, y) ->
+        let Ex3 rx = calc x in
+        let Ex3 ry = calc y in let Ex1 xcase = mult rx ry in Ex3 xcase
+    | Cond (b, t, e) ->
+        let Ex3 rt = calc t in
+        let Ex3 re = calc e in
+        let Ex2 xcase = cond (snd eval b) rt re in Ex3 xcase):
+    calc -> ex3) in
+  (calc,
+    ((function IsZero x -> let Ex3 r = calc x in is_zero r
+      | If (b, t, e) -> if_then (snd eval b) (snd eval t) (snd eval e)
+      | Pair (x, y) -> (snd eval x, snd eval y)
+      | Fst p -> let ((x, y): (b * _)) = snd eval p in x
+      | Snd p -> let ((x, y): (_ * b)) = snd eval p in y): b term -> b)) in
+  eval
+

src/InvarGenTTest.ml

@@ -120,16 +120,14 @@ let tests = "InvarGenT" >::: [
            test_case ~test_annot:true "simple_eval" ());
       "eval-annot" >::
         (fun () ->
-           todo "OCaml type-checking problem";
-           (* skip_if !debug "debug"; *)
+           skip_if !debug "debug";
            test_case ~test_annot:true "eval" ());
       "equational_reas-annot" >::
         (fun () ->
            skip_if !debug "debug";
            test_case ~test_annot:true "equational_reas" ());
       "mutual_recursion_eval-annot" >::
         (fun () ->
-           todo "OCaml type-checking problem";
            skip_if !debug "debug";
            test_case ~test_annot:true "mutual_recursion_eval" ());
     ]

src/OCaml.ml

@@ -21,7 +21,7 @@ let pr_tyvar ppf v =
     else fprintf ppf "%s" (var_str v)
   | VId _ ->
     assert (not !altsyn);
-    fprintf ppf "'%s" (var_str v)
+    fprintf ppf "_"
 
 let pr_tycns ppf c =
   fprintf ppf "%s" (String.uncapitalize (cns_str c))