Documentation

Aesop.Search.SearchM

structure Aesop.NormSimpContextextends Lean.Meta.Simp.Context :

config : Lean.Meta.Simp.Config
maxDischargeDepth : UInt32
simpTheorems : Lean.Meta.SimpTheoremsArray
congrTheorems : Lean.Meta.SimpCongrTheorems
parent? : Option Lean.Expr
dischargeDepth : UInt32
lctxInitIndices : Nat
inDSimp : Bool
enabled : Bool
useHyps : Bool
configStx? : Option Lean.Term
simprocs : Lean.Meta.Simp.SimprocsArray

Instances For

Aesop.instInhabitedNormSimpContext

instance Aesop.instInhabitedNormSimpContext :

Inhabited Aesop.NormSimpContext

Equations

Aesop.instInhabitedNormSimpContext = { default := { toContext := default, enabled := default, useHyps := default, configStx? := default, simprocs := default } }

structure Aesop.SearchM.Context :

ruleSet : Aesop.LocalRuleSet
normSimpContext : Aesop.NormSimpContext
options : Aesop.Options'
statsRef : Aesop.StatsRef

Instances For

instance Aesop.SearchM.instNonemptyContext :

Nonempty Aesop.SearchM.Context

Equations

Aesop.SearchM.instNonemptyContext = ⋯

structure Aesop.SearchM.State (Q : Type) [Aesop.Queue Q] :

iteration : Aesop.Iteration
queue : Q
maxRuleApplicationDepthReached : Bool

Instances For

instance Aesop.SearchM.instInhabitedState :

{a : Type} → [inst : Inhabited a] → {a_1 : Aesop.Queue a} → Inhabited (Aesop.SearchM.State a)

Equations

Aesop.SearchM.instInhabitedState = { default := { iteration := default, queue := default, maxRuleApplicationDepthReached := default } }

@[reducible, inline]

abbrev Aesop.SearchM (Q : Type) [Aesop.Queue Q] (α : Type) :

Equations

Aesop.SearchM Q = ReaderT Aesop.SearchM.Context (StateRefT' IO.RealWorld (Aesop.SearchM.State Q) (StateRefT' IO.RealWorld Aesop.Tree Lean.MetaM))

Instances For

instance Aesop.SearchM.instMonad {Q : Type} [Aesop.Queue Q] :

Monad (Aesop.SearchM Q)

Equations

Aesop.SearchM.instMonad = let __src := inferInstanceAs (Monad (Aesop.SearchM Q)); Monad.mk

instance Aesop.SearchM.instMonadRef {Q : Type} [Aesop.Queue Q] :

Lean.MonadRef (Aesop.SearchM Q)

Equations

Aesop.SearchM.instMonadRef = let __src := inferInstanceAs (Lean.MonadRef (Aesop.SearchM Q)); { getRef := Lean.getRef, withRef := fun {α : Type} => Lean.MonadRef.withRef }

instance Aesop.SearchM.instInhabited {Q : Type} [Aesop.Queue Q] {α : Type} :

Inhabited (Aesop.SearchM Q α)

Equations

Aesop.SearchM.instInhabited = { default := failure }

instance Aesop.SearchM.instMonadStateState {Q : Type} [Aesop.Queue Q] :

MonadState (Aesop.SearchM.State Q) (Aesop.SearchM Q)

Equations

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

instance Aesop.SearchM.instMonadReaderContext {Q : Type} [Aesop.Queue Q] :

MonadReader Aesop.SearchM.Context (Aesop.SearchM Q)

Equations

Aesop.SearchM.instMonadReaderContext = let __src := inferInstanceAs (MonadReaderOf Aesop.SearchM.Context (Aesop.SearchM Q)); { read := MonadReaderOf.read }

instance Aesop.SearchM.instMonadStats {Q : Type} [Aesop.Queue Q] :

Aesop.MonadStats (Aesop.SearchM Q)

Equations

Aesop.SearchM.instMonadStats = Aesop.MonadStats.mk do let __do_lift ← read pure __do_lift.statsRef

instance Aesop.SearchM.instMonadLiftTreeM {Q : Type} [Aesop.Queue Q] :

MonadLift Aesop.TreeM (Aesop.SearchM Q)

Equations

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

def Aesop.SearchM.run' {Q : Type} [Aesop.Queue Q] {α : Type} (ctx : Aesop.SearchM.Context) (σ : Aesop.SearchM.State Q) (t : Aesop.Tree) (x : Aesop.SearchM Q α) :

Lean.MetaM (α × Aesop.SearchM.State Q × Aesop.Tree × Aesop.Stats)

Equations

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

def Aesop.SearchM.run {Q : Type} [Aesop.Queue Q] {α : Type} (ruleSet : Aesop.LocalRuleSet) (options : Aesop.Options') (simpConfig : Lean.Meta.Simp.Config) (simpConfigStx? : Option Lean.Term) (goal : Lean.MVarId) (stats : Aesop.Stats) (x : Aesop.SearchM Q α) :

Lean.MetaM (α × Aesop.SearchM.State Q × Aesop.Tree × Aesop.Stats)

Equations

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

def Aesop.getTree {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q Aesop.Tree

Equations

Aesop.getTree = getThe Aesop.Tree

def Aesop.setTree {Q : Type} [Aesop.Queue Q] :

Aesop.Tree → Aesop.SearchM Q Unit

Equations

Aesop.setTree = Aesop.setThe Aesop.Tree

def Aesop.modifyTree {Q : Type} [Aesop.Queue Q] :

(Aesop.Tree → Aesop.Tree) → Aesop.SearchM Q Unit

Equations

Aesop.modifyTree = modifyThe Aesop.Tree

def Aesop.getIteration {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q Aesop.Iteration

Equations

Aesop.getIteration = do let __do_lift ← get pure __do_lift.iteration

def Aesop.incrementIteration {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q Unit

Equations

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

def Aesop.popGoal? {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q (Option Aesop.GoalRef)

Equations

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

def Aesop.enqueueGoals {Q : Type} [Aesop.Queue Q] (gs : Array Aesop.GoalRef) :

Aesop.SearchM Q Unit

Equations

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

def Aesop.setMaxRuleApplicationDepthReached {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q Unit

Equations

Aesop.setMaxRuleApplicationDepthReached = modify fun (s : Aesop.SearchM.State Q) => { iteration := s.iteration, queue := s.queue, maxRuleApplicationDepthReached := true }

def Aesop.wasMaxRuleApplicationDepthReached {Q : Type} [Aesop.Queue Q] :

Aesop.SearchM Q Bool

Equations

Aesop.wasMaxRuleApplicationDepthReached = do let __do_lift ← get pure __do_lift.maxRuleApplicationDepthReached