max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: reset lhsPrec, errorMsg in withCacheFn

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-10 15:18:01 +01:00
parent 22510db004
commit 0dea086669
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Parser/Types.lean
View file

@ -365,7 +365,11 @@ def adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p :
/--
Run `p` and record result in parser cache for any further invocation with this `parserName`, parser context, and parser state.
`p` cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. -/
`p` cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history.
As this excludes trailing parsers from being cached, we also reset `lhsPrec`, which is not read but set by leading parsers, to 0
in order to increase cache hits. Finally, `errorMsg` is also reset to `none` as a leading parser should not be called in the first
place if there was an error.
-/
def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.run do
let key := ⟨c.toCacheableParserContext, parserName, s.pos⟩
if let some r := s.cache.parserCache.find? key then
@ -374,7 +378,7 @@ def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.r
return ⟨s.stxStack.push r.stx, r.lhsPrec, r.newPos, s.cache, r.errorMsg⟩
let initDrop := s.stxStack.drop
let initStackSz := s.stxStack.raw.size
let s := p c { s with stxStack.drop := initStackSz }
let s := p c { s with stxStack.drop := initStackSz, lhsPrec := 0, errorMsg := none }
let s := { s with stxStack.drop := initDrop }
if s.stxStack.raw.size != initStackSz + 1 then
panic! s!"withCacheFn: unexpected stack growth {s.stxStack.raw}"