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.

• erased : Lean.PHashSet RuleName

  The set of rules that were erased from normRules, unsafeRules and safeRules. When we erase a rule which is present in any of these three 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 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)
• 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)
• 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.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) (goal : Lean.MVarId) (include? : NormRule → Bool) : Lean.MetaM (Array (IndexMatchResult NormRule))

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableNormalizationRules (rs : LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (IndexMatchResult NormRule))

Equations

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

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

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableUnsafeRules (rs : LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (IndexMatchResult UnsafeRule))

Equations

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

def Aesop.LocalRuleSet.applicableSafeRulesWith (rs : LocalRuleSet) (goal : Lean.MVarId) (include? : SafeRule → Bool) : Lean.MetaM (Array (IndexMatchResult (Rule SafeRuleInfo)))

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.applicableSafeRules (rs : LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (IndexMatchResult SafeRule))

Equations

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

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.