Documentation

Aesop.Rule.Forward

inductive Aesop.ForwardRulePriority :

The priority of a forward rule.

normSafe (n : Int) : ForwardRulePriority
If the rule is a norm or safe rule, its priority is an integer.
unsafe (p : Percent) : ForwardRulePriority
If the rule is an unsafe rule, its priority is a percentage representing the rule's success probability.

Instances For

instance Aesop.instInhabitedForwardRulePriority :

Inhabited ForwardRulePriority

Equations

Aesop.instInhabitedForwardRulePriority = { default := Aesop.ForwardRulePriority.normSafe default }

instance Aesop.instBEqForwardRulePriority :

BEq ForwardRulePriority

Equations

Aesop.instBEqForwardRulePriority = { beq := Aesop.beqForwardRulePriority✝ }

def Aesop.ForwardRulePriority.penalty? :

ForwardRulePriority → Option Int

If a ForwardRulePriority contains a penalty, extract it.

Equations

(Aesop.ForwardRulePriority.normSafe n).penalty? = some n
(Aesop.ForwardRulePriority.unsafe p).penalty? = none

def Aesop.ForwardRulePriority.successProbability? :

ForwardRulePriority → Option Percent

If a ForwardRulePriority contains a success probability, extract it.

Equations

def Aesop.ForwardRulePriority.compare (p₁ p₂ : ForwardRulePriority) :

Compare two rule priorities. Less means higher priority ('better'). Norm/safe rules have higher priority than unsafe rules. Among norm/safe rules, lower penalty is better. Among unsafe rules, higher percentage is better.

Equations

(Aesop.ForwardRulePriority.normSafe n).compare (Aesop.ForwardRulePriority.unsafe p) = Ordering.lt
(Aesop.ForwardRulePriority.unsafe p).compare (Aesop.ForwardRulePriority.normSafe n) = Ordering.gt
(Aesop.ForwardRulePriority.normSafe n₁).compare (Aesop.ForwardRulePriority.normSafe n₂) = compare n₁ n₂
(Aesop.ForwardRulePriority.unsafe p₁).compare (Aesop.ForwardRulePriority.unsafe p₂) = (compare p₁ p₂).swap

instance Aesop.ForwardRulePriority.instOrd :

Ord ForwardRulePriority

Equations

Aesop.ForwardRulePriority.instOrd = { compare := Aesop.ForwardRulePriority.compare }

instance Aesop.ForwardRulePriority.instToString :

ToString ForwardRulePriority

Equations

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

structure Aesop.ForwardRuleextends Aesop.ForwardRuleInfo :

A forward rule.

numPremises : Nat
numLevelParams : Nat
slotClusters : Array (Array Slot)
conclusionDeps : Array PremiseIndex
rulePatternInfo? : Option (RulePattern × PremiseIndex)
name : RuleName
The rule's name. Should be unique among all rules in a rule set.
term : RuleTerm
The theorem from which this rule is derived.
prio : ForwardRulePriority
The rule's priority.

Instances For

instance Aesop.instInhabitedForwardRule :

Inhabited ForwardRule

Equations

Aesop.instInhabitedForwardRule = { default := { toForwardRuleInfo := default, name := default, term := default, prio := default } }

instance Aesop.ForwardRule.instBEq :

BEq ForwardRule

Equations

Aesop.ForwardRule.instBEq = { beq := fun (r₁ r₂ : Aesop.ForwardRule) => r₁.name == r₂.name }

instance Aesop.ForwardRule.instHashable :

Hashable ForwardRule

Equations

Aesop.ForwardRule.instHashable = { hash := fun (r : Aesop.ForwardRule) => hash r.name }

instance Aesop.ForwardRule.instOrd :

Ord ForwardRule

Equations

Aesop.ForwardRule.instOrd = { compare := fun (r₁ r₂ : Aesop.ForwardRule) => (compare r₁.prio r₂.prio).then (compare r₁.name r₂.name) }

instance Aesop.ForwardRule.instToString :

ToString ForwardRule

Equations

Aesop.ForwardRule.instToString = { toString := fun (r : Aesop.ForwardRule) => toString "[" ++ toString r.prio ++ toString "] " ++ toString r.name ++ toString "" }

def Aesop.ForwardRule.destruct (r : ForwardRule) :

Is this rule a destruct rule (i.e., should we clear matched hyps)?

Equations

r.destruct = match r.name.builder with | Aesop.BuilderName.destruct => true | x => false