source
def Lean.Meta.Grind.AC.instHashableSeq_lean.hash :
Grind.AC.Seq → UInt64
Equations

- Lean.Meta.Grind.AC.instHashableSeq_lean.hash (Lean.Grind.AC.Seq.var a) = mixHash 0 (hash a)
- Lean.Meta.Grind.AC.instHashableSeq_lean.hash (Lean.Grind.AC.Seq.cons a a_1) = mixHash (mixHash 1 (hash a)) (Lean.Meta.Grind.AC.instHashableSeq_lean.hash a_1)

Instances For

source
instance Lean.Meta.Grind.AC.instHashableSeq_lean :
Hashable Grind.AC.Seq
Equations

- Lean.Meta.Grind.AC.instHashableSeq_lean = { hash := Lean.Meta.Grind.AC.instHashableSeq_lean.hash }

source
instance Lean.Meta.Grind.AC.instHashableExpr_lean :
Hashable Grind.AC.Expr
Equations

- Lean.Meta.Grind.AC.instHashableExpr_lean = { hash := Lean.Meta.Grind.AC.instHashableExpr_lean.hash }

source
def Lean.Meta.Grind.AC.instHashableExpr_lean.hash :
Grind.AC.Expr → UInt64
Equations

- Lean.Meta.Grind.AC.instHashableExpr_lean.hash (Lean.Grind.AC.Expr.var a) = mixHash 0 (hash a)
- Lean.Meta.Grind.AC.instHashableExpr_lean.hash (a.op a_1) = mixHash (mixHash 1 (Lean.Meta.Grind.AC.instHashableExpr_lean.hash a)) (Lean.Meta.Grind.AC.instHashableExpr_lean.hash a_1)

Instances For

source
structure Lean.Meta.Grind.AC.EqCnstr :
Type

- lhs : Grind.AC.Seq
- rhs : Grind.AC.Seq
- h : EqCnstrProof
- id : Nat

Instances For

source
inductive Lean.Meta.Grind.AC.EqCnstrProof :
Type

- core (a b : Expr) (ea eb : Grind.AC.Expr) : EqCnstrProof
- erase_dup (c : EqCnstr) : EqCnstrProof
- erase0 (c : EqCnstr) : EqCnstrProof
- swap (c : EqCnstr) : EqCnstrProof
- simp_exact (lhs : Bool) (c₁ c₂ : EqCnstr) : EqCnstrProof
- simp_ac (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- simp_suffix (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- simp_prefix (lhs : Bool) (s : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- simp_middle (lhs : Bool) (s₁ s₂ : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- superpose_ac (r₁ c r₂ : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- superpose (p s c : Grind.AC.Seq) (c₁ c₂ : EqCnstr) : EqCnstrProof
- superpose_ac_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
- superpose_head_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
- superpose_tail_idempotent (x : Grind.AC.Var) (c₁ : EqCnstr) : EqCnstrProof
- refl (s : Grind.AC.Seq) : EqCnstrProof
- erase_dup_rhs (c : EqCnstr) : EqCnstrProof
- erase0_rhs (c : EqCnstr) : EqCnstrProof

Instances For

source
instance Lean.Meta.Grind.AC.instInhabitedEqCnstrProof :
Inhabited EqCnstrProof
Equations

- Lean.Meta.Grind.AC.instInhabitedEqCnstrProof = { default := Lean.Meta.Grind.AC.EqCnstrProof.core default default default default }

source
instance Lean.Meta.Grind.AC.instInhabitedEqCnstr :
Inhabited EqCnstr
Equations

- Lean.Meta.Grind.AC.instInhabitedEqCnstr = { default := { lhs := default, rhs := default, h := default, id := 0 } }

source
def Lean.Meta.Grind.AC.EqCnstr.compare (c₁ c₂ : EqCnstr) :
Ordering
Equations

- c₁.compare c₂ = (compare c₁.lhs.length c₂.lhs.length).then (compare c₁.id c₂.id)

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.AC.Queue :
Type
Equations

- Lean.Meta.Grind.AC.Queue = Std.TreeSet Lean.Meta.Grind.AC.EqCnstr Lean.Meta.Grind.AC.EqCnstr.compare

Instances For

source
structure Lean.Meta.Grind.AC.DiseqCnstr :
Type

- lhs : Grind.AC.Seq
- rhs : Grind.AC.Seq
- h : DiseqCnstrProof

Instances For

source
inductive Lean.Meta.Grind.AC.DiseqCnstrProof :
Type

- core (a b : Expr) (ea eb : Grind.AC.Expr) : DiseqCnstrProof
- erase_dup (c : DiseqCnstr) : DiseqCnstrProof
- erase0 (c : DiseqCnstr) : DiseqCnstrProof
- simp_exact (lhs : Bool) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- simp_ac (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- simp_suffix (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- simp_prefix (lhs : Bool) (s : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- simp_middle (lhs : Bool) (s₁ s₂ : Grind.AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof

Instances For

source
structure Lean.Meta.Grind.AC.Struct :
Type

- id : Nat
- type : Expr
- u : Level

  Cached `getLevel type`

- op : Expr
- neutral? : Option Expr
- assocInst : Expr
- idempotentInst? : Option Expr
- commInst? : Option Expr
- neutralInst? : Option Expr
- nextId : Nat

  Next unique id for `EqCnstr`s.

- vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

- varMap : PHashMap ExprPtr Grind.AC.Var

  Mapping from `Expr` to a variable representing it.

- denote : PHashMap ExprPtr Grind.AC.Expr

  Mapping from Lean expressions to their representations as `AC.Expr`

- denoteEntries : PArray (Expr × Grind.AC.Expr)

  `denoteEntries` is `denote` as a `PArray` for deterministic traversal.

- queue : Queue

  Equations to process.

- basis : List EqCnstr

  Processed equations.

- diseqs : PArray DiseqCnstr

  Disequalities.

- recheck : Bool

  If `recheck` is `true`, then new equalities have been added to the basis since we checked disequalities and implied equalities.

Instances For

source
def Lean.Meta.Grind.AC.instInhabitedStruct.default :
Struct
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.Meta.Grind.AC.instInhabitedStruct :
Inhabited Struct
Equations

- Lean.Meta.Grind.AC.instInhabitedStruct = { default := Lean.Meta.Grind.AC.instInhabitedStruct.default }

source
structure Lean.Meta.Grind.AC.State :
Type

State for all associative operators detected by `grind`.

- structs : Array Struct

  Structures/operators detected. We expect to find a small number of associative operators in a given goal. Thus, using `Array` is fine here.

- opIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from operators to its "operator id". We cache failures using `none`. `opIdOf[op]` is `some id`, then `id < structs.size`.

- exprToOpIds : PHashMap ExprPtr (List Nat)

  Mapping from expressions/terms to their structure ids. Recall that term may be the argument of different operators.

- steps : Nat

Instances For

source
def Lean.Meta.Grind.AC.instInhabitedState.default :
State
Equations

- Lean.Meta.Grind.AC.instInhabitedState.default = { structs := default, opIdOf := default, exprToOpIds := default, steps := default }

Instances For

source
instance Lean.Meta.Grind.AC.instInhabitedState :
Inhabited State
Equations

- Lean.Meta.Grind.AC.instInhabitedState = { default := Lean.Meta.Grind.AC.instInhabitedState.default }

source
opaque Lean.Meta.Grind.AC.acExt :
SolverExtension State