sig
  type prog_symbol =
      PV of Ity.pvsymbol
    | RS of Expr.rsymbol
    | OO of Expr.Srs.t
  type namespace = {
    ns_ts : Ity.itysymbol Wstdlib.Mstr.t;
    ns_ps : Pmodule.prog_symbol Wstdlib.Mstr.t;
    ns_xs : Ity.xsymbol Wstdlib.Mstr.t;
    ns_ns : Pmodule.namespace Wstdlib.Mstr.t;
  }
  val empty_ns : Pmodule.namespace
  val ns_find_prog_symbol :
    Pmodule.namespace -> string list -> Pmodule.prog_symbol
  val ns_find_its : Pmodule.namespace -> string list -> Ity.itysymbol
  val ns_find_pv : Pmodule.namespace -> string list -> Ity.pvsymbol
  val ns_find_xs : Pmodule.namespace -> string list -> Ity.xsymbol
  val ns_find_ns : Pmodule.namespace -> string list -> Pmodule.namespace
  val ns_find_rs : Pmodule.namespace -> string list -> Expr.rsymbol
  type overload = FixedRes of Ity.ity | SameType | NoOver
  val overload_of_rs : Expr.rsymbol -> Pmodule.overload
  val overload_of_oo : Expr.Srs.t -> Pmodule.overload
  val ref_attr : Ident.attribute
  exception IncompatibleNotation of string
  type pmodule = private {
    mod_theory : Theory.theory;
    mod_units : Pmodule.mod_unit list;
    mod_export : Pmodule.namespace;
    mod_known : Pdecl.known_map;
    mod_local : Ident.Sid.t;
    mod_used : Ident.Sid.t;
  }
  and mod_unit =
      Udecl of Pdecl.pdecl
    | Uuse of Pmodule.pmodule
    | Uclone of Pmodule.mod_inst
    | Umeta of Theory.meta * Theory.meta_arg list
    | Uscope of string * Pmodule.mod_unit list
  and mod_inst = {
    mi_mod : Pmodule.pmodule;
    mi_ty : Ity.ity Ty.Mts.t;
    mi_ts : Ity.itysymbol Ty.Mts.t;
    mi_ls : Term.lsymbol Term.Mls.t;
    mi_pr : Decl.prsymbol Decl.Mpr.t;
    mi_pk : Decl.prop_kind Decl.Mpr.t;
    mi_pv : Ity.pvsymbol Term.Mvs.t;
    mi_rs : Expr.rsymbol Expr.Mrs.t;
    mi_xs : Ity.xsymbol Ity.Mxs.t;
    mi_df : Decl.prop_kind;
  }
  val empty_mod_inst : Pmodule.pmodule -> Pmodule.mod_inst
  type pmodule_uc = private {
    muc_theory : Theory.theory_uc;
    muc_units : Pmodule.mod_unit list;
    muc_import : Pmodule.namespace list;
    muc_export : Pmodule.namespace list;
    muc_known : Pdecl.known_map;
    muc_local : Ident.Sid.t;
    muc_used : Ident.Sid.t;
    muc_env : Env.env;
  }
  val create_module :
    Env.env -> ?path:string list -> Ident.preid -> Pmodule.pmodule_uc
  val close_module : Pmodule.pmodule_uc -> Pmodule.pmodule
  val open_scope : Pmodule.pmodule_uc -> string -> Pmodule.pmodule_uc
  val close_scope : Pmodule.pmodule_uc -> import:bool -> Pmodule.pmodule_uc
  val import_scope : Pmodule.pmodule_uc -> string list -> Pmodule.pmodule_uc
  val restore_path : Ident.ident -> string list * string * string list
  val restore_module_id : Ident.ident -> Pmodule.pmodule
  val restore_module : Theory.theory -> Pmodule.pmodule
  val use_export :
    Pmodule.pmodule_uc -> Pmodule.pmodule -> Pmodule.pmodule_uc
  val clone_export :
    ?loc:Loc.position ->
    Pmodule.pmodule_uc ->
    Pmodule.pmodule -> Pmodule.mod_inst -> Pmodule.pmodule_uc
  val add_meta :
    Pmodule.pmodule_uc ->
    Theory.meta -> Theory.meta_arg list -> Pmodule.pmodule_uc
  val add_pdecl :
    ?warn:bool ->
    vc:bool -> Pmodule.pmodule_uc -> Pdecl.pdecl -> Pmodule.pmodule_uc
  val mod_impl : Env.env -> Pmodule.pmodule -> Pmodule.pmodule
  val mod_impl_register :
    Env.env -> Pmodule.pmodule -> Pmodule.pmodule -> Pmodule.mod_inst -> unit
  val builtin_module : Pmodule.pmodule
  val bool_module : Pmodule.pmodule
  val unit_module : Pmodule.pmodule
  val highord_module : Pmodule.pmodule
  val tuple_module : int -> Pmodule.pmodule
  val ref_module : Pmodule.pmodule
  val its_ref : Ity.itysymbol
  val ts_ref : Ty.tysymbol
  val rs_ref : Expr.rsymbol
  val rs_ref_cons : Expr.rsymbol
  val rs_ref_proj : Expr.rsymbol
  val ls_ref_cons : Term.lsymbol
  val ls_ref_proj : Term.lsymbol
  type mlw_file = Pmodule.pmodule Wstdlib.Mstr.t
  val mlw_language : Pmodule.mlw_file Env.language
  val mlw_language_builtin : Env.pathname -> Pmodule.mlw_file
  exception ModuleNotFound of Env.pathname * string
  val read_module : Env.env -> Env.pathname -> string -> Pmodule.pmodule
  val print_unit : Stdlib.Format.formatter -> Pmodule.mod_unit -> unit
  val print_module : Stdlib.Format.formatter -> Pmodule.pmodule -> unit
end