refactor: ENodeKey => ExprPtr (#8674)

Author: leodemoura

src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.ExprPtr
 
 namespace Lean.Meta.Grind
 
@@ -58,7 +58,7 @@ instance : BEq AlphaKey where
   beq k₁ k₂ := alphaEq k₁.expr k₂.expr
 
 structure AlphaShareCommon.State where
-  map : PHashMap ENodeKey Expr := {}
+  map : PHashMap ExprPtr Expr := {}
   set : PHashSet AlphaKey := {}
 
 abbrev AlphaShareCommonM := StateM AlphaShareCommon.State

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Data.PersistentArray
 import Lean.Data.RBTree
-import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 
@@ -155,9 +155,9 @@ structure Ring where
   -/
   vars           : PArray Expr := {}
   /-- Mapping from `Expr` to a variable representing it. -/
-  varMap         : PHashMap ENodeKey Var := {}
+  varMap         : PHashMap ExprPtr Var := {}
   /-- Mapping from Lean expressions to their representations as `RingExpr` -/
-  denote         : PHashMap ENodeKey RingExpr := {}
+  denote         : PHashMap ExprPtr RingExpr := {}
   /-- Next unique id for `EqCnstr`s. -/
   nextId         : Nat := 0
   /-- Number of "steps": simplification and superposition. -/
@@ -189,9 +189,9 @@ structure State where
   /--
   Mapping from types to its "ring id". We cache failures using `none`.
   `typeIdOf[type]` is `some id`, then `id < rings.size`. -/
-  typeIdOf : PHashMap ENodeKey (Option Nat) := {}
+  typeIdOf : PHashMap ExprPtr (Option Nat) := {}
   /- Mapping from expressions/terms to their ring ids. -/
-  exprToRingId : PHashMap ENodeKey Nat := {}
+  exprToRingId : PHashMap ExprPtr Nat := {}
   steps := 0
   deriving Inhabited
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Int.Linear
 import Std.Internal.Rat
 import Lean.Data.PersistentArray
-import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
 
 namespace Lean.Meta.Grind.Arith.Cutsat
@@ -231,18 +231,18 @@ structure State where
   /-- Mapping from variables to their denotations. -/
   vars : PArray Expr := {}
   /-- Mapping from `Expr` to a variable representing it. -/
-  varMap  : PHashMap ENodeKey Var := {}
+  varMap  : PHashMap ExprPtr Var := {}
   /--
   Mapping from foreign terms to their variable and type (e.g., `Nat`). They are also marked using `markAsCutsatTerm`.
   -/
-  foreignVarMap : PHashMap ENodeKey (Var × ForeignType) := {}
+  foreignVarMap : PHashMap ExprPtr (Var × ForeignType) := {}
   foreignVars : PHashMap ForeignType (PArray Expr) := {}
   /--
   Some foreign variables encode nested terms such as `b+1`.
   This is a mapping from this kind of variable to the integer variable
   representing `natCast (b+1)`.
   -/
-  foreignDef : PHashMap ENodeKey Var := {}
+  foreignDef : PHashMap ExprPtr Var := {}
   /--
   Mapping from variables to divisibility constraints. Recall that we keep the divisibility constraint in solved form.
   Thus, we have at most one divisibility per variable. -/

src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Data.AssocList
 import Lean.Data.PersistentArray
-import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.Offset.Util
 
@@ -43,9 +43,9 @@ structure State where
   /-- Mapping from `NodeId` to the `Expr` represented by the node. -/
   nodes    : PArray Expr := {}
   /-- Mapping from `Expr` to a node representing it. -/
-  nodeMap  : PHashMap ENodeKey NodeId := {}
+  nodeMap  : PHashMap ExprPtr NodeId := {}
   /-- Mapping from `Expr` representing inequalites to constraints. -/
-  cnstrs   : PHashMap ENodeKey (Cnstr NodeId) := {}
+  cnstrs   : PHashMap ExprPtr (Cnstr NodeId) := {}
   /--
   Mapping from pairs `(u, v)` to a list of offset constraints on `u` and `v`.
   We use this mapping to implement exhaustive constraint propagation.

src/Lean/Meta/Tactic/Grind/ENodeKey.lean src/Lean/Meta/Tactic/Grind/ExprPtr.leansrc/Lean/Meta/Tactic/Grind/ENodeKey.lean renamed to src/Lean/Meta/Tactic/Grind/ExprPtr.lean

@@ -14,20 +14,20 @@ namespace Lean.Meta.Grind
   unsafe ptrEq a b
 
 /--
-Key for the `ENodeMap` and `ParentMap` map.
+Key for the `ENodeMap`, `ParentMap`, and other maps and sets.
 We use pointer addresses and rely on the fact all internalized expressions
 have been hash-consed, i.e., we have applied `shareCommon`.
 -/
-structure ENodeKey where
+structure ExprPtr where
   expr : Expr
 
 abbrev hashPtrExpr (e : Expr) : UInt64 :=
   unsafe (ptrAddrUnsafe e >>> 3).toUInt64
 
-instance : Hashable ENodeKey where
+instance : Hashable ExprPtr where
   hash k := hashPtrExpr k.expr
 
-instance : BEq ENodeKey where
+instance : BEq ExprPtr where
   beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -14,7 +14,7 @@ import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Ext
-import Lean.Meta.Tactic.Grind.ENodeKey
+import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.AlphaShareCommon
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.ExtAttr
@@ -418,7 +418,7 @@ inductive NewFact where
   | eq (lhs rhs proof : Expr) (isHEq : Bool)
   | fact (prop proof : Expr) (generation : Nat)
 
-abbrev ENodeMap := PHashMap ENodeKey ENode
+abbrev ENodeMap := PHashMap ExprPtr ENode
 
 /--
 Key for the congruence table.
@@ -503,7 +503,7 @@ abbrev CongrTable (enodeMap : ENodeMap) := PHashSet (CongrKey enodeMap)
 
 -- Remark: we cannot use pointer addresses here because we have to traverse the tree.
 abbrev ParentSet := Std.TreeSet Expr Expr.quickComp
-abbrev ParentMap := PHashMap ENodeKey ParentSet
+abbrev ParentMap := PHashMap ExprPtr ParentSet
 
 /--
 The E-matching module instantiates theorems using the `EMatchTheorem proof` and a (partial) assignment.
@@ -650,7 +650,7 @@ structure Split.State where
   /-- Case-splits that have been inserted at `candidates` at some point. -/
   added        : Std.HashSet SplitInfo := {}
   /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/
-  resolved     : PHashSet ENodeKey := {}
+  resolved     : PHashSet ExprPtr := {}
   /--
   Sequence of cases steps that generated this goal. We only use this information for diagnostics.
   Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
@@ -707,7 +707,7 @@ structure Goal where
   /-- Asserted facts -/
   facts        : PArray Expr := {}
   /-- Cached extensionality theorems for types. -/
-  extThms      : PHashMap ENodeKey (Array Ext.ExtTheorem) := {}
+  extThms      : PHashMap ExprPtr (Array Ext.ExtTheorem) := {}
   /-- State of the E-matching module. -/
   ematch       : EMatch.State
   /-- State of the case-splitting module. -/