Module Pmodule

module Pmodule: sig .. end

WhyML program modules

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 empty_ns : namespace

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_xs : namespace -> string list -> Ity.xsymbol

val ns_find_ns : namespace -> string list -> namespace

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

type overload =

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

val overload_of_rs : Expr.rsymbol -> overload

val overload_of_oo : Expr.Srs.t -> overload

val ref_attr : Ident.attribute

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_id : 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 : 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:Loc.position ->
       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.

val mod_impl : Env.env -> pmodule -> pmodule

val mod_impl_register : Env.env -> pmodule -> pmodule -> mod_inst -> unit

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 : 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

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 : Stdlib.Format.formatter -> mod_unit -> unit

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