inductive Aesop.RawHyp : Type

A hypothesis that has not yet been matched against a premise, or a rule pattern substitution.

• fvarId (fvarId : Lean.FVarId) : RawHyp

  The hypothesis.

• patSubst (subst : Substitution) : RawHyp

  The rule pattern substitution.

def Aesop.instInhabitedRawHyp.default : RawHyp

@[implicit_reducible]

instance Aesop.instInhabitedRawHyp : Inhabited RawHyp

def Aesop.instBEqRawHyp.beq : RawHyp → RawHyp → Bool

@[implicit_reducible]

instance Aesop.instBEqRawHyp : BEq RawHyp

@[implicit_reducible]

instance Aesop.instHashableRawHyp : Hashable RawHyp

def Aesop.instHashableRawHyp.hash : RawHyp → UInt64

@[implicit_reducible]

instance Aesop.instToMessageDataRawHyp : Lean.ToMessageData RawHyp

structure Aesop.Hyp : Type

A hypothesis that was matched against a premise, or a rule pattern substitution.

• fvarId? : Option Lean.FVarId

  The hypothesis, or none if this is a rule pattern substitution.

• subst : Substitution

  The substitution that results from matching the hypothesis against a premise or that was derived from the pattern.

def Aesop.instInhabitedHyp.default : Hyp

@[implicit_reducible]

instance Aesop.instInhabitedHyp : Inhabited Hyp

@[implicit_reducible]

instance Aesop.Hyp.instBEq : BEq Hyp

@[implicit_reducible]

instance Aesop.Hyp.instHashable : Hashable Hyp

def Aesop.Hyp.containsHyp (fvarId : Lean.FVarId) (h : Hyp) : Bool

Returns true if h is the hyp fvarId or is a pattern substitution containing fvarId.

def Aesop.Hyp.isPatSubst (h : Hyp) : Bool

Does this Hyp represent a pattern substitution?

structure Aesop.InstMap : Type

Partial matches associated with a particular slot instantiation. An entry s ↦ e ↦ (ms, hs) indicates that for the instantiation e of slot s, we have partial matches ms and hypotheses hs.

• map : Lean.PHashMap SlotIndex (EMap (Lean.PHashSet Match × Lean.PHashSet Hyp))

def Aesop.instInhabitedInstMap.default : InstMap

@[implicit_reducible]

instance Aesop.instInhabitedInstMap : Inhabited InstMap

@[implicit_reducible]

instance Aesop.InstMap.instEmptyCollection : EmptyCollection InstMap

@[implicit_reducible]

instance Aesop.InstMap.instToMessageData : Lean.ToMessageData InstMap

@[inline]

def Aesop.InstMap.find? (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) : Lean.MetaM (Option (Lean.PHashSet Match × Lean.PHashSet Hyp))

Returns the set of matches and hypotheses associated with a slot slot with instantiation inst.

@[inline]

def Aesop.InstMap.findD (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) : Lean.MetaM (Lean.PHashSet Match × Lean.PHashSet Hyp)

Returns the set of matches and hypotheses associated with a slot slot with instantiation inst, or (∅, ∅) if slot and inst do not have any associated matches.

def Aesop.InstMap.modify {α : Type} (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (f : Lean.PHashSet Match → Lean.PHashSet Hyp → Lean.PHashSet Match × Lean.PHashSet Hyp × α) : Lean.MetaM (InstMap × α)

Applies a transformation to the data associated with slot and inst. If there is no such data, the transformation is applied to (∅, ∅). Returns the new instantiation map and the result of f.

def Aesop.InstMap.insertHyp (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (hyp : Hyp) : Lean.MetaM (InstMap × Bool)

Inserts a hyp associated with slot slot and instantiation inst. The hyp must be a valid assignment for the slot's premise. Returns true if the hyp was not previously associated with slot and inst.

def Aesop.InstMap.insertMatchCore (imap : InstMap) (slot : SlotIndex) (inst : Lean.Expr) (m : Match) : Lean.MetaM (InstMap × Bool)

Inserts a match associated with slot slot and instantiation inst. The match's level must be slot. Returns true if the match was not previously associated with slot and inst.

def Aesop.InstMap.insertMatch (imap : InstMap) (var : PremiseIndex) (m : Match) : BaseM (InstMap × Bool)

Inserts a match. The match m is associated with the slot given by its level (i.e., the maximal slot for which m contains a hypothesis) and the instantiation of var given by the map's substitution. Returns true if the match was not previously associated with this slot and instantiation.

def Aesop.InstMap.modifyMapsForSlotsFrom (imap : InstMap) (slot : SlotIndex) (f : Lean.PHashSet Match → Lean.PHashSet Hyp → Lean.PHashSet Match × Lean.PHashSet Hyp) : InstMap

Modify the maps for slot slot and all later slots.

def Aesop.InstMap.eraseHyp (imap : InstMap) (hyp : Lean.FVarId) (slot : SlotIndex) : InstMap

Remove hyp from slot and all later slots. For each mapping s ↦ e ↦ (ms, hs) in imap, if s ≥ slot, then hyp is removed from hs and any matches containing hyp are removed from ms.

def Aesop.InstMap.erasePatSubst (imap : InstMap) (subst : Substitution) (slot : SlotIndex) : InstMap

Remove the pattern substitution subst from slot and all later slots. For each mapping s ↦ e ↦ (ms, hs) in imap, if s ≥ slot, then subst is removed from hs and any matches containing subst are removed from ms.

def Aesop.InstMap.stats (imap : InstMap) : Array ForwardInstantiationStats

Extract stats from an InstMap.

structure Aesop.VariableMap : Type

Map from variables to the matches and hypotheses of slots whose types contain the variables.

• map : Lean.PHashMap PremiseIndex InstMap

def Aesop.instInhabitedVariableMap.default : VariableMap

@[implicit_reducible]

instance Aesop.instInhabitedVariableMap : Inhabited VariableMap

@[implicit_reducible]

instance Aesop.VariableMap.instEmptyCollection : EmptyCollection VariableMap

@[implicit_reducible]

instance Aesop.VariableMap.instToMessageData : Lean.ToMessageData VariableMap

def Aesop.VariableMap.find? (vmap : VariableMap) (var : PremiseIndex) : Option InstMap

Get the InstMap associated with a variable.

def Aesop.VariableMap.find (vmap : VariableMap) (var : PremiseIndex) : InstMap

Get the InstMap associated with a variable, or an empty InstMap.

def Aesop.VariableMap.modifyM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (vmap : VariableMap) (var : PremiseIndex) (f : InstMap → m (InstMap × α)) : m (VariableMap × α)

Modify the InstMap associated to variable var. If no such InstMap exists, the function f is applied to the empty InstMap and the result is associated with var. Returns the new variable map and the result of f.

def Aesop.VariableMap.modify {α : Type u_1} (vmap : VariableMap) (var : PremiseIndex) (f : InstMap → InstMap × α) : VariableMap × α

Modify the InstMap associated to variable var. If no such InstMap exists, the function f is applied to the empty InstMap and the result is associated with var. Returns the new variable map and the result of f.

def Aesop.VariableMap.addHyp (vmap : VariableMap) (slot : Slot) (hyp : Hyp) : BaseM (VariableMap × Bool)

Add a hypothesis hyp. Precondition: hyp matches the premise of slot slot with substitution hyp.subst (and hence hyp.subst contains a mapping for each variable in slot.common). Returns true if the variable map changed.

def Aesop.VariableMap.addMatch (vmap : VariableMap) (nextSlot : Slot) (m : Match) : BaseM (VariableMap × Bool)

Add a match m. Precondition: nextSlot is the slot with index m.level + 1. Returns true if the variable map changed.

def Aesop.VariableMap.eraseHyp (vmap : VariableMap) (hyp : Lean.FVarId) (slot : SlotIndex) : VariableMap

Remove a hyp from slot and all later slots.

def Aesop.VariableMap.erasePatSubst (vmap : VariableMap) (subst : Substitution) (slot : SlotIndex) : VariableMap

Remove the pattern substitution subst from slot and all later slots.

def Aesop.VariableMap.findMatches (vmap : VariableMap) (slot : Slot) (subst : Substitution) : BaseM (Std.HashSet Match)

Find matches in slot slot - 1 whose substitutions are compatible with subst. Preconditions: slot.index is nonzero, slot.common is nonempty and each variable contained in slot.common is also contained in subst.

def Aesop.VariableMap.findHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) : BaseM (Std.HashSet Hyp)

Find hyps in slot whose substitutions are compatible with subst. Precondition: slot.common is nonempty and each variable contained in it is also contained in subst.

def Aesop.VariableMap.stats (vmap : VariableMap) : Array ForwardInstantiationStats

Extract stats from a VariableMap.

structure Aesop.ClusterState : Type

Structure representing the state of a slot cluster. Updates are performed lazily: the enqueueRawHyp method enqueues a hyp or patten subst to be added to the state, and the update method must be used to actually make the corresponding changes and potentially generate new complete matches.

• slots : Array Slot

  The cluster's slots.

• conclusionDeps : Array PremiseIndex

  The premises that appear in the rule's conclusion. These are the same for all cluster states of a rule, but are stored here for convenience.

• variableMap : VariableMap

  The variable map for this cluster.

• completeMatches : Lean.PHashSet Match

  Complete matches for this cluster.

• haveHypForEachSlot : Bool

  This flag is true if all slotQueues are potentially nonempty. Before that point, we do not add any hyps to the variable maps since the rule cannot possibly produce a complete match.

• slotQueues : Array (Array RawHyp)

  Hypotheses or pattern substitutions that have been added to the cluster state, but have not yet been added to the variableMap.

• slotQueues_size : self.slotQueues.size = self.slots.size

  There is exactly one queue for each slot.

@[implicit_reducible]

instance Aesop.ClusterState.instInhabited : Inhabited ClusterState

@[implicit_reducible]

instance Aesop.ClusterState.instToMessageData : Lean.ToMessageData ClusterState

@[always_inline]

def Aesop.ClusterState.slot! (cs : ClusterState) (slot : SlotIndex) : Slot

Get the slot with the given index. Panic if the index is invalid.

def Aesop.ClusterState.findSlot? (cs : ClusterState) (i : PremiseIndex) : Option Slot

Get the slot with the given premise index.

def Aesop.ClusterState.matchPremise? (premises : Array Lean.MVarId) (lmvarIds : Array Lean.LMVarId) (cs : ClusterState) (slot : SlotIndex) (hyp : Lean.FVarId) : BaseM (Option Substitution)

Match hypothesis hyp against the slot with index slot in cs (which must be a valid index).

structure Aesop.ClusterState.AddM.Context : Type

Context for the AddM monad.

• premiseMVars : Array Lean.MVarId

  Metavariables for the premises of the rule for which a hyp or match is being added. When adding hyps, they are unified with these metavariables.

• premiseLMVars : Array Lean.LMVarId

  Metavariables for level parameters appearing in the rule's premises.

@[reducible, inline]

abbrev Aesop.ClusterState.AddM (α : Type) : Type

A monad for operations that add hyps or matches to a cluster state. The monad's state is an array of complete matches discovered while adding hyps/matches.

def Aesop.ClusterState.AddM.run {α : Type} (premiseMVars : Array Lean.MVarId) (premiseLMVars : Array Lean.LMVarId) (x : AddM α) : BaseM (α × Array Match)

Run an AddM action.

partial def Aesop.ClusterState.addMatch (cs : ClusterState) (m : Match) : AddM ClusterState

Add a match to the cluster state.

partial def Aesop.ClusterState.addHyp (cs : ClusterState) (slot : Slot) (h : Hyp) : AddM ClusterState

Add a hypothesis to the cluster state. hyp.subst must be the substitution that results from applying h to slot.

partial def Aesop.ClusterState.addRawHyp (h : RawHyp) (slot : Slot) (cs : ClusterState) : AddM ClusterState

Add a hypothesis or pattern substitution to the cluster state.

partial def Aesop.ClusterState.addQueuedRawHyps (slot : Slot) (cs : ClusterState) : AddM ClusterState

Insert the raw hyps from slot's queue into the variable map.

def Aesop.ClusterState.enqueueRawHyp (h : RawHyp) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Add a hypothesis or pattern substitution to the queue for its slot.

def Aesop.ClusterState.eraseEnqueuedRawHyp (h : RawHyp) (slot : Slot) (cs : ClusterState) : ClusterState

Erase a RawHyp from the slot queue of the given slot.

def Aesop.ClusterState.eraseHyp (h : Lean.FVarId) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Erase a hypothesis from the cluster state's variable map.

def Aesop.ClusterState.erasePatSubst (subst : Substitution) (pi : PremiseIndex) (cs : ClusterState) : ClusterState

Erase a pattern substitution from the cluster state.

def Aesop.ClusterState.update (cs : ClusterState) : AddM ClusterState

Update a cluster change, adding any enqueued hypotheses. This may result in new complete matches.

def Aesop.ClusterState.stats (cs : ClusterState) : ForwardClusterStateStats

Extract stats from a ClusterState.

inductive Aesop.PatSubstSource : Type

The source of a pattern substitution. The same substitution can have multiple sources.

• hyp (fvarId : Lean.FVarId) : PatSubstSource

  The pattern substitution came from the given hypothesis.

• target : PatSubstSource

  The pattern substitution came from the goal's target.

def Aesop.instInhabitedPatSubstSource.default : PatSubstSource

@[implicit_reducible]

instance Aesop.instInhabitedPatSubstSource : Inhabited PatSubstSource

def Aesop.instHashablePatSubstSource.hash : PatSubstSource → UInt64

@[implicit_reducible]

instance Aesop.instHashablePatSubstSource : Hashable PatSubstSource

@[implicit_reducible]

instance Aesop.instBEqPatSubstSource : BEq PatSubstSource

def Aesop.instBEqPatSubstSource.beq : PatSubstSource → PatSubstSource → Bool

structure Aesop.RuleState : Type

Forward state for one rule. Updates are lazy: when adding a hyp or pattern subst to the rule, it is initially only enqueued in the cluster states. The update method must be called to actually make the corresponding changes, which result in new complete matches for the rule.

• rule : ForwardRule

  The rule to which this state belongs.

• clusterStates : Array ClusterState

  States for each of the rule's slot clusters.

• patSubstSources : Lean.PHashMap Substitution (Lean.PHashSet PatSubstSource)

  The sources of all pattern substitutions present in the clusterStates. Invariant: each pattern substitution in the cluster states is associated with a nonempty set.

@[implicit_reducible]

instance Aesop.instInhabitedRuleState : Inhabited RuleState

def Aesop.instInhabitedRuleState.default : RuleState

@[implicit_reducible]

instance Aesop.instToMessageDataRuleState : Lean.ToMessageData RuleState

def Aesop.ForwardRule.initialRuleState (r : ForwardRule) : RuleState

The initial (empty) rule state for a given forward rule.

def Aesop.RuleState.enqueueRawHyp (hyp : RawHyp) (pi : PremiseIndex) (rs : RuleState) : RuleState

Add a hypothesis or pattern substitution to the rule state. The hypothesis's type does not necessarily need to match the given premise. If it does not, this is detected by update and the hyp is not added.

def Aesop.RuleState.erasePatSubst (subst : Substitution) (source : PatSubstSource) (rs : RuleState) : RuleState

Erase a pattern substitution that was obtained from the given source.

def Aesop.RuleState.eraseHyp (h : Lean.FVarId) (pi : PremiseIndex) (rs : RuleState) : RuleState

Erase a hypothesis from the rule state.

def Aesop.RuleState.update (goal : Lean.MVarId) (rs : RuleState) : BaseM (RuleState × Array ForwardRuleMatch)

Add any enqueued hyps to the rule state, potentially generating new complete matches in the process.

def Aesop.RuleState.stats (rs : RuleState) : ForwardRuleStateStats

Extract stats from a RuleState.

structure Aesop.ForwardState : Type

State representing the non-complete matches of a given set of forward rules in a given local context.

• ruleStates : Lean.PHashMap RuleName RuleState

  Map from each rule's name to its RuleState

• hyps : Lean.PHashMap Lean.FVarId (Lean.PArray (RuleName × PremiseIndex))

  A map from hypotheses to the rules and premises that they matched against when they were initially added to the rule state. Invariant: the rule states in which a hypothesis h appear are exactly those identified by the rule names in hyps[h]. Furthermore, h only appears in slots with premise indices greater than or equal to those in hyps[h].

• patSubsts : Lean.PHashMap PatSubstSource (Lean.PArray (RuleName × Substitution))

  The pattern substitutions present in the rule states. Invariant: patSubsts maps the source s to a rule name r and pattern substitution i iff the rule state of r contains i with source s.

@[implicit_reducible]

instance Aesop.instInhabitedForwardState : Inhabited ForwardState

def Aesop.instInhabitedForwardState.default : ForwardState

@[implicit_reducible]

instance Aesop.ForwardState.instEmptyCollection : EmptyCollection ForwardState

@[implicit_reducible]

instance Aesop.ForwardState.instToMessageData : Lean.ToMessageData ForwardState

def Aesop.ForwardState.enqueueHyp (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : ForwardState

Add a hypothesis to the forward state. If fs represents a local context lctx, then fs.addHyp h ms represents lctx with h added. ms must overapproximate the rules for which h may unify with a maximal premise.

def Aesop.ForwardState.enqueuePatSubst (r : ForwardRule) (patSubst : Substitution) (source : PatSubstSource) (fs : ForwardState) : ForwardState

Add a pattern substitution to the forward state.

def Aesop.ForwardState.enqueuePatSubsts (source : PatSubstSource) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Add multiple pattern substitutions to the forward state.

def Aesop.ForwardState.enqueueHypWithPatSubsts (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Add a hypothesis and to the forward state, along with any rule pattern substitutions obtained from it.

def Aesop.ForwardState.erasePatSubsts (source : PatSubstSource) (fs : ForwardState) : ForwardState

Erase pattern substitutions with the given source.

def Aesop.ForwardState.eraseHyp (h : Lean.FVarId) (fs : ForwardState) : ForwardState

Remove a hypothesis from the forward state. If fs represents a local context lctx, then fs.eraseHyp h represents lctx with h removed.

def Aesop.ForwardState.eraseTargetPatSubsts (fs : ForwardState) : ForwardState

Erase all pattern substitutions whose source is the target.

def Aesop.ForwardState.enqueueTargetPatSubsts (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : ForwardState

Update the pattern substitutions after the goal's target changed. goal is the new goal. newPatSubsts are the new target's pattern substitutions.

def Aesop.ForwardState.update (goal : Lean.MVarId) (fs : ForwardState) (phase? : Option PhaseName) : BaseM (ForwardState × Array ForwardRuleMatch)

Update the forward state. This applies any previously enqueued changes to all rule states, potentially generating new complete matches in the process. If a phase is given, only rules from that phase are updated.

def Aesop.ForwardState.stats (fs : ForwardState) : ForwardStateStats

Extract stats from a ForwardState.