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

Theories

type theory = private {
   th_name : Ident.ident;
   th_path : string list;
   th_decls : tdecl list;
   th_ranges : tdecl Ty.Mts.t;
   th_floats : tdecl Ty.Mts.t;
   th_crcmap : Coercion.t;
   th_export : namespace;
   th_known : Decl.known_map;
   th_local : Ident.Sid.t;
   th_used : Ident.Sid.t;
}
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_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;
}
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.

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 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 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
exception NonLocal of Ident.ident
exception BadInstance of Ident.ident
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 RangeConflict of Ty.tysymbol
exception FloatConflict of Ty.tysymbol