From 7cdd8f81d7e3d302ee49ffdecc21b2bfeff09daf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 11 Nov 2022 14:07:15 +0100 Subject: [PATCH] refactor: simplify `withCacheFn` --- src/Lean/Parser/Types.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean index f8603940af..be0aff2186 100644 --- a/src/Lean/Parser/Types.lean +++ b/src/Lean/Parser/Types.lean @@ -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⟩ }