Previous  Up  Next

Module Theory

module Theory: sig .. end

Theories and Namespaces

type namespace = {
   ns_ts : Ty.tysymbol Wstdlib.Mstr.t;
   ns_ls : Term.lsymbol Wstdlib.Mstr.t;
   ns_pr : Decl.prsymbol Wstdlib.Mstr.t;
   ns_ns : namespace Wstdlib.Mstr.t;
} 
val empty_ns : namespace
val ns_find_ts : namespace -> string list -> Ty.tysymbol
val ns_find_ls : namespace -> string list -> Term.lsymbol
val ns_find_pr : namespace -> string list -> 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 Ty.ty
| MAts of Ty.tysymbol
| MAls of Term.lsymbol
| MApr of Decl.prsymbol
| MAstr of string
| MAint of int
| MAid of Ident.ident 
type meta = private {
   meta_name : string;
   meta_type : meta_arg_type list;
   meta_excl : bool;
   meta_desc : Pp.formatted;
   meta_tag : int;
} 
val print_meta_desc : 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:Pp.formatted -> string -> meta_arg_type list -> meta
val register_meta_excl : desc: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 : Ident.ident; (*

theory name

*)
   th_path : string list; (*

environment qualifiers

*)
   th_decls : tdecl list; (*

theory declarations

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

range type projections

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

float type projections

*)
   th_crcmap : Coercion.t; (*

implicit coercions

*)
   th_proved_wf : (Decl.prsymbol * Term.lsymbol) 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 : Decl.known_map; (*

known identifiers

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

locally declared idents

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

used theories

*)
} 
type tdecl = private {
   td_node : tdecl_node;
   td_tag : int;
} 
type tdecl_node =
| Decl of Decl.decl
| Use of theory
| Clone of theory * symbol_map
| Meta of meta * meta_arg list 
type symbol_map = {
   sm_ty : Ty.ty Ty.Mts.t;
   sm_ts : Ty.tysymbol Ty.Mts.t;
   sm_ls : Term.lsymbol Term.Mls.t;
   sm_pr : Decl.prsymbol 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 : Ident.ident;
   uc_path : string list;
   uc_decls : tdecl list;
   uc_ranges : tdecl Ty.Mts.t;
   uc_floats : tdecl Ty.Mts.t;
   uc_crcmap : Coercion.t;
   uc_proved_wf : (Decl.prsymbol * Term.lsymbol) Term.Mls.t; (*

see field th_proved_wf above

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

theories under constructions

val create_theory : ?path:string list -> 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 : 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 : Ident.ident -> theory

Declaration constructors

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

Use

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

Clone

type th_inst = {
   inst_ty : Ty.ty Ty.Mts.t;
   inst_ts : Ty.tysymbol Ty.Mts.t;
   inst_ls : Term.lsymbol Term.Mls.t;
   inst_pr : Decl.prop_kind Decl.Mpr.t;
   inst_df : Decl.prop_kind;
} 
val empty_inst : th_inst
val warn_clone_not_abstract : Loc.position -> theory -> unit
val warning_clone_not_abstract : Loc.warning_id
val warn_axiom_abstract : 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 -> Decl.decl -> theory_uc
type bad_instance =
| BadI of Ident.ident
| BadI_ty_vars of Ty.tysymbol
| BadI_ty_ner of Ty.tysymbol
| BadI_ty_impure of Ty.tysymbol
| BadI_ty_arity of Ty.tysymbol
| BadI_ty_rec of Ty.tysymbol
| BadI_ty_mut_lhs of Ty.tysymbol
| BadI_ty_mut_rhs of Ty.tysymbol
| BadI_ty_alias of Ty.tysymbol
| BadI_field of Ty.tysymbol * Term.vsymbol
| BadI_field_type of Ty.tysymbol * Term.vsymbol
| BadI_field_ghost of Ty.tysymbol * Term.vsymbol
| BadI_field_mut of Ty.tysymbol * Term.vsymbol
| BadI_field_inv of Ty.tysymbol * Term.vsymbol
| BadI_ls_type of Term.lsymbol * Ty.ty * Ty.ty
| BadI_ls_kind of Term.lsymbol
| BadI_ls_arity of Term.lsymbol
| BadI_ls_rs of Term.lsymbol
| BadI_rs_arity of Ident.ident
| BadI_rs_type of Ident.ident * exn
| BadI_rs_kind of Ident.ident
| BadI_rs_ghost of Ident.ident
| BadI_rs_mask of Ident.ident
| BadI_rs_reads of Ident.ident * Term.Svs.t
| BadI_rs_writes of Ident.ident * Term.Svs.t
| BadI_rs_taints of Ident.ident * Term.Svs.t
| BadI_rs_covers of Ident.ident * Term.Svs.t
| BadI_rs_resets of Ident.ident * Term.Svs.t
| BadI_rs_raises of Ident.ident * Ident.Sid.t
| BadI_rs_spoils of Ident.ident * Ty.Stv.t
| BadI_rs_oneway of Ident.ident
| BadI_xs_type of Ident.ident
| BadI_xs_mask of Ident.ident 
exception NonLocal of Ident.ident
exception BadInstance of bad_instance
exception CannotInstantiate of 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 Ty.tysymbol
exception FloatConflict of Ty.tysymbol
exception IllFormedWf of Decl.prsymbol * Term.lsymbol
exception ProvedWfConflict of Term.lsymbol