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

refactor: simplify withCacheFn

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-11 14:07:15 +01:00
parent d44b70c24b
commit 7cdd8f81d7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -392,7 +392,7 @@ def withCacheFn (parserName : Name) (p : ParserFn) : ParserFn := fun c s => Id.r
--dbg_trace "parser cache hit: {parserName}:{s.pos} -> {r.stx}"
return ⟨s.stxStack.push r.stx, r.lhsPrec, r.newPos, s.cache, r.errorMsg⟩
let initStackSz := s.stxStack.raw.size
let s := withStackDrop initStackSz (fun c s => p c { s with lhsPrec := 0, errorMsg := none }) c s
let s := withStackDrop initStackSz p c { s with lhsPrec := 0, errorMsg := none }
if s.stxStack.raw.size != initStackSz + 1 then
panic! s!"withCacheFn: unexpected stack growth {s.stxStack.raw}"
{ s with cache.parserCache := s.cache.parserCache.insert key ⟨s.stxStack.back, s.lhsPrec, s.pos, s.errorMsg⟩ }