only parenthesize hole solutions that need it

README.md

@@ -472,7 +472,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,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 -> ()

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/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
@@ -254,6 +255,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
@@ -423,7 +425,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"
@@ -676,6 +679,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 -> (
@@ -737,7 +741,6 @@ end
 include Asai.StructuredReporter.Make (Code)
 open Code
 
-
 let struct_at_degenerated_type eta name =
   match eta with
   | `Eta -> Checking_tuple_at_degenerated_record name

lib/parser/command.ml

@@ -69,7 +69,7 @@ module Command = struct
         number : int;
         wsnumber : Whitespace.t list;
         wscoloneq : Whitespace.t list;
-        mutable tm : observation;
+        tm : observation;
       }
     | Show of {
         wsshow : Whitespace.t list;
@@ -763,7 +763,10 @@ let execute : action_taken:(unit -> unit) -> get_file:(string -> Scope.trie) ->
                 let ppf = Format.formatter_of_buffer buf in
                 (Printconfig.as_case @@ fun () -> pp_term `None ppf data.tm);
                 Format.pp_print_flush ppf ();
-                Reporter.try_with ~fatal:(fun _ -> data.tm <- Term (parenthesize tm)) @@ fun () ->
+                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

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 []
 

lib/top/top.ml

@@ -58,21 +58,20 @@ let set_refls str =
       refl_char := c.[0];
       refl_names := names
 
-(* Execute a parsed command (if requested by Flags), alert about open holes, and reformat it (if requested by Flags). *)
+(* 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 -> Print.pp_ws `None ppf ws
+  | ws, None -> fun () -> Execute.reformat_maybe @@ fun ppf -> Print.pp_ws `None ppf ws
   | ws, Some cmd ->
-      let reformat_end () =
+      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 ->
         Print.pp_ws `None ppf ws;
         let last = Parser.Command.pp_command ppf cmd in
         Print.pp_ws `None ppf last;
-        Format.pp_print_newline ppf () in
-      Fun.protect
-        (fun () -> if (Execute.Flags.read ()).execute then Execute.execute_command cmd)
-        ~finally:reformat_end;
-      let n = Eternity.unsolved () in
-      if n > 0 then Reporter.emit (Open_holes n)
+        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

proofgeneral/narya.el

@@ -25,6 +25,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)."
@@ -75,15 +78,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))
@@ -109,10 +112,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
@@ -322,7 +329,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)
@@ -349,7 +356,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)
@@ -358,7 +367,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))))))
 

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. : ℕ

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