From 09f613111bdded9a5c23b2a060e5929224e02ce0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Feb 2020 19:16:46 -0800
Subject: [PATCH] perf: remove `used` field

The trick is to use `()` to initialize `keys`.
`()` is not a valid `Expr` in our runtime.
---
 src/Init/Lean/Util/FindExpr.lean    |  6 +++---
 src/Init/Lean/Util/ReplaceExpr.lean | 14 ++++++--------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/Init/Lean/Util/FindExpr.lean b/src/Init/Lean/Util/FindExpr.lean
index c18cc9b31c..88d4db3650 100644
--- a/src/Init/Lean/Util/FindExpr.lean
+++ b/src/Init/Lean/Util/FindExpr.lean
@@ -15,7 +15,7 @@ namespace FindImpl
 abbrev cacheSize : USize := 8192
 
 structure State :=
-(keys : Array Expr)
+(keys : Array Expr) -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
 
 abbrev FindM := StateM State
 
@@ -41,8 +41,8 @@ else do
     | Expr.proj _ _ b _      => findM? b
     | e                      => failure
 
-def initCache : State :=
-{ keys    := mkArray cacheSize.toNat (arbitrary _) }
+unsafe def initCache : State :=
+{ keys    := mkArray cacheSize.toNat (cast lcProof ()) }
 
 @[inline] unsafe def findExprUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
 (findM? p cacheSize e).run' initCache
diff --git a/src/Init/Lean/Util/ReplaceExpr.lean b/src/Init/Lean/Util/ReplaceExpr.lean
index e3a072cce0..471f7a4cdd 100644
--- a/src/Init/Lean/Util/ReplaceExpr.lean
+++ b/src/Init/Lean/Util/ReplaceExpr.lean
@@ -14,14 +14,13 @@ namespace ReplaceImpl
 abbrev cacheSize : USize := 8192
 
 structure State :=
-(keys    : Array Expr)
-(used    : Array Bool)
+(keys    : Array Expr) -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
 (results : Array Expr)
 
 abbrev ReplaceM := StateM State
 
 @[inline] unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
-modify $ fun s => { keys := s.keys.uset i key lcProof, used := s.used.uset i true lcProof, results := s.results.uset i result lcProof };
+modify $ fun s => { keys := s.keys.uset i key lcProof, results := s.results.uset i result lcProof };
 pure result
 
 @[specialize] unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) : Expr → ReplaceM Expr
@@ -29,7 +28,7 @@ pure result
   c ← get;
   let h := ptrAddrUnsafe e;
   let i := h % size;
-  if c.used.uget i lcProof && ptrAddrUnsafe (c.keys.uget i lcProof) == h then
+  if ptrAddrUnsafe (c.keys.uget i lcProof) == h then
     pure $ c.results.uget i lcProof
   else match f? e with
     | some eNew => cache i e eNew
@@ -43,10 +42,9 @@ pure result
       | Expr.localE _ _ _ _    => unreachable!
       | e                      => pure e
 
-def initCache : State :=
-{ keys    := mkArray cacheSize.toNat (arbitrary _),
-  results := mkArray cacheSize.toNat (arbitrary _),
-  used    := mkArray cacheSize.toNat false }
+unsafe def initCache : State :=
+{ keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
+  results := mkArray cacheSize.toNat (arbitrary _) }
 
 @[inline] unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
 (replaceUnsafeM f? cacheSize e).run' initCache