Solver for preorders, partial orders, linear orders, and support for offsets.

@[reducible, inline]

abbrev Lean.Meta.Grind.Order.NodeId : Type

Equations

• Lean.Meta.Grind.Order.NodeId = Nat

inductive Lean.Meta.Grind.Order.CnstrKind : Type

• le : CnstrKind
• lt : CnstrKind

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedCnstrKind : Inhabited CnstrKind

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstrKind = { default := Lean.Meta.Grind.Order.instInhabitedCnstrKind.default }

structure Lean.Meta.Grind.Order.Cnstr (α : Type) : Type

A constraint of the form u ≤ v + k (u < v + k if strict := true) Remark: If the order does not support offsets, then k is zero. h? := some h if the Lean expression is not definitionally equal to the constraint, but provably equal with proof h.

• kind : CnstrKind
• u : α
• v : α
• k : Int
• e : Expr

  Denotation of this constraint as an expression.

• h? : Option Expr

  If h? := some h, then h is proof for that the expression associated with this constraint is equal to e. Recall that the input constraints are normalized. For example, given x y : Int, x ≤ y is internally represented as x ≤ y + 0

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedCnstr {a✝ : Type} [Inhabited a✝] : Inhabited (Cnstr a✝)

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstr = { default := Lean.Meta.Grind.Order.instInhabitedCnstr.default }

structure Lean.Meta.Grind.Order.Weight : Type

• k : Int
• strict : Bool

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedWeight : Inhabited Weight

Equations

• Lean.Meta.Grind.Order.instInhabitedWeight = { default := Lean.Meta.Grind.Order.instInhabitedWeight.default }

structure Lean.Meta.Grind.Order.ProofInfo : Type

Auxiliary structure used for proof extraction.

• w : NodeId
• k : Weight
• proof : Expr

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedProofInfo : Inhabited ProofInfo

Equations

• Lean.Meta.Grind.Order.instInhabitedProofInfo = { default := Lean.Meta.Grind.Order.instInhabitedProofInfo.default }

inductive Lean.Meta.Grind.Order.ToPropagate : Type

Auxiliary inductive type for representing constraints and equalities that should be propagated to core. Recall that we cannot compute proofs until the short-distance data-structures have been fully updated when a new edge is inserted. Thus, we store the information to be propagated into a list. See field propagate in State.

• eqTrue (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : ToPropagate
• eqFalse (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : ToPropagate
• eq (u v : NodeId) : ToPropagate

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedToPropagate : Inhabited ToPropagate

Equations

• Lean.Meta.Grind.Order.instInhabitedToPropagate = { default := Lean.Meta.Grind.Order.instInhabitedToPropagate.default }

structure Lean.Meta.Grind.Order.Struct : Type

Per-goal solver state of an order structure. The instances and the canonical ≤/< functions live in Sym.Arith.Order (see Sym.Arith.classifyOrder?); id is the index of that record, and structs in State is indexed by the same ids.

• id : Nat
• nodes : PArray Expr

  Mapping from NodeId to the Expr represented by the node.

• nodeMap : PHashMap ExprPtr NodeId

  Mapping from Expr to a node representing it.

• cnstrs : PHashMap ExprPtr (Cnstr NodeId)

  Mapping from Expr representing inequalities to constraints.

• cnstrsOf : PHashMap (NodeId × NodeId) (List (Cnstr NodeId × Expr))

  Mapping from pairs (u, v) to a list of constraints on u and v. We use this mapping to implement exhaustive constraint propagation.

• sources : PArray (AssocList NodeId Weight)

  For each node with id u, sources[u] contains pairs (v, k) s.t. there is a path from v to u with weight k.

• targets : PArray (AssocList NodeId Weight)

  For each node with id u, targets[u] contains pairs (v, k) s.t. there is a path from u to v with weight k.

• proofs : PArray (AssocList NodeId ProofInfo)

  Proof reconstruction information. For each node with id u, proofs[u] contains pairs (v, { w, proof }) s.t. there is a path from u to v, and w is the penultimate node in the path, and proof is the justification for the last edge.

• propagate : List ToPropagate

  Truth values and equalities to propagate to core.

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedStruct : Inhabited Struct

Equations

• Lean.Meta.Grind.Order.instInhabitedStruct = { default := Lean.Meta.Grind.Order.instInhabitedStruct.default }

structure Lean.Meta.Grind.Order.TermMapEntry : Type

Entry/Value for the map termMap in State

• e : Expr
• h : Expr
• α : Expr

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedTermMapEntry : Inhabited TermMapEntry

Equations

• Lean.Meta.Grind.Order.instInhabitedTermMapEntry = { default := Lean.Meta.Grind.Order.instInhabitedTermMapEntry.default }

structure Lean.Meta.Grind.Order.State : Type

State for all order types detected by grind.

• structs : Array Struct

  Order structures detected.

• typeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "structure id". We cache failures using none. typeIdOf[type] is some id, then id < structs.size.

• exprToStructId : PHashMap ExprPtr Nat

  Mapping from expressions/terms to their structure ids.

• termMap : PHashMap ExprPtr TermMapEntry

  Mapping from terms/constraints that have been mapped into Rings before being internalized. Example: given x y : Nat, x ≤ y + 1 is mapped to Int.ofNat x ≤ Int.ofNat y + 1, and proof of equivalence.

• termMapInv : PHashMap ExprPtr (Expr × Expr)

  termMap inverse

@[instance_reducible]

instance Lean.Meta.Grind.Order.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Order.instInhabitedState = { default := Lean.Meta.Grind.Order.instInhabitedState.default }

opaque Lean.Meta.Grind.Order.orderExt : SolverExtension State

def Lean.Meta.Grind.Order.get' : GoalM State

Equations

• Lean.Meta.Grind.Order.get' = Lean.Meta.Grind.Order.orderExt.getState

@[inline]

def Lean.Meta.Grind.Order.modify' (f : State → State) : GoalM Unit

Equations

• Lean.Meta.Grind.Order.modify' f = Lean.Meta.Grind.Order.orderExt.modifyState f