Module Pmodule

module Pmodule: sig .. end

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 : prog_symbol Wstdlib.Mstr.t;
   ns_xs : Ity.xsymbol Wstdlib.Mstr.t;
   ns_ns : namespace Wstdlib.Mstr.t;
}
val ns_find_prog_symbol : namespace -> string list -> prog_symbol
val ns_find_its : namespace -> string list -> Ity.itysymbol
val ns_find_pv : namespace -> string list -> Ity.pvsymbol
val ns_find_rs : namespace -> string list -> Expr.rsymbol
val ns_find_xs : namespace -> string list -> Ity.xsymbol
val ns_find_ns : namespace -> string list -> namespace
type overload = 
| FixedRes of Ity.ity
| SameType
| NoOver
val overload_of_rs : Expr.rsymbol -> overload
exception IncompatibleNotation of string

Module

type pmodule = private {
   mod_theory : Theory.theory;
   mod_units : mod_unit list;
   mod_export : namespace;
   mod_known : Pdecl.known_map;
   mod_local : Ident.Sid.t;
   mod_used : Ident.Sid.t;
}
type mod_unit = 
| Udecl of Pdecl.pdecl
| Uuse of pmodule
| Uclone of mod_inst
| Umeta of Theory.meta * Theory.meta_arg list
| Uscope of string * mod_unit list
type mod_inst = {
   mi_mod : 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 -> mod_inst

Module under construction

type pmodule_uc = private {
   muc_theory : Theory.theory_uc;
   muc_units : mod_unit list;
   muc_import : namespace list;
   muc_export : 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_uc
val close_module : pmodule_uc -> pmodule
val open_scope : pmodule_uc -> string -> pmodule_uc
val close_scope : pmodule_uc -> import:bool -> pmodule_uc
val import_scope : pmodule_uc -> string list -> pmodule_uc
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 -> pmodule

retrieves a module from its underlying theory raises Not_found if no such module exists

Use and clone

val use_export : pmodule_uc -> pmodule -> pmodule_uc
val clone_export : pmodule_uc ->
pmodule -> mod_inst -> pmodule_uc

Logic decls

val add_meta : pmodule_uc ->
Theory.meta -> Theory.meta_arg list -> pmodule_uc

Program decls

val add_pdecl : ?warn:bool ->
vc:bool -> pmodule_uc -> Pdecl.pdecl -> pmodule_uc

add_pdecl ~vc m d adds declaration d in module m. If vc is true, VC is computed and added to m.

Builtin symbols

val builtin_module : pmodule
val bool_module : pmodule
val unit_module : pmodule
val highord_module : pmodule
val tuple_module : int -> pmodule

WhyML language

type mlw_file = pmodule Wstdlib.Mstr.t 
val mlw_language : mlw_file Env.language
val mlw_language_builtin : Env.pathname -> mlw_file
exception ModuleNotFound of Env.pathname * string
val read_module : Env.env -> Env.pathname -> string -> pmodule

Pretty-printing

val print_unit : Format.formatter -> mod_unit -> unit
val print_module : Format.formatter -> pmodule -> unit