🐛🕳 Debug holes

src/elaborator/Elaborator.ml

@@ -12,21 +12,22 @@ module T = R.Tactic
 let unleash_hole loc : T.check =
   T.Check.peek @@ fun goal ->
   let bnds = R.Eff.Generalize.quote_ctx () in
-
-  let p =
+  let goal = R.Eff.quote goal.tp in
+  let top_tp =
     let make_pi bnd bdy =
       match bnd with
       | R.Eff.Generalize.VirType tp -> S.VirPi (tp, bdy)
       | R.Eff.Generalize.Type tp -> S.Pi (tp, bdy)
     in
-    let tp =
-      R.Eff.with_top_env @@ fun () ->
-      R.Eff.eval @@
-      List.fold_right make_pi bnds @@ R.Eff.quote goal.tp
-    in
-    Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp}
+    S.vir_pi S.tp_ulvl @@ List.fold_right make_pi bnds @@ goal
   in
-
+  let p =
+    let vtp = R.Eff.with_top_env @@ fun () -> R.Eff.eval top_tp in
+    Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp = vtp}
+  in
+  Format.printf "Unleashed hole %a@." CS.dump_name p;
+  List.iter R.Eff.Generalize.(function VirType tp | Type tp -> Format.printf "%a@." S.dump tp) bnds;
+  Format.printf "⊢ %a @." S.dump goal;
   T.Check.infer @@
   let head = R.Structural.global_var p @@ R.ULvl.base in
   let app _ (l, itm) = l + 1, R.Pi.app ~itm ~ctm:(T.Check.infer @@ R.Structural.level l) in
@@ -82,10 +83,10 @@ and check tm : T.check =
   | CS.Pair (tm1, tm2) ->
     R.Sigma.pair ~cfst:(check tm1) ~csnd:(check tm2)
   | CS.Univ s ->
-    R.Univ.univ (check_shift s)
+    R.Univ.univ @@ check_shift s
   | CS.Hole ->
     unleash_hole tm.loc
-  | _ -> T.Check.infer (infer tm)
+  | _ -> T.Check.infer @@ infer tm
 
 
 (* the public interface *)

src/elaborator/Syntax.ml

@@ -2,9 +2,7 @@ open Asai
 
 type name = Yuujinchou.Trie.path
 
-let dump_name fmt n =
-  Format.fprintf fmt "@[%a@]"
-    (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ".") Format.pp_print_string) n
+let dump_name = NbE.Syntax.dump_name
 
 type bound_name = name option
 

src/nbe/Domain.ml

@@ -53,3 +53,17 @@ module ULvl =
 let univ_top = Univ ULvl.top
 
 let vir_univ = VirUniv
+
+let debug_show_head : con -> string = 
+  function
+  | Cut _ -> "<cut>"
+  | Unfold _ -> "<unfold>"
+  | Pi _ -> "<pi>"
+  | Lam _ -> "<lam>"
+  | Sigma _ -> "<sigma>"
+  | Pair _ -> "<pair>"
+  | Univ _ -> "<univ>"
+  | VirPi _ -> "<vir-pi>"
+  | TpULvl -> "<tp-ulvl>"
+  | ULvl _ -> "<ulvl>"
+  | VirUniv -> "<vir-univ>"

src/nbe/NbE.ml

@@ -18,4 +18,5 @@ let app_ulvl ~tp ~ulvl =
   match force_all tp with
   | VirPi (TpULvl, fam) ->
     inst_clo' fam ulvl
-  | _ -> invalid_arg "app_ulvl"
+  | tp ->
+    invalid_arg ("app_ulvl: " ^ Domain.debug_show_head tp)

src/parser/Term.ml

@@ -18,6 +18,7 @@ let parser atomic_term_ =
   | x:name up s:shift -> S.Var (x, Some s)
   | c:term_constant -> c ~shift:None
   | c:term_constant up s:shift -> c ~shift:(Some s)
+  | question -> S.Hole
 and atomic_term = located atomic_term_
 and parser atomic_shift =
   | plus i:pos_num -> S.Translate i

src/parser/Token.ml

@@ -25,6 +25,7 @@ let section_end = keyword |> Earley.apply @@ function CmdSectionEnd {check_tag}
 let at = Earley.greedy @@ parser {STR(Emoji.bullseye) | "@"} -> ()
 let colon = Earley.greedy @@ parser ":" -> ()
 let comma = Earley.greedy @@ parser "," -> ()
+let question = Earley.greedy @@ parser "?" -> ()
 let dollar = Earley.greedy @@ parser {STR(Emoji.back_arrow) | STR(Emoji.dollar_banknote) | "$"} -> ()
 let equal = Earley.greedy @@ parser { STR(Emoji.heavy_equals_sign) | "=" } -> ()
 let maps_to = Earley.greedy @@ parser {STR(Emoji.left_arrow_curving_right) | "=>"} -> ()

src/parser/Token.mli

@@ -25,6 +25,7 @@ val maps_to : unit Earley_core.Earley.grammar
 val multiply : unit Earley_core.Earley.grammar
 val plus : unit Earley_core.Earley.grammar
 val right_arrow : unit Earley_core.Earley.grammar
+val question : unit Earley_core.Earley.grammar
 val semi : unit Earley_core.Earley.grammar
 val semisemi : unit Earley_core.Earley.grammar
 val times : unit Earley_core.Earley.grammar