Only parenthesize hole-filling terms that need it

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.
 

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,14 +182,18 @@ 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 -> ()
 
 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

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
 

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

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;

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;

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;
 }
 

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 }

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)

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 "@[<v 0>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 -> (

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