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.

instance Aesop.instInhabitedRawHyp : Inhabited RawHyp

instance Aesop.instBEqRawHyp : BEq RawHyp

instance Aesop.instHashableRawHyp : Hashable 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.

instance Aesop.instInhabitedHyp : Inhabited Hyp

instance Aesop.Hyp.instBEq : BEq Hyp

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 (Lean.PHashMap RPINF (Lean.PHashSet Match × Lean.PHashSet Hyp))

instance Aesop.instInhabitedInstMap : Inhabited InstMap

instance Aesop.InstMap.instEmptyCollection : EmptyCollection InstMap

instance Aesop.InstMap.instToMessageData : Lean.ToMessageData InstMap

@[inline]

def Aesop.InstMap.find? (imap : InstMap) (slot : SlotIndex) (inst : RPINF) : 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 : RPINF) : 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 u_1} (imap : InstMap) (slot : SlotIndex) (inst : RPINF) (f : Lean.PHashSet Match → Lean.PHashSet Hyp → Lean.PHashSet Match × Lean.PHashSet Hyp × α) : InstMap × α

Applies a transfomation to the data associated to 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 : RPINF) (hyp : Hyp) : 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 : RPINF) (m : Match) : 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) : 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.

structure Aesop.VariableMap : Type

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

• map : Lean.PHashMap PremiseIndex InstMap

instance Aesop.instInhabitedVariableMap : Inhabited VariableMap

instance Aesop.VariableMap.instEmptyCollection : EmptyCollection VariableMap

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.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) : 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) : 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) : 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.findMatches.prevSlotMatches (vmap : VariableMap) (slot : Slot) (subst : Substitution) (var : PremiseIndex) : Lean.PHashSet Match

def Aesop.VariableMap.findHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) : 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.findHyps.slotHyps (vmap : VariableMap) (slot : Slot) (subst : Substitution) (var : PremiseIndex) : Lean.PHashSet Hyp

structure Aesop.ClusterState : Type

Structure representing the state of a slot cluster.

• 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.

• addHypsLazily : Bool

  When this flag is true, hyps are added to the slotQueues rather than the variableMap. This is an optimisation that avoids performing unifications until a rule can potentially generate a complete match. More precisely:

  • addHypsLazily is initially set to true.
  • While addHypsLazily is true, hyps are added to (and deleted from) the slotQueues and are not added to the variableMap. Once an addition causes all slot queues to have at least one element, addHypsLazily is permanently set to false and hyps for slot 0 are added to the variableMap.
  • While addHypsLazily is false:
    • Hyps for slot i are added directly to the variable maps if i = 0 or the slot i - 1 has matches. Otherwise they are added to the slot queue for i. (More precisely, we only track whether slot i - 1 has had matches at some point. This allows us to ignore deletions.)
    • The insertion of a match into slot i causes all hyps at slot i + 1 to be moved from the slot queue into the variableMap.
• 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.

• slotMaybeHasMatches : Array Bool

  The ith element of this array is true if a match was at some point added to slot i.

• slotMaybeHasMatches_size : self.slotMaybeHasMatches.size = self.slots.size

  There is exactly one boolean for each slot.

instance Aesop.ClusterState.instInhabited : Inhabited ClusterState

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).

def Aesop.ClusterState.matchPremise?.updateSubst (hyp : Lean.FVarId) (premises : Array Lean.MVarId) (var : PremiseIndex) (subst : Substitution) : BaseM Substitution

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. Returns the new cluster state and any new complete matches for this cluster.

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.addRawHypCore (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) (slot : Slot) (cs : ClusterState) : ClusterState

Add a hypothesis or pattern substitution to the queue for its slot. If afterwards each slot queue contains at least one element, then the returned cluster state cs has cs.addHypsLazily = false.

def Aesop.ClusterState.addRawHyp (cs : ClusterState) (i : PremiseIndex) (h : RawHyp) : AddM ClusterState

Add a hypothesis or pattern substitution to the cluster state. If a hypothesis is given and its type does not match the premise corresponding to slot, it is not added.

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.

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.

instance Aesop.instInhabitedPatSubstSource : Inhabited PatSubstSource

instance Aesop.instHashablePatSubstSource : Hashable PatSubstSource

instance Aesop.instBEqPatSubstSource : BEq PatSubstSource

structure Aesop.RuleState : Type

Forward state for one 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.

instance Aesop.instInhabitedRuleState : Inhabited RuleState

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.addRawHyp (goal : Lean.MVarId) (h : RawHyp) (pi : PremiseIndex) (rs : RuleState) : BaseM (RuleState × Array CompleteMatch)

Add a hypothesis or pattern substitution to the rule state. Returns the new rule state and any newly completed matches. If a hypothesis is given and it does not match premise pi, nothing happens.

def Aesop.RuleState.addRawHyp.getCompleteMatches (clusterStates : Array ClusterState) (clusterIdx : Nat) (newCompleteMatches : Array Match) : Array CompleteMatch

def Aesop.RuleState.addRawHyp.addMatches (completeMatches : Array CompleteMatch) (clusterMatches : Array Match) : Array CompleteMatch

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.

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.

• hypTypes : Lean.PHashSet RPINF

  Normalised types of all non-implementation detail hypotheses in the local context.

instance Aesop.instInhabitedForwardState : Inhabited ForwardState

instance Aesop.ForwardState.instEmptyCollection : EmptyCollection ForwardState

instance Aesop.ForwardState.instToMessageData : Lean.ToMessageData ForwardState

def Aesop.ForwardState.addHypCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.addHyp (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.addPatSubstCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (r : ForwardRule) (patSubst : Substitution) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add a pattern substitution to the forward state.

def Aesop.ForwardState.addPatSubst (goal : Lean.MVarId) (r : ForwardRule) (patSubst : Substitution) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add a pattern substitution to the forward state.

def Aesop.ForwardState.addPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add multiple pattern substitutions to the forward state.

def Aesop.ForwardState.addPatSubsts (goal : Lean.MVarId) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

Add multiple pattern substitutions to the forward state.

def Aesop.ForwardState.addHypWithPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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

def Aesop.ForwardState.addHypWithPatSubsts (goal : Lean.MVarId) (h : Lean.FVarId) (ms : Array (ForwardRule × PremiseIndex)) (patSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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) (type : RPINF) (fs : ForwardState) : ForwardState

Remove a hypothesis from the forward state. If fs represents a local context lctx, then fs.eraseHyp h ms represents lctx with h removed. type must be the normalised type of h. ms must contain all rules for which h may unify with a maximal premise.

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

Erase all pattern substitutions whose source is the target.

def Aesop.ForwardState.updateTargetPatSubstsCore (ruleMatches : Array ForwardRuleMatch) (goal : Lean.MVarId) (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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.updateTargetPatSubsts (goal : Lean.MVarId) (newPatSubsts : Array (ForwardRule × Substitution)) (fs : ForwardState) : BaseM (ForwardState × Array ForwardRuleMatch)

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