Debug.

src/lang.ml

@@ -233,6 +233,7 @@ let check_ps l a =
 
 (** Evaluate an expression to a value. *)
 let rec eval env e =
+  (* Printf.printf "* eval: %s\n" (to_string e); *)
   match e.desc with
   | Coh (l,_) ->
     let rec aux t = function
@@ -262,14 +263,18 @@ let rec eval env e =
     let u = eval env u in
     V.Id (t, u)
   | Obj -> V.Obj
-  | Hom (a, b) -> V.Hom (eval env a, eval env b)
+  | Hom (a, b) ->
+    (* Printf.printf "Hom : %s / %s\n%!" (to_string a) (to_string b); *)
+    (* Printf.printf "env : %s\n" (string_of_context env); *)
+    V.Hom (eval env a, eval env b)
   | Prod (a, b) -> V.Prod (eval env a, eval env b)
   | Type -> V.Type
   | Hole (m, _) -> V.Meta m
 
 (** Infer the type of an expression. *)
 let rec infer k tenv env e =
   (* printf "* infer %s\n%!" (to_string e); *)
+  (* printf "  tenv : %s\n\n%!" (string_of_context tenv); *)
   (* printf "  env : %s\n%!" (string_of_context env); *)
   match e.desc with
   | Coh (l, a) ->
@@ -290,10 +295,13 @@ let rec infer k tenv env e =
     )
   | Abs (x,a,t) ->
     check k tenv env a V.Type;
+    (* Printf.printf "   started with %s : %s\n%!" x (to_string a); *)
     let a = eval env a in
+    (* Printf.printf "   type evaluates to %s\n%!" (V.to_string a); *)
     let _ =
       let x' = V.var k in
-      infer (k+1) ((x, a)::tenv) ((x, x')::env) t
+      (* Printf.printf "   *** add %s : %s\n" x (V.to_string a); *)
+      infer (k+1) ((x,a)::tenv) ((x,x')::env) t
     in
     let b v = infer k ((x,a)::tenv) ((x,v)::env) t in
     V.Pi (a, b)
@@ -351,7 +359,7 @@ let rec infer k tenv env e =
   | Hole (_, a) -> a
 
 and check k tenv env e a =
-  (* printf "*** check %s : %s\n%!" (to_string e) (V.to_string a); *)
+  (* printf "* check %s : %s\n%!" (to_string e) (V.to_string a); *)
   let b = infer k tenv env e in
   try
     if not (b = V.Obj && a = V.Type) then V.unify k b a

src/test.cccatt

@@ -63,7 +63,7 @@ let id (a : .) (x : a) := ap a a (I a) x
 
 let id' (a : .) (x : a) := ap _ _ (I _) x
 
-let ap' (a b : .) (x : a) (f : a -> b) := ap _ _ f x
+# let ap' (a b : .) (x : a) (f : a -> b) := ap _ _ f x
 
 ## Testing identities
 

src/value.ml

@@ -18,6 +18,7 @@ type t =
 and meta =
   {
     pos : Pos.t option;
+    id : int;
     mutable value : t option;
   }
 
@@ -29,7 +30,12 @@ and neutral =
 
 let var k = Neutral (Var k)
 
-let meta ?pos () = { pos; value = None }
+let meta =
+  let id = ref 0 in
+  fun ?pos () ->
+    incr id;
+    let id = !id in
+    { pos; id; value = None }
 
 let metavariable ?pos () = Meta (meta ?pos ())
 
@@ -51,7 +57,7 @@ let rec to_string k ?(pa=false) t =
     (
       match m.value with
       | Some t -> Printf.sprintf "[%s]" (to_string k t)
-      | None -> "_"
+      | None -> Printf.sprintf "?%d" m.id
     )
   | Neutral n ->
     let rec aux = function
@@ -91,7 +97,7 @@ let print_metavariables_elaboration t =
          | Some v -> to_string v
          | None -> "?"
        in
-       if m.pos <> None then printf "... at %s, elaborated to %s\n" (Pos.to_string (Option.get m.pos)) v
+       if m.pos <> None then printf "... at %s, ?%d elaborated to %s\n" (Pos.to_string (Option.get m.pos)) m.id v
     )
 
 let rec homs l a =
@@ -103,6 +109,7 @@ exception Unification
 
 (** Make sure that two values are equal (and raise [Unification] if this cannot be the case). *)
 let rec unify k t t' =
+  (* Printf.printf "unify %s with %s\n" (to_string t) (to_string t'); *)
   let rec neutral k t t' =
     match t, t' with
     | App (t, u), App (t', u') -> neutral k t t'; unify k u u'
@@ -121,5 +128,7 @@ let rec unify k t t' =
   | Meta { value = Some t; _ }, t' -> unify k t t'
   | t, Meta { value = Some t'; _ } -> unify k t t'
   | Meta m, t
-  | t, Meta m -> m.value <- Some t
+  | t, Meta m ->
+    (* printf "... ?%d becomes %s\n" m.id (to_string t); *)
+    m.value <- Some t
   | _ -> raise Unification