Documentation

Aesop.Search.SearchM

structure Aesop.NormSimpContext :

toContext : Lean.Meta.Simp.Context
enabled : Bool
useHyps : Bool
configStx? : Option Lean.Term
simprocs : Lean.Meta.Simp.SimprocsArray

Instances For

Aesop.instInhabitedNormSimpContext

instance Aesop.instInhabitedNormSimpContext :

Inhabited NormSimpContext

Equations

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

structure Aesop.SearchM.Context :

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

Instances For

instance Aesop.SearchM.instNonemptyContext :

Nonempty Context

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

iteration : Iteration
queue : Q
maxRuleApplicationDepthReached : Bool

Instances For

instance Aesop.SearchM.instInhabitedState {a✝ : Type} [Inhabited a✝] {a✝¹ : Queue a✝} :

Inhabited (State a✝)

Equations

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

@[reducible, inline]

abbrev Aesop.SearchM (Q : Type) [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} [Queue Q] :

Monad (SearchM Q)

Equations

Aesop.SearchM.instMonad = Monad.mk

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

Lean.MonadRef (SearchM Q)

Equations

Aesop.SearchM.instMonadRef = { getRef := Lean.getRef, withRef := @Lean.MonadRef.withRef (Aesop.SearchM Q) (inferInstanceAs (Lean.MonadRef (Aesop.SearchM Q))) }

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

Inhabited (SearchM Q α)

Equations

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

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

MonadState (State Q) (SearchM Q)

Equations

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

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

MonadReader Context (SearchM Q)

Equations

Aesop.SearchM.instMonadReaderContext = { read := MonadReaderOf.read }

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

MonadStats (SearchM Q)

Equations

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

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

MonadLift TreeM (SearchM Q)

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

Aesop.getTree = getThe Aesop.Tree

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

Tree → SearchM Q Unit

Equations

Aesop.setTree = Aesop.setThe Aesop.Tree

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

(Tree → Tree) → SearchM Q Unit

Equations

Aesop.modifyTree = modifyThe Aesop.Tree

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

SearchM Q Iteration

Equations

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

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

Equations

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

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

SearchM Q (Option GoalRef)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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