diff --git a/src/Lean/Util/ForEachExprWhere.lean b/src/Lean/Util/ForEachExprWhere.lean index 963e4baa33..88a5e18e1e 100644 --- a/src/Lean/Util/ForEachExprWhere.lean +++ b/src/Lean/Util/ForEachExprWhere.lean @@ -19,11 +19,13 @@ If `p` holds for most subterms, then it is more efficient to use `forEach f e`. namespace ForEachExprWhere abbrev cacheSize : USize := 8192 - 1 +private def notAnExpr : Unit × Unit := ⟨⟨⟩, ⟨⟩⟩ + structure State where /-- Implements caching trick similar to the one used at `FindExpr` and `ReplaceExpr`. -/ - visited : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr + visited : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `notAnExpr` is not a valid Expr /-- Set of visited subterms that satisfy the predicate `p`. We have to use this set to make sure `f` is applied at most once of each subterm that satisfies `p`. @@ -31,7 +33,7 @@ structure State where checked : Std.HashSet Expr unsafe def initCache : State := { - visited := .replicate cacheSize.toNat (cast lcProof ()) + visited := .replicate cacheSize.toNat (cast lcProof notAnExpr) checked := {} } diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 1f49e4d29f..e159c3e20b 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -55,8 +55,10 @@ unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr | e => pure e visit e +private def notAnExpr : Unit × Unit := ⟨⟨⟩, ⟨⟩⟩ + unsafe def initCache : State := - { keys := .replicate cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr` + { keys := .replicate cacheSize.toNat (cast lcProof notAnExpr), -- `notAnExpr` is not a valid `Expr` results := .replicate cacheSize.toNat default } unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr := diff --git a/tests/lean/run/addDecorationsWithoutPartial.lean b/tests/lean/run/addDecorationsWithoutPartial.lean index 548b229aab..e8f648acf9 100644 --- a/tests/lean/run/addDecorationsWithoutPartial.lean +++ b/tests/lean/run/addDecorationsWithoutPartial.lean @@ -36,8 +36,10 @@ unsafe def replaceUnsafeM (size : USize) (e : Expr) (f? : (e' : Expr) → sizeOf | e => pure e visit e +private def notAnExpr : Unit × Unit := ⟨⟨⟩, ⟨⟩⟩ + unsafe def initCache : State := - { keys := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr` + { keys := mkArray cacheSize.toNat (cast lcProof notAnExpr), -- `notAnExpr` is not a valid `Expr` results := mkArray cacheSize.toNat default } unsafe def replaceUnsafe (e : Expr) (f? : (e' : Expr) → sizeOf e' ≤ sizeOf e → Option Expr) : Expr :=