Documentation

Aesop.BaseM

structure Aesop.BaseM.State :

State of the BaseM monad.

rulePatternCache : RulePatternCache
The rule pattern cache.
rpinfCache : RPINFCache
The RPINF cache.
stats : Stats
Stats collected during an Aesop call.

Instances For

instance Aesop.BaseM.instInhabitedState :

Inhabited State

Equations

Aesop.BaseM.instInhabitedState = { default := { rulePatternCache := default, rpinfCache := default, stats := default } }

instance Aesop.instEmptyCollectionState :

EmptyCollection BaseM.State

Equations

Aesop.instEmptyCollectionState = { emptyCollection := { rulePatternCache := ∅, rpinfCache := ∅, stats := ∅ } }

@[reducible, inline]

abbrev Aesop.BaseM (α : Type) :

Aesop's base monad. Contains no interesting data, only various caches and stats.

Equations

Aesop.BaseM = StateRefT' IO.RealWorld Aesop.BaseM.State Lean.MetaM

Instances For

def Aesop.BaseM.run {α : Type} (x : BaseM α) (stats : Stats := ∅) :

Lean.MetaM (α × Stats)

Run a BaseM action.

Equations

x.run stats = do let __discr ← StateRefT'.run x { rulePatternCache := ∅, rpinfCache := ∅, stats := stats } match __discr with | (a, s) => pure (a, s.stats)

instance Aesop.BaseM.instMonadHashMapCacheAdapterExprEntry :

Lean.MonadHashMapCacheAdapter Lean.Expr RulePatternCache.Entry BaseM

Equations

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

instance Aesop.BaseM.instMonadHashMapCacheAdapterExprRPINFRaw :

Lean.MonadHashMapCacheAdapter Lean.Expr RPINFRaw BaseM

Equations

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

instance Aesop.BaseM.instMonadStats :

MonadStats BaseM

Equations

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

instance Aesop.BaseM.instMonadBacktrackSavedState :

Lean.MonadBacktrack Lean.Meta.SavedState BaseM

Equations

Aesop.BaseM.instMonadBacktrackSavedState = { saveState := liftM Lean.Meta.saveState, restoreState := fun (x : Lean.Meta.SavedState) => liftM x.restore }