structure Aesop.Match : Type

A match associates hypotheses to (a prefix of) the slots of a slot cluster.

• subst : Substitution

  The substitution induced by the hyps or pattern substitutions added to the slots.

• patInstSubsts : Array Substitution

  The pattern substitutions that have been added to the match.

• level : SlotIndex

  The match's level is the index of the maximal slot for which a hyp or pattern substitution has been added to the match.

• forwardDeps : Array PremiseIndex

  Premises that appear in slots which are as yet unassigned in this match (i.e., in slots with index greater than level). This is a property of the rule, but we include it here because it's used to check whether two matches are equivalent.

• conclusionDeps : Array PremiseIndex

  Premises that appear in the rule's conclusion. This is a property of the rule, but we include it here because it's used to check whether two matches are equivalent.

instance Aesop.instInhabitedMatch : Inhabited Match

Equations

• Aesop.instInhabitedMatch = { default := { subst := default, patInstSubsts := default, level := default, forwardDeps := default, conclusionDeps := default } }

def Aesop.Match.equiv (m₁ m₂ : Match) : Bool

Two matches are equivalent if (a) they have the same level; (b) for each premise that appears in a slot greater than the matches' level, their substitution assigns the same value; (c) for each premise that appears in the rule's conclusion, their substitution assigns the same value.

If we already have a match m₁ and we obtain an equivalent match m₂, then m₂ is redundant. This is because if the matches are partial, then m₂ can be completed by exactly the hypotheses that complete m₁, since they agree on the premise instantiations that are relevant for the possible completions. And if the matches are complete, then they assign the same instantiations to the variables that appear in the rule's conclusion, and these are the only ones that ultimately matter.

Equations

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

instance Aesop.Match.instBEq : BEq Match

Equations

• Aesop.Match.instBEq = { beq := Aesop.Match.equiv }

instance Aesop.Match.instHashable : Hashable Match

Equations

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

instance Aesop.Match.instOrd : Ord Match

Equations

• Aesop.Match.instOrd = { compare := fun (m₁ m₂ : Aesop.Match) => (compare m₁.level m₂.level).then (if (m₁ == m₂) = true then Ordering.eq else compare m₁.subst m₂.subst) }

instance Aesop.Match.instToMessageData : Lean.ToMessageData Match

Equations

• Aesop.Match.instToMessageData = { toMessageData := fun (m : Aesop.Match) => Lean.toMessageData "" ++ Lean.toMessageData m.subst ++ Lean.toMessageData "" }

structure Aesop.CompleteMatch : Type

A complete match contains complete matches for each slot cluster. This means there is one match for each slot cluster and each such match contains a hypothesis for each of the slots.

• clusterMatches : Array Match

instance Aesop.instInhabitedCompleteMatch : Inhabited CompleteMatch

Equations

• Aesop.instInhabitedCompleteMatch = { default := { clusterMatches := default } }

instance Aesop.instBEqCompleteMatch : BEq CompleteMatch

Equations

• Aesop.instBEqCompleteMatch = { beq := Aesop.beqCompleteMatch✝ }

instance Aesop.instHashableCompleteMatch : Hashable CompleteMatch

Equations

• Aesop.instHashableCompleteMatch = { hash := Aesop.hashCompleteMatch✝ }

instance Aesop.instEmptyCollectionCompleteMatch : EmptyCollection CompleteMatch

Equations

• Aesop.instEmptyCollectionCompleteMatch = { emptyCollection := { clusterMatches := ∅ } }

instance Aesop.instOrdCompleteMatch : Ord CompleteMatch

Equations

• Aesop.instOrdCompleteMatch = { compare := fun (m₁ m₂ : Aesop.CompleteMatch) => Aesop.compareArraySizeThenLex compare m₁.clusterMatches m₂.clusterMatches }

structure Aesop.ForwardRuleMatch : Type

An entry in the forward state queues. Represents a complete match.

• rule : ForwardRule

  The rule to which this match belongs.

• match : CompleteMatch

  The match.

instance Aesop.instInhabitedForwardRuleMatch : Inhabited ForwardRuleMatch

Equations

• Aesop.instInhabitedForwardRuleMatch = { default := { rule := default, «match» := default } }

instance Aesop.instBEqForwardRuleMatch : BEq ForwardRuleMatch

Equations

• Aesop.instBEqForwardRuleMatch = { beq := Aesop.beqForwardRuleMatch✝ }

instance Aesop.instHashableForwardRuleMatch : Hashable ForwardRuleMatch

Equations

• Aesop.instHashableForwardRuleMatch = { hash := Aesop.hashForwardRuleMatch✝ }

instance Aesop.ForwardRuleMatch.ord : Ord ForwardRuleMatch

Compare two queue entries by rule priority, rule name and the expressions contained in the match. Higher-priority rules are considered less (since the queues are min-queues). The ordering on expressions is arbitrary.

Equations

• Aesop.ForwardRuleMatch.ord = { compare := fun (m₁ m₂ : Aesop.ForwardRuleMatch) => (compare m₁.rule m₂.rule).then (compare m₁.match m₂.match) }

def Aesop.ForwardRuleMatch.le (m₁ m₂ : ForwardRuleMatch) : Bool

Compare two queue entries by rule priority, rule name and the expressions contained in the match. Higher-priority rules are considered less (since the queues are min-queues). The ordering on expressions is arbitrary.

Equations

• m₁.le m₂ = (compare m₁ m₂).isLE