## Node IDs #

source
structure Aesop.GoalId :
Type

- toNat : Nat

Instances For

source
def Aesop.instInhabitedGoalId.default :
GoalId
Equations

- Aesop.instInhabitedGoalId.default = { toNat := default }

Instances For

source
instance Aesop.instInhabitedGoalId :
Inhabited GoalId
Equations

- Aesop.instInhabitedGoalId = { default := Aesop.instInhabitedGoalId.default }

source
def Aesop.instDecidableEqGoalId.decEq (x✝ x✝¹ : GoalId) :
Decidable (x✝ = x✝¹)
Equations

- Aesop.instDecidableEqGoalId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source
instance Aesop.instDecidableEqGoalId :
DecidableEq GoalId
Equations

- Aesop.instDecidableEqGoalId = Aesop.instDecidableEqGoalId.decEq

source
def Aesop.GoalId.zero :
GoalId
Equations

- Aesop.GoalId.zero = { toNat := 0 }

Instances For

source
def Aesop.GoalId.one :
GoalId
Equations

- Aesop.GoalId.one = { toNat := 1 }

Instances For

source
def Aesop.GoalId.succ :
GoalId → GoalId
Equations

- { toNat := n }.succ = { toNat := n + 1 }

Instances For

source
def Aesop.GoalId.dummy :
GoalId
Equations

- Aesop.GoalId.dummy = { toNat := 1000000000000000 }

Instances For

source
instance Aesop.GoalId.instLT :
LT GoalId
Equations

- Aesop.GoalId.instLT = { lt := fun (n m : Aesop.GoalId) => n.toNat < m.toNat }

source
instance Aesop.GoalId.instDecidableRelLt :
DecidableRel fun (x1 x2 : GoalId) => x1 < x2
Equations

- n.instDecidableRelLt m = inferInstanceAs (Decidable (n.toNat < m.toNat))

source
instance Aesop.GoalId.instToString :
ToString GoalId
Equations

- Aesop.GoalId.instToString = { toString := fun (n : Aesop.GoalId) => toString n.toNat }

source
instance Aesop.GoalId.instHashable :
Hashable GoalId
Equations

- Aesop.GoalId.instHashable = { hash := fun (n : Aesop.GoalId) => hash n.toNat }

## Rule Application IDs #

source
structure Aesop.RappId :
Type

- toNat : Nat

Instances For

source
def Aesop.instInhabitedRappId.default :
RappId
Equations

- Aesop.instInhabitedRappId.default = { toNat := default }

Instances For

source
instance Aesop.instInhabitedRappId :
Inhabited RappId
Equations

- Aesop.instInhabitedRappId = { default := Aesop.instInhabitedRappId.default }

source
def Aesop.instDecidableEqRappId.decEq (x✝ x✝¹ : RappId) :
Decidable (x✝ = x✝¹)
Equations

- Aesop.instDecidableEqRappId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source
instance Aesop.instDecidableEqRappId :
DecidableEq RappId
Equations

- Aesop.instDecidableEqRappId = Aesop.instDecidableEqRappId.decEq

source
def Aesop.RappId.zero :
RappId
Equations

- Aesop.RappId.zero = { toNat := 0 }

Instances For

source
def Aesop.RappId.succ :
RappId → RappId
Equations

- { toNat := n }.succ = { toNat := n + 1 }

Instances For

source
def Aesop.RappId.one :
RappId
Equations

- Aesop.RappId.one = { toNat := 1 }

Instances For

source
def Aesop.RappId.dummy :
RappId
Equations

- Aesop.RappId.dummy = { toNat := 1000000000000000 }

Instances For

source
instance Aesop.RappId.instLT :
LT RappId
Equations

- Aesop.RappId.instLT = { lt := fun (n m : Aesop.RappId) => n.toNat < m.toNat }

source
instance Aesop.RappId.instDecidableRelLt :
DecidableRel fun (x1 x2 : RappId) => x1 < x2
Equations

- n.instDecidableRelLt m = inferInstanceAs (Decidable (n.toNat < m.toNat))

source
instance Aesop.RappId.instToString :
ToString RappId
Equations

- Aesop.RappId.instToString = { toString := fun (n : Aesop.RappId) => toString n.toNat }

source
instance Aesop.RappId.instHashable :
Hashable RappId
Equations

- Aesop.RappId.instHashable = { hash := fun (n : Aesop.RappId) => hash n.toNat }

## Iterations #

source
def Aesop.Iteration :
Type
Equations

- Aesop.Iteration = Nat

Instances For

source
instance Aesop.instInhabitedIteration :
Inhabited Iteration
Equations

- Aesop.instInhabitedIteration = instInhabitedNat

source
@[inline]
def Aesop.Iteration.one :
Iteration
Equations

- Aesop.Iteration.one = Aesop.Iteration.ofNat✝ 1

Instances For

source
@[inline]
def Aesop.Iteration.succ (i : Iteration) :
Iteration
Equations

- i.succ = Aesop.Iteration.ofNat✝ (Aesop.Iteration.toNat✝ i + 1)

Instances For

source
def Aesop.Iteration.none :
Iteration
Equations

- Aesop.Iteration.none = Aesop.Iteration.ofNat✝ 0

Instances For

source
instance Aesop.Iteration.instDecidableEq :
DecidableEq Iteration
Equations

- Aesop.Iteration.instDecidableEq = inferInstanceAs (DecidableEq Nat)

source
instance Aesop.Iteration.instToString :
ToString Iteration
Equations

- Aesop.Iteration.instToString = inferInstanceAs (ToString Nat)

source
instance Aesop.Iteration.instLT :
LT Iteration
Equations

- Aesop.Iteration.instLT = inferInstanceAs (LT Nat)

source
instance Aesop.Iteration.instLE :
LE Iteration
Equations

- Aesop.Iteration.instLE = inferInstanceAs (LE Nat)

source
instance Aesop.Iteration.instDecidableRelLt :
DecidableRel fun (x1 x2 : Iteration) => x1 < x2
Equations

- Aesop.Iteration.instDecidableRelLt = inferInstanceAs (DecidableRel fun (x1 x2 : Nat) => x1 < x2)

source
instance Aesop.Iteration.instDecidableRelLe :
DecidableRel fun (x1 x2 : Iteration) => x1 ≤ x2
Equations

- Aesop.Iteration.instDecidableRelLe = inferInstanceAs (DecidableRel fun (x1 x2 : Nat) => x1 ≤ x2)

## The Tree #

source
inductive Aesop.NodeState :
Type

At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:

- `proven`: the node is proven.
- `unprovable`: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.
- `unknown`: neither of the above.

Every node starts in the `unknown` state and may later become either `proven` or `unprovable`. After this, the state does not change any more.

- unknown : NodeState
- proven : NodeState
- unprovable : NodeState

Instances For

source
def Aesop.instInhabitedNodeState.default :
NodeState
Equations

- Aesop.instInhabitedNodeState.default = Aesop.NodeState.unknown

Instances For

source
instance Aesop.instInhabitedNodeState :
Inhabited NodeState
Equations

- Aesop.instInhabitedNodeState = { default := Aesop.instInhabitedNodeState.default }

source
instance Aesop.instBEqNodeState :
BEq NodeState
Equations

- Aesop.instBEqNodeState = { beq := Aesop.instBEqNodeState.beq }

source
def Aesop.instBEqNodeState.beq :
NodeState → NodeState → Bool
Equations

- Aesop.instBEqNodeState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance Aesop.NodeState.instToString :
ToString NodeState
Equations

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

source
def Aesop.NodeState.isUnknown :
NodeState → Bool
Equations

- Aesop.NodeState.unknown.isUnknown = true
- x✝.isUnknown = false

Instances For

source
def Aesop.NodeState.isProven :
NodeState → Bool
Equations

- Aesop.NodeState.proven.isProven = true
- x✝.isProven = false

Instances For

source
def Aesop.NodeState.isUnprovable :
NodeState → Bool
Equations

- Aesop.NodeState.unprovable.isUnprovable = true
- x✝.isUnprovable = false

Instances For

source
def Aesop.NodeState.isIrrelevant :
NodeState → Bool
Equations

- Aesop.NodeState.proven.isIrrelevant = true
- Aesop.NodeState.unprovable.isIrrelevant = true
- Aesop.NodeState.unknown.isIrrelevant = false

Instances For

source
def Aesop.NodeState.toEmoji :
NodeState → String
Equations

- Aesop.NodeState.proven.toEmoji = Aesop.nodeProvedEmoji
- Aesop.NodeState.unprovable.toEmoji = Aesop.nodeUnprovableEmoji
- Aesop.NodeState.unknown.toEmoji = Aesop.nodeUnknownEmoji

Instances For

source
inductive Aesop.GoalState :
Type

A refinement of the `NodeState`, distinguishing between goals proven during normalisation and goals proven by a child rule application.

- unknown : GoalState
- provenByRuleApplication : GoalState
- provenByNormalization : GoalState
- unprovable : GoalState

Instances For

source
instance Aesop.instInhabitedGoalState :
Inhabited GoalState
Equations

- Aesop.instInhabitedGoalState = { default := Aesop.instInhabitedGoalState.default }

source
def Aesop.instInhabitedGoalState.default :
GoalState
Equations

- Aesop.instInhabitedGoalState.default = Aesop.GoalState.unknown

Instances For

source
def Aesop.instBEqGoalState.beq :
GoalState → GoalState → Bool
Equations

- Aesop.instBEqGoalState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance Aesop.instBEqGoalState :
BEq GoalState
Equations

- Aesop.instBEqGoalState = { beq := Aesop.instBEqGoalState.beq }

source
instance Aesop.GoalState.instToString :
ToString GoalState
Equations

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

source
def Aesop.GoalState.isProvenByRuleApplication :
GoalState → Bool
Equations

- Aesop.GoalState.provenByRuleApplication.isProvenByRuleApplication = true
- x✝.isProvenByRuleApplication = false

Instances For

source
def Aesop.GoalState.isProvenByNormalization :
GoalState → Bool
Equations

- Aesop.GoalState.provenByNormalization.isProvenByNormalization = true
- x✝.isProvenByNormalization = false

Instances For

source
def Aesop.GoalState.isProven :
GoalState → Bool
Equations

- Aesop.GoalState.provenByRuleApplication.isProven = true
- Aesop.GoalState.provenByNormalization.isProven = true
- x✝.isProven = false

Instances For

source
def Aesop.GoalState.isUnprovable :
GoalState → Bool
Equations

- Aesop.GoalState.unprovable.isUnprovable = true
- x✝.isUnprovable = false

Instances For

source
def Aesop.GoalState.isUnknown :
GoalState → Bool
Equations

- Aesop.GoalState.unknown.isUnknown = true
- x✝.isUnknown = false

Instances For

source
def Aesop.GoalState.toNodeState :
GoalState → NodeState
Equations

- Aesop.GoalState.unknown.toNodeState = Aesop.NodeState.unknown
- Aesop.GoalState.provenByRuleApplication.toNodeState = Aesop.NodeState.proven
- Aesop.GoalState.provenByNormalization.toNodeState = Aesop.NodeState.proven
- Aesop.GoalState.unprovable.toNodeState = Aesop.NodeState.unprovable

Instances For

source
def Aesop.GoalState.isIrrelevant (s : GoalState) :
Bool
Equations

- s.isIrrelevant = s.toNodeState.isIrrelevant

Instances For

source
def Aesop.GoalState.toEmoji :
GoalState → String
Equations

- Aesop.GoalState.unknown.toEmoji = Aesop.nodeUnknownEmoji
- Aesop.GoalState.provenByRuleApplication.toEmoji = Aesop.nodeProvedEmoji
- Aesop.GoalState.provenByNormalization.toEmoji = Aesop.nodeProvedEmoji
- Aesop.GoalState.unprovable.toEmoji = Aesop.nodeUnprovableEmoji

Instances For

source
inductive Aesop.NormalizationState :
Type

- notNormal : NormalizationState
- normal (postGoal : Lean.MVarId) (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState
- provenByNormalization (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState

Instances For

source
def Aesop.instInhabitedNormalizationState.default :
NormalizationState
Equations

- Aesop.instInhabitedNormalizationState.default = Aesop.NormalizationState.notNormal

Instances For

source
instance Aesop.instInhabitedNormalizationState :
Inhabited NormalizationState
Equations

- Aesop.instInhabitedNormalizationState = { default := Aesop.instInhabitedNormalizationState.default }

source
def Aesop.NormalizationState.isNormal :
NormalizationState → Bool
Equations

- Aesop.NormalizationState.notNormal.isNormal = false
- (Aesop.NormalizationState.normal postGoal postState script).isNormal = true
- (Aesop.NormalizationState.provenByNormalization postState script).isNormal = true

Instances For

source
def Aesop.NormalizationState.isProvenByNormalization :
NormalizationState → Bool
Equations

- Aesop.NormalizationState.notNormal.isProvenByNormalization = false
- (Aesop.NormalizationState.normal postGoal postState script).isProvenByNormalization = false
- (Aesop.NormalizationState.provenByNormalization postState script).isProvenByNormalization = true

Instances For

source
def Aesop.NormalizationState.normalizedGoal? :
NormalizationState → Option Lean.MVarId
Equations

- Aesop.NormalizationState.notNormal.normalizedGoal? = none
- (Aesop.NormalizationState.provenByNormalization postState script).normalizedGoal? = none
- (Aesop.NormalizationState.normal g postState script).normalizedGoal? = some g

Instances For

source
inductive Aesop.GoalOrigin :
Type

A goal `G` can be added to the tree for three reasons:

1. `G` was produced by its parent rule as a subgoal. This is the most common reason.
2. `G` was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of which `G` is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal `1` is copied to goal `2` and goal `2` is copied to goal `3`, they are all part of the equivalence class with representative `1`.

- subgoal : GoalOrigin
- copied («from» rep : GoalId) : GoalOrigin
- droppedMVar : GoalOrigin

Instances For

source
instance Aesop.instInhabitedGoalOrigin :
Inhabited GoalOrigin
Equations

- Aesop.instInhabitedGoalOrigin = { default := Aesop.instInhabitedGoalOrigin.default }

source
def Aesop.instInhabitedGoalOrigin.default :
GoalOrigin
Equations

- Aesop.instInhabitedGoalOrigin.default = Aesop.GoalOrigin.subgoal

Instances For

source
def Aesop.GoalOrigin.originalGoalId? :
GoalOrigin → Option GoalId
Equations

- (Aesop.GoalOrigin.copied «from» rep).originalGoalId? = some rep
- x✝.originalGoalId? = none

Instances For

source
def Aesop.GoalOrigin.toString :
GoalOrigin → String
Equations

- Aesop.GoalOrigin.subgoal.toString = "subgoal"
- (Aesop.GoalOrigin.copied «from» rep).toString = toString "copy of " ++ toString «from» ++ toString ", originally " ++ toString rep
- Aesop.GoalOrigin.droppedMVar.toString = "dropped mvar"

Instances For

source
structure Aesop.GoalData (Rapp MVarCluster : Type) :
Type

- id : GoalId
- parent : IO.Ref MVarCluster
- children : Array (IO.Ref Rapp)
- origin : GoalOrigin
- depth : Nat
- state : GoalState
- isIrrelevant : Bool
- isForcedUnprovable : Bool
- preNormGoal : Lean.MVarId
- normalizationState : NormalizationState
- mvars : UnorderedArraySet Lean.MVarId
- forwardState : ForwardState

  The forward state reflects the local context of the current goal. Before normalisation, this is the local context of `preNormGoal`; after normalisation, it is the local context of the post-normalisation goal (unless normalisation solved the goal, in which case the forward state is undetermined).

- forwardRuleMatches : ForwardRuleMatches

  Complete matches of forward rules for the current goal (in the same sense as above).

- successProbability : Percent
- addedInIteration : Iteration
- lastExpandedInIteration : Iteration
- unsafeRulesSelected : Bool
- unsafeQueue : UnsafeQueue
- failedRapps : Array RegularRule

Instances For

source
instance Aesop.instNonemptyGoalData {Rapp✝ MVarCluster✝ : Type} [Nonempty MVarCluster✝] :
Nonempty (GoalData Rapp✝ MVarCluster✝)
source
structure Aesop.MVarClusterData (Goal Rapp : Type) :
Type

- parent? : Option (IO.Ref Rapp)
- goals : Array (IO.Ref Goal)
- isIrrelevant : Bool
- state : NodeState

Instances For

source
def Aesop.instInhabitedMVarClusterData.default {a✝ a✝¹ : Type} :
MVarClusterData a✝ a✝¹
Equations

- Aesop.instInhabitedMVarClusterData.default = { parent? := default, goals := default, isIrrelevant := default, state := default }

Instances For

source
instance Aesop.instInhabitedMVarClusterData {a✝ a✝¹ : Type} :
Inhabited (MVarClusterData a✝ a✝¹)
Equations

- Aesop.instInhabitedMVarClusterData = { default := Aesop.instInhabitedMVarClusterData.default }

source
structure Aesop.RappData (Goal MVarCluster : Type) :
Type

- id : RappId
- parent : IO.Ref Goal
- children : Array (IO.Ref MVarCluster)
- state : NodeState
- isIrrelevant : Bool
- appliedRule : RegularRule
- scriptSteps? : Option (Array Script.LazyStep)
- originalSubgoals : Array Lean.MVarId
- successProbability : Percent
- metaState : Lean.Meta.SavedState
- introducedMVars : UnorderedArraySet Lean.MVarId
- assignedMVars : UnorderedArraySet Lean.MVarId

Instances For

source
instance Aesop.instNonemptyRappData {Goal✝ : Type} [Nonempty Goal✝] {MVarCluster✝ : Type} :
Nonempty (RappData Goal✝ MVarCluster✝)
source
unsafe inductive Aesop.GoalUnsafe :
Type

- mk (d : GoalData RappUnsafe MVarClusterUnsafe) : GoalUnsafe

Instances For

source
unsafe inductive Aesop.MVarClusterUnsafe :
Type

- mk (d : MVarClusterData GoalUnsafe RappUnsafe) : MVarClusterUnsafe

Instances For

source
unsafe inductive Aesop.RappUnsafe :
Type

- mk (d : RappData GoalUnsafe MVarClusterUnsafe) : RappUnsafe

Instances For

source
structure Aesop.TreeSpec :
Type 1

- Goal : Type
- Rapp : Type
- MVarCluster : Type
- introGoal : GoalData self.Rapp self.MVarCluster → self.Goal
- elimGoal : self.Goal → GoalData self.Rapp self.MVarCluster
- introRapp : RappData self.Goal self.MVarCluster → self.Rapp
- elimRapp : self.Rapp → RappData self.Goal self.MVarCluster
- introMVarCluster : MVarClusterData self.Goal self.Rapp → self.MVarCluster
- elimMVarCluster : self.MVarCluster → MVarClusterData self.Goal self.Rapp

Instances For

source
instance Aesop.instNonemptyTreeSpec :
Nonempty TreeSpec
source
unsafe def Aesop.treeImpl :
TreeSpec
Equations

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

Instances For

source
@[implemented_by Aesop.treeImpl]
opaque Aesop.tree :
TreeSpec
source
def Aesop.Goal :
Type
Equations

- Aesop.Goal = Aesop.tree.Goal

Instances For

source
def Aesop.Rapp :
Type
Equations

- Aesop.Rapp = Aesop.tree.Rapp

Instances For

source
def Aesop.MVarCluster :
Type
Equations

- Aesop.MVarCluster = Aesop.tree.MVarCluster

Instances For

source
@[reducible, inline]
abbrev Aesop.GoalRef :
Type
Equations

- Aesop.GoalRef = IO.Ref Aesop.Goal

Instances For

source
@[reducible, inline]
abbrev Aesop.RappRef :
Type
Equations

- Aesop.RappRef = IO.Ref Aesop.Rapp

Instances For

source
@[reducible, inline]
abbrev Aesop.MVarClusterRef :
Type
Equations

- Aesop.MVarClusterRef = IO.Ref Aesop.MVarCluster

Instances For

source
@[inline]
def Aesop.MVarCluster.mk :
MVarClusterData Goal Rapp → MVarCluster
Equations

- Aesop.MVarCluster.mk = Aesop.tree.introMVarCluster

Instances For

source
instance Aesop.MVarCluster.instNonempty :
Nonempty MVarCluster
source
@[inline]
def Aesop.MVarCluster.elim :
MVarCluster → MVarClusterData Goal Rapp
Equations

- Aesop.MVarCluster.elim = Aesop.tree.elimMVarCluster

Instances For

source
@[inline]
def Aesop.MVarCluster.modify (f : MVarClusterData Goal Rapp → MVarClusterData Goal Rapp) (c : MVarCluster) :
MVarCluster
Equations

- Aesop.MVarCluster.modify f c = Aesop.MVarCluster.mk (f c.elim)

Instances For

source
@[inline]
def Aesop.MVarCluster.parent? (c : MVarCluster) :
Option RappRef
Equations

- c.parent? = c.elim.parent?

Instances For

source
@[inline]
def Aesop.MVarCluster.setParent (parent? : Option RappRef) (c : MVarCluster) :
MVarCluster
Equations

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

Instances For

source
@[inline]
def Aesop.MVarCluster.goals (c : MVarCluster) :
Array GoalRef
Equations

- c.goals = c.elim.goals

Instances For

source
@[inline]
def Aesop.MVarCluster.setGoals (goals : Array GoalRef) (c : MVarCluster) :
MVarCluster
Equations

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

Instances For

source
@[inline]
def Aesop.MVarCluster.isIrrelevant (c : MVarCluster) :
Bool
Equations

- c.isIrrelevant = c.elim.isIrrelevant

Instances For

source
@[inline]
def Aesop.MVarCluster.setIsIrrelevant (isIrrelevant : Bool) (c : MVarCluster) :
MVarCluster
Equations

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

Instances For

source
@[inline]
def Aesop.MVarCluster.state (c : MVarCluster) :
NodeState
Equations

- c.state = c.elim.state

Instances For

source
@[inline]
def Aesop.MVarCluster.setState (state : NodeState) (c : MVarCluster) :
MVarCluster
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.mk :
GoalData Rapp MVarCluster → Goal
Equations

- Aesop.Goal.mk = Aesop.tree.introGoal

Instances For

source
@[inline]
def Aesop.Goal.elim :
Goal → GoalData Rapp MVarCluster
Equations

- Aesop.Goal.elim = Aesop.tree.elimGoal

Instances For

source
@[inline]
def Aesop.Goal.modify (f : GoalData Rapp MVarCluster → GoalData Rapp MVarCluster) (g : Goal) :
Goal
Equations

- Aesop.Goal.modify f g = Aesop.Goal.mk (f g.elim)

Instances For

source
@[inline]
def Aesop.Goal.id (g : Goal) :
GoalId
Equations

- g.id = g.elim.id

Instances For

source
@[inline]
def Aesop.Goal.parent (g : Goal) :
MVarClusterRef
Equations

- g.parent = g.elim.parent

Instances For

source
@[inline]
def Aesop.Goal.children (g : Goal) :
Array RappRef
Equations

- g.children = g.elim.children

Instances For

source
@[inline]
def Aesop.Goal.origin (g : Goal) :
GoalOrigin
Equations

- g.origin = g.elim.origin

Instances For

source
@[inline]
def Aesop.Goal.depth (g : Goal) :
Nat
Equations

- g.depth = g.elim.depth

Instances For

source
@[inline]
def Aesop.Goal.state (g : Goal) :
GoalState
Equations

- g.state = g.elim.state

Instances For

source
@[inline]
def Aesop.Goal.isIrrelevant (g : Goal) :
Bool
Equations

- g.isIrrelevant = g.elim.isIrrelevant

Instances For

source
@[inline]
def Aesop.Goal.isForcedUnprovable (g : Goal) :
Bool
Equations

- g.isForcedUnprovable = g.elim.isForcedUnprovable

Instances For

source
@[inline]
def Aesop.Goal.preNormGoal (g : Goal) :
Lean.MVarId
Equations

- g.preNormGoal = g.elim.preNormGoal

Instances For

source
@[inline]
def Aesop.Goal.normalizationState (g : Goal) :
NormalizationState
Equations

- g.normalizationState = g.elim.normalizationState

Instances For

source
@[inline]
def Aesop.Goal.mvars (g : Goal) :
UnorderedArraySet Lean.MVarId
Equations

- g.mvars = g.elim.mvars

Instances For

source
@[inline]
def Aesop.Goal.forwardState (g : Goal) :
ForwardState
Equations

- g.forwardState = g.elim.forwardState

Instances For

source
@[inline]
def Aesop.Goal.forwardRuleMatches (g : Goal) :
ForwardRuleMatches
Equations

- g.forwardRuleMatches = g.elim.forwardRuleMatches

Instances For

source
@[inline]
def Aesop.Goal.successProbability (g : Goal) :
Percent
Equations

- g.successProbability = g.elim.successProbability

Instances For

source
@[inline]
def Aesop.Goal.addedInIteration (g : Goal) :
Iteration
Equations

- g.addedInIteration = g.elim.addedInIteration

Instances For

source
@[inline]
def Aesop.Goal.lastExpandedInIteration (g : Goal) :
Iteration
Equations

- g.lastExpandedInIteration = g.elim.lastExpandedInIteration

Instances For

source
@[inline]
def Aesop.Goal.failedRapps (g : Goal) :
Array RegularRule
Equations

- g.failedRapps = g.elim.failedRapps

Instances For

source
@[inline]
def Aesop.Goal.unsafeRulesSelected (g : Goal) :
Bool
Equations

- g.unsafeRulesSelected = g.elim.unsafeRulesSelected

Instances For

source
@[inline]
def Aesop.Goal.unsafeQueue (g : Goal) :
UnsafeQueue
Equations

- g.unsafeQueue = g.elim.unsafeQueue

Instances For

source
@[inline]
def Aesop.Goal.unsafeQueue? (g : Goal) :
Option UnsafeQueue
Equations

- g.unsafeQueue? = if g.unsafeRulesSelected = true then some g.unsafeQueue else none

Instances For

source
@[inline]
def Aesop.Goal.setId (id : GoalId) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setParent (parent : MVarClusterRef) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setChildren (children : Array RappRef) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setOrigin (origin : GoalOrigin) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setDepth (depth : Nat) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setIsIrrelevant (isIrrelevant : Bool) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setIsForcedUnprovable (isForcedUnprovable : Bool) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setPreNormGoal (preNormGoal : Lean.MVarId) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setNormalizationState (normalizationState : NormalizationState) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setMVars (mvars : UnorderedArraySet Lean.MVarId) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setForwardState (forwardState : ForwardState) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setForwardRuleMatches (forwardRuleMatches : ForwardRuleMatches) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setSuccessProbability (successProbability : Percent) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setAddedInIteration (addedInIteration : Iteration) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setLastExpandedInIteration (lastExpandedInIteration : Iteration) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setUnsafeQueue (unsafeQueue : UnsafeQueue) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setState (state : GoalState) (g : Goal) :
Goal
Equations

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

Instances For

source
@[inline]
def Aesop.Goal.setFailedRapps (failedRapps : Array RegularRule) (g : Goal) :
Goal
Equations

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

Instances For

source
instance Aesop.Goal.instNonempty :
Nonempty Goal
source
instance Aesop.Goal.instBEq :
BEq Goal
Equations

- Aesop.Goal.instBEq = { beq := fun (g₁ g₂ : Aesop.Goal) => g₁.id == g₂.id }

source
instance Aesop.Goal.instHashable :
Hashable Goal
Equations

- Aesop.Goal.instHashable = { hash := fun (g : Aesop.Goal) => hash g.id }

source
@[inline]
def Aesop.Rapp.mk :
RappData Goal MVarCluster → Rapp
Equations

- Aesop.Rapp.mk = Aesop.tree.introRapp

Instances For

source
@[inline]
def Aesop.Rapp.elim :
Rapp → RappData Goal MVarCluster
Equations

- Aesop.Rapp.elim = Aesop.tree.elimRapp

Instances For

source
@[inline]
def Aesop.Rapp.modify (f : RappData Goal MVarCluster → RappData Goal MVarCluster) (r : Rapp) :
Rapp
Equations

- Aesop.Rapp.modify f r = Aesop.Rapp.mk (f r.elim)

Instances For

source
@[inline]
def Aesop.Rapp.id (r : Rapp) :
RappId
Equations

- r.id = r.elim.id

Instances For

source
@[inline]
def Aesop.Rapp.parent (r : Rapp) :
GoalRef
Equations

- r.parent = r.elim.parent

Instances For

source
@[inline]
def Aesop.Rapp.children (r : Rapp) :
Array MVarClusterRef
Equations

- r.children = r.elim.children

Instances For

source
@[inline]
def Aesop.Rapp.state (r : Rapp) :
NodeState
Equations

- r.state = r.elim.state

Instances For

source
@[inline]
def Aesop.Rapp.isIrrelevant (r : Rapp) :
Bool
Equations

- r.isIrrelevant = r.elim.isIrrelevant

Instances For

source
@[inline]
def Aesop.Rapp.appliedRule (r : Rapp) :
RegularRule
Equations

- r.appliedRule = r.elim.appliedRule

Instances For

source
@[inline]
def Aesop.Rapp.scriptSteps? (r : Rapp) :
Option (Array Script.LazyStep)
Equations

- r.scriptSteps? = r.elim.scriptSteps?

Instances For

source
@[inline]
def Aesop.Rapp.originalSubgoals (r : Rapp) :
Array Lean.MVarId
Equations

- r.originalSubgoals = r.elim.originalSubgoals

Instances For

source
@[inline]
def Aesop.Rapp.successProbability (r : Rapp) :
Percent
Equations

- r.successProbability = r.elim.successProbability

Instances For

source
@[inline]
def Aesop.Rapp.metaState (r : Rapp) :
Lean.Meta.SavedState
Equations

- r.metaState = r.elim.metaState

Instances For

source
@[inline]
def Aesop.Rapp.introducedMVars (r : Rapp) :
UnorderedArraySet Lean.MVarId
Equations

- r.introducedMVars = r.elim.introducedMVars

Instances For

source
@[inline]
def Aesop.Rapp.assignedMVars (r : Rapp) :
UnorderedArraySet Lean.MVarId
Equations

- r.assignedMVars = r.elim.assignedMVars

Instances For

source
@[inline]
def Aesop.Rapp.setId (id : RappId) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setParent (parent : GoalRef) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setChildren (children : Array MVarClusterRef) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setState (state : NodeState) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setIsIrrelevant (isIrrelevant : Bool) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setAppliedRule (appliedRule : RegularRule) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setScriptSteps? (scriptSteps? : Option (Array Script.LazyStep)) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setOriginalSubgoals (originalSubgoals : Array Lean.MVarId) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setSuccessProbability (successProbability : Percent) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setMetaState (metaState : Lean.Meta.SavedState) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setIntroducedMVars (introducedMVars : UnorderedArraySet Lean.MVarId) (r : Rapp) :
Rapp
Equations

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

Instances For

source
@[inline]
def Aesop.Rapp.setAssignedMVars (assignedMVars : UnorderedArraySet Lean.MVarId) (r : Rapp) :
Rapp
Equations

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

Instances For

source
instance Aesop.Rapp.instNonempty :
Nonempty Rapp
source
instance Aesop.Rapp.instBEq :
BEq Rapp
Equations

- Aesop.Rapp.instBEq = { beq := fun (r₁ r₂ : Aesop.Rapp) => r₁.id == r₂.id }

source
instance Aesop.Rapp.instHashable :
Hashable Rapp
Equations

- Aesop.Rapp.instHashable = { hash := fun (r : Aesop.Rapp) => hash r.id }

## Miscellaneous Queries #

source
def Aesop.Rapp.isSafe (r : Rapp) :
Bool
Equations

- r.isSafe = (r.appliedRule.isSafe && r.assignedMVars.isEmpty)

Instances For

source
@[inline]
def Aesop.Goal.postNormGoalAndMetaState? (g : Goal) :
Option (Lean.MVarId × Lean.Meta.SavedState)
Equations

- g.postNormGoalAndMetaState? = match g.normalizationState with | Aesop.NormalizationState.normal postGoal postState script => some (postGoal, postState) | x => none

Instances For

source
def Aesop.Goal.postNormGoal? (g : Goal) :
Option Lean.MVarId
Equations

- g.postNormGoal? = Option.map (fun (x : Lean.MVarId × Lean.Meta.SavedState) => x.fst) g.postNormGoalAndMetaState?

Instances For

source
def Aesop.Goal.currentGoal (g : Goal) :
Lean.MVarId
Equations

- g.currentGoal = g.postNormGoal?.getD g.preNormGoal

Instances For

source
def Aesop.Goal.parentRapp? (g : Goal) :
BaseIO (Option RappRef)
Equations

- g.parentRapp? = do let __do_lift ← ST.Ref.get g.parent pure __do_lift.parent?

Instances For

source
def Aesop.Goal.parentMetaState (g : Goal) (rootMetaState : Lean.Meta.SavedState) :
BaseIO Lean.Meta.SavedState
Equations

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

Instances For

source
def Aesop.Goal.currentGoalAndMetaState (g : Goal) (rootMetaState : Lean.Meta.SavedState) :
Lean.MetaM (Lean.MVarId × Lean.Meta.SavedState)
Equations

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

Instances For

source
def Aesop.Goal.safeRapps (g : Goal) :
BaseIO (Array RappRef)
Equations

- g.safeRapps = Array.filterM (fun (rref : Aesop.RappRef) => do let __do_lift ← ST.Ref.get rref pure __do_lift.isSafe) g.children

Instances For

source
def Aesop.Goal.hasSafeRapp (g : Goal) :
BaseIO Bool
Equations

- g.hasSafeRapp = Array.anyM (fun (rref : Aesop.RappRef) => do let __do_lift ← ST.Ref.get rref pure __do_lift.isSafe) g.children

Instances For

source
def Aesop.Goal.isUnsafeExhausted (g : Goal) :
Bool
Equations

- g.isUnsafeExhausted = (g.unsafeRulesSelected && Subarray.isEmpty g.unsafeQueue)

Instances For

source
def Aesop.Goal.isExhausted (g : Goal) :
BaseIO Bool
Equations

- g.isExhausted = (pure g.isUnsafeExhausted <||> g.hasSafeRapp)

Instances For

source
def Aesop.Goal.isActive (g : Goal) :
BaseIO Bool
Equations

- g.isActive = do let __do_lift ← pure g.isIrrelevant <||> g.isExhausted pure !__do_lift

Instances For

source
def Aesop.Goal.hasProvableRapp (g : Goal) :
BaseIO Bool
Equations

- g.hasProvableRapp = Array.anyM (fun (r : Aesop.RappRef) => do let __do_lift ← ST.Ref.get r pure !__do_lift.state.isUnprovable) g.children

Instances For

source
def Aesop.Goal.firstProvenRapp? (g : Goal) :
BaseIO (Option RappRef)
Equations

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

Instances For

source
def Aesop.Goal.hasMVar (g : Goal) :
Bool
Equations

- g.hasMVar = !g.mvars.isEmpty

Instances For

source
def Aesop.Goal.priority (g : Goal) :
Percent
Equations

- g.priority = g.successProbability * Aesop.unificationGoalPenalty ^ g.mvars.size

Instances For

source
def Aesop.Goal.isNormal (g : Goal) :
Bool
Equations

- g.isNormal = g.normalizationState.isNormal

Instances For

source
def Aesop.Goal.originalGoalId (g : Goal) :
GoalId
Equations

- g.originalGoalId = g.origin.originalGoalId?.getD g.id

Instances For

source
def Aesop.Goal.isRoot (g : Goal) :
BaseIO Bool
Equations

- g.isRoot = do let __do_lift ← g.parentRapp? pure __do_lift.isNone

Instances For

source
def Aesop.Rapp.introducesMVar (r : Rapp) :
Bool
Equations

- r.introducesMVar = !r.introducedMVars.isEmpty

Instances For

source
def Aesop.Rapp.parentPostNormMetaState (r : Rapp) (rootMetaState : Lean.Meta.SavedState) :
BaseIO Lean.Meta.SavedState
Equations

- r.parentPostNormMetaState rootMetaState = do let __do_lift ← ST.Ref.get r.parent __do_lift.parentMetaState rootMetaState

Instances For

source
def Aesop.Rapp.foldSubgoalsM {m : Type → Type} {σ : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (init : σ) (f : σ → GoalRef → m σ) (r : Rapp) :
m σ
Equations

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

Instances For

source
def Aesop.Rapp.forSubgoalsM {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (f : GoalRef → m Unit) (r : Rapp) :
m Unit
Equations

- Aesop.Rapp.forSubgoalsM f r = Array.forM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref Array.forM f __do_lift.goals) r.children

Instances For

source
def Aesop.Rapp.subgoals {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (r : Rapp) :
m (Array GoalRef)
Equations

- r.subgoals = Aesop.Rapp.foldSubgoalsM #[] (fun (subgoals : Array Aesop.GoalRef) (gref : Aesop.GoalRef) => pure (subgoals.push gref)) r

Instances For

source
def Aesop.Rapp.depth (r : Rapp) :
BaseIO Nat
Equations

- r.depth = do let __do_lift ← ST.Ref.get r.parent pure __do_lift.depth

Instances For

source
def Aesop.MVarCluster.provenGoal? (c : MVarCluster) :
BaseIO (Option GoalRef)
Equations

- c.provenGoal? = Array.findM? (fun (gref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get gref pure __do_lift.state.isProven) c.goals

Instances For

source
def Aesop.RappRef.getChildAuxDeclNameGenerator (r : RappRef) :
BaseIO Lean.DeclNameGenerator

Get a `DeclNameGenerator` for auxiliary declarations that can be used by children of this rapp. Successive calls to this function return `DeclNameGenerators` that are guaranteed to generate distinct names.

Equations

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

Instances For