Module Theory

module Theory: sig .. end
Theories and Namespaces


Theories and Namespaces
type namespace = {
   ns_ts : Ty.tysymbol Stdlib.Mstr.t;
   ns_ls : Term.lsymbol Stdlib.Mstr.t;
   ns_pr : Decl.prsymbol Stdlib.Mstr.t;
   ns_ns : namespace Stdlib.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

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

Theories


type theory = private {
   th_name : Ident.ident;
   th_path : string list;
   th_decls : tdecl list;
   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 = private 
| Decl of Decl.decl
| Use of theory
| Clone of theory * symbol_map
| Meta of meta * meta_arg list
type symbol_map = private {
   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 
a theory under construction
val create_theory : ?path:string list -> Ident.preid -> theory_uc
val close_theory : theory_uc -> theory
val open_namespace : theory_uc -> string -> theory_uc
val close_namespace : theory_uc -> bool -> theory_uc
val get_namespace : theory_uc -> namespace
val get_known : theory_uc -> Decl.known_map
val get_rev_decls : theory_uc -> tdecl list
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

Use


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

Clone


type th_inst = {
   inst_ts : Ty.tysymbol Ty.Mts.t;
   inst_ls : Term.lsymbol Term.Mls.t;
   inst_lemma : Decl.Spr.t;
   inst_goal : Decl.Spr.t;
}
val empty_inst : th_inst
val create_inst : ts:(Ty.tysymbol * Ty.tysymbol) list ->
ls:(Term.lsymbol * Term.lsymbol) list ->
lemma:Decl.prsymbol list -> goal:Decl.prsymbol list -> 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 create_null_clone : theory -> tdecl
val is_empty_sm : symbol_map -> bool

Meta


val create_meta : meta -> meta_arg list -> tdecl
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
val clone_meta : tdecl -> symbol_map -> tdecl
clone_meta td_meta sm produces from td_meta a new Meta tdecl instantiated with respect to sm.

Base theories


val builtin_theory : theory
val bool_theory : theory
val unit_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 CannotInstantiate of Ident.ident
exception BadInstance of Ident.ident * 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