Module Monads.RefineM

The elaboration monad is the "maximal" monad that can run code from any of the other monads.

include Basis.Monad.MonadReaderStateResult with type global := St.t with type local := RefineEnv.t
include Basis.Monad.S
type 'a m
val ret : 'a -> 'a m
val bind : 'a m -> ('a -> 'b m) -> 'b m
val read : RefineEnv.t m
val scope : (RefineEnv.t -> RefineEnv.t) -> 'a m -> 'a m
val get : St.t m
val set : St.t -> unit m
val modify : (St.t -> St.t) -> unit m
val run : St.t -> RefineEnv.t -> 'a m -> ('a, exn) Stdlib.result
val run_exn : St.t -> RefineEnv.t -> 'a m -> 'a
val throw : exn -> 'a m
val trap : 'a m -> ('a, exn) Stdlib.result m
val lift_qu : 'a quote -> 'a m
val lift_conv_ : unit conversion -> unit m
val lift_ev : 'a evaluate -> 'a m
val lift_cmp : 'a compute -> 'a m
val restrict : D.cof list -> 'a m -> 'a m
val globally : 'a m -> 'a m
val emit : ?lvl:Log.level -> Basis.LexingUtil.span option -> (Stdlib.Format.formatter -> 'a -> unit) -> 'a -> unit m
val abort_if_inconsistent : 'a m -> 'a m -> 'a m