fix: actually rewind the scope for *parsing* when in a hole context

Author: mikeshulman

lib/parser/command.ml

@@ -240,6 +240,9 @@ 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* tm = C.term [] in
        return (Some number, wsin, wsnumber, tm))
       </> let* tm = C.term [] in
@@ -550,6 +553,9 @@ 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* tm = C.term [] in
     return
       (Solve { wssolve; number; wsnumber; column; wscolumn; wscoloneq; tm; parenthesized = false })
@@ -558,6 +564,9 @@ 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* tm = C.term [] in
     let* tms =
       zero_or_more
@@ -710,7 +719,8 @@ module Parse = struct
     Range.run ~env @@ fun () ->
     let p =
       C.Lex_and_parse.make Lexer.Parser.start
-        (C.Basic.make_partial () (if or_echo then command_or_echo () else command ())) in
+        (C.Basic.make_partial (Origin.current ())
+           (if or_echo then command_or_echo () else command ())) in
     let out, p = run p in
     (C.ensure_success p, (env, out))
 
@@ -726,7 +736,8 @@ module Parse = struct
     Range.run ~env @@ fun () ->
     let p =
       C.Lex_and_parse.make_next p
-        (C.Basic.make_partial () (if or_echo then command_or_echo () else command ())) in
+        (C.Basic.make_partial (Origin.current ())
+           (if or_echo then command_or_echo () else command ())) in
     let out, p = run p in
     (C.ensure_success p, (env, out))
 

lib/parser/parse.ml

@@ -1,5 +1,6 @@
 open Util
 open Core.Reporter
+open Core.Origin
 open Fmlib_parse
 open Notation
 module TokMap = Map.Make (Token)
@@ -21,7 +22,8 @@ end
 
 (* The functor that defines all the term-parsing combinators. *)
 module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct
-  module Basic = Token_parser.Make (Unit) (Lexer.Token_whitespace) (Final) (SemanticError)
+  (* The "state" is an Origin.  Normally the origin is stored globally with a State effect, but we sometimes need to change the origin temporarily during parsing (e.g. to go back in time and parse a term using the notations that were in scope in the past) and doing that with effects doesn't interact well with fmlib's continuation-based parser monad.  So we store the origin used for parsing in fmlib's built-in state parameter instead, and initialize it with the overall current origin when beginning parsing. *)
+  module Basic = Token_parser.Make (Origin) (Lexer.Token_whitespace) (Final) (SemanticError)
   open Basic
 
   (* We aren't using Fmlib's error reporting, so there's no point in supplying it nonempty "expect" strings. *)
@@ -108,7 +110,8 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct
       (lt, ls) No.iinterval -> (rt, rs) tokmap -> (lt, ls) right_wrapped_parse t =
    fun tight stop ->
     let* res =
-      (let* inner_loc, (inner, notn) = located (entry (Scope.Situation.left_closeds ())) in
+      (let* origin = get in
+       let* inner_loc, (inner, notn) = located (entry (Scope.Situation.left_closeds_at origin)) in
        match notn with
        | Open_in_interval (lt, _) -> No.plusomega_nlt lt (* This case is impossible *)
        | Closed_in_interval notn -> (
@@ -219,18 +222,20 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct
     | None -> succeed first_arg
     | Some nontrivial ->
         (* Now we start by looking ahead one token.  If we see one of the specified ending ops, or the initial op of a left-open tree with looser tightness than the lower endpoint of the current interval (with strictness determined by the tree in question), we return the result argument without parsing any more.  Note that the order matters, in case the next token could have more than one role.  Ending ops are tested first, which means that if a certain operator could end an "inner term" in an outer containing notation, it always does, even if it could also be interpreted as some infix notation inside that inner term.  If a certain token could be the initial op of more than one left-open, we stop here if *any* of those is looser; we don't backtrack and try other possibilities.  So the rule is that if multiple notations start with the same token, the looser one is used preferentially in cases when it matters.  (In cases where it doesn't matter, i.e. they would both be allowed at the same grouping relative to other notations, we can proceed to parse a merged tree containing both of them and decide later which one it is.)  *)
+        let* origin = get in
         followed_by
           (step (fun state _ (tok, _) ->
                if TokMap.mem tok stop then Some (first_arg, state)
                else
                  let open Monad.Ops (Monad.Maybe) in
-                 let* (No.Interval ivl) = Scope.Situation.left_opens tok in
+                 let* (No.Interval ivl) = Scope.Situation.left_opens_at origin tok in
                  let t = tight.endpoint 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 =
-               (let* inner_loc, (inner, notn) = located (entry (Scope.Situation.tighters tight)) in
+               (let* inner_loc, (inner, notn) =
+                  located (entry (Scope.Situation.tighters_at origin tight)) in
                 match notn with
                 | Open_in_interval (left_ok, notn) -> (
                     match (first_arg.get (interval_left notn), right notn) with
@@ -397,7 +402,7 @@ module Combinators (Final : Fmlib_std.Interfaces.ANY) = struct
     | Error e -> fatal (Anomaly ("Outer term failed: " ^ e))
 
   module Lex_and_parse =
-    Parse_with_lexer.Make_utf8 (Unit) (Lexer.Token_whitespace) (Final) (SemanticError)
+    Parse_with_lexer.Make_utf8 (Origin) (Lexer.Token_whitespace) (Final) (SemanticError)
       (Lexer.Parser)
       (Basic.Parser)
 
@@ -438,7 +443,9 @@ 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 ?li ?ri ())) in
+    let p =
+      C.Lex_and_parse.make Lexer.Parser.start
+        (C.Basic.make (Origin.current ()) (C.term_only ?li ?ri ())) in
     let p = run p in
     C.ensure_success p
 

lib/parser/scope.ml

@@ -90,19 +90,35 @@ module Situation = struct
 
   let get () = M.exclusively @@ fun () -> (Versioned.get scopes).inner.situation
 
+  let get_at origin =
+    M.exclusively @@ fun () ->
+    match Versioned.get_at scopes origin with
+    | Some s -> s.inner.situation
+    | None -> fatal (Anomaly "invalid origin in Scope.Situation.get_at")
+
   let modify f =
     M.exclusively @@ fun () ->
     let s = Versioned.get scopes in
     let x, situation = f s.inner.situation in
     Versioned.set scopes { s with inner = { s.inner with situation } };
     x
 
+  let left_closeds_at : Origin.t -> (No.plus_omega, No.strict) Notation.entry =
+   fun origin -> left_closeds (get_at origin)
+
   let left_closeds : unit -> (No.plus_omega, No.strict) Notation.entry =
    fun () -> left_closeds (get ())
 
+  let tighters_at : type strict tight.
+      Origin.t -> (tight, strict) No.iinterval -> (tight, strict) Notation.entry =
+   fun origin i -> tighters (get_at origin) i
+
   let tighters : type strict tight. (tight, strict) No.iinterval -> (tight, strict) Notation.entry =
    fun i -> tighters (get ()) i
 
+  let left_opens_at : Origin.t -> Token.t -> No.interval option =
+   fun origin tok -> left_opens (get_at origin) tok
+
   let left_opens : Token.t -> No.interval option = fun tok -> left_opens (get ()) tok
 
   let unparse : Situation.PrintKey.t -> User.notation option =

lib/parser/scope.mli

@@ -90,8 +90,11 @@ val check_name : Trie.path -> Asai.Range.t option -> unit
 
 module Situation : sig
   val get : unit -> Situation.t
+  val left_closeds_at : Origin.t -> (No.plus_omega, No.strict) Notation.entry
   val left_closeds : unit -> (No.plus_omega, No.strict) Notation.entry
+  val tighters_at : Origin.t -> ('tight, 'strict) No.iinterval -> ('tight, 'strict) Notation.entry
   val tighters : ('tight, 'strict) No.iinterval -> ('tight, 'strict) Notation.entry
+  val left_opens_at : Origin.t -> Token.t -> No.interval option
   val left_opens : Token.t -> No.interval option
   val unparse : Situation.PrintKey.t -> User.notation option
   val add : ('left, 'tight, 'right) Notation.notation -> unit

test/black/holes.t/holes.ny

@@ -20,6 +20,17 @@ axiom a_very_long_function : A → A → A → A → A → A → A → B
 
 def f' : A → B ≔ ?
 
+{` Check whether notations that were in scope at the time of a hole are still available when solving the hole even if they're no longer in scope at the current time, while notations defined later are not in scope for the hole. `}
+section sec ≔
+
+  notation "&" ≔ b
+
+  def f' : A → B ≔ ¿_ ↦ &ʔ
+
+end
+
+notation "$" ≔ b
+
 def ℕ : Type ≔ data [ zero. : ℕ | suc. : ℕ → ℕ ]
 
 def plus (m n : ℕ) : ℕ ≔ match n [ zero. ↦ ? | suc. n ↦ ? ]