Working better.

src/dune

@@ -27,6 +27,7 @@
    (progn
     (run ./cccatt.exe test.cccatt)
     (run ./cccatt.exe curry.cccatt)
+    (run ./cccatt.exe implicit.cccatt)
    )
  )
 )

src/extlib.ml

@@ -58,4 +58,12 @@ module Pos = struct
           Printf.sprintf "line %d characters %d-%d" l1 c1 c2
       else
         Printf.sprintf "from line %d character %d to line %d character %d" l1 c1 l2 c2
+
+  module Option = struct
+    type nonrec t = t option
+
+    let to_string = function
+      | Some pos -> to_string pos
+      | None -> "unknown position"
+  end
 end

src/implicit.cccatt

@@ -8,23 +8,24 @@ coh S {a b c : .} : (a → b → c) → (a → b) → a → c
 
 coh ap {a b : .} (t : a → b) (u : a) : b
 
-# let id := ap (ap S K) K
+# let id {a : .} : a -> a := ap (ap S K) K
 
-# coh comp (a b c : .) (f : a → b) (g : b → c) : a → c
+coh comp {a b c : .} (f : a → b) (g : b → c) : a → c
 
-# coh B (a b c : .) : (b -> c) -> (a -> b) -> a -> c
+coh B {a b c : .} : (b -> c) -> (a -> b) -> a -> c
 
-# coh B' (a b c : .) : (a -> b) -> (b -> c) -> a -> c
+coh B' {a b c : .} : (a -> b) -> (b -> c) -> a -> c
 
-# coh W (a b : .) : (a -> a -> b) -> (a -> b)
+coh W {a b : .} : (a -> a -> b) -> (a -> b)
 
-# coh C (a b c : .) : (a -> b -> c) -> b -> a -> c
+coh C {a b c : .} : (a -> b -> c) -> b -> a -> c
 
-# let test (a b : .) : b -> a -> b := K b a
+# let test {a b : .} : b -> a -> b := K
 
-# # this can be obtained directly or defined
-# coh K' (a b : .) : a -> b -> b
-# let K' (a b : .) : a -> b -> b := ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)
+# this can be obtained directly or defined
+coh K' (a b : .) : a -> b -> b
+# let K' {a b : .} : a -> b -> b := ap (K (b -> b) a) (I b)
+let K' {a b : .} : a -> b -> b := ap K (I {b})
 
 # ## Test
 

src/lang.ml

@@ -431,7 +431,15 @@ and check tenv env e a =
   let e, b = infer tenv env e in
   try if not (b.desc = Obj && a.desc = Type) then unify b a; e
   with
-  | Unification -> failure e.pos "got %s but %s expected" (to_string b) (to_string a)
+  | Unification ->
+    (
+      match b.desc with
+      | Pi (`Implicit, _, _, _) ->
+        (* Printf.printf "check add hole to %s\n%!" (to_string e); *)
+        let e = mk ~pos:e.pos (App (`Implicit, e, hole ())) in
+        check tenv env e a
+      | _ -> failure e.pos "got %s but %s expected" (to_string b) (to_string a)
+    )
 
 (** All metavariables of a term. *)
 let metavariables e =
@@ -473,6 +481,13 @@ let print_metavariables_elaboration m =
          printf "=?.?= at %s, ?%d elaborated to %s\n" (Pos.to_string (Option.get m.pos)) m.id v
     ) m
 
+let print_unelaborated_metavariables m =
+  List.iter
+    (fun (m:meta) ->
+       if m.value = None then
+         printf "=?.?= warning: unelaborated ?%d at %s\n%!" m.id (Pos.Option.to_string m.pos)
+    ) m
+
 let exec_command (tenv, env) p =
   match p with
   | Let (x, a, e) ->
@@ -493,6 +508,7 @@ let exec_command (tenv, env) p =
     (* print_endline "checking"; *)
     let v = eval env e in
     print_metavariables_elaboration m;
+    print_unelaborated_metavariables m;
     let tenv = (x,a)::tenv in
     let env = (x,v)::env in
     printf "=^.^= defined %s : %s\n%!" x (to_string a);