Module Mlw_module

module Mlw_module: sig .. end

Program modules



type type_symbol = 
| PT of Mlw_ty.T.itysymbol
| TS of Ty.tysymbol
type prog_symbol = 
| PV of Mlw_ty.pvsymbol
| PS of Mlw_expr.psymbol
| PL of Mlw_expr.plsymbol
| XS of Mlw_ty.xsymbol
| LS of Term.lsymbol
type namespace = {
   ns_ts : type_symbol Stdlib.Mstr.t;
   ns_ps : prog_symbol Stdlib.Mstr.t;
   ns_ns : namespace Stdlib.Mstr.t;
}
val ns_find_type_symbol : namespace -> string list -> type_symbol
val ns_find_prog_symbol : namespace -> string list -> prog_symbol
val ns_find_its : namespace -> string list -> Mlw_ty.T.itysymbol
val ns_find_ts : namespace -> string list -> Ty.tysymbol
val ns_find_pv : namespace -> string list -> Mlw_ty.pvsymbol
val ns_find_ps : namespace -> string list -> Mlw_expr.psymbol
val ns_find_pl : namespace -> string list -> Mlw_expr.plsymbol
val ns_find_xs : namespace -> string list -> Mlw_ty.xsymbol
val ns_find_ls : namespace -> string list -> Term.lsymbol
val ns_find_ns : namespace -> string list -> namespace

Module


type modul = private {
   mod_theory : Theory.theory;
   mod_decls : Mlw_decl.pdecl list;
   mod_export : namespace;
   mod_known : Mlw_decl.known_map;
   mod_local : Ident.Sid.t;
   mod_used : Ident.Sid.t;
}

Module under construction


type module_uc 
val create_module : Env.env -> ?path:string list -> Ident.preid -> module_uc
val close_module : module_uc -> modul
val open_namespace : module_uc -> string -> module_uc
val close_namespace : module_uc -> bool -> module_uc
val get_theory : module_uc -> Theory.theory_uc
val get_namespace : module_uc -> namespace
val get_known : module_uc -> Mlw_decl.known_map
val restore_path : Ident.ident -> string list * string * string list
restore_path id returns the triple (library path, module, qualified symbol name) if the ident was ever introduced in a module declaration. If the ident was declared in several different modules, the first association is retained. If id is a module name, the third component is an empty list. Raises Not_found if the ident was never declared in/as a module.
val restore_module : Theory.theory -> modul
retrieves a module from its underlying theory raises Not_found if no such module exists

Use and clone


val use_export : module_uc -> modul -> module_uc
type mod_inst = {
   inst_pv : Mlw_ty.pvsymbol Mlw_ty.Mpv.t;
   inst_ps : Mlw_expr.psymbol Mlw_expr.Mps.t;
}
val clone_export : module_uc ->
modul ->
mod_inst -> Theory.th_inst -> module_uc

Logic decls


val add_decl : module_uc -> Decl.decl -> module_uc
val use_export_theory : module_uc -> Theory.theory -> module_uc
val clone_export_theory : module_uc ->
Theory.theory -> Theory.th_inst -> module_uc
val add_meta : module_uc ->
Theory.meta -> Theory.meta_arg list -> module_uc

Program decls


val add_pdecl : wp:bool -> module_uc -> Mlw_decl.pdecl -> module_uc
add_pdecl ~wp m d adds declaration d in module m. If wp is true, VC is computed and added to m.
exception TooLateInvariant
val add_invariant : module_uc ->
Mlw_ty.T.itysymbol -> Mlw_ty.post -> module_uc

Builtin symbols


val xs_exit : Mlw_ty.xsymbol

WhyML language


type mlw_file = modul Stdlib.Mstr.t * Theory.theory Stdlib.Mstr.t 
val mlw_language : mlw_file Env.language
exception ModuleNotFound of Env.pathname * string
exception ModuleOrTheoryNotFound of Env.pathname * string
type module_or_theory = 
| Module of modul
| Theory of Theory.theory
val read_module : Env.env -> Env.pathname -> string -> modul
val read_module_or_theory : Env.env -> Env.pathname -> string -> module_or_theory