Scopes and the environment monad

cvc5 creates sorts, terms and solvers through a term manager, and objects of two managers must never meet. This library hides term managers behind the class Ω: an instance stands for "the term manager of the current scope", and nearly every type and function takes one implicitly.

Work happens in the Env monad (EnvT for another base monad), and Env.run/Env.runIO run it in a fresh scope. As with runST, nothing mentioning the scope can escape the run, and two scopes' sorts and terms cannot be mixed, nested runs included.

class Cvc.Ω : Type 1

The current scope: an instance stands for one term manager.

Only Env.run and its variants make one, so a sort, term or solver cannot leave the run it was made in, nor meet one made in another run, nested runs included.

• scope : Type

structure Cvc.State : Type

What an Env threads: the scope's term manager and the sorts declared in it.

• tm : cvc5.TermManager
• declaredSorts : Std.HashMap String cvc5.Sort

structure Cvc.EnvT [Ω] (m : Type → Type) (α : Type) : Type

The environment monad transformer.

• runOn : StateRefT' IO.RealWorld Cvc.State (Cvc.ResT m) α

def Cvc.Env [Ω] (α : Type) : Type

The environment monad.

Equations

• Cvc.Env = Cvc.EnvT BaseIO

def Cvc.EnvT.pure {m : Type → Type} [Ω] [M : Monad m] {α : Type} (a : α) : EnvT m α

Equations

• Cvc.EnvT.pure a = { runOn := fun (x : ST.Ref IO.RealWorld Cvc.State) => pure (Except.ok a) }

def Cvc.EnvT.bind {m : Type → Type} [Ω] [M : Monad m] {α β : Type} (code : EnvT m α) (f : α → EnvT m β) : EnvT m β

Equations

• code.bind f = { runOn := fun (state : ST.Ref IO.RealWorld Cvc.State) => do let a ← Cvc.EnvT.runOn✝ code state Cvc.EnvT.runOn✝ (f a) state }

@[instance_reducible]

instance Cvc.EnvT.instMonad {m : Type → Type} [Ω] [M : Monad m] : Monad (EnvT m)

Equations

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

def Cvc.EnvT.liftBaseIO {m : Type → Type} [Ω] [M : Monad m] {α : Type} [MonadLiftT BaseIO m] (code : BaseIO α) : EnvT m α

Equations

• Cvc.EnvT.liftBaseIO code = { runOn := fun (x : ST.Ref IO.RealWorld Cvc.State) => liftM code }

@[instance_reducible]

instance Cvc.EnvT.instMonadLiftBaseIOOfMonadLiftT {m : Type → Type} [Ω] [M : Monad m] [MonadLiftT BaseIO m] : MonadLift BaseIO (EnvT m)

Equations

• Cvc.EnvT.instMonadLiftBaseIOOfMonadLiftT = { monadLift := fun {α : Type} => Cvc.EnvT.liftBaseIO }

def Cvc.EnvT.liftIO {m : Type → Type} [Ω] [M : Monad m] {α : Type} [MonadLiftT BaseIO m] (code : IO α) : EnvT m α

Equations

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

@[instance_reducible]

instance Cvc.EnvT.instMonadLiftIOOfMonadLiftTBaseIO {m : Type → Type} [Ω] [M : Monad m] [MonadLiftT BaseIO m] : MonadLift IO (EnvT m)

Equations

• Cvc.EnvT.instMonadLiftIOOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.EnvT.liftIO }

def Cvc.EnvT.liftEnv {m : Type → Type} [Ω] {α : Type} [L : MonadLiftT BaseIO m] (code : Env α) : EnvT m α

Equations

• Cvc.EnvT.liftEnv code = { runOn := monadLift ∘ Cvc.EnvT.runOn✝ code }

@[instance_reducible]

instance Cvc.EnvT.instMonadLiftEnvOfMonadLiftTBaseIO {m : Type → Type} [Ω] [MonadLiftT BaseIO m] : MonadLift Env (EnvT m)

Equations

• Cvc.EnvT.instMonadLiftEnvOfMonadLiftTBaseIO = { monadLift := fun {α : Type} => Cvc.EnvT.liftEnv }

def Cvc.EnvT.liftResT {m : Type → Type} [Ω] {α : Type} (a? : ResT m α) : EnvT m α

Equations

• Cvc.EnvT.liftResT a? = { runOn := fun (_state : ST.Ref IO.RealWorld Cvc.State) => a? }

@[instance_reducible]

instance Cvc.EnvT.instMonadLiftResT {m : Type → Type} [Ω] : MonadLift (ResT m) (EnvT m)

Equations

• Cvc.EnvT.instMonadLiftResT = { monadLift := fun {α : Type} => Cvc.EnvT.liftResT }

def Cvc.EnvT.throw {m : Type → Type} [Ω] [M : Monad m] {α : Type} (e : Error) : EnvT m α

Equations

• Cvc.EnvT.throw e = { runOn := fun (_state : ST.Ref IO.RealWorld Cvc.State) => throw e }

def Cvc.EnvT.tryCatch {m : Type → Type} [Ω] [M : Monad m] {α : Type} (code : EnvT m α) (errorDo : Error → EnvT m α) : EnvT m α

Equations

• code.tryCatch errorDo = { runOn := fun (state : ST.Ref IO.RealWorld Cvc.State) => tryCatch (Cvc.EnvT.runOn✝ code state) fun (e : Cvc.Error) => Cvc.EnvT.runOn✝ (errorDo e) state }

@[instance_reducible]

instance Cvc.EnvT.instMonadExceptOfError {m : Type → Type} [Ω] [M : Monad m] : MonadExceptOf Error (EnvT m)

Equations

• Cvc.EnvT.instMonadExceptOfError = { throw := fun {α : Type} => Cvc.EnvT.throw, tryCatch := fun {α : Type} => Cvc.EnvT.tryCatch }

@[instance_reducible]

instance Cvc.EnvT.instInhabited {m : Type → Type} [Ω] [M : Monad m] {α : Type} : Inhabited (EnvT m α)

Equations

• Cvc.EnvT.instInhabited = { default := Cvc.throwInternal "`Inhabited` witness" }

@[instance_reducible]

instance Cvc.EnvT.instInhabitedEnv [Ω] {α : Type} : Inhabited (Env α)

Equations

• Cvc.EnvT.instInhabitedEnv = { default := Cvc.EnvT.instInhabitedEnv._aux_1 }

def Cvc.Env.liftBaseIO [Ω] {α : Type} (code : BaseIO α) : Env α

Equations

• Cvc.Env.liftBaseIO code = Cvc.EnvT.liftBaseIO code

@[instance_reducible]

instance Cvc.Env.instMonadLiftBaseIO [Ω] : MonadLift BaseIO Env

Equations

• Cvc.Env.instMonadLiftBaseIO = { monadLift := fun {α : Type} => Cvc.Env.liftBaseIO }

def Cvc.Env.liftIO [Ω] {α : Type} (code : IO α) : Env α

Equations

• Cvc.Env.liftIO code = Cvc.EnvT.liftIO code

@[instance_reducible]

instance Cvc.Env.instMonadLiftIO [Ω] : MonadLift IO Env

Equations

• Cvc.Env.instMonadLiftIO = { monadLift := fun {α : Type} => Cvc.Env.liftIO }

@[instance_reducible]

instance Cvc.Env.instMonad [Ω] : Monad Env

Equations

• Cvc.Env.instMonad = Cvc.EnvT.instMonad

@[instance_reducible]

instance Cvc.Env.instMonadLiftResTBaseIO [Ω] : MonadLift (ResT BaseIO) Env

Equations

• Cvc.Env.instMonadLiftResTBaseIO = Cvc.EnvT.instMonadLiftResT

@[instance_reducible]

instance Cvc.Env.instMonadExceptOfError [Ω] : MonadExceptOf Error Env

Equations

• Cvc.Env.instMonadExceptOfError = Cvc.EnvT.instMonadExceptOfError

@[instance_reducible]

instance Cvc.Env.instMonadLiftEnvTBaseIO [Ω] : MonadLift (EnvT BaseIO) Env

Equations

• Cvc.Env.instMonadLiftEnvTBaseIO = { monadLift := fun {α : Type} => id }

def Cvc.EnvT.run {m : Type → Type} {α : Type} [Monad m] [MonadLiftT BaseIO m] (code : [inst : Ω] → EnvT m α) : m (Res α)

Runs code in a fresh scope, with a term manager of its own, answering its result or error.

α is chosen outside the scope, so nothing mentioning the scope can escape the run.

Equations

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

def Cvc.Env.run {α : Type} (code : [inst : Ω] → Env α) : BaseIO (Res α)

Runs code in a fresh scope, with a term manager of its own, answering its result or error.

α is chosen outside the scope, so nothing mentioning the scope can escape the run.

Equations

• Cvc.Env.run code = Cvc.EnvT.run fun [Cvc.Ω] => code

def Cvc.Env.runIO {α : Type} (code : [inst : Ω] → Env α) : IO α

Env.run, raising an error as an IO exception.

Equations

• Cvc.Env.runIO code = do let __do_lift ← liftM (Cvc.Env.run fun [Cvc.Ω] => code) match __do_lift with | Except.ok a => pure a | Except.error e => throw (IO.Error.userError e.toString)