From 5bdda4a652057c523ba43e71b7aef7b4b8c6e987 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Fri, 18 Oct 2024 14:54:18 +0200
Subject: [PATCH] Show elaboration.

---
 src/lang.ml     |  5 +++--
 src/test.cccatt |  2 +-
 src/value.ml    | 46 ++++++++++++++++++++++++++++++++++++++--------
 3 files changed, 42 insertions(+), 11 deletions(-)

diff --git a/src/lang.ml b/src/lang.ml
index e05ade9..222baae 100644
--- a/src/lang.ml
+++ b/src/lang.ml
@@ -316,7 +316,7 @@ let rec infer k tenv env e =
         let a' =
           let mk = mk ~pos:e.pos in
           let rec readback = function
-            | V.Meta { contents = Some a } -> readback a
+            | V.Meta { value = Some a; _ } -> readback a
             | V.Obj -> mk Obj
             | V.Neutral (V.Var _) as var -> mk (Var (List.assoc' var env))
             | V.Hom (a, b) -> mk (Hom (readback a, readback b))
@@ -345,9 +345,10 @@ let rec infer k tenv env e =
     check k tenv env b V.Obj;
     V.Obj
   | Type -> V.Type
-  | Hole -> V.metavariable ()
+  | Hole -> V.metavariable ~pos:e.pos ()
 
 and check k tenv env e 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
diff --git a/src/test.cccatt b/src/test.cccatt
index 06213f9..8361859 100644
--- a/src/test.cccatt
+++ b/src/test.cccatt
@@ -83,7 +83,7 @@ coh ap-comp (a b c : .) (f : a -> b) (g : b -> c) (x : a) : ap a c (comp a b c f
 
 coh ax3 (a b : .) : ap (a -> b -> b) ((a -> b) -> a -> b) (S a b b) (ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)) = I (a -> b)
 
-coh ax3 (a b : .) : ap (a -> b -> b) ((a -> b) -> a -> b) (S a b b) (ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)) = I (a -> b)
+# coh ax3 (a b : .) : ap (a -> b -> b) ((a -> b) -> a -> b) (S a b b) (ap (b -> b) (a -> b -> b) (K (b -> b) a) (I b)) = I _
 
 # coh ax4 (a b c : .) : ap
 
diff --git a/src/value.ml b/src/value.ml
index 309a7f2..a135e61 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -1,5 +1,8 @@
 (** Values (i.e. evaluated expressions). *)
 
+open Extlib
+open Common
+
 (** A value. *)
 type t =
   | Abs of (t -> t)
@@ -9,9 +12,15 @@ type t =
   | Pi of t * (t -> t) (** a meta-arrow *)
   | Id of t * t
   | Type
-  | Meta of t option ref (** a metavariable *)
+  | Meta of meta (** a metavariable *)
   | Neutral of neutral
 
+and meta =
+  {
+    pos : Pos.t option;
+    mutable value : t option;
+  }
+
 (** A neutral value. *)
 and neutral =
   | Coh
@@ -20,7 +29,7 @@ and neutral =
 
 let var k = Neutral (Var k)
 
-let metavariable () = Meta (ref None)
+let metavariable ?pos () = Meta { pos; value = None }
 
 let rec to_string k ?(pa=false) t =
   let pa s = if pa then "(" ^ s ^ ")" else s in
@@ -36,9 +45,9 @@ let rec to_string k ?(pa=false) t =
     Printf.sprintf "(%s : %s) => %s" (to_string k x) (to_string k a) (to_string (k+1) (b x)) |> pa
   | Id (a, b) -> Printf.sprintf "%s = %s" (to_string k a) (to_string k b) |> pa
   | Type -> "Type"
-  | Meta t ->
+  | Meta m ->
     (
-      match !t with
+      match m.value with
       | Some t -> Printf.sprintf "[%s]" (to_string k t)
       | None -> "_"
     )
@@ -52,6 +61,24 @@ let rec to_string k ?(pa=false) t =
     in
     aux n
 
+let rec has_metavariable = function
+  | Obj
+  | Type
+  | Meta { value = None; _ } -> false
+  | Hom (a, b)
+  | Prod (a, b)
+  | Id (a, b) -> has_metavariable a || has_metavariable b
+  | Abs t -> has_metavariable (t (var 0))
+  | Pi (a, b) -> has_metavariable a || has_metavariable (b (var 0))
+  | Meta { value = Some a; _ } -> has_metavariable a
+  | Neutral n ->
+    let rec aux = function
+      | Coh
+      | Var _ -> false
+      | App (n, a) -> aux n || has_metavariable a
+    in
+    aux n
+
 (** String representation of a value. *)
 let to_string ?(k=0) = to_string k
 
@@ -79,8 +106,11 @@ let rec unify k t t' =
   | Pi (a, t), Pi (a', t') -> let x = var k in unify k a a'; unify (k+1) (t x) (t' x)
   | Obj, Obj
   | Type, Type -> ()
-  | Meta { contents = Some t }, _ -> unify k t t'
-  | _, Meta { contents = Some t'} -> unify k t t'
-  | Meta x, t
-  | t, Meta x -> x := Some t
+  | Meta { value = Some t; _ }, _ -> unify k t t'
+  | _, Meta { value = Some t'; _ } -> unify k t t'
+  | Meta m, t
+  | t, Meta m ->
+    if m.pos <> None && not (has_metavariable t) then
+      printf "... at %s, elaborated to %s\n" (Pos.to_string (Option.get m.pos)) (to_string t);
+    m.value <- Some t
   | _ -> raise Unification