Module 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
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 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 trap : 'a m -> ('a, exn) Stdlib.result 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 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
val refine_err : RefineError.t -> 'a m
val update_span : Basis.LexingUtil.span option -> 'a m -> 'a m
val abstract : Ident.t -> D.tp -> (D.con -> '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 add_hole : (D.tp * D.cof * D.tm_clo) -> unit m
val get_holes : (D.tp * D.cof * D.tm_clo) list m
val get_local_tp : int -> D.tp m
val get_local : int -> D.con 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 eval : S.t -> D.con m
val eval_tp : S.tp -> D.tp m
val quote_con : D.tp -> D.con -> S.t m
val quote_tp : D.tp -> S.tp m
val quote_cut : D.cut -> S.t m
val quote_cof : D.cof -> S.t m
val quote_dim : D.dim -> S.t m
val equate_tp : D.tp -> D.tp -> unit m
val equate : D.tp -> D.con -> D.con -> unit m
val with_pp : (Basis.Pp.env -> 'a m) -> 'a m
val expected_connective : RefineError.connective -> D.tp -> 'a m
val expected_field : D.tele -> S.t -> Ident.t -> 'a m
val field_names_mismatch : expected:Ident.user list -> actual:Ident.user list -> 'a m
val destruct_cells : Env.cell list -> (Ident.t * S.tp) list m
val multi_pi : Env.cell list -> S.tp m -> S.tp m
val multi_ap : Env.cell Bwd.bwd -> D.cut -> D.cut
val print_state : string option -> (Ident.t * S.tp) list -> S.tp -> unit m
val print_boundary : S.t -> D.tp -> D.cof -> D.tm_clo -> unit m
val boundary_satisfied : S.t -> D.tp -> D.cof -> D.tm_clo -> [> `BdrySat | `BdryUnsat ] m