From bc3183c09b7dd157adb16a225c09f8d0a36b1d62 Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Wed, 13 Jul 2022 08:24:32 +0200 Subject: [PATCH 1/9] style: reformat --- src/elaborator/Elaborator.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 664b882..7f14c10 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -82,10 +82,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 *) From 616cad460d2b503ff0d7ca7787280aa14c96091f Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Wed, 13 Jul 2022 08:24:39 +0200 Subject: [PATCH 2/9] feat: add holes to parser --- src/parser/Term.ml | 1 + src/parser/Token.ml | 1 + src/parser/Token.mli | 1 + 3 files changed, 3 insertions(+) diff --git a/src/parser/Term.ml b/src/parser/Term.ml index 2cb3086..895577a 100644 --- a/src/parser/Term.ml +++ b/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 diff --git a/src/parser/Token.ml b/src/parser/Token.ml index ce28a9f..236b9e8 100644 --- a/src/parser/Token.ml +++ b/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) | "=>"} -> () diff --git a/src/parser/Token.mli b/src/parser/Token.mli index 7fd033a..0701ed5 100644 --- a/src/parser/Token.mli +++ b/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 From 1e58beccad63e0a799865fc72ab7aa215ed88db0 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 13 Jul 2022 23:14:21 -0700 Subject: [PATCH 3/9] fix: abstract over TpUlvl when unleashing holes, add small debug printer --- src/elaborator/Elaborator.ml | 3 +-- src/nbe/Domain.ml | 14 ++++++++++++++ src/nbe/NbE.ml | 3 ++- 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 7f14c10..90ad5d6 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -22,11 +22,10 @@ let unleash_hole loc : T.check = let tp = R.Eff.with_top_env @@ fun () -> R.Eff.eval @@ - List.fold_right make_pi bnds @@ R.Eff.quote goal.tp + S.vir_pi S.tp_ulvl @@ List.fold_right make_pi bnds @@ R.Eff.quote goal.tp in Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp} in - 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 diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml index 6fb2c16..8f9154c 100644 --- a/src/nbe/Domain.ml +++ b/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 _ -> "" + | Unfold _ -> "" + | Pi _ -> "" + | Lam _ -> "" + | Sigma _ -> "" + | Pair _ -> "" + | Univ _ -> "" + | VirPi _ -> "" + | TpULvl -> "" + | ULvl _ -> "" + | VirUniv -> "" \ No newline at end of file diff --git a/src/nbe/NbE.ml b/src/nbe/NbE.ml index 7e539ab..ba8bc55 100644 --- a/src/nbe/NbE.ml +++ b/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) From e748a0138b613129c8c331a23e1c9b5c9f731a0c Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Fri, 15 Jul 2022 10:59:59 +0200 Subject: [PATCH 4/9] fix: in unleash_hole, goal type was quoted in the wrong env --- src/elaborator/Elaborator.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 90ad5d6..26b7cce 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -12,19 +12,17 @@ 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 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 @@ - S.vir_pi S.tp_ulvl @@ 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 @@ R.Eff.quote goal.tp + 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 T.Check.infer @@ let head = R.Structural.global_var p @@ R.ULvl.base in From ce81aeefdbd2985f40bd51608d0af1599189e442 Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Fri, 15 Jul 2022 11:23:22 +0200 Subject: [PATCH 5/9] feat: add dumper for core syntax --- src/elaborator/Syntax.ml | 4 +--- src/nbe/Syntax.ml | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/elaborator/Syntax.ml b/src/elaborator/Syntax.ml index f230c51..49cedb0 100644 --- a/src/elaborator/Syntax.ml +++ b/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 diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml index ddf63d8..aad4277 100644 --- a/src/nbe/Syntax.ml +++ b/src/nbe/Syntax.ml @@ -57,7 +57,7 @@ let rec dump fmt = | VirPi (base, fam) -> Format.fprintf fmt "@[<7>VirPi (@[%a@],@ @[%a@])@]" dump base dump fam | Pi (base, fam) -> - Format.fprintf fmt "@[<7>Pi (@[%a@],@ @[%a@])@]" dump base dump fam + Format.fprintf fmt "@[<7>VirPi (@[%a@],@ @[%a@])@]" dump base dump fam | Sigma (base, fam) -> Format.fprintf fmt "@[<7>Sigma (@[%a@],@ @[%a@])@]" dump base dump fam | TpULvl -> From 33321f57dc0ae3ab66585d9ac4c8045c263a8549 Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Fri, 15 Jul 2022 11:23:33 +0200 Subject: [PATCH 6/9] feat: print something when we unleash a hole --- src/elaborator/Elaborator.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 26b7cce..817f8e5 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -24,6 +24,8 @@ let unleash_hole loc : T.check = 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 : %a @." CS.dump_name p S.dump top_tp; + let vtp = R.Eff.with_top_env @@ fun () -> R.Eff.eval top_tp in 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 From aee3ad210b1e0e24024ab85a569a9b8fcdca80d0 Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Fri, 15 Jul 2022 11:38:58 +0200 Subject: [PATCH 7/9] fix: remove duplicate line --- src/elaborator/Elaborator.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 817f8e5..205a9c5 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -25,7 +25,6 @@ let unleash_hole loc : T.check = Eff.unleash ?loc None @@ R.ResolveData.Axiom {tp = vtp} in Format.printf "Unleashed hole %a : %a @." CS.dump_name p S.dump top_tp; - let vtp = R.Eff.with_top_env @@ fun () -> R.Eff.eval top_tp in 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 From 0b68870ba337f0ccabb3e3b2548f25a2e2245189 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Sat, 16 Jul 2022 17:08:06 -0700 Subject: [PATCH 8/9] fix: print Pi as Pi, not VirPi --- src/nbe/Syntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml index aad4277..ddf63d8 100644 --- a/src/nbe/Syntax.ml +++ b/src/nbe/Syntax.ml @@ -57,7 +57,7 @@ let rec dump fmt = | VirPi (base, fam) -> Format.fprintf fmt "@[<7>VirPi (@[%a@],@ @[%a@])@]" dump base dump fam | Pi (base, fam) -> - Format.fprintf fmt "@[<7>VirPi (@[%a@],@ @[%a@])@]" dump base dump fam + Format.fprintf fmt "@[<7>Pi (@[%a@],@ @[%a@])@]" dump base dump fam | Sigma (base, fam) -> Format.fprintf fmt "@[<7>Sigma (@[%a@],@ @[%a@])@]" dump base dump fam | TpULvl -> From eebaad2bcee47af732def7f1cd2a5af179d1696f Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Sat, 16 Jul 2022 17:23:20 -0700 Subject: [PATCH 9/9] feat: print context/goal at hole instead of hole type --- src/elaborator/Elaborator.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index 205a9c5..41d5864 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -12,19 +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 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 - S.vir_pi S.tp_ulvl @@ List.fold_right make_pi bnds @@ R.Eff.quote goal.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 : %a @." CS.dump_name p S.dump top_tp; + 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