structure Aesop.BaseRuleSet : Type

The Aesop-specific parts of an Aesop rule set. A BaseRuleSet stores global Aesop rules, e.g. safe and unsafe rules. It does not store simp theorems for the builtin norm simp rule; these are instead stored in a simp extension.

• normRules : Index NormRuleInfo

  Normalisation rules registered in this rule set.

• unsafeRules : Index UnsafeRuleInfo

  Unsafe rules registered in this rule set.

• safeRules : Index SafeRuleInfo

  Safe rules registered in this rule set.

• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)

  Rules for the builtin unfold rule. A pair (decl, unfoldThm?) in this map represents a declaration decl which should be unfolded. unfoldThm? should be the output of getUnfoldEqnFor? decl and is cached here for efficiency.

• forwardRules : ForwardIndex

  Forward rules. There's a special procedure for applying forward rules, so we don't store them in the regular indices.

• forwardRuleNames : Lean.PHashSet RuleName

  The names of all rules in forwardRules.

• rulePatterns : RulePatternIndex

  An index for the rule patterns associated with rules contained in this rule set. When rules are removed from the rule set, their patterns are not removed from this index.

• erased : Lean.PHashSet RuleName

  The set of rules that were erased from normRules, unsafeRules, safeRules and forwardRules. When we erase a rule which is present in any of these four indices, the rule is not removed from the indices but just added to this set. By contrast, when we erase a rule from unfoldRules, we actually delete it.

• ruleNames : Lean.PHashMap Lean.Name (UnorderedArraySet RuleName)

  A cache of the names of all rules registered in this rule set. Invariant: ruleNames contains exactly the names of the rules present in normRules, unsafeRules, safeRules, forwardRules and unfoldRules and not present in erased. We use this cache (a) to quickly determine whether a rule is present in the rule set and (b) to find the full rule names associated with the fvar or const identified by a name.

Instances For

• Aesop.instEmptyCollectionBaseRuleSet
• Aesop.instInhabitedBaseRuleSet

instance Aesop.instInhabitedBaseRuleSet : Inhabited BaseRuleSet

Equations

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

structure Aesop.GlobalRuleSetextends Aesop.BaseRuleSet : Type

A global Aesop rule set. When we tag a declaration with @[aesop], it is stored in one or more of these rule sets. Internally, a GlobalRuleSet is composed of a BaseRuleSet (stored in an Aesop rule set extension) plus a set of simp theorems (stored in a SimpExtension).

• normRules : Index NormRuleInfo
• unsafeRules : Index UnsafeRuleInfo
• safeRules : Index SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• forwardRules : ForwardIndex
• forwardRuleNames : Lean.PHashSet RuleName
• rulePatterns : RulePatternIndex
• erased : Lean.PHashSet RuleName
• ruleNames : Lean.PHashMap Lean.Name (UnorderedArraySet RuleName)
• simpTheorems : Lean.Meta.SimpTheorems

  The simp theorems stored in this rule set.

• simprocs : Lean.Meta.Simprocs

  The simprocs stored in this rule set.

Instances For

• Aesop.instEmptyCollectionGlobalRuleSet
• Aesop.instInhabitedGlobalRuleSet

instance Aesop.instInhabitedGlobalRuleSet : Inhabited GlobalRuleSet

Equations

• Aesop.instInhabitedGlobalRuleSet = { default := { toBaseRuleSet := default, simpTheorems := default, simprocs := default } }

structure Aesop.LocalRuleSetextends Aesop.BaseRuleSet : Type

The rule set used by an Aesop tactic call. A local rule set is produced by combining several global rule sets and possibly adding or erasing some individual rules.

• normRules : Index NormRuleInfo
• unsafeRules : Index UnsafeRuleInfo
• safeRules : Index SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• forwardRules : ForwardIndex
• forwardRuleNames : Lean.PHashSet RuleName
• rulePatterns : RulePatternIndex
• erased : Lean.PHashSet RuleName
• ruleNames : Lean.PHashMap Lean.Name (UnorderedArraySet RuleName)
• simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)

  The simp theorems used by the builtin norm simp rule.

• simpTheoremsArrayNonempty : 0 < self.simpTheoremsArray.size

  The simp theorems array must contain at least one SimpTheorems structure. When a simp theorem is added to a LocalRuleSet, it is stored in this first SimpTheorems structure.

• simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs)

  The simprocs used by the builtin norm simp rule.

• simprocsArrayNonempty : 0 < self.simprocsArray.size

  The simprocs array must contain at least one Simprocs structure, for the same reason as above.

• localNormSimpRules : Array LocalNormSimpRule

  FVars that were explicitly added as simp rules.

Instances For

• Aesop.instEmptyCollectionLocalRuleSet
• Aesop.instInhabitedLocalRuleSet

@[always_inline]

def Aesop.GlobalRuleSet.onBaseM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : BaseRuleSet → m (BaseRuleSet × α)) (rs : GlobalRuleSet) : m (GlobalRuleSet × α)

Equations

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

@[always_inline]

def Aesop.GlobalRuleSet.onBase {α : Type u_1} (f : BaseRuleSet → BaseRuleSet × α) (rs : GlobalRuleSet) : GlobalRuleSet × α

Equations

• Aesop.GlobalRuleSet.onBase f rs = Aesop.GlobalRuleSet.onBaseM f rs

@[always_inline]

def Aesop.GlobalRuleSet.modifyBaseM {m : Type → Type u_1} [Monad m] (f : BaseRuleSet → m BaseRuleSet) (rs : GlobalRuleSet) : m GlobalRuleSet

Equations

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

@[always_inline]

def Aesop.GlobalRuleSet.modifyBase (f : BaseRuleSet → BaseRuleSet) (rs : GlobalRuleSet) : GlobalRuleSet

Equations

• Aesop.GlobalRuleSet.modifyBase f rs = Aesop.GlobalRuleSet.modifyBaseM f rs

@[always_inline]

def Aesop.LocalRuleSet.onBaseM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : BaseRuleSet → m (BaseRuleSet × α)) (rs : LocalRuleSet) : m (LocalRuleSet × α)

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.onBase {α : Type u_1} (f : BaseRuleSet → BaseRuleSet × α) (rs : LocalRuleSet) : LocalRuleSet × α

Equations

• Aesop.LocalRuleSet.onBase f rs = Aesop.LocalRuleSet.onBaseM f rs

def Aesop.LocalRuleSet.modifyBaseM {m : Type → Type u_1} [Monad m] (f : BaseRuleSet → m BaseRuleSet) (rs : LocalRuleSet) : m LocalRuleSet

Equations

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

def Aesop.LocalRuleSet.modifyBase (f : BaseRuleSet → BaseRuleSet) (rs : LocalRuleSet) : LocalRuleSet

Equations

• Aesop.LocalRuleSet.modifyBase f rs = Aesop.LocalRuleSet.modifyBaseM f rs

def Aesop.BaseRuleSet.trace (rs : BaseRuleSet) (traceOpt : TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.GlobalRuleSet.trace (rs : GlobalRuleSet) (traceOpt : TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.LocalRuleSet.trace (rs : LocalRuleSet) (traceOpt : TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.LocalRuleSet.trace.printSimpSetName : Lean.Name → String

Equations

• Aesop.LocalRuleSet.trace.printSimpSetName `_ = "<default>"
• Aesop.LocalRuleSet.trace.printSimpSetName x✝ = toString x✝

def Aesop.BaseRuleSet.empty : BaseRuleSet

Equations

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

instance Aesop.instEmptyCollectionBaseRuleSet : EmptyCollection BaseRuleSet

Equations

• Aesop.instEmptyCollectionBaseRuleSet = { emptyCollection := Aesop.BaseRuleSet.empty }

def Aesop.GlobalRuleSet.empty : GlobalRuleSet

Equations

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

instance Aesop.instEmptyCollectionGlobalRuleSet : EmptyCollection GlobalRuleSet

Equations

• Aesop.instEmptyCollectionGlobalRuleSet = { emptyCollection := Aesop.GlobalRuleSet.empty }

def Aesop.LocalRuleSet.empty : LocalRuleSet

Equations

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

instance Aesop.instEmptyCollectionLocalRuleSet : EmptyCollection LocalRuleSet

Equations

• Aesop.instEmptyCollectionLocalRuleSet = { emptyCollection := Aesop.LocalRuleSet.empty }

instance Aesop.instInhabitedLocalRuleSet : Inhabited LocalRuleSet

Equations

• Aesop.instInhabitedLocalRuleSet = { default := ∅ }

def Aesop.BaseRuleSet.contains (rs : BaseRuleSet) (n : RuleName) : Bool

Equations

• rs.contains n = (!Aesop.BaseRuleSet.isErased✝ rs n && match Lean.PersistentHashMap.find? rs.ruleNames n.name with | some ns => Aesop.UnorderedArraySet.contains n ns | x => false)

def Aesop.GlobalRuleSet.contains (rs : GlobalRuleSet) (n : RuleName) : Bool

Equations

• rs.contains n = (rs.contains n || n.builder == Aesop.BuilderName.simp && n.scope == Aesop.ScopeName.global && Aesop.SimpTheorems.containsDecl rs.simpTheorems n.name)

def Aesop.LocalRuleSet.containsGlobalSimpTheorem (rs : LocalRuleSet) (decl : Lean.Name) : Bool

Equations

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

def Aesop.LocalRuleSet.contains (rs : LocalRuleSet) (n : RuleName) : Bool

Equations

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

def Aesop.BaseRuleSet.merge (rs₁ rs₂ : BaseRuleSet) : BaseRuleSet

Equations

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

def Aesop.BaseRuleSet.add (rs : BaseRuleSet) (r : BaseRuleSetMember) : BaseRuleSet

Equations

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

def Aesop.BaseRuleSet.add.addRulePattern (n : RuleName) (pat? : Option RulePattern) (rs : BaseRuleSet) : BaseRuleSet

Equations

• One or more equations did not get rendered due to their size.
• Aesop.BaseRuleSet.add.addRulePattern n none rs = rs

def Aesop.LocalRuleSet.add (rs : LocalRuleSet) : LocalRuleSetMember → LocalRuleSet

Equations

• One or more equations did not get rendered due to their size.
• rs.add (Aesop.LocalRuleSetMember.global (Aesop.GlobalRuleSetMember.base m)) = Aesop.LocalRuleSet.modifyBase (fun (x : Aesop.BaseRuleSet) => x.add m) rs

def Aesop.BaseRuleSet.erase (rs : BaseRuleSet) (f : RuleFilter) : BaseRuleSet × Bool

Equations

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

def Aesop.GlobalRuleSet.erase (rs : GlobalRuleSet) (f : RuleFilter) : GlobalRuleSet × Bool

Equations

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

def Aesop.LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) : LocalRuleSet × Bool

Equations

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

def Aesop.LocalRuleSet.applicableNormalizationRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : NormRule → Bool) : BaseM (Array (IndexMatchResult NormRule))

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableNormalizationRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult NormRule))

Equations

• rs.applicableNormalizationRules fms goal = rs.applicableNormalizationRulesWith fms goal fun (x : Aesop.NormRule) => true

def Aesop.LocalRuleSet.applicableUnsafeRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : UnsafeRule → Bool) : BaseM (Array (IndexMatchResult UnsafeRule))

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableUnsafeRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult UnsafeRule))

Equations

• rs.applicableUnsafeRules fms goal = rs.applicableUnsafeRulesWith fms goal fun (x : Aesop.UnsafeRule) => true

def Aesop.LocalRuleSet.applicableSafeRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : SafeRule → Bool) : BaseM (Array (IndexMatchResult SafeRule))

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableSafeRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult SafeRule))

Equations

• rs.applicableSafeRules fms goal = rs.applicableSafeRulesWith fms goal fun (x : Aesop.SafeRule) => true

def Aesop.LocalRuleSet.applicableForwardRulesWith (rs : LocalRuleSet) (e : Lean.Expr) (include? : ForwardRule → Bool) : Lean.MetaM (Array (ForwardRule × PremiseIndex))

Equations

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

def Aesop.LocalRuleSet.applicableForwardRulesWith.mkMsg (r : ForwardRule) (i : PremiseIndex) : Lean.MessageData

Equations

• Aesop.LocalRuleSet.applicableForwardRulesWith.mkMsg r i = Lean.toMessageData "" ++ Lean.toMessageData r ++ Lean.toMessageData ", premise " ++ Lean.toMessageData i ++ Lean.toMessageData ""

@[always_inline]

def Aesop.LocalRuleSet.applicableForwardRules (rs : LocalRuleSet) (e : Lean.Expr) : Lean.MetaM (Array (ForwardRule × PremiseIndex))

Equations

• rs.applicableForwardRules e = rs.applicableForwardRulesWith e fun (x : Aesop.ForwardRule) => true

def Aesop.LocalRuleSet.constForwardRuleMatches (rs : LocalRuleSet) : Array ForwardRuleMatch

Equations

• rs.constForwardRuleMatches = rs.forwardRules.getConstRuleMatches

def Aesop.LocalRuleSet.forwardRulePatternSubstsInExpr (rs : LocalRuleSet) (e : Lean.Expr) : BaseM (Array (ForwardRule × Substitution))

Equations

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

def Aesop.LocalRuleSet.forwardRulePatternSubstsInLocalDecl (rs : LocalRuleSet) (ldecl : Lean.LocalDecl) : BaseM (Array (ForwardRule × Substitution))

Equations

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

def Aesop.LocalRuleSet.unindex (rs : LocalRuleSet) (p : RuleName → Bool) : LocalRuleSet

Equations

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

@[always_inline]

def Aesop.unindexPredicate? (options : Options') : Option (RuleName → Bool)

Equations

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

def Aesop.mkLocalRuleSet (rss : Array (GlobalRuleSet × Lean.Name × Lean.Name)) (options : Options') : Lean.CoreM LocalRuleSet

Equations

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