Previous  Up  Next

Module Theory

module Theory: sig .. end

Theories and Namespaces

type namespace = {
   ns_ts : Why3.Ty.tysymbol Why3.Wstdlib.Mstr.t;
   ns_ls : Why3.Term.lsymbol Why3.Wstdlib.Mstr.t;
   ns_pr : Why3.Decl.prsymbol Why3.Wstdlib.Mstr.t;
   ns_ns : namespace Why3.Wstdlib.Mstr.t;
} 
val empty_ns : namespace
val ns_find_ts : namespace -> string list -> Why3.Ty.tysymbol
val ns_find_ls : namespace -> string list -> Why3.Term.lsymbol
val ns_find_pr : namespace -> string list -> Why3.Decl.prsymbol
val ns_find_ns : namespace -> string list -> namespace
val import_namespace : namespace -> string list -> namespace

Meta properties

type meta_arg_type =
| MTty
| MTtysymbol
| MTlsymbol
| MTprsymbol
| MTstring
| MTint
| MTid 
type meta_arg =
| MAty of Why3.Ty.ty
| MAts of Why3.Ty.tysymbol
| MAls of Why3.Term.lsymbol
| MApr of Why3.Decl.prsymbol
| MAstr of string
| MAint of int
| MAid of Why3.Ident.ident 
type meta = private {
   meta_name : string;
   meta_type : meta_arg_type list;
   meta_excl : bool;
   meta_desc : Why3.Pp.formatted;
   meta_tag : int;
} 
val print_meta_desc : Why3.Pp.formatter -> meta -> unit
module Mmeta: Extmap.S  with type key = meta
module Smeta: Extset.S  with module M = Mmeta
module Hmeta: Exthtbl.S  with type key = meta
val meta_equal : meta -> meta -> bool
val meta_hash : meta -> int
val register_meta : desc:Why3.Pp.formatted -> string -> meta_arg_type list -> meta
val register_meta_excl : desc:Why3.Pp.formatted -> string -> meta_arg_type list -> meta

With exclusive metas, each new meta cancels the previous one. Useful for transformation or printer parameters

val lookup_meta : string -> meta
val list_metas : unit -> meta list
val meta_range : meta
val meta_float : meta
val meta_model_projection : meta

meta declaring a function symbol p of type t1 -> t2 as a model projection for type `t1`, meaning that when a counterexample value is requested for a variable x of type t1, then a value for p x is queried

val meta_record : meta
val meta_proved_wf : meta

meta used to declare than a given predicate symbol is proved well-founded

Theories

type theory = private {
   th_name : Why3.Ident.ident; (*

theory name

*)
   th_path : string list; (*

environment qualifiers

*)
   th_decls : tdecl list; (*

theory declarations

*)
   th_ranges : tdecl Why3.Ty.Mts.t; (*

range type projections

*)
   th_floats : tdecl Why3.Ty.Mts.t; (*

float type projections

*)
   th_crcmap : Why3.Coercion.t; (*

implicit coercions

*)
   th_proved_wf : (Why3.Decl.prsymbol * Why3.Term.lsymbol) Why3.Term.Mls.t; (*

Mapping of predicate symbols r to symbols pr,wf, for which a meta "vc:proved_wf" r pr was set, and pr checked to refer to a proposition of the form (wf r). Note that wf is any lsymbol, it is NOT checked that it is equal to the stdlib symbol relations.WellFounded.well_founded (it is too early to do that in this module).

*)
   th_export : namespace; (*

exported namespace

*)
   th_known : Why3.Decl.known_map; (*

known identifiers

*)
   th_local : Why3.Ident.Sid.t; (*

locally declared idents

*)
   th_used : Why3.Ident.Sid.t; (*

used theories

*)
} 
type tdecl = private {
   td_node : tdecl_node;
   td_tag : int;
} 
type tdecl_node =
| Decl of Why3.Decl.decl
| Use of theory
| Clone of theory * symbol_map
| Meta of meta * meta_arg list 
type symbol_map = {
   sm_ty : Why3.Ty.ty Why3.Ty.Mts.t;
   sm_ts : Why3.Ty.tysymbol Why3.Ty.Mts.t;
   sm_ls : Why3.Term.lsymbol Why3.Term.Mls.t;
   sm_pr : Why3.Decl.prsymbol Why3.Decl.Mpr.t;
} 
module Mtdecl: Extmap.S  with type key = tdecl
module Stdecl: Extset.S  with module M = Mtdecl
module Htdecl: Exthtbl.S  with type key = tdecl
val td_equal : tdecl -> tdecl -> bool
val td_hash : tdecl -> int

Constructors and utilities

type theory_uc = private {
   uc_name : Why3.Ident.preid;
   uc_path : string list;
   uc_decls : tdecl list;
   uc_ranges : tdecl Why3.Ty.Mts.t;
   uc_floats : tdecl Why3.Ty.Mts.t;
   uc_crcmap : Why3.Coercion.t;
   uc_proved_wf : (Why3.Decl.prsymbol * Why3.Term.lsymbol) Why3.Term.Mls.t; (*

see field th_proved_wf above

*)
   uc_prefix : string list;
   uc_import : namespace list;
   uc_export : namespace list;
   uc_known : Why3.Decl.known_map;
   uc_local : Why3.Ident.Sid.t;
   uc_used : Why3.Ident.Sid.t;
}

theories under constructions

val create_theory : ?path:string list -> Why3.Ident.preid -> theory_uc
val close_theory : theory_uc -> theory
val open_scope : theory_uc -> string -> theory_uc
val close_scope : theory_uc -> import:bool -> theory_uc
val import_scope : theory_uc -> string list -> theory_uc
val get_namespace : theory_uc -> namespace
val restore_path : Why3.Ident.ident -> string list * string * string list

restore_path id returns the triple (library path, theory, qualified symbol name) if the ident was ever introduced in a theory declaration. If the ident was declared in several different theories, the first association is retained. If id is a theory name, the third component is an empty list. Raises Not_found if the ident was never declared in/as a theory.

val restore_theory : Why3.Ident.ident -> theory

Declaration constructors

val create_decl : Why3.Decl.decl -> tdecl
val add_decl : ?warn:bool -> theory_uc -> Why3.Decl.decl -> theory_uc
val add_ty_decl : theory_uc -> Why3.Ty.tysymbol -> theory_uc
val add_data_decl : theory_uc -> Why3.Decl.data_decl list -> theory_uc
val add_param_decl : theory_uc -> Why3.Term.lsymbol -> theory_uc
val add_logic_decl : theory_uc -> Why3.Decl.logic_decl list -> theory_uc
val add_ind_decl : theory_uc ->
       Why3.Decl.ind_sign -> Why3.Decl.ind_decl list -> theory_uc
val add_prop_decl : ?warn:bool ->
       theory_uc ->
       Why3.Decl.prop_kind ->
       Why3.Decl.prsymbol -> Why3.Term.term -> theory_uc
val attr_w_non_conservative_extension_no : Why3.Ident.attribute

Use

val create_use : theory -> tdecl
val use_export : theory_uc -> theory -> theory_uc

Clone

type th_inst = {
   inst_ty : Why3.Ty.ty Why3.Ty.Mts.t;
   inst_ts : Why3.Ty.tysymbol Why3.Ty.Mts.t;
   inst_ls : Why3.Term.lsymbol Why3.Term.Mls.t;
   inst_pr : Why3.Decl.prop_kind Why3.Decl.Mpr.t;
   inst_df : Why3.Decl.prop_kind;
} 
val empty_inst : th_inst
val warn_clone_not_abstract : Why3.Loc.position -> theory -> unit
val warning_clone_not_abstract : Why3.Loc.warning_id
val warn_axiom_abstract : Why3.Loc.warning_id
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val add_clone_internal : unit ->
       theory_uc -> theory -> symbol_map -> theory_uc

Meta

val meta_coercion : meta
val create_meta : meta -> meta_arg list -> tdecl
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
val clone_meta : tdecl -> theory -> symbol_map -> tdecl option

clone_meta td_meta th sm produces from td_meta a new Meta tdecl instantiated with respect to sm. Returns None if td_meta mentions proposition symbols that were not cloned (e.g. goals) or type symbols that were cloned into complex types.

Base theories

val builtin_theory : theory
val ignore_theory : theory
val bool_theory : theory
val highord_theory : theory
val tuple_theory : int -> theory
val tuple_theory_name : string -> int option
val add_decl_with_tuples : theory_uc -> Why3.Decl.decl -> theory_uc
type bad_instance =
| BadI of Why3.Ident.ident
| BadI_ty_vars of Why3.Ty.tysymbol
| BadI_ty_ner of Why3.Ty.tysymbol
| BadI_ty_impure of Why3.Ty.tysymbol
| BadI_ty_arity of Why3.Ty.tysymbol
| BadI_ty_rec of Why3.Ty.tysymbol
| BadI_ty_mut_lhs of Why3.Ty.tysymbol
| BadI_ty_mut_rhs of Why3.Ty.tysymbol
| BadI_ty_alias of Why3.Ty.tysymbol
| BadI_field of Why3.Ty.tysymbol * Why3.Term.vsymbol
| BadI_field_type of Why3.Ty.tysymbol * Why3.Term.vsymbol
| BadI_field_ghost of Why3.Ty.tysymbol * Why3.Term.vsymbol
| BadI_field_mut of Why3.Ty.tysymbol * Why3.Term.vsymbol
| BadI_field_inv of Why3.Ty.tysymbol * Why3.Term.vsymbol
| BadI_ls_type of Why3.Term.lsymbol * Why3.Ty.ty * Why3.Ty.ty
| BadI_ls_kind of Why3.Term.lsymbol
| BadI_ls_arity of Why3.Term.lsymbol
| BadI_ls_rs of Why3.Term.lsymbol
| BadI_rs_arity of Why3.Ident.ident
| BadI_rs_type of Why3.Ident.ident * exn
| BadI_rs_kind of Why3.Ident.ident
| BadI_rs_ghost of Why3.Ident.ident
| BadI_rs_mask of Why3.Ident.ident
| BadI_rs_reads of Why3.Ident.ident * Why3.Term.Svs.t
| BadI_rs_writes of Why3.Ident.ident * Why3.Term.Svs.t
| BadI_rs_taints of Why3.Ident.ident * Why3.Term.Svs.t
| BadI_rs_covers of Why3.Ident.ident * Why3.Term.Svs.t
| BadI_rs_resets of Why3.Ident.ident * Why3.Term.Svs.t
| BadI_rs_raises of Why3.Ident.ident * Why3.Ident.Sid.t
| BadI_rs_spoils of Why3.Ident.ident * Why3.Ty.Stv.t
| BadI_rs_oneway of Why3.Ident.ident
| BadI_xs_type of Why3.Ident.ident
| BadI_xs_mask of Why3.Ident.ident 
exception NonLocal of Why3.Ident.ident
exception BadInstance of bad_instance
exception CannotInstantiate of Why3.Ident.ident
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
exception KnownMeta of meta
exception UnknownMeta of string
exception BadMetaArity of meta * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
exception IllFormedMeta of meta * string
exception RangeConflict of Why3.Ty.tysymbol
exception FloatConflict of Why3.Ty.tysymbol
exception IllFormedWf of Why3.Decl.prsymbol * Why3.Term.lsymbol
exception ProvedWfConflict of Why3.Term.lsymbol