Solver-mode monadic environments #
An answer from the solver splits the world, and the queries that make sense differ in each branch:
a model exists only where the answer was sat, a synthesis solution only where one was found. Each
branch gets its own monad, privately wrapping EnvT.
env_gen% fills one in: the Monad, MonadExcept and lifting instances, including a private
lift from EnvT. That lift being private is the whole mechanism — user code cannot run arbitrary
EnvT code, a check in particular, inside a block that only holds because of an earlier answer.
Private means private to the module the macro is expanded in, so a module declaring mode monads
keeps the ability to lift into them and no one else gets it.
A mode monad is declared in two steps, the structure and then the macro:
/-- Code running where the solver last answered sat. -/
structure EnvSatT (solver : Solver) (m : Type → Type) (α : Type) where
private wrap ::
private toEnv : EnvT m α
env_gen% EnvSatT / EnvSat
Fills in the mode monad envT and its BaseIO version env, as Cvc.Gen.SolverMode says.
Equations
- One or more equations did not get rendered due to their size.