Reformat the whole command when solving a hole

bin/narya.ml

@@ -3,6 +3,7 @@
 open Bwd
 open Util
 open Core
+open Origin
 open Parser
 open React
 open Lwt
@@ -207,6 +208,7 @@ let rec interact_pg () : unit =
               Format.printf "\x0C[data]\x0C\n%!";
               if Parser.Command.parenthesized cmd then Format.printf "parenthesized\n"
               else Format.printf "unparenthesized\n";
+              Format.printf "%s\n" (Origin.to_string (Origin.current ()));
               Mlist.miter
                 (fun [ (h, s, e) ] -> Format.printf "%d %d %d\n" h (s - offset) (e - offset))
                 [ newholes ];

docs/source/interactive.rst

@@ -98,6 +98,6 @@ On the other hand, solving a hole changes the text of the Emacs buffer, and ther
 Reformatting solved holes
 -------------------------
 
-By default, when filling a hole interactively with ProofGeneral, the term you enter is automatically reformatted.  In particular, line breaks and indenting spaces are inserted in (what Narya thinks are) appropriate places (and removed from what it thinks are inappropriate places), and ASCII operators such as ``->`` and ``|->`` are replaced by their Unicode equivalents such as → and ↦.  Unfortunately, at present the solving term is reformatted entirely on its own without reference to the command in which it appears, so after it is inserted the overall command may still be badly formatted, especially if you inserted a case tree structure such as ``match``.  Currently the only solution to this is to retract the command after solving the hole and then re-process it to reformat it.
+By default, when filling a hole interactively with ProofGeneral, the command containing the new term is automatically reformatted.  In particular, line breaks and indenting spaces are inserted in (what Narya thinks are) appropriate places (and removed from what it thinks are inappropriate places), and ASCII operators such as ``->`` and ``|->`` are replaced by their Unicode equivalents such as → and ↦.
 
-As with reformatting of commands and source files, reformatting of hole-solving terms is affected by the command-line flags ``-unicode`` and ``-ascii`` (print operators as → or ``->``, respectively).  You can also turn off solve-reformatting entirely by setting the Emacs customization variable ``narya-reformat-holes`` to ``nil``.  However, if you don't like the way Narya reformats your terms, I would appreciate it if you give me feedback about it rather than (or, at least, in addition to) turning it off.
+As with reformatting of commands and source files, reformatting of hole-solving terms is affected by the command-line flags ``-unicode`` and ``-ascii`` (print operators as → or ``->``, respectively), and you can also turn off automatica reformatting entirely by setting the Emacs customization variable ``narya-reformat-commands`` to ``nil``.  However, if you don't like the way Narya reformats your terms, I would appreciate it if you give me feedback about it rather than (or, at least, in addition to) turning it off.

docs/source/top-level-interface.rst

@@ -400,15 +400,16 @@ Narya comes with an "opinionated code formatter" like `gofmt <https://go.dev/blo
 
 There are currently two ways to use the formatter.  Firstly, every time you run Narya on a source file, it automatically reformats that file.  (It only reformats files supplied explictly on the command line, not other files loaded by these.)  If this resulted in any changes, it copies the original file to a backup file with a ``.bak.N`` extension; this is a temporary feature to ensure you can recover your code in case of bugs in the reformatter, and will probably go away once there is enough evidence that the reformatter is trustworthy.  (Please report any bugs in the reformatter, especially serious ones that change the meaning of the code, make it non-reparseable, lose comments, etc.!  Also, reformatting is supposed to be idempotent: if reformatting code twice without editing it in the middle makes any changes the second time, that is also a bug.)
 
-Secondly, every time you process a command in ProofGeneral, that command is automatically reformatted.  If you retract the command, it remains reformatted.  To undo the reformatting, you can use Emacs' undo operation (``C-/``); this will also retract the command, if it is still in the processed region.
+Secondly, every time you process a command in ProofGeneral, or solve a hole in a previously processed command, that command is automatically reformatted.  If you retract the command, it remains reformatted.  To undo the reformatting, you can use Emacs' undo operation (``C-/``); this will also retract the command, if it is still in the processed region.
 
 Processing an entire file in ProofGeneral does not have *exactly* the same reformatting effect as running Narya on it from the command line.  They should reformat individual commands in the same way, but the command-line reformatter also ensures that distinct commands are separated by single blank lines (suitably interpreted in the presence of comments).  ProofGeneral can't do this, as it doesn't even pass blank lines and comments between commands to the Narya subprocess.  However, most people already separate their commands by single blank lines, so this difference is not usually a serious issue.  If a file has been formatted by the command-line reformatter, processing it in Proof General should not *change* that formatting (if it does, please report a bug).
 
-It is not currently possible to reformat code without simultaneously typechecking it.  The presence of user-definable mixfix notations that can also be imported from other files means that any reformatter must be at least partially context-aware.  It would probably be possible to implement a reformatter that resolves user-defined notations without typechecking definitions, but this is not a high priority.
+It is not currently possible to reformat code without typechecking it.  The presence of user-definable mixfix notations that can also be imported from other files means that any reformatter must be at least partially context-aware.  It would probably be possible to implement a reformatter that resolves user-defined notations without typechecking definitions, but this is not a high priority.
 
 Currently there is only one configuration option for the code formatter: whether to print Unicode characters such as → or their ASCII equivalents such as ``->``.  This can be set on the command line with the flags ``-unicode`` and ``-ascii``, and in ProofGeneral with the state-preserving ``display`` command.  In accord with the goal of opinionated code formatters -- to eliminate time wasted by arguing about formatting, including formatter options -- I do not plan to add more configuration options; although I'll listen if you have a case to make for one.  Suggestions for improvements and changes to the standard formatting style are also welcome, although I can't promise to adopt them.
 
-It is possible to turn off the code formatter.  The Emacs customization variables ``narya-reformat-commands`` and ``narya-reformat-holes`` will turn off reformatting in ProofGeneral, and the command-line option ``-no-format`` will turn off reformatting of input files.  However, if you don't like the way Narya reformats your code, I would appreciate it if you give me feedback about this rather than (or, at least, in addition to) turning it off entirely.
+It is possible to turn off the code formatter.  Unsetting the Emacs customization variable ``narya-reformat-commands`` will turn off reformatting in ProofGeneral, and the command-line option ``-no-format`` will turn off reformatting of input files.  However, if you don't like the way Narya reformats your code, I would appreciate it if you give me feedback about this rather than (or, at least, in addition to) turning it off entirely.  If ``narya-reformat-commands`` is turned off, you can manually reformat a command in the processed region with ``C-M-q``.  (Reformatting unprocessed commands would be too error-prone, as noted above: Narya wouldn't be able to tell which notations are in scope.)
+
 
 jsNarya
 -------

lib/core/origin.ml

@@ -39,6 +39,9 @@ module Instant = struct
       counter := !counter - 1;
       Some !counter)
     else None
+
+  let of_int x = x
+  let ( <= ) x y = x <= y
 end
 
 module Origin = struct
@@ -149,9 +152,11 @@ module Origin = struct
   (* Go back in time temporarily to a particular instant, run a callback command, and then return to the present.  The callback can modify the past state (of all versioned objects), with resulting effects on the present.  However, if it throws an exception, any such changes that it's made are discarded.  Used for commands like "solve" and "split". *)
   let rewind_command (instant : Instant.t) (f : unit -> 'a) : 'a =
     match S.get () with
-    | Present _ ->
-        S.run ~init:(Past instant) @@ fun () ->
-        List.fold_left (fun g rewinder -> rewinder.wrap instant g) f !rewinds ()
+    | Present now ->
+        if instant <= now then
+          S.run ~init:(Past instant) @@ fun () ->
+          List.fold_left (fun g rewinder -> rewinder.wrap instant g) f !rewinds ()
+        else raise (Failure "can't go back to the future")
     | _ -> raise (Failure "can only go back in time from the present")
 
   (* Similarly, but always behave as if an exception were thrown, so that no changes made in the past are permanent.  Used for commands like "echo" in the context of a hole, which might allow holes that should not be saved. *)

lib/core/origin.mli

@@ -8,6 +8,9 @@ end
 
 module Instant : sig
   type t
+
+  val of_int : int -> t
+  val ( <= ) : t -> t -> bool
 end
 
 module Origin : sig

lib/core/reporter.ml

@@ -257,6 +257,7 @@ module Code = struct
     | Break : t
     | Accumulated : string * t Asai.Diagnostic.t Bwd.t -> t
     | No_holes_allowed : [ `Command of string | `File of string | `Other of string ] -> t
+    | Invalid_instant : string -> t
     | Cyclic_term : t
     | Oracle_failed : string * printable -> t
     | Invalid_flags : t
@@ -414,6 +415,7 @@ module Code = struct
     | Break -> Error
     | Accumulated _ -> Error
     | No_holes_allowed _ -> Error
+    | Invalid_instant _ -> Bug
     | Wrong_dimension_of_field _ -> Error
     | Invalid_field_suffix _ -> Error
     | Cyclic_term -> Error
@@ -542,6 +544,7 @@ module Code = struct
     | Too_many_commands -> "E2000"
     | Forbidden_interactive_command _ -> "E2001"
     | No_holes_allowed _ -> "E2002"
+    | Invalid_instant _ -> "E2003"
     (* def *)
     | Redefining_constant _ -> "E2100"
     | Invalid_constant_name _ -> "E2101"
@@ -1033,6 +1036,7 @@ module Code = struct
           | `Command cmd -> textf "command '%s' cannot contain holes" cmd
           | `File file -> textf "imported file '%s' cannot contain holes" file
           | `Other where -> textf "%s cannot contain holes" where)
+      | Invalid_instant instant -> textf "invalid instant: %s" instant
       | Ill_scoped_connection -> text "ill-scoped connection"
       | Cyclic_term -> text "cycle in graphical term"
       | Oracle_failed (str, tm) -> textf "oracle failed: %s: %a" str pp_printed (print tm)

lib/parser/command.ml

@@ -135,6 +135,13 @@ module Command = struct
         wsprefix : Whitespace.t list;
         wscoloneq : Whitespace.t list;
       }
+    | Fmt of {
+        wsfmt : Whitespace.t list;
+        instant : Instant.t;
+        wsinstant : Whitespace.t list;
+        wscoloneq : Whitespace.t list;
+        cmd : t;
+      }
     | End of { wsend : Whitespace.t list }
     | Quit of Whitespace.t list
     | Bof of Whitespace.t list
@@ -231,6 +238,12 @@ module Parse = struct
         | Ident [ num ] -> Option.map (fun n -> ((n, ws), state)) (int_of_string_opt num)
         | _ -> None)
 
+  (* Go back in time for parsing only, to use the notations in scope at a given instant.  The usual origin algebraic effect doesn't mesh well with the continuation-based parser monad, so we have to use the built-in parser state. *)
+  let set_instant ?severity past =
+    match Origin.current () with
+    | Instant now when Instant.(past <= now) -> set (Instant past)
+    | _ -> fatal ?severity (Invalid_instant (Origin.to_string (Instant past)))
+
   let echo =
     let* wsecho, eval =
       (let* wsecho = token Echo in
@@ -240,9 +253,8 @@ module Parse = struct
     let* number, wsin, wsnumber, tm =
       (let* wsin = token In in
        let* number, wsnumber = integer in
-       (* Go back in time for parsing, to use the notations in scope at that hole. *)
        let (Found_hole { instant; _ }) = Global.find_hole number in
-       let* () = set (Instant instant) in
+       let* () = set_instant instant in
        let* tm = C.term [] in
        return (Some number, wsin, wsnumber, tm))
       </> let* tm = C.term [] in
@@ -553,9 +565,8 @@ module Parse = struct
     let* number, wsnumber = integer in
     let* column, wscolumn = integer </> return (0, []) in
     let* wscoloneq = token Coloneq in
-    (* Go back in time for parsing, to use the notations in scope at that hole. *)
     let (Found_hole { instant; _ }) = Global.find_hole number in
-    let* () = set (Instant instant) in
+    let* () = set_instant instant in
     let* tm = C.term [] in
     return
       (Solve { wssolve; number; wsnumber; column; wscolumn; wscoloneq; tm; parenthesized = false })
@@ -564,9 +575,8 @@ module Parse = struct
     let* wssplit = token Split in
     let* number, wsnumber = integer in
     let* wscoloneq = token Coloneq in
-    (* Go back in time for parsing, to use the notations in scope at that hole. *)
     let (Found_hole { instant; _ }) = Global.find_hole number in
-    let* () = set (Instant instant) in
+    let* () = set_instant instant in
     let* tm = C.term [] in
     let* tms =
       zero_or_more
@@ -675,7 +685,16 @@ module Parse = struct
     let* () = expect_end () in
     return Command.Eof
 
-  let command () =
+  let rec fmt () =
+    let* wsfmt = token Fmt in
+    let* instant, wsinstant = integer in
+    let instant = Instant.of_int instant in
+    let* wscoloneq = token Coloneq in
+    let* () = set_instant ~severity:Error instant in
+    let* cmd = command () in
+    return (Fmt { wsfmt; instant; wsinstant; wscoloneq; cmd })
+
+  and command () =
     bof
     </> axiom
     </> def_and
@@ -690,6 +709,7 @@ module Parse = struct
     </> option
     </> undo
     </> section
+    </> fmt ()
     </> endcmd
     </> quit
     </> eof
@@ -779,6 +799,7 @@ let to_string : Command.t -> string = function
   | Quit _ -> "quit"
   | Undo _ -> "undo"
   | Section _ -> "section"
+  | Fmt _ -> "fmt"
   | End _ -> "end"
   | Bof _ -> "bof"
   | Eof -> "eof"
@@ -1222,6 +1243,7 @@ let execute ~(action_taken : unit -> unit) ~(get_file : string -> Scope.trie) (c
       Global.run_command ~holes_allowed:(Error (to_string cmd)) @@ fun () ->
       Scope.start_section prefix;
       (None, fun _ -> Some (Section_opened prefix))
+  | Fmt _ -> (None, [])
   | End _ -> (
       Global.run_command ~holes_allowed:(Error (to_string cmd)) @@ fun () ->
       match Scope.end_section () with
@@ -1335,9 +1357,8 @@ let pp_attribute : type a.
 let pp_command : t -> PPrint.document * Whitespace.t list =
  fun cmd ->
   let open PPrint in
-  (* Indent when inside of sections. *)
-  let indent = Scope.count_sections () * 2 in
-  let indent, doc, ws =
+  let rec go cmd =
+    let indent = Scope.count_sections () * 2 in
     match cmd with
     | Axiom { wsaxiom; nonparam; name; loc = _; wsname; parameters; wscolon; ty = Wrap ty } ->
         let pparams, wparams = pp_parameters wsname parameters in
@@ -1494,6 +1515,9 @@ let pp_command : t -> PPrint.document * Whitespace.t list =
           ^^ Token.pp Coloneq
           ^^ pp_ws `None ws,
           rest )
+    | Fmt { instant; cmd; _ } ->
+        (* We ignore the whitespace in the fmt command itself, since its purpose is to pretty-print the argument command.  We also ignore the current indent, since the recursive call takes place in the past and therefore will use the correct indentation for the past. *)
+        Origin.rewind_command instant @@ fun () -> go cmd
     | End { wsend } ->
         let ws, rest = Whitespace.split wsend in
         (indent, Token.pp End ^^ pp_ws `None ws, rest)
@@ -1502,6 +1526,8 @@ let pp_command : t -> PPrint.document * Whitespace.t list =
     | Eof -> (indent, empty, [])
     (* These commands can't appear in a source file, and ProofGeneral doesn't need any reformatting info from them, so we display nothing.  In fact, in the case of Undo, PG uses this emptiness to determine that it should not replace any command in the buffer. *)
     | Show _ | Display _ | Undo _ -> (indent, empty, []) in
+  (* Indent when inside of sections. *)
+  let indent, doc, ws = go cmd in
   (* "nest" only has effect *after* linebreaks, so we have to separately indent the first line. *)
   (nest indent (blank indent ^^ doc), ws)
 

lib/parser/lexer.ml

@@ -112,17 +112,17 @@ let rec hole_contents () : string t =
 
 let hole : Token.t t =
   (let* _ = uchar query in
-   return (Hole None))
+   return (Hole { number = None; contents = None }))
   </> (let* contents = hole_contents () in
-       return (Hole (Some contents)))
+       return (Hole { number = None; contents = Some contents }))
   </> (let* _ = uchar dblquery in
        (* Numbered hole *)
        backtrack
-         (let* _ = word is_digit is_digit "hole number" in
+         (let* number = word is_digit is_digit "hole number" in
           (let* _ = uchar query in
-           return (Hole None))
+           return (Hole { number = Some number; contents = None }))
           </> let* contents = hole_contents () in
-              return (Hole (Some contents)))
+              return (Hole { number = Some number; contents = Some contents }))
          "numbered hole"
        </> return DblQuery)
   (* Grab other hole-like sequences, which won't parse but which we don't want the user to use elsewhere. *)
@@ -346,6 +346,7 @@ let get_reserved_word = function
   | "option" -> Some Option
   | "undo" -> Some Undo
   | "section" -> Some Section
+  | "fmt" -> Some Fmt
   | "end" -> Some End
   | "_" -> Some Underscore
   | _ -> None