why3 1.2.0 · OCaml Package

why3

type prog_symbol =

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

type 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_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

val ref_attr : Ident.attribute

exception IncompatibleNotation of string

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;

}

and 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

and 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

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

val restore_module : Theory.theory -> pmodule

val use_export : pmodule_uc -> pmodule -> pmodule_uc

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

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

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

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

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

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

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

package why3