diff --git a/README.md b/README.md index 8cdfa818..fb82c699 100644 --- a/README.md +++ b/README.md @@ -476,7 +476,7 @@ When Narya reaches the end of a file (or command-line `-e` string) in which any Generally the purpose of leaving a hole is to see its displayed type and context, making it easier to *fill* the hole by a term. The most straightforward way to fill a hole is to edit the source code to replace the `?` by a term (perhaps containing other holes) and reload the file. In interactive mode, if you just entered a command containing a hole, you can `undo 1` to cancel the original command containing the hole, press Up-arrow or Meta+P to recover it in the history, edit it to replace the `?`, and re-execute it. And in ProofGeneral mode, you can use `C-c C-u` or `C-c RET` to retract the hole-creating command (along with any commands after it) and edit it (or just start editing it and it will auto-retract), and then re-process it with `C-c C-n`. -It is also possible to fill a hole *without* retracting the command or any other commands after it. In ProofGeneral mode, if you position the cursor over a hole (perhaps using `C-c C-j` and `C-c C-k` to move between holes) and type `C-c C-SPC`, ProofGeneral will prompt you for a term with which to solve the hole. If this term does successfully solve the hole, it will be inserted to replace the `?` in the buffer, without retracting the original command or anything after it. (Currently, extra parentheses will always be inserted around the new term to ensure that it parses in its new location; eventually they will only be inserted if necessary.) This enables you to process a bunch of commands containing holes, some of which might be slow to run, and then progressively work on filling the holes in any desired order without having to retract and re-process anything. +It is also possible to fill a hole *without* retracting the command or any other commands after it. In ProofGeneral mode, if you position the cursor over a hole (perhaps using `C-c C-j` and `C-c C-k` to move between holes) and type `C-c C-SPC`, ProofGeneral will prompt you for a term with which to solve the hole. If this term does successfully solve the hole, it will be inserted to replace the `?` in the buffer, without retracting the original command or anything after it. This enables you to process a bunch of commands containing holes, some of which might be slow to run, and then progressively work on filling the holes in any desired order without having to retract and re-process anything. Of course, the term that you fill a hole with contain other holes. The term solving a hole is parsed and typechecked *in the context where the hole was created*. Thus it can refer by name to variables that were in the context at that point (like `X` above) and constants that were defined at that point, and use notations that were in effect at that point, but not constants or notations that were defined later. diff --git a/bin/narya.ml b/bin/narya.ml index 3c071c41..b689c84b 100644 --- a/bin/narya.ml +++ b/bin/narya.ml @@ -105,14 +105,20 @@ let rec repl terminal history buf = let str = Buffer.contents buf in let* () = Lwt_io.flush Lwt_io.stdout in (* In interactive mode, we display all messages verbosely, and don't quit on fatal errors except for the Quit command. *) - Reporter.try_with - ~emit:(fun d -> Reporter.display ~output:stdout d) - ~fatal:(fun d -> - Reporter.display ~output:stdout d; - match d.message with - | Quit _ -> exit 0 - | _ -> ()) - (fun () -> do_command (Command.parse_single str)); + ( Reporter.try_with + ~emit:(fun d -> Reporter.display ~output:stdout d) + ~fatal:(fun d -> + Reporter.display ~output:stdout d; + match d.message with + | Quit _ -> exit 0 + | _ -> ()) + @@ fun () -> + match Command.parse_single str with + | _, Some cmd when (Execute.Flags.read ()).execute -> + Execute.execute_command cmd; + let n = Eternity.unsolved () in + if n > 0 then Reporter.emit (Open_holes n) + | _ -> () ); LTerm_history.add history (Zed_string.of_utf8 (String.trim str)); repl terminal history None) else ( @@ -153,17 +159,19 @@ let rec interact_pg () : unit = done; let cmd = Buffer.contents buf in let holes = ref Emp in + let parens = ref false in ( Global.HolePos.run ~init:{ holes = Emp; offset = 0 } @@ fun () -> Reporter.try_with (* ProofGeneral sets TERM=dumb, but in fact it can display ANSI colors, so we tell Asai to override TERM and use colors unconditionally. *) ~emit:(fun d -> match d.message with | Hole _ -> holes := Snoc (!holes, d.message) + | Needs_parentheses -> parens := true | _ -> Reporter.display ~use_ansi:true ~output:stdout d) ~fatal:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d) (fun () -> try - do_command (Command.parse_single cmd); + let _reformat = do_command (Command.parse_single cmd) in Format.printf "\x0C[goals]\x0C\n%!"; Mbwd.miter (fun [ h ] -> @@ -174,7 +182,10 @@ let rec interact_pg () : unit = let st = Global.HolePos.get () in Mbwd.miter (fun [ (h, s, e) ] -> Format.printf "%d %d %d\n" h (s - st.offset) (e - st.offset)) - [ st.holes ] + [ st.holes ]; + Format.printf "\x0C[reformat]\x0C\n%!"; + (* reformat (); *) + if !parens then Format.printf "parens\n%!" else Format.printf "noparens\n%!" with Sys.Break -> Reporter.fatal Break) ); interact_pg () with End_of_file -> () @@ -182,6 +193,7 @@ let rec interact_pg () : unit = let () = try run_top @@ fun () -> + (* Note: run_top executes the input files, so here we only have to do the interaction. *) Mbwd.miter (fun [ file ] -> let p, src = Parser.Command.Parse.start_parse (`File file) in diff --git a/js/jsnarya.ml b/js/jsnarya.ml index b7fc0cc1..a48e6c24 100644 --- a/js/jsnarya.ml +++ b/js/jsnarya.ml @@ -18,7 +18,9 @@ let interact_js : string -> string = Reporter.try_with ~emit:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d) ~fatal:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d) - (fun () -> do_command (Command.parse_single cmd)); + (fun () -> + let _ : unit -> unit = do_command (Command.parse_single cmd) in + ()); Out_channel.flush stdout; Buffer.contents buf diff --git a/lib/core/check.ml b/lib/core/check.ml index a294cf04..4e069883 100644 --- a/lib/core/check.ml +++ b/lib/core/check.ml @@ -433,13 +433,13 @@ let rec check : | Record _, Kinetic l -> kinetic_of_potential l ctx tm ty "sig" | Data _, Kinetic l -> kinetic_of_potential l ctx tm ty "data" (* If the user left a hole, we create an eternal metavariable. *) - | Hole (vars, pos), _ -> + | Hole (vars, pos, li, ri), _ -> (* Holes aren't numbered by the file they appear in. *) let meta = Meta.make_hole (Ctx.raw_length ctx) (Ctx.dbwd ctx) (energy status) in let ty, termctx = Readback.Displaying.run ~env:true @@ fun () -> (readback_val ctx ty, readback_ctx ctx) in - Global.add_hole meta pos ~vars ~termctx ~ty ~status; + Global.add_hole meta pos ~vars ~termctx ~ty ~status ~li ~ri; Meta (meta, energy status) (* If we have a synthesizing term, we synthesize it. *) | Synth stm, _ -> check_of_synth status ctx stm tm.loc ty diff --git a/lib/core/dump.ml b/lib/core/dump.ml index d81e2a56..7c846131 100644 --- a/lib/core/dump.ml +++ b/lib/core/dump.ml @@ -168,7 +168,7 @@ let rec check : type a. formatter -> a check -> unit = | Codata _ -> fprintf ppf "Codata(?)" | Record (_, _, _) -> fprintf ppf "Record(?)" | Refute (_, _) -> fprintf ppf "Refute(?)" - | Hole (_, _) -> fprintf ppf "Hole" + | Hole (_, _, _, _) -> fprintf ppf "Hole" | Realize x -> fprintf ppf "Realize %a" check x | ImplicitApp (fn, args) -> fprintf ppf "ImplicitApp (%a," synth fn.value; diff --git a/lib/core/global.ml b/lib/core/global.ml index 63aa4444..3fe371b1 100644 --- a/lib/core/global.ml +++ b/lib/core/global.ml @@ -24,7 +24,7 @@ type data = { constants : ((emp, kinetic) term * definition, Code.t) Result.t Constant.Map.t; metas : metamap; (* These two data pertain to the *currently executing command*: they store information about the holes and the global metavariables it has created. The purpose is that if and when that command completes, we notify the user about the holes and save the metavariables to the correct global state. In particular, during a "solve" command, the global state is rewound in time, but any newly created global metavariables need to be put into the "present" global state that it was rewound from. *) - current_holes : (Meta.wrapped * printable * unit Asai.Range.located) Bwd.t; + current_holes : (Meta.wrapped * printable * Asai.Range.t) Bwd.t; current_metas : metamap; (* These are the eternal holes that exist. We store them so that when commands creating holes are undone, those holes can be discarded. *) holes : Meta.WrapSet.t; @@ -67,6 +67,8 @@ type eternity = { ('a, 'b) Termctx.t -> ('b, kinetic) term -> ('b, 's) status -> + No.interval option -> + No.interval option -> unit; } @@ -140,7 +142,11 @@ let add_error c e = let add_meta m ~termctx ~ty ~tm ~energy = let tm = (tm :> [ `Defined of ('b, 's) term | `Axiom | `Undefined ]) in S.modify @@ fun d -> - { d with current_metas = d.current_metas |> Metamap.add m (Ok { tm; termctx; ty; energy }) } + { + d with + current_metas = + d.current_metas |> Metamap.add m (Ok { tm; termctx; ty; energy; li = None; ri = None }); + } (* Set the definition of a Global metavariable, required to already exist but not be defined. *) let set_meta m ~tm = @@ -171,14 +177,14 @@ let () = let with_holes env f = HolesAllowed.run ~env f (* Add a new hole. This is an eternal metavariable, so we pass off to Eternity, and also save some information about it locally so that we can discard it if the command errors (in interactive mode this doesn't stop the program) and notify the user if the command succeeds, and also discard it if this command is later undone. *) -let add_hole m pos ~vars ~termctx ~ty ~status = +let add_hole m loc ~vars ~termctx ~ty ~status ~li ~ri = match HolesAllowed.read () with | Ok () -> - !eternity.add m vars termctx ty status; + !eternity.add m vars termctx ty status (Some li) (Some ri); S.modify @@ fun d -> { d with - current_holes = Snoc (d.current_holes, (Wrap m, Termctx.PHole (vars, termctx, ty), pos)); + current_holes = Snoc (d.current_holes, (Wrap m, Termctx.PHole (vars, termctx, ty), loc)); holes = Meta.WrapSet.add (Wrap m) d.holes; } | Error cmd -> fatal (No_holes_allowed cmd) @@ -293,15 +299,15 @@ let do_holes make_msg = let d = S.get () in emit (make_msg (Bwd.length d.current_holes)); Mbwd.miter - (fun [ (Meta.Wrap m, p, (pos : unit Asai.Range.located)) ] -> + (fun [ (Meta.Wrap m, p, (loc : Asai.Range.t)) ] -> emit (Hole (Meta.name m, p)); - let s, e = Asai.Range.split (Option.get pos.loc) in + let s, e = Asai.Range.split loc in HolePos.modify (fun st -> { st with holes = Snoc (st.holes, (Meta.hole_number m, s.offset, e.offset)) })) [ d.current_holes ]; d.current_metas -(* At the end of a succesful normal command, notify the user of generated holes, save the newly created metavariables, and return the number of holes created to notify the user of. *) +(* At the end of a succesful normal command, notify the user of generated holes and save the newly created metavariables. *) let end_command make_msg = let metas = do_holes make_msg in save_metas metas; diff --git a/lib/core/global.mli b/lib/core/global.mli index b6a78505..c7f3de8c 100644 --- a/lib/core/global.mli +++ b/lib/core/global.mli @@ -29,11 +29,13 @@ val with_holes : (unit, string) Result.t -> (unit -> 'a) -> 'a val add_hole : ('a, 'b, 's) Meta.t -> - unit Asai.Range.located -> + Asai.Range.t -> vars:(string option, 'a) Bwv.t -> termctx:('a, 'b) Termctx.t -> ty:('b, kinetic) term -> status:('b, 's) Status.status -> + li:No.interval -> + ri:No.interval -> unit val hole_exists : ('a, 'b, 's) Meta.t -> bool @@ -58,6 +60,8 @@ type eternity = { ('a, 'b) Termctx.t -> ('b, kinetic) term -> ('b, 's) Status.status -> + No.interval option -> + No.interval option -> unit; } diff --git a/lib/core/metadef.ml b/lib/core/metadef.ml index 25291e65..650d21ee 100644 --- a/lib/core/metadef.ml +++ b/lib/core/metadef.ml @@ -1,5 +1,6 @@ (* This module should not be opened, but used qualified. *) +open Util open Syntax open Term @@ -9,12 +10,15 @@ type ('a, 'b, 's) t = { (* If a metavariable were "lifted" to top level with pi-types, then its type would be the pi-type over its context of the type in that context. We instead store them separately without doing the lifting. *) termctx : ('a, 'b) Termctx.t; ty : ('b, kinetic) term; + (* Holes also store their tightness intervals so we can tell whether a term would parse to replace them *) + li : No.interval option; + ri : No.interval option; } -let make ~energy ~tm ~termctx ~ty = { energy; tm; termctx; ty } +let make ~energy ~tm ~termctx ~ty ~li ~ri = { energy; tm; termctx; ty; li; ri } (* Define or redefine a metavariable. *) let define : type a b s. (b, s) term -> (a, b, s) t -> (a, b, s) t = fun tm m -> match m with - | { tm = _; termctx; ty; energy } -> { tm = `Defined tm; termctx; ty; energy } + | { tm = _; termctx; ty; energy; li; ri } -> { tm = `Defined tm; termctx; ty; energy; li; ri } diff --git a/lib/core/raw.ml b/lib/core/raw.ml index 8bedf5d7..51b03f26 100644 --- a/lib/core/raw.ml +++ b/lib/core/raw.ml @@ -143,8 +143,8 @@ module Make (I : Indices) = struct | Record : ('a, 'c, 'ac) Namevec.t located * ('ac, 'd, 'acd) tel * opacity -> 'a check (* Empty match against the first one of the arguments belonging to an empty type. *) | Refute : 'a synth located list * [ `Explicit | `Implicit ] -> 'a check - (* A hole must store the entire "state" from when it was entered, so that the user can later go back and fill it with a term that would have been valid in its original position. This includes the variables in lexical scope, which are available only during parsing, so we store them here at that point. During typechecking, when the actual metavariable is created, we save the lexical scope along with its other context and type data. A hole also stores its source location so that proofgeneral can create an overlay at that place. *) - | Hole : 'a I.scope * unit located -> 'a check + (* A hole must store the entire "state" from when it was entered, so that the user can later go back and fill it with a term that would have been valid in its original position. This includes the variables in lexical scope, which are available only during parsing, so we store them here at that point. During typechecking, when the actual metavariable is created, we save the lexical scope along with its other context and type data. A hole also stores its source location so that proofgeneral can create an overlay at that place, and the notation tightnesses of the hole location. *) + | Hole : 'a I.scope * Asai.Range.t * No.interval * No.interval -> 'a check (* Force a leaf of the case tree *) | Realize : 'a check -> 'a check (* Pass the type being checked against as the implicit first argument of a function. *) @@ -292,7 +292,7 @@ module Resolve (R : Resolver) = struct let fields2, _ = tel ctx2 fields ad in Record (locate_opt xs.loc xs2, fields2, opaq) | Refute (args, sort) -> Refute (List.map (synth ctx) args, sort) - | Hole (scope, loc) -> Hole (R.rescope ctx scope, loc) + | Hole (scope, loc, li, ri) -> Hole (R.rescope ctx scope, loc, li, ri) | Realize x -> Realize (check ctx (locate_opt tm.loc x)).value | ImplicitApp (fn, args) -> ImplicitApp (synth ctx fn, List.map (fun (l, x) -> (l, check ctx x)) args) diff --git a/lib/core/reporter.ml b/lib/core/reporter.ml index 4b0e55aa..cb2bb919 100644 --- a/lib/core/reporter.ml +++ b/lib/core/reporter.ml @@ -133,6 +133,7 @@ module Code = struct | Locked_variable : t | Locked_axiom : printable -> t | Hole : string * printable -> t + | Needs_parentheses : t | No_open_holes : t | Open_holes : int -> t | Open_holes_remaining : Asai.Range.source -> t @@ -255,6 +256,7 @@ module Code = struct | Locked_variable -> Error | Locked_axiom _ -> Error | Hole _ -> Info + | Needs_parentheses -> Info | No_open_holes -> Info | Open_holes _ -> Warning | Open_holes_remaining _ -> Error @@ -425,7 +427,8 @@ module Code = struct | No_such_hole _ -> "E3001" | Open_holes_remaining _ -> "E3002" | Hole _ -> "I3003" - | No_open_holes -> "3004" + | No_open_holes -> "I3004" + | Needs_parentheses -> "I3005" (* Command progress and success *) | Constant_defined _ -> "I0000" | Constant_assumed _ -> "I0001" @@ -679,6 +682,7 @@ module Code = struct | Locked_axiom a -> textf "axiom %a locked behind external degeneracy" pp_printed (print a) | Hole (n, ty) -> textf "@[hole %s:@,@,%a@]" n pp_printed (print ty) | No_open_holes -> text "no open holes" + | Needs_parentheses -> text "needs parentheses" | Open_holes n -> if n = 1 then text "there is 1 open hole" else textf "there are %d open holes" n | Open_holes_remaining src -> ( diff --git a/lib/parser/builtins.ml b/lib/parser/builtins.ml index 305a575e..15ff5271 100644 --- a/lib/parser/builtins.ml +++ b/lib/parser/builtins.ml @@ -510,10 +510,8 @@ let pp_abs cube space ppf obs ws = let () = set_processor abs (process_abs `Normal); set_processor cubeabs (process_abs `Cube); - set_print abs (pp_abs `Normal); - set_print cubeabs (pp_abs `Cube); - set_print_as_case abs (pp_abs `Normal); - set_print_as_case cubeabs (pp_abs `Cube) + set_print abs ~in_case:true (pp_abs `Normal); + set_print cubeabs ~in_case:true (pp_abs `Cube) (* ******************** The universe @@ -698,9 +696,7 @@ let pp_tuple space ppf obs ws = pp_ws space ppf wsrparen; pp_close_box ppf () -let () = - set_print parens pp_tuple; - set_print_as_case parens pp_tuple +let () = set_print parens ~in_case:true pp_tuple (* ******************** Comatches @@ -1391,11 +1387,11 @@ and pp_match box space ppf obs ws = (* Matches and comatches are only valid in case trees. *) let () = - set_print_as_case implicit_mtch (pp_match true); - set_print_as_case explicit_mtch (pp_match true); - set_print_as_case mtchlam (pp_match true); - set_print_as_case comatch (pp_match true); - set_print_as_case empty_co_match (pp_match true) + set_print implicit_mtch ~in_case:true (pp_match true); + set_print explicit_mtch ~in_case:true (pp_match true); + set_print mtchlam ~in_case:true (pp_match true); + set_print comatch ~in_case:true (pp_match true); + set_print empty_co_match ~in_case:true (pp_match true) (* ******************** Codatatypes @@ -1491,7 +1487,7 @@ let pp_codata space ppf obs ws = pp_ws space ppf wsrbrack; pp_close_box ppf () -let () = set_print codata pp_codata +let () = set_print codata ~in_case:true pp_codata (* ******************** Record types @@ -1650,7 +1646,7 @@ let pp_record space ppf obs ws = pp_ws space ppf wsrparen; pp_close_box ppf () -let () = set_print record pp_record +let () = set_print record ~in_case:true pp_record (* ******************** Datatypes @@ -1786,7 +1782,7 @@ let pp_data space ppf obs ws = pp_ws space ppf wsrbrack; pp_close_box ppf () -let () = set_print data pp_data +let () = set_print data ~in_case:true pp_data (* ******************** Forwards Lists @@ -1882,31 +1878,6 @@ let () = set_processor bwd { process = (fun ctx obs loc _ -> process_bwd ctx (Bwd.of_list obs) loc) }; set_print bwd (pp_lst "<") -(* ******************** - Holes - ******************** *) - -let hole = make "hole" Outfix - -let () = - set_tree hole (Closed_entry (eop Query (Done_closed hole))); - set_processor hole - { - process = - (fun ctx obs loc _ -> - match obs with - | [] -> { value = Hole (ctx, locate () loc); loc } - | _ -> fatal (Anomaly "invalid notation arguments for hole")); - }; - set_print hole @@ fun space ppf obs ws -> - match obs with - | [] -> - let wshole, ws = take Query ws in - taken_last ws; - pp_print_string ppf "?"; - pp_ws space ppf wshole - | _ -> fatal (Anomaly (Printf.sprintf "invalid notation arguments for hole: %d" (List.length ws))) - (* ******************** Generating the state ******************** *) @@ -1933,7 +1904,6 @@ let builtins = |> Situation.add record |> Situation.add data |> Situation.add fwd - |> Situation.add bwd - |> Situation.add hole) + |> Situation.add bwd) let run : type a. (unit -> a) -> a = fun f -> Situation.run_on !builtins f diff --git a/lib/parser/command.ml b/lib/parser/command.ml index 9c167f2a..de3cee7f 100644 --- a/lib/parser/command.ml +++ b/lib/parser/command.ml @@ -14,6 +14,7 @@ open Reporter open User open Modifier module Trie = Yuujinchou.Trie +module TermParse = Parse type def = { wsdef : Whitespace.t list; @@ -604,7 +605,7 @@ let parse_single (content : string) : Whitespace.t list * Command.t option = | _ -> Core.Reporter.fatal (Anomaly "interactive parse doesn't start with Bof") let show_hole err = function - | Eternity.Find_number (m, { tm = `Undefined; termctx; ty; energy = _ }, { vars; _ }) -> + | Eternity.Find_number (m, { tm = `Undefined; termctx; ty; _ }, { vars; _ }) -> emit (Hole (Meta.name m, Termctx.PHole (vars, termctx, ty))) | _ -> fatal err @@ -698,8 +699,8 @@ let execute : action_taken:(unit -> unit) -> get_file:(string -> Scope.trie) -> readback_at Ctx.empty etm ety else ctm in let bty = readback_at Ctx.empty ety (Syntax.universe D.zero) in - let utm = unparse Names.empty btm Interval.entire Interval.entire in - let uty = unparse Names.empty bty Interval.entire Interval.entire in + let utm = unparse Names.empty btm No.Interval.entire No.Interval.entire in + let uty = unparse Names.empty bty No.Interval.entire No.Interval.entire in let ppf = Format.std_formatter in pp_open_vbox ppf 2; pp_term `None ppf (Term utm); @@ -781,19 +782,38 @@ let execute : action_taken:(unit -> unit) -> get_file:(string -> Scope.trie) -> () | _ -> ()) (Trie.to_seq (Trie.find_subtree [ "notations" ] trie)) - | Solve { number; tm = Term tm; _ } -> ( + | Solve data -> ( (* Solve does NOT create a new history entry because it is NOT undoable. *) let (Find_number - (m, { tm = metatm; termctx; ty; energy = _ }, { global; scope; status; vars })) = - Eternity.find_number number in + (m, { tm = metatm; termctx; ty; energy = _; li; ri }, { global; scope; status; vars })) + = + Eternity.find_number data.number in match metatm with | `Undefined -> History.run_with_scope ~init_visible:scope @@ fun () -> - let tm = process vars tm in + let (Term tm) = data.tm in + let ptm = process vars tm in (* 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. *) Global.HolePos.modify (fun st -> - { st with offset = (fst (Asai.Range.split (Option.get tm.loc))).offset }); - Core.Command.execute (Solve (global, status, termctx, tm, ty, Eternity.solve m)) + { st with offset = (fst (Asai.Range.split (Option.get ptm.loc))).offset }); + let solve ctm = + Eternity.solve m ctm; + match (li, ri) with + | Some (Interval li), Some (Interval ri) -> + let buf = Buffer.create 20 in + let ppf = Format.formatter_of_buffer buf in + (Print.State.as_case @@ fun () -> pp_term `None ppf data.tm); + Format.pp_print_flush ppf (); + Reporter.try_with ~fatal:(fun _ -> + (* data.tm <- Term (parenthesize tm) *) + emit Needs_parentheses) + @@ fun () -> + let _ = + TermParse.Term.parse ~li:(Interval li) ~ri:(Interval ri) + (`String { content = Buffer.contents buf; title = None }) in + () + | _ -> fatal (Anomaly "tightness missing for hole") in + Core.Command.execute (Solve (global, status, termctx, ptm, ty, solve)) | `Defined _ | `Axiom -> (* Yes, this is an anomaly and not a user error, because find_number should only be looking at the unsolved holes. *) fatal (Anomaly "hole already defined")) diff --git a/lib/parser/eternity.ml b/lib/parser/eternity.ml index 9fa784c4..ab5e7a7d 100644 --- a/lib/parser/eternity.ml +++ b/lib/parser/eternity.ml @@ -50,13 +50,15 @@ let () = let* x = Metamap.find_opt m (S.get ()).map in return x.def); add = - (fun m vars termctx ty status -> + (fun m vars termctx ty status li ri -> S.modify (fun { map } -> { map = Metamap.add m { - def = Metadef.make ~tm:`Undefined ~termctx ~ty ~energy:(Status.energy status); + def = + Metadef.make ~tm:`Undefined ~termctx ~ty ~energy:(Status.energy status) ~li + ~ri; homewhen = { global = Global.get (); scope = Scope.get_visible (); status; vars }; } diff --git a/lib/parser/interval.ml b/lib/parser/interval.ml deleted file mode 100644 index 0a356c9b..00000000 --- a/lib/parser/interval.ml +++ /dev/null @@ -1,47 +0,0 @@ -open Util - -(* An "upper tightness interval" is of the form (p,+ω] or [p,+ω] for some tightness p. Ordinarily we would call these "open" and "closed" intervals, but due to the potential confusion with "closed" and "open" notations we call them instead "strict" and "nonstrict". *) - -type ('a, 's) tt = { strictness : 's No.strictness; endpoint : 'a No.t } -type t = Interval : ('s, 'a) tt -> t - -let empty : (No.plus_omega, No.strict) tt = { strictness = Strict; endpoint = No.plus_omega } - -let entire : (No.minus_omega, No.nonstrict) tt = - { strictness = Nonstrict; endpoint = No.minus_omega } - -let plus_omega_only : (No.plus_omega, No.nonstrict) tt = - { strictness = Nonstrict; endpoint = No.plus_omega } - -let to_string = function - | Interval { strictness = Nonstrict; endpoint } -> - Printf.sprintf "[%s,inf]" (No.to_string endpoint) - | Interval { strictness = Strict; endpoint } -> Printf.sprintf "(%s,inf]" (No.to_string endpoint) - -let contains : type a s b. (a, s) tt -> b No.t -> (a, s, b) No.lt option = - fun { strictness; endpoint } x -> No.compare strictness endpoint x - -let union : t -> t -> t = - fun (Interval t1 as i1) (Interval t2 as i2) -> - match No.compare Strict t1.endpoint t2.endpoint with - | Some _ -> i1 - | None -> ( - match No.compare Strict t2.endpoint t1.endpoint with - | Some _ -> i2 - | None -> ( - match (t1.strictness, t2.strictness) with - | Strict, Strict -> Interval { t1 with strictness = Strict } - | _ -> Interval { t1 with strictness = Nonstrict })) - -type (_, _, _, _) subset = - | Subset_strict : ('t2, No.strict, 't1) No.lt -> ('t1, 's1, 't2, 's2) subset - | Subset_eq : ('t, 's, 't, 's) subset - | Subset_nonstrict_strict : ('t, No.strict, 't, No.nonstrict) subset - -let subset_contains : - type t1 s1 t2 s2 a. (t1, s1, t2, s2) subset -> (t1, s1, a) No.lt -> (t2, s2, a) No.lt = - fun sub lt1 -> - match sub with - | Subset_strict lt2 -> No.lt_trans Strict_any lt2 lt1 - | Subset_eq -> lt1 - | Subset_nonstrict_strict -> No.lt_to_le lt1 diff --git a/lib/parser/notation.ml b/lib/parser/notation.ml index 34a459f4..f7579291 100644 --- a/lib/parser/notation.ml +++ b/lib/parser/notation.ml @@ -131,6 +131,9 @@ and (_, _, _, _) parse = | Superscript : ('lt, 'ls, No.plus_omega, No.strict) parse located option * string * Whitespace.t list -> ('lt, 'ls, 'rt, 'rs) parse + | Hole : + ('lt, 'ls) No.iinterval * ('rt, 'rs) No.iinterval * Whitespace.t list + -> ('lt, 'ls, 'rt, 'rs) parse (* A postproccesing function has to be polymorphic over the length of the context so as to produce intrinsically well-scoped terms. Thus, we have to wrap it as a field of a record (or object). The whitespace argument is often ignored, but it allows complicated notation processing functions to be shared between the processor and the printer, and sometimes the processing functions need to inspect the sequence of tokens which is stored with the whitespace. *) and processor = { @@ -164,9 +167,9 @@ and ('left, 'tight, 'right) notation = { (* The remaining fields are mutable because they have to be able to refer to the notation object itself, so we have a circular data structure. They aren't expected to mutate further after being set once. Thus we store them as options, to record whether they have been set. *) mutable tree : ('left, 'tight) notation_entry option; mutable processor : processor option; - (* Some notations only make sense in terms, others only make sense in case trees, and some make sense in either. Thus, a notation can supply either or both of these printing functions. *) mutable print : printer option; - mutable print_as_case : printer option; + (* Whether this notation can appear in a case tree. Otherwise, encountering it terminates the case tree in a leaf. *) + mutable print_in_case : bool; } module Notation = struct @@ -208,7 +211,7 @@ let notn : (* When parsing from left to right, we have to return a partial parse tree without knowing yet what tightness interval it will have to be in from the right. So we return it as a callback that takes that interval as an argument and can fail, returning the name of the offending notation if it fails. One could argue that instead the allowable tightness intervals should be returned along with the partial parse tree and used to restrict the allowable notations parsed afterwards. But that would require indexing those pre-merged trees by *two* tightness values, so that we'd have to maintain n² such trees where n is the number of tightness values in use, and that makes me worry a bit about efficiency. Doing it this way also makes it easier to trap it and issue a more informative error message. *) type ('lt, 'ls) right_wrapped_parse = { - get : 'rt 'rs. ('rt, 'rs) Interval.tt -> (('lt, 'ls, 'rt, 'rs) parse located, string) Result.t; + get : 'rt 'rs. ('rt, 'rs) No.iinterval -> (('lt, 'ls, 'rt, 'rs) parse located, string) Result.t; } (* The primary key is used to compare notations. *) @@ -231,12 +234,12 @@ let left n = n.left let right n = n.right (* A notation has associated upper tightness intervals on both the left and the right, which specify what tightnesses of other notations can appear in an open subterm on that side. Thus, both of these intervals start at the tightness of the notation, with their open- or closed-ness determined by its associativity. *) -let interval_left : ('s opn, 'tight, 'right) notation -> ('tight, 's) Interval.tt = +let interval_left : ('s opn, 'tight, 'right) notation -> ('tight, 's) No.iinterval = fun n -> let (Open strictness) = left n in { strictness; endpoint = tightness n } -let interval_right : ('left, 'tight, 's opn) notation -> ('tight, 's) Interval.tt = +let interval_right : ('left, 'tight, 's opn) notation -> ('tight, 's) No.iinterval = fun n -> let (Open strictness) = right n in { strictness; endpoint = tightness n } @@ -261,9 +264,11 @@ let set_processor n c = | None -> n.processor <- Some c let print n = n.print -let set_print n p = n.print <- Some p -let print_as_case n = n.print_as_case -let set_print_as_case n p = n.print_as_case <- Some p +let print_in_case n = n.print_in_case + +let set_print n ?(in_case = false) p = + n.print <- Some p; + n.print_in_case <- in_case (* Create a new notation with specified name, fixity, and tightness. Its mutable fields must be set later. *) let make : @@ -282,8 +287,8 @@ let make : right; tree = None; print = None; - print_as_case = None; processor = None; + print_in_case = false; } let rec split_last_whitespace (ws : Whitespace.alist) : Whitespace.alist * Whitespace.t list = @@ -330,7 +335,10 @@ let rec split_ending_whitespace : ({ value = Field (f, first); loc }, rest) | Superscript (x, s, ws) -> let first, rest = Whitespace.split ws in - ({ value = Superscript (x, s, first); loc }, rest)) + ({ value = Superscript (x, s, first); loc }, rest) + | Hole (li, ri, ws) -> + let first, rest = Whitespace.split ws in + ({ value = Hole (li, ri, first); loc }, rest)) (* Helper functions for constructing notation trees *) @@ -363,16 +371,16 @@ let rec to_branch : type t s. (t, s) tree -> (t, s) branch option = function | Lazy (lazy t) -> to_branch t let rec lower_tree : - type t1 s1 t2 s2. (t2, s2, t1, s1) Interval.subset -> (t2, s2) tree -> (t1, s1) tree = + type t1 s1 t2 s2. (t2, s2, t1, s1) No.Interval.subset -> (t2, s2) tree -> (t1, s1) tree = fun sub xs -> match xs with | Inner br -> Inner (lower_branch sub br) - | Done_open (lt, n) -> Done_open (Interval.subset_contains sub lt, n) + | Done_open (lt, n) -> Done_open (No.Interval.subset_contains sub lt, n) | Done_closed n -> Done_closed n | Lazy tr -> Lazy (lazy (lower_tree sub (Lazy.force tr))) and lower_branch : - type t1 s1 t2 s2. (t2, s2, t1, s1) Interval.subset -> (t2, s2) branch -> (t1, s1) branch = + type t1 s1 t2 s2. (t2, s2, t1, s1) No.Interval.subset -> (t2, s2) branch -> (t1, s1) branch = fun sub { ops; field; term } -> { ops = TokMap.map (lower_tree sub) ops; @@ -380,7 +388,8 @@ and lower_branch : term = Option.map (TokMap.map (lower_tree sub)) term; } -let lower : type t1 s1 t2 s2. (t2, s2, t1, s1) Interval.subset -> (t2, s2) entry -> (t1, s1) entry = +let lower : + type t1 s1 t2 s2. (t2, s2, t1, s1) No.Interval.subset -> (t2, s2) entry -> (t1, s1) entry = fun sub map -> TokMap.map (lower_tree sub) map let rec names : type t s. (t, s) tree -> string list = function @@ -397,7 +406,7 @@ and names_tmap : type t s. (t, s) tree TokMap.t -> string list = let rec merge_tree : type t1 s1 t2 s2. - (t2, s2, t1, s1) Interval.subset -> (t1, s1) tree -> (t2, s2) tree -> (t1, s1) tree = + (t2, s2, t1, s1) No.Interval.subset -> (t1, s1) tree -> (t2, s2) tree -> (t1, s1) tree = fun sub xs ys -> let open Monad.Ops (Monad.Maybe) in Option.value @@ -416,7 +425,7 @@ let rec merge_tree : and merge_tmap : type t1 s1 t2 s2. - (t2, s2, t1, s1) Interval.subset -> + (t2, s2, t1, s1) No.Interval.subset -> (t1, s1) tree TokMap.t -> (t2, s2) tree TokMap.t -> (t1, s1) tree TokMap.t = @@ -430,7 +439,7 @@ and merge_tmap : and merge_branch : type t1 s1 t2 s2. - (t2, s2, t1, s1) Interval.subset -> (t1, s1) branch -> (t2, s2) branch -> (t1, s1) branch = + (t2, s2, t1, s1) No.Interval.subset -> (t1, s1) branch -> (t2, s2) branch -> (t1, s1) branch = fun sub x y -> let ops = merge_tmap sub x.ops y.ops in let field = merge_opt (merge_tree sub) (lower_tree sub) x.field y.field in @@ -439,5 +448,5 @@ and merge_branch : let merge : type t1 t2 s1 s2. - (t2, s2, t1, s1) Interval.subset -> (t1, s1) entry -> (t2, s2) entry -> (t1, s1) entry = + (t2, s2, t1, s1) No.Interval.subset -> (t1, s1) entry -> (t2, s2) entry -> (t1, s1) entry = fun sub xs ys -> merge_tmap sub xs ys diff --git a/lib/parser/notation.mli b/lib/parser/notation.mli index 0e7784fa..838a91a5 100644 --- a/lib/parser/notation.mli +++ b/lib/parser/notation.mli @@ -58,6 +58,9 @@ and (_, _, _, _) parse = | Superscript : ('lt, 'ls, No.plus_omega, No.strict) parse located option * string * Whitespace.t list -> ('lt, 'ls, 'rt, 'rs) parse + | Hole : + ('lt, 'ls) No.iinterval * ('rt, 'rs) No.iinterval * Whitespace.t list + -> ('lt, 'ls, 'rt, 'rs) parse and ('left, 'tight) notation_entry = | Open_entry : ('tight, No.nonstrict) entry -> ('strict opn, 'tight) notation_entry @@ -122,23 +125,22 @@ val notn : ('left, 'tight, 'right, 'lt, 'ls, 'rt, 'rs) parsed_notn -> ('left, 'tight, 'right) notation type ('lt, 'ls) right_wrapped_parse = { - get : 'rt 'rs. ('rt, 'rs) Interval.tt -> (('lt, 'ls, 'rt, 'rs) parse located, string) Result.t; + get : 'rt 'rs. ('rt, 'rs) No.iinterval -> (('lt, 'ls, 'rt, 'rs) parse located, string) Result.t; } val name : ('left, 'tight, 'right) notation -> string val tightness : ('left, 'tight, 'right) notation -> 'tight No.t val left : ('left, 'tight, 'right) notation -> 'left openness val right : ('left, 'tight, 'right) notation -> 'right openness -val interval_left : ('s opn, 'tight, 'right) notation -> ('tight, 's) Interval.tt -val interval_right : ('left, 'tight, 's opn) notation -> ('tight, 's) Interval.tt +val interval_left : ('s opn, 'tight, 'right) notation -> ('tight, 's) No.iinterval +val interval_right : ('left, 'tight, 's opn) notation -> ('tight, 's) No.iinterval val tree : ('left, 'tight, 'right) notation -> ('left, 'tight) notation_entry val set_tree : ('left, 'tight, 'right) notation -> ('left, 'tight) notation_entry -> unit val processor : ('left, 'tight, 'right) notation -> processor val set_processor : ('left, 'tight, 'right) notation -> processor -> unit val print : ('left, 'tight, 'right) notation -> printer option -val set_print : ('left, 'tight, 'right) notation -> printer -> unit -val print_as_case : ('left, 'tight, 'right) notation -> printer option -val set_print_as_case : ('left, 'tight, 'right) notation -> printer -> unit +val print_in_case : ('left, 'tight, 'right) notation -> bool +val set_print : ('left, 'tight, 'right) notation -> ?in_case:bool -> printer -> unit val make : string -> ('left, 'tight, 'right) fixity -> ('left, 'tight, 'right) notation val equal : ('l1, 't1, 'r1) notation -> ('l2, 't2, 'r2) notation -> bool @@ -164,7 +166,10 @@ val eops : (TokMap.key * 'a) list -> 'a TokMap.t val empty_entry : 'a TokMap.t (* *) -val lower : ('t2, 's2, 't1, 's1) Interval.subset -> ('t2, 's2) entry -> ('t1, 's1) entry +val lower : ('t2, 's2, 't1, 's1) No.Interval.subset -> ('t2, 's2) entry -> ('t1, 's1) entry val merge : - ('t2, 's2, 't1, 's1) Interval.subset -> ('t1, 's1) entry -> ('t2, 's2) entry -> ('t1, 's1) entry + ('t2, 's2, 't1, 's1) No.Interval.subset -> + ('t1, 's1) entry -> + ('t2, 's2) entry -> + ('t1, 's1) entry diff --git a/lib/parser/parse.ml b/lib/parser/parse.ml index 80475bc1..6d40875d 100644 --- a/lib/parser/parse.ml +++ b/lib/parser/parse.ml @@ -51,8 +51,8 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct inner_nonterm br obs ws (* This is an *interior* term, so it has no tightness restrictions on what notations can occur inside, and is ended by the specified ending tokens. *) - let* subterm = lclosed Interval.entire e in - match subterm.get Interval.entire with + let* subterm = lclosed No.Interval.entire e in + match subterm.get No.Interval.entire with | Ok tm -> tree_op e (Snoc (obs, Term tm)) ws | Error n -> fatal (Anomaly (Printf.sprintf "Interior term failed on notation %s" n))) | Inner ({ term = None; _ } as br) -> inner_nonterm br obs ws @@ -116,7 +116,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct (* "lclosed" is passed an upper tightness interval and an additional set of ending ops (stored as a map, since that's how they occur naturally, but here we ignore the values and look only at the keys). It parses an arbitrary left-closed tree (pre-merged). The interior terms are calls to "lclosed" with the next ops passed as the ending ones. *) and lclosed : type lt ls rt rs. - (lt, ls) Interval.tt -> (rt, rs) tree TokMap.t -> (lt, ls) right_wrapped_parse t = + (lt, ls) No.iinterval -> (rt, rs) tree TokMap.t -> (lt, ls) right_wrapped_parse t = fun tight stop -> let* res = (let* inner_loc, (inner, ws, notn) = located (entry (Situation.Current.left_closeds ())) in @@ -136,7 +136,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct get = (* Both the notation and anything in its right-open argument must be allowed in a right-tightness interval. *) (fun ivl -> - match Interval.contains ivl (tightness notn) with + match No.Interval.contains ivl (tightness notn) with | None -> Error (name notn) | Some right_ok -> ( match last_arg.get ivl with @@ -157,17 +157,19 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct (* Constructor names have already been validated by the lexer. *) | Constr x -> Some ((`Constr x, w), state) | Underscore -> Some ((`Placeholder, w), state) + | Query -> Some ((`Hole, w), state) | _ -> None)) in with_supers { get = - (fun _ -> + (fun ri -> Ok (locate loc (match tm with | `Ident x -> Ident (x, w) | `Constr x -> Constr (x, w) - | `Placeholder -> Placeholder w))); + | `Placeholder -> Placeholder w + | `Hole -> Hole (tight, ri, w)))); } in (* Then "lclosed" ends by calling "lopen" with its interval and ending ops, and also its own result (with extra argument added if necessary). Note that we don't incorporate d.tightness here; it is only used to find the delimiter of the right-hand argument if the notation we parsed was right-open. In particular, therefore, a right-closed notation can be followed by anything, even a left-open notation that binds tighter than it does; the only restriction is if we're inside the right-hand argument of some containing right-open notation, so we inherit a "tight" from there. *) lopen tight stop res @@ -201,7 +203,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct { get = (fun _ -> - match arg.get Interval.empty with + match arg.get No.Interval.empty with | Ok x -> Ok { @@ -221,12 +223,12 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct (* "lopen" is passed an upper tightness interval and a set of ending ops, plus a parsed result for the left open argument and the tightness of the outermost notation in that argument if it is right-open. *) and lopen : type lt ls rt rs. - (lt, ls) Interval.tt -> + (lt, ls) No.iinterval -> (rt, rs) tree TokMap.t -> (lt, ls) right_wrapped_parse -> (lt, ls) right_wrapped_parse t = fun tight stop first_arg -> - match Interval.contains tight No.plus_omega with + match No.Interval.contains tight No.plus_omega with (* If the left tightness interval is the empty one (+ω,+ω], we aren't allowed to go on at all. Otherwise, we need to get a witness of nonemptiness of that interval, for the case when we end up with an application. *) | None -> succeed first_arg | Some nontrivial -> @@ -238,7 +240,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct let open Monad.Ops (Monad.Maybe) in let* (Interval ivl) = Situation.Current.left_opens tok in let t = tight.endpoint in - let* _ = Interval.contains ivl t in + let* _ = No.Interval.contains ivl t in return (first_arg, state))) (* Otherwise, we parse either an arbitrary left-closed tree (applying the given result to it as a function) or an arbitrary left-open tree with tightness in the given interval (passing the given result as the starting open argument). Interior terms are treated as in "lclosed". *) (let* res = @@ -267,7 +269,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct get = (fun ivl -> match - (last_arg.get ivl, Interval.contains ivl (tightness notn)) + (last_arg.get ivl, No.Interval.contains ivl (tightness notn)) with | Ok last, Some right_ok -> Ok @@ -280,7 +282,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct | _, None -> Error (name notn)); }) | Closed_in_interval notn -> ( - match (first_arg.get Interval.plus_omega_only, right notn) with + match (first_arg.get No.Interval.plus_omega_only, right notn) with | Error e, _ -> fail (No_relative_precedence (inner_loc, e, "application")) | Ok fn, Closed -> let* sups = supers in @@ -288,7 +290,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct { get = (fun ivl -> - match Interval.contains ivl No.plus_omega with + match No.Interval.contains ivl No.plus_omega with | None -> Error "application 1" | Some right_ok -> ( let arg = @@ -313,8 +315,8 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct (fun ivl -> match ( last_arg.get ivl, - Interval.contains ivl (tightness notn), - Interval.contains ivl No.plus_omega ) + No.Interval.contains ivl (tightness notn), + No.Interval.contains ivl No.plus_omega ) with | Ok last, Some right_ok, Some right_app -> let arg_loc = Range.merge_opt (Some inner_loc) last.loc in @@ -348,29 +350,31 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct | Constr x -> Some ((`Constr x, w), state) | Underscore -> Some ((`Placeholder, w), state) | Field x -> Some ((`Field x, w), state) + | Query -> Some ((`Hole, w), state) | _ -> None)) in let* sups = supers in - match first_arg.get Interval.plus_omega_only with + match first_arg.get No.Interval.plus_omega_only with | Error e -> fail (No_relative_precedence (arg_loc, e, "application")) | Ok fn -> return { get = (fun ivl -> - match Interval.contains ivl No.plus_omega with + match No.Interval.contains ivl No.plus_omega with | Some right_ok -> ( let arg = superify { get = - (fun _ -> + (fun ri -> Ok (locate arg_loc (match arg with | `Ident x -> Ident (x, w) | `Constr x -> Constr (x, w) | `Placeholder -> Placeholder w - | `Field x -> Field (x, w)))); + | `Field x -> Field (x, w) + | `Hole -> Hole (No.Interval.empty, ri, w)))); } sups in match arg.get ivl with @@ -389,14 +393,15 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct succeed first_arg (* The master term-parsing combinator parses an lclosed of arbitrary tightness, with specified ending tokens. If the ending tokens are empty, it must extend until the next token that can't be part of a term (like a command name or EOF). It does NOT parse the initial Bof token, since it can also appear as part of a command. *) - let term toks = + let term ?(li = No.Interval No.Interval.entire) ?(ri = No.Interval No.Interval.entire) toks = + let Interval li, Interval ri = (li, ri) in let tokmap = List.fold_left (fun map tok -> TokMap.add tok (Lazy (lazy (fatal (Anomaly "dummy notation tree accessed")))) map) TokMap.empty toks in - let* tm = lclosed Interval.entire tokmap in - match tm.get Interval.entire with + let* tm = lclosed li tokmap in + match tm.get ri with | Ok tm -> return (Term tm) | Error e -> fatal (Anomaly ("Outer term failed: " ^ e)) @@ -423,15 +428,15 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct let bof = step (fun state _ (tok, ws) -> if tok = Bof then Some (ws, state) else None) (* TODO: Save the whitespace! *) - let term_only () = + let term_only ?li ?ri () = let* _ = bof in - term [] + term ?li ?ri [] end module Term = struct module C = Combinators (ParseTree) - let parse (source : Asai.Range.source) : C.Lex_and_parse.t = + let parse ?li ?ri (source : Asai.Range.source) : C.Lex_and_parse.t = let (env : Range.Data.t), run = match source with | `String src -> @@ -442,7 +447,7 @@ module Term = struct ( { source = `File name; length = In_channel.length ic }, fun p -> C.Lex_and_parse.run_on_channel ic p ) in Range.run ~env @@ fun () -> - let p = C.Lex_and_parse.make Lexer.Parser.start (C.Basic.make () (C.term_only ())) in + let p = C.Lex_and_parse.make Lexer.Parser.start (C.Basic.make () (C.term_only ?li ?ri ())) in let p = run p in C.ensure_success p diff --git a/lib/parser/postprocess.ml b/lib/parser/postprocess.ml index 7a3db497..08a285c3 100644 --- a/lib/parser/postprocess.ml +++ b/lib/parser/postprocess.ml @@ -106,6 +106,7 @@ let rec process : { value = Synth (Act (str, s, body)); loc } | None -> fatal (Invalid_degeneracy str)) | Superscript (None, _, _) -> fatal (Anomaly "degeneracy is head") + | Hole (li, ri, _) -> { value = Hole (ctx, Option.get loc, Interval li, Interval ri); loc } and process_spine : type n lt ls rt rs. diff --git a/lib/parser/print.ml b/lib/parser/print.ml index dfc0bfa3..86446cb9 100644 --- a/lib/parser/print.ml +++ b/lib/parser/print.ml @@ -136,12 +136,10 @@ let pp_ws (space : space) (ppf : formatter) (ws : Whitespace.t list) : unit = (* Print a parse tree. *) let rec pp_term (space : space) (ppf : formatter) (wtr : observation) : unit = let (Term tr) = wtr in - match State.read () with - | `Case -> ( - match tr.value with - | Notn n -> pp_notn_case space ppf (notn n) (args n) (whitespace n) - | _ -> State.as_term @@ fun () -> pp_term space ppf wtr) - | `Term -> ( + match tr.value with + | Notn n when print_in_case (notn n) -> pp_notn space ppf (notn n) (args n) (whitespace n) + | _ -> ( + State.as_term @@ fun () -> match tr.value with | Notn n -> pp_notn space ppf (notn n) (args n) (whitespace n) | App _ -> @@ -167,6 +165,9 @@ let rec pp_term (space : space) (ppf : formatter) (wtr : observation) : unit = pp_ws space ppf w | Superscript (None, s, w) -> pp_superscript ppf s; + pp_ws space ppf w + | Hole (_, _, w) -> + pp_print_string ppf "?"; pp_ws space ppf w) and pp_superscript ppf str = @@ -180,19 +181,6 @@ and pp_superscript ppf str = pp_utf_8 ppf str; pp_utf_8 ppf ")" -and pp_notn_case : - type left tight right. - space -> - formatter -> - (left, tight, right) notation -> - observation list -> - Whitespace.alist -> - unit = - fun space ppf n obs ws -> - match print_as_case n with - | Some pp -> pp space ppf obs ws - | None -> State.as_term @@ fun () -> pp_notn space ppf n obs ws - and pp_notn : type left tight right. space -> diff --git a/lib/parser/situation.ml b/lib/parser/situation.ml index 72b61555..cf2829ae 100644 --- a/lib/parser/situation.ml +++ b/lib/parser/situation.ml @@ -27,7 +27,7 @@ type t = { (* For each upper tightness interval, we store a pre-merged tree of all left-closed trees along with all left-open trees whose tightness lies in that interval. In particular, for the empty interval (+ω,+ω] this contains only the left-closed trees, and for the entire interval [-ω,+ω] it contains all notation trees. *) tighters : unit EntryMap.t; (* We store a map associating to each starting token of a left-open notation its left-hand upper tightness interval. If there is more than one left-open notation starting with the same token, we store the loosest such interval. *) - left_opens : Interval.t TokMap.t; + left_opens : No.interval TokMap.t; (* For unparsing we also store backwards maps turning constants and constructors into notations. Since the arguments of a notation can occur in a different order from those of the constant or constructor, we store lists of the argument names in the order they occur in the pattern and in the term value. Note that these permutations are only used for printing; when parsing, the postprocessor function must ALSO incorporate the inverse permutation. *) unparse : User.notation PrintMap.t; } @@ -95,13 +95,13 @@ let add : type left tight right. (left, tight, right) notation -> t -> t = let left_opens = match (left n, tree n) with | Open _, Open_entry tr -> - let ivl = Interval.Interval (interval_left n) in + let ivl = No.Interval (interval_left n) in TokMap.fold (fun tok _ map -> TokMap.update tok (function | None -> Some ivl - | Some ivl2 -> Some (Interval.union ivl ivl2)) + | Some ivl2 -> Some (No.Interval.union ivl ivl2)) map) tr s.left_opens | Closed, _ -> s.left_opens in @@ -156,14 +156,14 @@ module Current = struct let left_closeds : unit -> (No.plus_omega, No.strict) entry = fun () -> (Option.get (EntryMap.find_opt No.plus_omega (S.get ()).tighters)).strict - let tighters : type strict tight. (tight, strict) Interval.tt -> (tight, strict) entry = + let tighters : type strict tight. (tight, strict) No.iinterval -> (tight, strict) entry = fun { strictness; endpoint } -> let ep = Option.get (EntryMap.find_opt endpoint (S.get ()).tighters) in match strictness with | Nonstrict -> ep.nonstrict | Strict -> ep.strict - let left_opens : Token.t -> Interval.t option = + let left_opens : Token.t -> No.interval option = fun tok -> TokMap.find_opt tok (S.get ()).left_opens let unparse : PrintKey.t -> User.notation option = fun c -> PrintMap.find_opt c (S.get ()).unparse diff --git a/lib/parser/unparse.ml b/lib/parser/unparse.ml index 2646f4bc..3999c9b2 100644 --- a/lib/parser/unparse.ml +++ b/lib/parser/unparse.ml @@ -49,7 +49,7 @@ let parenthesize_maybe (tm : ('lt, 'ls, 'rt, 'rs) parse located) = type unparser = { unparse : 'lt 'ls 'rt 'rs. - ('lt, 'ls) Interval.tt -> ('rt, 'rs) Interval.tt -> ('lt, 'ls, 'rt, 'rs) parse located; + ('lt, 'ls) No.iinterval -> ('rt, 'rs) No.iinterval -> ('lt, 'ls, 'rt, 'rs) parse located; } (* Unparse a notation together with all its arguments. *) @@ -57,8 +57,8 @@ let unparse_notation : type left tight right lt ls rt rs. (left, tight, right) notation -> unparser Bwd.t -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun notn args li ri -> let t = tightness notn in @@ -67,15 +67,16 @@ let unparse_notation : | Open _, Open _ -> ( match split_first args with | Some (first, Snoc (inner, last)) -> ( - let inner = Bwd.map (fun tm -> Term (tm.unparse Interval.entire Interval.entire)) inner in - match (Interval.contains li t, Interval.contains ri t) with + let inner = + Bwd.map (fun tm -> Term (tm.unparse No.Interval.entire No.Interval.entire)) inner in + match (No.Interval.contains li t, No.Interval.contains ri t) with | Some left_ok, Some right_ok -> let first = first.unparse li (interval_left notn) in let last = last.unparse (interval_right notn) ri in unlocated (infix ~notn ~ws:[] ~first ~inner ~last ~left_ok ~right_ok) | _ -> - let first = first.unparse Interval.entire (interval_left notn) in - let last = last.unparse (interval_right notn) Interval.entire in + let first = first.unparse No.Interval.entire (interval_left notn) in + let last = last.unparse (interval_right notn) No.Interval.entire in let left_ok = No.minusomega_le t in let right_ok = No.minusomega_le t in parenthesize (unlocated (infix ~notn ~ws:[] ~first ~inner ~last ~left_ok ~right_ok))) @@ -83,31 +84,33 @@ let unparse_notation : | Closed, Open _ -> ( match args with | Snoc (inner, last) -> ( - let inner = Bwd.map (fun tm -> Term (tm.unparse Interval.entire Interval.entire)) inner in - match Interval.contains ri t with + let inner = + Bwd.map (fun tm -> Term (tm.unparse No.Interval.entire No.Interval.entire)) inner in + match No.Interval.contains ri t with | Some right_ok -> let last = last.unparse (interval_right notn) ri in unlocated (prefix ~notn ~ws:[] ~inner ~last ~right_ok) | _ -> - let last = last.unparse (interval_right notn) Interval.entire in + let last = last.unparse (interval_right notn) No.Interval.entire in let right_ok = No.minusomega_le t in parenthesize (unlocated (prefix ~notn ~ws:[] ~inner ~last ~right_ok))) | _ -> fatal (Anomaly "missing argument unparsing prefix")) | Open _, Closed -> ( match split_first args with | Some (first, inner) -> ( - let inner = Bwd.map (fun tm -> Term (tm.unparse Interval.entire Interval.entire)) inner in - match Interval.contains li t with + let inner = + Bwd.map (fun tm -> Term (tm.unparse No.Interval.entire No.Interval.entire)) inner in + match No.Interval.contains li t with | Some left_ok -> let first = first.unparse li (interval_left notn) in unlocated (postfix ~notn ~ws:[] ~first ~inner ~left_ok) | _ -> - let first = first.unparse Interval.entire (interval_left notn) in + let first = first.unparse No.Interval.entire (interval_left notn) in let left_ok = No.minusomega_le t in parenthesize (unlocated (postfix ~notn ~ws:[] ~first ~inner ~left_ok))) | _ -> fatal (Anomaly "missing argument unparsing postfix")) | Closed, Closed -> - let inner = Bwd.map (fun tm -> Term (tm.unparse Interval.entire Interval.entire)) args in + let inner = Bwd.map (fun tm -> Term (tm.unparse No.Interval.entire No.Interval.entire)) args in unlocated (outfix ~notn ~ws:[] ~inner) (* Unparse a variable name, possibly anonymous. *) @@ -119,7 +122,7 @@ let unparse_var : type lt ls rt rs. string option -> (lt, ls, rt, rs) parse loca let rec unparse_abs : type li ls ri rs. string option Bwd.t -> - (li, ls) Interval.tt -> + (li, ls) No.iinterval -> (li, ls, No.plus_omega) No.lt -> (ri, rs, No.plus_omega) No.lt -> (li, ls, ri, rs) parse located = @@ -196,8 +199,8 @@ let rec unparse : type n lt ls rt rs s. n Names.t -> (n, s) term -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars tm li ri -> match tm with @@ -228,18 +231,18 @@ let rec unparse : unparse_spine vars (`Field (head, fld)) (Bwd.map (make_unparser vars) args) li ri) | Act (tm, s) -> unparse_act vars { unparse = (fun li ri -> unparse vars tm li ri) } s li ri | Let (x, tm, body) -> ( - let tm = unparse vars tm Interval.entire Interval.entire in + let tm = unparse vars tm No.Interval.entire No.Interval.entire in (* If a let-in doesn't fit in its interval, we have to parenthesize it. *) let x, vars = Names.add_cube D.zero vars x in - match Interval.contains ri No.minus_omega with + match No.Interval.contains ri No.minus_omega with | Some right_ok -> - let body = unparse vars body Interval.entire ri in + let body = unparse vars body No.Interval.entire ri in unlocated (prefix ~notn:letin ~ws:[] ~inner:(Snoc (Snoc (Emp, Term (unparse_var x)), Term tm)) ~last:body ~right_ok) | None -> - let body = unparse vars body Interval.entire Interval.entire in + let body = unparse vars body No.Interval.entire No.Interval.entire in let right_ok = No.le_refl No.minus_omega in parenthesize (unlocated @@ -258,7 +261,7 @@ let rec unparse : ~inner: (Abwd.fold (fun fld (tm, l) acc -> - let tm = unparse vars tm Interval.entire Interval.entire in + let tm = unparse vars tm No.Interval.entire No.Interval.entire in Snoc ( acc, Term @@ -286,7 +289,7 @@ let rec unparse : | Some args -> let inner = Mbwd.mmap - (fun [ tm ] -> Term (unparse vars tm Interval.entire Interval.entire)) + (fun [ tm ] -> Term (unparse vars tm No.Interval.entire No.Interval.entire)) [ args ] in unlocated (outfix ~notn:fwd ~ws:[] ~inner) | None -> ( @@ -294,7 +297,7 @@ let rec unparse : | Some args -> let inner = Mbwd.mmap - (fun [ tm ] -> Term (unparse vars tm Interval.entire Interval.entire)) + (fun [ tm ] -> Term (unparse vars tm No.Interval.entire No.Interval.entire)) [ args ] in unlocated (outfix ~notn:bwd ~ws:[] ~inner) | None -> @@ -319,8 +322,8 @@ and unparse_spine : | `Degen of string | `Unparser of unparser ] -> unparser Bwd.t -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars head args li ri -> (* First we check whether the head is a term with an associated notation, and if so whether it is applied to enough arguments to instantiate that notation. *) @@ -344,10 +347,10 @@ and unparse_spine : | `Unparser tm -> tm.unparse li ri) | Snoc (args, arg) -> ( (* As before, if the application doesn't fit in its tightness interval, we have to parenthesize it. *) - match (Interval.contains li No.plus_omega, Interval.contains ri No.plus_omega) with + match (No.Interval.contains li No.plus_omega, No.Interval.contains ri No.plus_omega) with | Some left_ok, Some right_ok -> - let fn = unparse_spine vars head args li Interval.plus_omega_only in - let arg = arg.unparse Interval.empty ri in + let fn = unparse_spine vars head args li No.Interval.plus_omega_only in + let arg = arg.unparse No.Interval.empty ri in (* We parenthesize the argument if the style dictates and it doesn't already have parentheses. *) let arg = match Display.argstyle () with @@ -356,8 +359,9 @@ and unparse_spine : unlocated (App { fn; arg; left_ok; right_ok }) | _ -> let fn = - unparse_spine vars head args Interval.plus_omega_only Interval.plus_omega_only in - let arg = arg.unparse Interval.empty Interval.plus_omega_only in + unparse_spine vars head args No.Interval.plus_omega_only No.Interval.plus_omega_only + in + let arg = arg.unparse No.Interval.empty No.Interval.plus_omega_only in let arg = match Display.argstyle () with | `Spaces -> arg @@ -371,20 +375,20 @@ and unparse_field : n Names.t -> (n, kinetic) term -> Field.t -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars tm fld li ri -> match unparse_field_var vars tm fld with | Some res -> res | None -> ( - match (Interval.contains li No.plus_omega, Interval.contains ri No.plus_omega) with + match (No.Interval.contains li No.plus_omega, No.Interval.contains ri No.plus_omega) with | Some left_ok, Some right_ok -> - let fn = unparse vars tm li Interval.plus_omega_only in + let fn = unparse vars tm li No.Interval.plus_omega_only in let arg = unlocated (Field (Field.to_string fld, [])) in unlocated (App { fn; arg; left_ok; right_ok }) | _ -> - let fn = unparse vars tm Interval.plus_omega_only Interval.plus_omega_only in + let fn = unparse vars tm No.Interval.plus_omega_only No.Interval.plus_omega_only in let arg = unlocated (Field (Field.to_string fld, [])) in let left_ok = No.le_refl No.plus_omega in let right_ok = No.le_refl No.plus_omega in @@ -414,8 +418,8 @@ and unparse_lam : n Names.t -> string option Bwd.t -> (n, s) term -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun cube vars xs body li ri -> match body with @@ -446,8 +450,8 @@ and unparse_lam_done : n Names.t -> string option Bwd.t -> (n, s) term -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun cube vars xs body li ri -> let notn = @@ -455,17 +459,17 @@ and unparse_lam_done : | `Cube -> cubeabs | `Normal -> abs in (* Of course, if we don't fit in the tightness interval, we have to parenthesize. *) - match (Interval.contains li No.minus_omega, Interval.contains ri No.minus_omega) with + match (No.Interval.contains li No.minus_omega, No.Interval.contains ri No.minus_omega) with | Some left_ok, Some right_ok -> let li_ok = No.lt_trans Any_strict left_ok No.minusomega_lt_plusomega in let first = unparse_abs xs li li_ok No.minusomega_lt_plusomega in - let last = unparse vars body Interval.entire ri in + let last = unparse vars body No.Interval.entire ri in unlocated (infix ~notn ~ws:[] ~first ~inner:Emp ~last ~left_ok ~right_ok) | _ -> let first = - unparse_abs xs Interval.entire (No.le_plusomega No.minus_omega) No.minusomega_lt_plusomega - in - let last = unparse vars body Interval.entire Interval.entire in + unparse_abs xs No.Interval.entire (No.le_plusomega No.minus_omega) + No.minusomega_lt_plusomega in + let last = unparse vars body No.Interval.entire No.Interval.entire in let left_ok = No.le_refl No.minus_omega in let right_ok = No.le_refl No.minus_omega in parenthesize (unlocated (infix ~notn ~ws:[] ~first ~inner:Emp ~last ~left_ok ~right_ok)) @@ -475,8 +479,8 @@ and unparse_act : n Names.t -> unparser -> (a, b) deg -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars tm s li ri -> match is_id_deg s with @@ -484,7 +488,8 @@ and unparse_act : | None -> ( match name_of_deg s with | Some str -> unparse_spine vars (`Degen str) (Snoc (Emp, tm)) li ri - | None -> unlocated (Superscript (Some (tm.unparse li Interval.empty), string_of_deg s, []))) + | None -> + unlocated (Superscript (Some (tm.unparse li No.Interval.empty), string_of_deg s, []))) (* We group together all the 0-dimensional dependent pi-types in a notation, so we recursively descend through the term picking those up until we find a non-pi-type, a higher-dimensional pi-type, or a non-dependent pi-type, in which case we pass it off to unparse_pis_final. *) and unparse_pis : @@ -492,8 +497,8 @@ and unparse_pis : n Names.t -> unparser Bwd.t -> (n, kinetic) term -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars accum tm li ri -> match tm with @@ -509,7 +514,8 @@ and unparse_pis : (fun _ _ -> unparse_pi_dom (Option.get (NICubeOf.find_top x)) - (unparse vars (CubeOf.find_top doms) (interval_right asc) Interval.entire)); + (unparse vars (CubeOf.find_top doms) (interval_right asc) + No.Interval.entire)); } )) (CodCube.find_top cods) li ri | None, Eq -> @@ -561,18 +567,18 @@ and unparse_arrow : type n lt ls rt rs. unparser -> unparser -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun dom cod li ri -> - match (Interval.contains li No.zero, Interval.contains ri No.zero) with + match (No.Interval.contains li No.zero, No.Interval.contains ri No.zero) with | Some left_ok, Some right_ok -> let first = dom.unparse li (interval_left arrow) in let last = cod.unparse (interval_right arrow) ri in unlocated (infix ~notn:arrow ~ws:[] ~first ~inner:Emp ~last ~left_ok ~right_ok) | _ -> - let first = dom.unparse Interval.entire (interval_left arrow) in - let last = cod.unparse (interval_right arrow) Interval.entire in + let first = dom.unparse No.Interval.entire (interval_left arrow) in + let last = cod.unparse (interval_right arrow) No.Interval.entire in let left_ok = No.minusomega_lt_zero in let right_ok = No.minusomega_lt_zero in parenthesize (unlocated (infix ~notn:arrow ~ws:[] ~first ~inner:Emp ~last ~left_ok ~right_ok)) @@ -582,8 +588,8 @@ and unparse_pis_final : n Names.t -> unparser Bwd.t -> unparser -> - (lt, ls) Interval.tt -> - (rt, rs) Interval.tt -> + (lt, ls) No.iinterval -> + (rt, rs) No.iinterval -> (lt, ls, rt, rs) parse located = fun vars accum tm li ri -> match split_first accum with @@ -643,10 +649,11 @@ let rec unparse_ctx : (* We treat an invisible binding as consisting of all nameless variables, and autogenerate names for them all. *) let x, names = Names.add_cube_autogen (CubeOf.dim bindings) names in let do_binding (b : b Termctx.binding) (res : S.t) : unit * S.t = - let ty = Term (unparse names b.ty Interval.entire Interval.entire) in + let ty = Term (unparse names b.ty No.Interval.entire No.Interval.entire) in let tm = - Option.map (fun t -> Term (unparse names t Interval.entire Interval.entire)) b.tm - in + Option.map + (fun t -> Term (unparse names t No.Interval.entire No.Interval.entire)) + b.tm in ((), Snoc (res, (x, `Renamed, tm, Some ty))) in let _, result = M.miterM { it = (fun _ [ b ] res -> do_binding b res) } [ bindings ] result in @@ -683,10 +690,11 @@ let rec unparse_ctx : match (hasfields, is_id_sface fab) with | Has_fields, Some _ -> ((), res) | _ -> - let ty = Term (unparse names b.ty Interval.entire Interval.entire) in + let ty = Term (unparse names b.ty No.Interval.entire No.Interval.entire) in let tm = - Option.map (fun t -> Term (unparse names t Interval.entire Interval.entire)) b.tm - in + Option.map + (fun t -> Term (unparse names t No.Interval.entire No.Interval.entire)) + b.tm in let (SFace_of_plus (_, fa, fb)) = sface_of_plus plusdim fab in let fastr = "." ^ string_of_sface fa in let add_fa = @@ -704,7 +712,7 @@ let rec unparse_ctx : let _, result = M.miterM (fun [ (x, orig); (_, _, ty) ] res -> - let ty = Term (unparse names ty Interval.entire Interval.entire) in + let ty = Term (unparse names ty No.Interval.entire No.Interval.entire) in let res = Snoc (res, (x, merge_orig orig, None, Some ty)) in ((), res)) [ fs; fields ] result in @@ -729,24 +737,25 @@ let () = | PTerm (ctx, tm) -> Printed ( Print.pp_term `None, - Term (unparse (Names.of_ctx ctx) tm Interval.entire Interval.entire) ) + Term (unparse (Names.of_ctx ctx) tm No.Interval.entire No.Interval.entire) ) | PVal (ctx, tm) -> Printed ( Print.pp_term `None, Term - (unparse (Names.of_ctx ctx) (readback_val ctx tm) Interval.entire Interval.entire) - ) + (unparse (Names.of_ctx ctx) (readback_val ctx tm) No.Interval.entire + No.Interval.entire) ) | PNormal (ctx, tm) -> Printed ( Print.pp_term `None, - Term (unparse (Names.of_ctx ctx) (readback_nf ctx tm) Interval.entire Interval.entire) - ) + Term + (unparse (Names.of_ctx ctx) (readback_nf ctx tm) No.Interval.entire + No.Interval.entire) ) | PUninst (ctx, tm) -> Printed ( Print.pp_term `None, Term - (unparse (Names.of_ctx ctx) (readback_uninst ctx tm) Interval.entire Interval.entire) - ) + (unparse (Names.of_ctx ctx) (readback_uninst ctx tm) No.Interval.entire + No.Interval.entire) ) | PConstant name -> Printed ((fun ppf x -> Uuseg_string.pp_utf_8 ppf (String.concat "." x)), Scope.name_of name) @@ -756,7 +765,7 @@ let () = ( (fun ppf (ctx, ty) -> Print.pp_hole ppf ctx ty), let vars, names = Names.uniquify_vars vars in let names, ctx = unparse_ctx names `Unlocked (Bwv.permute vars p) ctx in - let ty = unparse names ty Interval.entire Interval.entire in + let ty = unparse names ty No.Interval.entire No.Interval.entire in (ctx, Term ty) ) | Dump.Val tm -> Printed (Dump.value, tm) | Dump.Uninst tm -> Printed (Dump.uninst, tm) diff --git a/lib/top/execute.ml b/lib/top/execute.ml index 5862dbd5..50d99cf0 100644 --- a/lib/top/execute.ml +++ b/lib/top/execute.ml @@ -55,6 +55,8 @@ end module Flags = Algaeff.Reader.Make (FlagData) let () = Flags.register_printer (function `Read -> Some "unhandled Flags.read effect") + +(* TODO: Perhaps these should use a customizable formatter, since we may be reformatting source files. *) let reformat_maybe f = if (Flags.read ()).reformat then f std_formatter else () let reformat_maybe_ws f = if (Flags.read ()).reformat then f std_formatter else [] @@ -273,7 +275,7 @@ and execute_source ?(init_visible = (Flags.read ()).init_visible) compunit | _ -> Reporter.fatal_diagnostic d); Scope.get_export () -(* Subroutine that parses and executes all the commands in a source. *) +(* Parse, execute (if requested by Flags), and reformat (if requested by Flags) all the commands in a source. *) and batch first ws p src = let reformat_end () = reformat_maybe (fun ppf -> diff --git a/lib/top/top.ml b/lib/top/top.ml index 1e1dfdc9..ce589e16 100644 --- a/lib/top/top.ml +++ b/lib/top/top.ml @@ -60,18 +60,20 @@ let set_refls str = refl_char := c.[0]; refl_names := names -(* Given a command and preceeding whitespace, execute the command (if we are executing commands), alert about open holes, and print the reformatted command if requested. *) +(* Execute a parsed command (if requested by Flags), alert about open holes, and return a function that reformats it (if requested by Flags). *) let do_command = function - | ws, None -> Execute.reformat_maybe @@ fun ppf -> pp_ws `None ppf ws + | ws, None -> fun () -> Execute.reformat_maybe @@ fun ppf -> pp_ws `None ppf ws | ws, Some cmd -> - if !execute then Execute.execute_command cmd; - let n = Eternity.unsolved () in - if n > 0 then Reporter.emit (Open_holes n); - Execute.reformat_maybe @@ fun ppf -> - pp_ws `None ppf ws; - let last = Parser.Command.pp_command ppf cmd in - pp_ws `None ppf last; - Format.pp_print_newline ppf () + if (Execute.Flags.read ()).execute then ( + Execute.execute_command cmd; + let n = Eternity.unsolved () in + if n > 0 then Reporter.emit (Open_holes n)); + fun () -> + Execute.reformat_maybe @@ fun ppf -> + pp_ws `None ppf ws; + let last = Parser.Command.pp_command ppf cmd in + pp_ws `None ppf last; + Format.pp_print_newline ppf () (* This exception is raised when a fatal error occurs in loading the non-interactive inputs. The caller should catch it and perform an appropriate kind of "exit". *) exception Exit diff --git a/lib/util/no.ml b/lib/util/no.ml index 9468873f..0758fc7c 100644 --- a/lib/util/no.ml +++ b/lib/util/no.ml @@ -869,3 +869,51 @@ module Map = struct }) end end + +(* An "upper interval" is of the form (p,+ω] or [p,+ω] for some tightness p. Ordinarily we would call these "open" and "closed" intervals, but due to the potential confusion with "closed" and "open" notations we call them instead "strict" and "nonstrict". *) + +type ('a, 's) iinterval = { strictness : 's strictness; endpoint : 'a t } +type interval = Interval : ('s, 'a) iinterval -> interval + +module Interval = struct + let empty : (plus_omega, strict) iinterval = { strictness = Strict; endpoint = plus_omega } + + let entire : (minus_omega, nonstrict) iinterval = + { strictness = Nonstrict; endpoint = minus_omega } + + let plus_omega_only : (plus_omega, nonstrict) iinterval = + { strictness = Nonstrict; endpoint = plus_omega } + + let to_string = function + | Interval { strictness = Nonstrict; endpoint } -> + Printf.sprintf "[%s,inf]" (to_string endpoint) + | Interval { strictness = Strict; endpoint } -> Printf.sprintf "(%s,inf]" (to_string endpoint) + + let contains : type a s b. (a, s) iinterval -> b t -> (a, s, b) lt option = + fun { strictness; endpoint } x -> compare strictness endpoint x + + let union : interval -> interval -> interval = + fun (Interval t1 as i1) (Interval t2 as i2) -> + match compare Strict t1.endpoint t2.endpoint with + | Some _ -> i1 + | None -> ( + match compare Strict t2.endpoint t1.endpoint with + | Some _ -> i2 + | None -> ( + match (t1.strictness, t2.strictness) with + | Strict, Strict -> Interval { t1 with strictness = Strict } + | _ -> Interval { t1 with strictness = Nonstrict })) + + type (_, _, _, _) subset = + | Subset_strict : ('t2, strict, 't1) lt -> ('t1, 's1, 't2, 's2) subset + | Subset_eq : ('t, 's, 't, 's) subset + | Subset_nonstrict_strict : ('t, strict, 't, nonstrict) subset + + let subset_contains : + type t1 s1 t2 s2 a. (t1, s1, t2, s2) subset -> (t1, s1, a) lt -> (t2, s2, a) lt = + fun sub lt1 -> + match sub with + | Subset_strict lt2 -> lt_trans Strict_any lt2 lt1 + | Subset_eq -> lt1 + | Subset_nonstrict_strict -> lt_to_le lt1 +end diff --git a/lib/util/no.mli b/lib/util/no.mli index 5ab361a1..deae6d96 100644 --- a/lib/util/no.mli +++ b/lib/util/no.mli @@ -80,3 +80,22 @@ module Map : sig val add_cut : 'b Key.t -> (('x, 'b) lower -> ('x, 'b) upper -> ('x, 'b) F.t) -> 'x t -> 'x t end end + +type ('a, 's) iinterval = { strictness : 's strictness; endpoint : 'a t } +type interval = Interval : ('s, 'a) iinterval -> interval + +module Interval : sig + val empty : (plus_omega, strict) iinterval + val entire : (minus_omega, nonstrict) iinterval + val plus_omega_only : (plus_omega, nonstrict) iinterval + val to_string : interval -> string + val contains : ('a, 's) iinterval -> 'b t -> ('a, 's, 'b) lt option + val union : interval -> interval -> interval + + type (_, _, _, _) subset = + | Subset_strict : ('t2, strict, 't1) lt -> ('t1, 's1, 't2, 's2) subset + | Subset_eq : ('t, 's, 't, 's) subset + | Subset_nonstrict_strict : ('t, strict, 't, nonstrict) subset + + val subset_contains : ('t1, 's1, 't2, 's2) subset -> ('t1, 's1, 'a) lt -> ('t2, 's2, 'a) lt +end diff --git a/proofgeneral/narya.el b/proofgeneral/narya.el index ca8e5c0f..15b57274 100644 --- a/proofgeneral/narya.el +++ b/proofgeneral/narya.el @@ -32,6 +32,9 @@ (defvar narya-pending-hole-positions nil "Temporary storage for hole positions when executing commands invisibly.") +(defvar narya-pending-hole-parens nil + "Whether to parenthesize the hole-filling term.") + (defun narya-create-hole-overlays (start-position relative-positions) "Create overlays for holes given a starting position and a list of relative positions. Each entry in RELATIVE-POSITIONS should be a list of the form (START-OFFSET END-OFFSET HOLE-ID)." @@ -82,15 +85,15 @@ If called with an invisible command, store hole data in a global variable instead of creating overlays immediately. Otherwise, create overlays for new holes. -This function also performs part of `proof-shell-handle-delayed-output`'s -role, updating `proof-shell-last-output-kind` to avoid duplicated output +This function also performs part of `proof-shell-handle-delayed-output''s +role, updating `proof-shell-last-output-kind' to avoid duplicated output handling in Proof General." ;; Retrieve action information from `proof-action-list`. (let ((span (caar proof-action-list)) (cmd (nth 1 (car proof-action-list))) (flags (nth 3 (car proof-action-list))) ;; Variables to mark positions in `string` as we parse. - (rstart 0) (rend 0) (gstart 0) (gend 0) (dpos 0) + (rstart 0) (rend 0) (gstart 0) (gend 0) (dpos 0) (parens 0) ;; Temporary storage for hole data. (parsed-hole-data nil) (error-found nil)) @@ -116,10 +119,14 @@ handling in Proof General." (hend-offset (string-to-number (match-string 3 string)))) (setq dpos (match-end 0)) (list hstart-offset hend-offset hole)))) + ;; Now grab the reformatting info + (string-match "\x0C\\[reformat\\]\x0C\n\\(.*\\)" string dpos) + (setq parens (match-string 1 string)) ;; Handle parsed hole data based on the visibility of the command (if (member 'invisible flags) ;; For invisible commands, store the parsed data globally - (setq narya-pending-hole-positions parsed-hole-data) + (setq narya-pending-hole-positions parsed-hole-data + narya-pending-hole-parens (equal parens "parens")) ;; For visible commands, create overlays directly (when span ;; Only proceed if `span` is non-nil (proof-with-script-buffer @@ -329,7 +336,7 @@ handling in Proof General." (defun narya-solve-hole () "Solve the current hole with a user-provided term, using any -pending hole data stored by `narya-handle-output`." +pending hole data stored by `narya-handle-output'." (interactive) ;; Check for an overlay marking the current hole at point. (let ((hole-overlay (car (seq-filter (lambda (ovl) @@ -356,7 +363,9 @@ pending hole data stored by `narya-handle-output`." ;; order so that if the hole is at the very end of the ;; processed region, the inserted term will end up ;; *inside* the processed region. - (insert "(" term ")") ;; Use parentheses to guarantee correct parsing. + (if narya-pending-hole-parens + (insert "(" term ")") ;; Use parentheses to guarantee correct parsing. + (insert term)) (delete-region (point) (overlay-end hole-overlay)) ;; Delete the overlay for the solved hole and update the hole list. (delete-overlay hole-overlay) @@ -365,7 +374,7 @@ pending hole data stored by `narya-handle-output`." ;; Process any pending hole positions saved in `narya-handle-output`. (when narya-pending-hole-positions ;; Use the helper function to create overlays for new holes. - (narya-create-hole-overlays (+ byte-insert-start 1) narya-pending-hole-positions)) ;;adjust start-pos for added parenthesis + (narya-create-hole-overlays (+ byte-insert-start (if narya-pending-hole-parens 1 0)) narya-pending-hole-positions)) ;;adjust start-pos for added parenthesis ;; Clear the global pending hole data after processing. (setq narya-pending-hole-positions nil)))))) diff --git a/test/black/holes.t/holes.ny b/test/black/holes.t/holes.ny index ad4ccc84..3be12485 100644 --- a/test/black/holes.t/holes.ny +++ b/test/black/holes.t/holes.ny @@ -4,9 +4,13 @@ axiom B : Type def id : Type → Type ≔ X ↦ X -def f : A → B ≔ ? +axiom b : B -def f' : A → B ≔ x ↦ ? +axiom g : (A → B) → A → B + +def f : A → B ≔ g ? + +def f' : A → B ≔ ? def ℕ : Type ≔ data [ | zero. : ℕ diff --git a/test/black/holes.t/run.t b/test/black/holes.t/run.t index 8a13c8ac..22c36100 100644 --- a/test/black/holes.t/run.t +++ b/test/black/holes.t/run.t @@ -8,6 +8,12 @@ ￫ info[I0000] ￮ constant id defined + ￫ info[I0001] + ￮ axiom b assumed + + ￫ info[I0001] + ￮ axiom g assumed + ￫ info[I0000] ￮ constant f defined, containing 1 hole @@ -23,9 +29,8 @@ ￫ info[I3003] ￮ hole ?1: - x : A ---------------------------------------------------------------------- - B + A → B ￫ info[I0000] ￮ constant ℕ defined diff --git a/test/testutil/repl.ml b/test/testutil/repl.ml index 4cc17c70..a8106683 100644 --- a/test/testutil/repl.ml +++ b/test/testutil/repl.ml @@ -101,7 +101,7 @@ let print (tm : string) : unit = let etm = eval_term (Emp D.zero) ctm in Readback.Displaying.run ~env:true @@ fun () -> let btm = readback_at Ctx.empty etm ety in - let utm = unparse Names.empty btm Interval.entire Interval.entire in + let utm = unparse Names.empty btm No.Interval.entire No.Interval.entire in pp_term `None Format.std_formatter (Term utm); Format.pp_print_newline Format.std_formatter () | _ -> fatal (Nonsynthesizing "argument of print") diff --git a/test/testutil/showparse.ml b/test/testutil/showparse.ml index 181dfa7b..64fc04eb 100644 --- a/test/testutil/showparse.ml +++ b/test/testutil/showparse.ml @@ -12,6 +12,7 @@ and parse_tree = | Constr of string | Field of string | Superscript of parse_tree option * string + | Hole let rec get_obs (obs : Notation.observation) : obs = match obs with @@ -28,6 +29,7 @@ and get_tree : type lt ls rt rs. (lt, ls, rt, rs) Notation.parse -> parse_tree = | Field (x, _) -> Field x | Superscript (None, s, _) -> Superscript (None, s) | Superscript (Some x, s, _) -> Superscript (Some (get_tree x.value), s) + | Hole _ -> Hole let parse tm = let p = Parse.Term.parse (`String { content = tm; title = Some "user-supplied term" }) in