Core.RefineMonad
module D = CodeUnit.Domain
module S = CodeUnit.Syntax
module Env = RefineEnv
include module type of 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 := Core.Monads.St.t
with type local := RefineEnv.t
val read : RefineEnv.t m
val scope : (RefineEnv.t -> RefineEnv.t) -> 'a m -> 'a m
val get : Core.Monads.St.t m
val set : Core.Monads.St.t -> unit m
val modify : (Core.Monads.St.t -> Core.Monads.St.t) -> unit m
val run : Core.Monads.St.t -> RefineEnv.t -> 'a m -> ('a, exn) Stdlib.result
val run_exn : Core.Monads.St.t -> RefineEnv.t -> 'a m -> 'a
val throw : exn -> 'a m
val lift_qu : 'a Monads.quote -> 'a m
val lift_conv_ : unit Monads.conversion -> unit m
val lift_ev : 'a Monads.evaluate -> 'a m
val lift_cmp : 'a Monads.compute -> 'a m
val restrict : Core.Monads.D.cof list -> 'a m -> 'a m
val emit :
?lvl:Log.level ->
Basis.LexingUtil.span option ->
(Stdlib.Format.formatter -> 'a -> unit) ->
'a ->
unit m
val refine_err : RefineError.t -> 'a m
val update_span : Basis.LexingUtil.span option -> 'a m -> 'a m
val add_global :
unfolder:CodeUnit.Global.t option ->
shadowing:bool ->
Ident.t ->
D.tp ->
CodeUnit.Global.t m
val get_global : CodeUnit.Global.t -> D.tp m
val resolve :
Ident.t ->
[ `Local of int | `Global of CodeUnit.Global.t | `Unbound ] m
val resolve_unfolder_syms : Ident.t list -> CodeUnit.Global.t list m
val get_lib : Bantorra.Manager.library m
val with_unit : Bantorra.Manager.library -> CodeUnit.id -> 'a m -> 'a m
val import : shadowing:bool -> Namespace.pattern -> CodeUnit.id -> unit m
val loading_status :
CodeUnit.CodeUnitID.t ->
[ `Loaded | `Loading | `Unloaded ] m
val view : shadowing:bool -> Namespace.pattern -> unit m
val export : shadowing:bool -> Namespace.pattern -> unit m
val repack : shadowing:bool -> Namespace.pattern -> unit m
val with_section :
shadowing:bool ->
prefix:Namespace.path option ->
'a m ->
'a m
val with_pp : (Basis.Pp.env -> 'a m) -> 'a m
val expected_connective : RefineError.connective -> D.tp -> 'a m
val field_names_mismatch :
expected:Ident.user list ->
actual:Ident.user list ->
'a m