From da6efe1bca4722e2258babe799ec533bf1c1ddab Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 5 Nov 2022 14:04:41 +0100
Subject: [PATCH] fix: make parser caching sound (I hope?)

---
 src/Lean/Data/OpenDecl.lean    |  1 +
 src/Lean/Data/Options.lean     |  8 ++++++++
 src/Lean/Parser/Basic.lean     | 26 +++++++++++++++++---------
 src/Lean/Parser/Extension.lean |  9 ++++-----
 stage0/src/stdlib_flags.h      |  2 +-
 5 files changed, 31 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Data/OpenDecl.lean b/src/Lean/Data/OpenDecl.lean
index fad2a52564..6f761dcf2f 100644
--- a/src/Lean/Data/OpenDecl.lean
+++ b/src/Lean/Data/OpenDecl.lean
@@ -11,6 +11,7 @@ namespace Lean
 inductive OpenDecl where
   | simple   (ns : Name) (except : List Name)
   | explicit (id : Name) (declName : Name)
+  deriving BEq, Hashable
 
 namespace OpenDecl
 instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 9e16003d2a..4aa9c6e367 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -16,6 +16,14 @@ instance : Inhabited Options where
   default := {}
 instance : ToString Options := inferInstanceAs (ToString KVMap)
 instance : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
+instance : BEq Options := inferInstanceAs (BEq KVMap)
+instance : Hashable Options where
+  hash opts :=
+    let _ : Hashable DataValue := ⟨fun
+      | .ofString v | .ofBool v | .ofName v | .ofNat v | .ofInt v => hash v
+      -- `Syntax` should never be an option value
+      | .ofSyntax _ => 0⟩
+    hash opts.entries
 
 structure OptionDecl where
   declName : Name := by exact decl_name%
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 96332d3b4a..9dab951edc 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -100,22 +100,30 @@ structure InputContext where
   fileMap  : FileMap
   deriving Inhabited
 
-/-- Input context derived from elaboration of previous commands. -/
-structure ParserModuleContext where
-  env           : Environment
+structure ParserModuleContextCacheKey where
   options       : Options
   -- for name lookup
   currNamespace : Name := .anonymous
   openDecls     : List OpenDecl := []
+  deriving BEq, Hashable
 
-structure ParserContext extends InputContext, ParserModuleContext where
+/-- Input context derived from elaboration of previous commands. -/
+structure ParserModuleContext extends ParserModuleContextCacheKey where
+  -- within a command parse currently determined by initial state plus `openDecls`
+  env : Environment
+
+structure ParserContextCacheKey extends ParserModuleContextCacheKey where
   prec               : Nat
-  tokens             : TokenTable
   -- used for bootstrapping only
   quotDepth          : Nat := 0
   suppressInsideQuot : Bool := false
   savedPos?          : Option String.Pos := none
   forbiddenTk?       : Option Token := none
+  deriving BEq, Hashable
+
+structure ParserContext extends ParserContextCacheKey, InputContext, ParserModuleContext where
+  -- within a command parse currently determined by initial state plus `openDecls`
+  tokens : TokenTable
 
 structure Error where
   unexpected : String := ""
@@ -152,9 +160,8 @@ structure TokenCacheEntry where
   stopPos  : String.Pos := 0
   token    : Syntax := Syntax.missing
 
-structure CategoryCacheKey where
+structure CategoryCacheKey extends ParserContextCacheKey where
   cat : Name
-  prec : Nat
   pos : String.Pos
   deriving BEq, Hashable
 
@@ -1703,12 +1710,13 @@ def categoryParserFn (catName : Name) : ParserFn := fun ctx s =>
 
 def categoryParser (catName : Name) (prec : Nat) : Parser := {
   fn := fun c s => Id.run do
-    let key := ⟨catName, prec, s.pos⟩
+    let c := { c with prec }
+    let key := ⟨c.toParserContextCacheKey, catName, s.pos⟩
     if let some r := s.cache.categoryCache.find? key then
       match s with
       | ⟨stack, _, _, cache, _⟩ => return ⟨stack.push r.stx, r.lhsPrec, r.newPos, cache, r.errorMsg⟩
     let initStackSz := s.stackSize
-    let s := categoryParserFn catName { c with prec := prec } s
+    let s := categoryParserFn catName c s
     if s.stackSize > initStackSz + 1 then
       panic! s!"categoryParser: unexpected stack growth {s.stxStack}"
     let s := if s.stackSize == initStackSz then s.pushSyntax .missing else s
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index a39aacb152..71f3acceca 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -445,11 +445,10 @@ def mkInputContext (input : String) (fileName : String) : InputContext := {
   fileMap  := input.toFileMap
 }
 
-def mkParserContext (ictx : InputContext) (pmctx : ParserModuleContext) : ParserContext := {
-  prec                  := 0,
-  toInputContext        := ictx,
-  toParserModuleContext := pmctx,
-  tokens                := getTokenTable pmctx.env
+def mkParserContext (ictx : InputContext) (pmctx : ParserModuleContext) : ParserContext := { pmctx with
+  prec           := 0,
+  toInputContext := ictx,
+  tokens         := getTokenTable pmctx.env,
 }
 
 def mkParserState (input : String) : ParserState :=
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index aae6413ccc..82742d5e98 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     opts = opts.update({"pp", "rawOnError"}, true);