Skip to content

Commit f28e800

Browse files
mikeshulmanmikeshulman
committed
use unparser in all cases of split
1 parent 1967920 commit f28e800

File tree

2 files changed

+169
-57
lines changed

2 files changed

+169
-57
lines changed

‎lib/parser/command.ml‎

Lines changed: 124 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ open Modifier
1616
open Printable
1717
module Trie = Yuujinchou.Trie
1818
module TermParse = Parse
19+
open Asai.Range
1920

2021
type _ Effect.t += Chdir : string -> string Effect.t
2122

@@ -734,7 +735,7 @@ module Parse = struct
734735
end
735736

736737
let parse_single (content : string) : Whitespace.t list * Command.t option =
737-
let src : Asai.Range.source = `String { content; title = None } in
738+
let src : source = `String { content; title = None } in
738739
let p, src = Parse.start_parse ~or_echo:true src in
739740
match Parse.final p with
740741
| Bof ws ->
@@ -781,21 +782,21 @@ let condense : Command.t -> [ `Import | `Option | `None | `Bof ] = function
781782
| Option _ -> .
782783
| _ -> `None
783784

785+
let tok t : observation = Token (t, ([], None))
786+
784787
(* Subroutine for "split" that generates the cases in a multiple match. *)
785788
let split_match_cases : type a b.
786789
(a, b) Ctx.t ->
787790
(string option, a) Bwv.t ->
788791
(Whitespace.t list * wrapped_parse) list ->
789792
observation list list =
790793
fun ctx vars tms ->
791-
let open Asai.Range in
792794
let module S = Monad.State (Bool) in
793795
let module LS = Monad.ListT (S) in
794796
let open Monad.Ops (LS) in
795-
let tok t : observation = Token (t, ([], None)) in
796797
let rec do_args : type a p ap.
797798
(a, p, ap) Term.Telescope.t ->
798-
(No.plus_omega, No.strict, No.plus_omega, No.nonstrict) parse Asai.Range.located list =
799+
(No.plus_omega, No.strict, No.plus_omega, No.nonstrict) parse located list =
799800
fun args ->
800801
match args with
801802
| Emp -> []
@@ -811,7 +812,7 @@ let split_match_cases : type a b.
811812
| (_, Wrap tm) :: tms -> (
812813
match process vars tm with
813814
| { value = Synth rtm; loc } -> (
814-
let _, sty = Check.synth (Kinetic `Nolet) ctx (Asai.Range.locate_opt loc rtm) in
815+
let _, sty = Check.synth (Kinetic `Nolet) ctx (locate_opt loc rtm) in
815816
match View.view_type sty "split" with
816817
| Canonical (_, Data { dim; constrs; _ }, _, _) ->
817818
let* () =
@@ -996,7 +997,7 @@ let execute ~(action_taken : unit -> unit) ~(get_file : string -> Scope.trie) (c
996997
let ptm = process vars tm in
997998
(* We set the hole location offset to the start of the *term*, so that ProofGeneral can create hole overlays in the right places when solving a hole and creating new holes. *)
998999
let tmloc = ptm.loc <|> Anomaly "missing location in solve" in
999-
let offset = (fst (Asai.Range.split tmloc)).offset in
1000+
let offset = (fst (split tmloc)).offset in
10001001
(* Now we typecheck the supplied term. *)
10011002
let ctx = Norm.eval_ctx termctx in
10021003
let ety = Norm.eval_term (Ctx.env ctx) ty in
@@ -1017,63 +1018,95 @@ let execute ~(action_taken : unit -> unit) ~(get_file : string -> Scope.trie) (c
10171018
let (Found_hole { instant; termctx; ty; vars; parametric; _ }) =
10181019
Global.find_hole data.number in
10191020
Global.rewind_command ~parametric ~holes_allowed:(Ok ()) instant @@ fun () ->
1020-
let content =
1021-
let ctx = Norm.eval_ctx termctx in
1021+
(* We have to generate a bunch of holes, possibly in different tightness intervals. *)
1022+
let hole li ri = locate_opt None (Hole { li; ri; num = ref (-1); ws = []; contents = None }) in
1023+
let ehole = hole No.Interval.entire No.Interval.entire in
1024+
let ctx = Norm.eval_ctx termctx in
1025+
(* I don't think we actually use this, but it's "correct" to put it in. *)
1026+
let _, names = Names.uniquify_vars vars in
1027+
let term =
10221028
match data.tms with
10231029
| [ (_, Wrap { value = Placeholder _; _ }) ] -> (
10241030
let ety = Norm.eval_term (Ctx.env ctx) ty in
10251031
match View.view_type ety "split" with
10261032
| Canonical (_, Pi (_, doms, _), _, _) ->
1027-
let cube, mapsto =
1033+
let cube, mapsto, notn =
10281034
match D.compare_zero (CubeOf.dim doms) with
1029-
| Zero -> (`Normal, Token.Mapsto)
1030-
| Pos _ -> (`Cube, Token.DblMapsto) in
1035+
| Zero -> (`Normal, Token.Mapsto, Builtins.abs)
1036+
| Pos _ -> (`Cube, Token.DblMapsto, Builtins.cubeabs) in
10311037
let xs = Domvars.get_pi_vars ctx cube Emp ety in
10321038
(* TODO: Should generate real variable names. *)
1033-
String.concat " " (Bwd_extra.to_list_map (Option.value ~default:"_") xs)
1034-
^ Token.to_string mapsto
1035-
^ " ?"
1039+
let vars =
1040+
unparse_abs
1041+
(Bwd.map (fun x -> (x, `Explicit)) xs)
1042+
{ strictness = No.Nonstrict; endpoint = No.minus_omega }
1043+
(No.minusomega_le No.plus_omega) No.minusomega_lt_plusomega in
1044+
locate_opt None
1045+
@@ infix ~notn ~first:vars
1046+
~inner:(Single (Left (mapsto, ([], None))))
1047+
~last:ehole ~left_ok:(No.le_refl No.minus_omega)
1048+
~right_ok:(No.le_refl No.minus_omega)
10361049
| Canonical (_, Codata { eta; fields; _ }, ins, _) -> (
10371050
let m = cod_left_ins ins in
10381051
let do_field : type a n et.
1039-
(a * n * et) Term.CodatafieldAbwd.entry -> string list -> string list =
1052+
(a * n * et) Term.CodatafieldAbwd.entry ->
1053+
(string * string list) list ->
1054+
(string * string list) list =
10401055
fun (Term.CodatafieldAbwd.Entry (fld, cdf)) acc ->
10411056
match cdf with
1042-
| Lower _ -> Field.to_string fld :: acc
1057+
| Lower _ -> (Field.to_string fld, []) :: acc
10431058
| Higher _ ->
10441059
let i = Field.dim fld in
10451060
let pbijs = List.of_seq (all_pbij_between m i) in
10461061
List.fold_right
10471062
(fun (Pbij_between pbij) acc ->
1048-
(Field.to_string fld ^ string_of_pbij pbij) :: acc)
1063+
(Field.to_string fld, strings_of_pbij pbij) :: acc)
10491064
pbijs acc in
10501065
let fields = Bwd.fold_right do_field fields [] in
10511066
match eta with
10521067
| Eta ->
1053-
Token.to_string LParen
1054-
^ String.concat ", "
1055-
(List.map
1056-
(fun fld ->
1057-
fld ^ " " ^ Token.to_string Coloneq ^ " " ^ Token.to_string (Hole None))
1058-
fields)
1059-
^ Token.to_string RParen
1068+
let inner =
1069+
Multiple
1070+
( Left (LParen, ([], None)),
1071+
Bwd_extra.intersperse (tok (Op ","))
1072+
(Bwd_extra.of_list_map
1073+
(fun (fld, pbij) ->
1074+
if List.length pbij > 0 then
1075+
fatal (Anomaly "record type has higher field");
1076+
Term
1077+
(locate_opt None
1078+
(infix ~notn:Builtins.coloneq
1079+
~first:(locate_opt None (Ident ([ fld ], [])))
1080+
~inner:(Single (Left (Coloneq, ([], None))))
1081+
~last:ehole ~left_ok:(No.le_refl No.minus_omega)
1082+
~right_ok:(No.le_refl No.minus_omega))))
1083+
fields),
1084+
Left (RParen, ([], None)) ) in
1085+
locate_opt None @@ outfix ~notn:parens ~inner
10601086
| Noeta ->
1061-
Token.to_string LBracket
1062-
^ String.concat " | "
1063-
(List.map
1064-
(fun fld ->
1065-
"."
1066-
^ fld
1067-
^ " "
1068-
^ Token.to_string Mapsto
1069-
^ " "
1070-
^ Token.to_string (Hole None))
1071-
fields)
1072-
^ Token.to_string RBracket)
1087+
let mapsto =
1088+
match D.compare_zero m with
1089+
| Zero -> Token.Mapsto
1090+
| Pos _ -> Token.DblMapsto in
1091+
let inner =
1092+
Multiple
1093+
( Left (LBracket, ([], None)),
1094+
List.fold_left
1095+
(fun acc (fld, pbij) ->
1096+
acc
1097+
<: tok (Op "|")
1098+
<: Term (locate_opt None (Field (fld, pbij, [])))
1099+
<: tok mapsto
1100+
<: Term ehole)
1101+
Emp fields,
1102+
Left (RBracket, ([], None)) ) in
1103+
locate_opt None @@ outfix ~notn:Builtins.comatch ~inner)
10731104
| Canonical (_, Data { constrs = Snoc (Emp, (constr, Dataconstr { args; _ })); _ }, _, _)
10741105
->
10751106
let nargs = Fwn.to_int (Term.Telescope.length args) in
1076-
Constr.to_string constr ^ "." ^ String.concat "" (List.init nargs (fun _ -> " ?"))
1107+
unparse_spine names (`Constr constr)
1108+
(Bwd.init nargs (fun _ -> { unparse = (fun li ri -> hole li ri) }))
1109+
No.Interval.entire No.Interval.entire
10771110
| Canonical (_, Data { constrs = Emp; _ }, _, _) ->
10781111
fatal (Invalid_split (`Goal, "empty datatype"))
10791112
| Canonical (_, Data { constrs = Snoc (Snoc (_, _), _); _ }, _, _) ->
@@ -1084,26 +1117,60 @@ let execute ~(action_taken : unit -> unit) ~(get_file : string -> Scope.trie) (c
10841117
let tok t : observation = Token (t, ([], None)) in
10851118
let comma_tms =
10861119
List.tl
1087-
@@
1088-
let open Monad.Ops (Monad.List) in
1089-
let* wscomma, Wrap tm = data.tms in
1090-
[ Token (Op ",", (wscomma, None)); Term tm ] in
1091-
let lines = split_match_cases ctx vars data.tms in
1092-
let mtch =
1093-
Asai.Range.locate_opt None
1094-
@@ outfix ~notn:Builtins.implicit_mtch
1095-
~inner:
1096-
(Multiple
1097-
( Left (Match, ([], None)),
1098-
Emp
1099-
<@ comma_tms
1100-
<: tok LBracket
1101-
<@ List.flatten (List.map (fun line -> tok (Op "|") :: line) lines),
1102-
Left (RBracket, ([], None)) )) in
1103-
let buf = Buffer.create 10 in
1104-
PPrint.(
1105-
ToBuffer.pretty 1.0 (Display.columns ()) buf (pp_complete_term (Wrap mtch) `None));
1106-
Buffer.contents buf in
1120+
(let open Monad.Ops (Monad.List) in
1121+
let* wscomma, Wrap tm = data.tms in
1122+
[ Token (Op ",", (wscomma, None)); Term tm ]) in
1123+
let module S = Monad.State (Bool) in
1124+
let module LS = Monad.ListT (S) in
1125+
let open Monad.Ops (LS) in
1126+
let rec constr_args : type a p ap.
1127+
?acc:unparser Bwd.t -> (a, p, ap) Term.Telescope.t -> unparser Bwd.t =
1128+
fun ?(acc = Emp) -> function
1129+
| Emp -> acc
1130+
| Ext (x, _, args) ->
1131+
constr_args ~acc:(Snoc (acc, { unparse = (fun _ _ -> unparse_var x) })) args
1132+
in
1133+
let rec go = function
1134+
| [] ->
1135+
let* higher = LS.lift S.get in
1136+
let mapsto = if higher then Token.DblMapsto else Mapsto in
1137+
return [ tok mapsto; Term ehole ]
1138+
| (_, Wrap tm) :: tms -> (
1139+
match process vars tm with
1140+
| { value = Synth rtm; loc } -> (
1141+
let _, sty = Check.synth (Kinetic `Nolet) ctx (locate_opt loc rtm) in
1142+
match View.view_type sty "split" with
1143+
| Canonical (_, Data { dim; constrs; _ }, _, _) ->
1144+
let* () =
1145+
match D.compare_zero dim with
1146+
| Zero -> return ()
1147+
| Pos _ -> LS.lift (S.put true) in
1148+
let* c, Dataconstr { args; _ } = S.return (Bwd.to_list constrs) in
1149+
let first =
1150+
Term
1151+
(unparse_spine names (`Constr c) (constr_args args) No.Interval.entire
1152+
No.Interval.entire) in
1153+
let* rest = go tms in
1154+
if List.length rest = 2 then return (first :: rest)
1155+
else return (first :: tok (Op ",") :: rest)
1156+
| _ -> fatal (Invalid_split (`Term, "non-datatype")))
1157+
| _ -> fatal (Nonsynthesizing "splitting term")) in
1158+
let lines = fst (go data.tms false) in
1159+
locate_opt None
1160+
@@ outfix ~notn:Builtins.implicit_mtch
1161+
~inner:
1162+
(Multiple
1163+
( Left (Match, ([], None)),
1164+
Emp
1165+
<@ comma_tms
1166+
<: tok LBracket
1167+
<@ List.flatten (List.map (fun line -> tok (Op "|") :: line) lines),
1168+
Left (RBracket, ([], None)) )) in
1169+
let buf = Buffer.create 10 in
1170+
let s = Display.get () in
1171+
Display.run ~init:{ s with holes = `Without_number } @@ fun () ->
1172+
PPrint.(ToBuffer.pretty 1.0 (Display.columns ()) buf (pp_complete_term (Wrap term) `None));
1173+
let content = Buffer.contents buf in
11071174
let ptm = TermParse.Term.(final (parse (`String { title = None; content }))) in
11081175
let disp = Display.get () in
11091176
Display.run ~init:{ disp with holes = `Without_number } @@ fun () ->

‎test/black/holes.t/split.ny‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
{` This file is NOT executed by run.t. It's for manual testing of the PG split function C-c C-y. `}
2+
3+
def ℕ : Type ≔ data [ zero. | suc. (n : ℕ) ]
4+
5+
def plus (m n : ℕ) : ℕ ≔ match m, n [
6+
| zero., zero. ↦ ¿ʔ
7+
| zero., suc. n ↦ ¿ʔ
8+
| suc. m, zero. ↦ ¿ʔ
9+
| suc. m, suc. n ↦ ¿ʔ]
10+
11+
def ⊥ : Type ≔ data []
12+
13+
def foo (x : ℕ) (y : ⊥) : Type ≔ ¿ʔ
14+
15+
def bar (x : ℕ) (y0 y1 : ℕ) (y2 : Id ℕ y0 y1) : Type ≔ ¿ʔ
16+
17+
def baz : Type ≔ data [ baz. (y0 y1 : ℕ) (y2 : Id ℕ y0 y1) ]
18+
19+
def bazzz (x : baz) : Type ≔ match x [
20+
| baz. _ _ zero. ⤇ ℕ
21+
| baz. _ _ (suc. n) ⤇ bazzz (baz. n.0 n.1 n.2)]
22+
23+
def f : (a : ℕ) (b : ℕ) → Type ≔ ¿ʔ
24+
25+
axiom g : ℕ → ℕ
26+
def ge : Id ((x : ℕ) → ℕ) g g ≔ ¿ʔ
27+
28+
def ℕ×ℕ : Type ≔ sig ( fst : ℕ, snd : ℕ )
29+
30+
def nn : ℕ×ℕ ≔ ¿ʔ
31+
32+
axiom mm : ℕ×ℕ
33+
def mme : Id ℕ×ℕ mm mm ≔ ¿ʔ
34+
35+
def Sℕ : Type ≔ codata [ s .head : ℕ | s .tail : Sℕ ]
36+
37+
def sn : Sℕ ≔ ¿ʔ
38+
axiom sm : Sℕ
39+
def sme : Id Sℕ sm sm ≔ ¿ʔ
40+
41+
def √ℕ : Type ≔ codata [ x .root.e : ℕ ]
42+
43+
def qn : √ℕ ≔ ¿ʔ
44+
axiom qm : √ℕ
45+
def qme : Id √ℕ qm qm ≔ ¿ʔ

0 commit comments

Comments
 (0)