Module Pmodule

module Pmodule: sig .. end

WhyML program modules

type prog_symbol =

`\|`	`PV of Why3.Ity.pvsymbol`
`\|`	`RS of Why3.Expr.rsymbol`
`\|`	`OO of Why3.Expr.Srs.t`

type namespace = {

	`ns_ts : Why3.Ity.itysymbol Why3.Wstdlib.Mstr.t;`
	`ns_ps : prog_symbol Why3.Wstdlib.Mstr.t;`
	`ns_xs : Why3.Ity.xsymbol Why3.Wstdlib.Mstr.t;`
	`ns_ns : namespace Why3.Wstdlib.Mstr.t;`

}

val empty_ns : namespace

val ns_find_prog_symbol : namespace -> string list -> prog_symbol

val ns_find_its : namespace -> string list -> Why3.Ity.itysymbol

val ns_find_pv : namespace -> string list -> Why3.Ity.pvsymbol

val ns_find_xs : namespace -> string list -> Why3.Ity.xsymbol

val ns_find_ns : namespace -> string list -> namespace

val ns_find_rs : namespace -> string list -> Why3.Expr.rsymbol

type overload =

`\|`	`FixedRes of Why3.Ity.ity`
`\|`	`SameType`
`\|`	`NoOver`

val overload_of_rs : Why3.Expr.rsymbol -> overload

val overload_of_oo : Why3.Expr.Srs.t -> overload

val ref_attr : Why3.Ident.attribute

exception IncompatibleNotation of string

Module

type pmodule0 = private {

	`mod_theory : Why3.Theory.theory;`
	`mod_units : mod_unit list;`
	`mod_export : namespace;`
	`mod_known : Why3.Pdecl.known_map;`
	`mod_local : Why3.Ident.Sid.t;`
	`mod_used : Why3.Ident.Sid.t;`

}

type mod_unit =

`\|`	`Udecl of Why3.Pdecl.pdecl`
`\|`	`Uuse of pmodule0`
`\|`	`Uclone of mod_inst`
`\|`	`Umeta of Why3.Theory.meta * Why3.Theory.meta_arg list`
`\|`	`Uscope of string * mod_unit list`

type mod_inst = {

	`mi_mod : pmodule0;`
	`mi_ty : Why3.Ity.ity Why3.Ty.Mts.t;`
	`mi_ts : Why3.Ity.itysymbol Why3.Ty.Mts.t;`
	`mi_ls : Why3.Term.lsymbol Why3.Term.Mls.t;`
	`mi_pr : Why3.Decl.prsymbol Why3.Decl.Mpr.t;`
	`mi_pk : Why3.Decl.prop_kind Why3.Decl.Mpr.t;`
	`mi_pv : Why3.Ity.pvsymbol Why3.Term.Mvs.t;`
	`mi_rs : Why3.Expr.rsymbol Why3.Expr.Mrs.t;`
	`mi_xs : Why3.Ity.xsymbol Why3.Ity.Mxs.t;`
	`mi_df : Why3.Decl.prop_kind;`

}

type pmodule = private {

	`mod_inst : mod_inst;`
	`mod_intf : pmodule0;`
	`mod_impl : pmodule0;`

}

A pmodule m consists of two old-style pmodule0. Its interface m.mod_intf is the "logical" version of the module, to be used in most place. It is a copy of I in the case of a module A : I module. Its implementation m.mod_impl is the "execution" version of the module, to be used during extraction or execution. It corresponds to the body of A in the module A : I case. m.mod_inst maps the symbols from the interface to the corresponding ones in the implementation.

val mod_name : pmodule -> Why3.Ident.ident

returns the name of the given pmodule, that is the name of is interface.

val mod_theory : pmodule -> Why3.Theory.theory

returns the pmodule's theory, that is, the theory of its interface.

val mod_export_intf : pmodule -> namespace

returns the mod_export field from the interface of this pmodule

val mod_export_impl : pmodule -> namespace

returns the mod_export field from the implementation of this pmodule

val mod_known_intf : pmodule -> Why3.Pdecl.known_map

returns the mod_known field from the interface of this pmodule

val mod_known_impl : pmodule -> Why3.Pdecl.known_map

returns the mod_known field from the implementation of this pmodule

val empty_mod_inst : pmodule -> mod_inst

Module under construction

type pmodule_uc0 = private {

	`muc_theory : Why3.Theory.theory_uc;`
	`muc_units : mod_unit list;`
	`muc_import : namespace list;`
	`muc_export : namespace list;`
	`muc_known : Why3.Pdecl.known_map;`
	`muc_local : Why3.Ident.Sid.t;`
	`muc_used : Why3.Ident.Sid.t;`
	`muc_env : Why3.Env.env;`

}

type pmodule_uc = private {

	`muc_intf : pmodule_uc0;`
	`muc_impl : pmodule_uc0;`

}

val create_module : Why3.Env.env -> ?path:string list -> Why3.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 : Why3.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_id : Why3.Ident.ident -> pmodule

retrieves a module from a program symbol defined in it Raises Not_found if the ident was never declared in/as a module.

val restore_module : Why3.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 : ?loc:Why3.Loc.position ->
       pmodule_uc ->
       pmodule -> mod_inst -> pmodule_uc

Logic decls

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

Program decls

val add_pdecl : ?warn:bool ->
       vc:bool -> pmodule_uc -> Why3.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.

val close_module_with_intf : pmodule_uc -> pmodule -> pmodule * pmodule

Builtin symbols

val builtin_module : pmodule

val bool_module : pmodule

val unit_module : pmodule

val highord_module : pmodule

val tuple_module : int -> pmodule

val ref_module : pmodule

val its_ref : Why3.Ity.itysymbol

val ts_ref : Why3.Ty.tysymbol

val rs_ref : Why3.Expr.rsymbol

val rs_ref_cons : Why3.Expr.rsymbol

val rs_ref_proj : Why3.Expr.rsymbol

val ls_ref_cons : Why3.Term.lsymbol

val ls_ref_proj : Why3.Term.lsymbol

WhyML language

type mlw_file = pmodule Why3.Wstdlib.Mstr.t

val mlw_language : mlw_file Why3.Env.language

val mlw_language_builtin : Why3.Env.pathname -> mlw_file

exception ModuleNotFound of Why3.Env.pathname * string

val read_module : Why3.Env.env -> Why3.Env.pathname -> string -> pmodule

Pretty-printing

val print_unit : Stdlib.Format.formatter -> mod_unit -> unit

val print_module : Stdlib.Format.formatter -> pmodule -> unit