From e7bf1cd3dc79fb64d5d1529a3fdaec0a587c1073 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Nov 2022 13:46:54 +0100
Subject: [PATCH] refactor: simplify `adaptUncacheableContextFn`

compiler.ir.result reports 0 allocations on happy path
---
 src/Lean/Parser/Types.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index 00fa3c7de2..7ff6c91a21 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -361,10 +361,9 @@ def adaptCacheableContext (f : CacheableParserContext → CacheableParserContext
 
 /-- Run `p` under the given context transformation with a fresh cache, restore outer cache afterwards. -/
 def adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p : ParserFn) : ParserFn := fun c s =>
-  -- extract and temporarily reset parser cache
-  let ⟨stack, lhsPrec, pos, ⟨tkCache, pCache⟩, errorMsg⟩ := s
-  let ⟨stack, lhsPrec, pos, ⟨tkCache, _⟩, errorMsg⟩ := p ⟨f c.toParserContextCore⟩ ⟨stack, lhsPrec, pos, ⟨tkCache, {}⟩, errorMsg⟩
-  ⟨stack, lhsPrec, pos, ⟨tkCache, pCache⟩, errorMsg⟩
+  let parserCache := s.cache.parserCache
+  let s' := p ⟨f c.toParserContextCore⟩ { s with cache.parserCache := {} }
+  { s' with cache.parserCache := parserCache }
 
 /--
 Run `p` and record result in parser cache for any further invocation with this `parserName`, parser context, and parser state.