package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
type meta_arg_type =
  1. | MTty
  2. | MTtysymbol
  3. | MTlsymbol
  4. | MTprsymbol
  5. | MTstring
  6. | MTint
type meta_arg =
  1. | MAty of Ty.ty
  2. | MAts of Ty.tysymbol
  3. | MAls of Term.lsymbol
  4. | MApr of Decl.prsymbol
  5. | MAstr of string
  6. | MAint of int
type meta = private {
  1. meta_name : string;
  2. meta_type : meta_arg_type list;
  3. meta_excl : bool;
  4. meta_desc : Pp.formatted;
  5. meta_tag : int;
}
val print_meta_desc : Pp.formatter -> meta -> unit
module Mmeta : sig ... end
module Smeta : sig ... end
module Hmeta : sig ... end
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
val lookup_meta : string -> meta
val list_metas : unit -> meta list
val meta_range : meta
val meta_float : meta
val meta_projection : meta
type theory = private {
  1. th_name : Ident.ident;
  2. th_path : string list;
  3. th_decls : tdecl list;
  4. th_ranges : tdecl Ty.Mts.t;
  5. th_floats : tdecl Ty.Mts.t;
  6. th_crcmap : Coercion.t;
  7. th_export : namespace;
  8. th_known : Decl.known_map;
  9. th_local : Ident.Sid.t;
  10. th_used : Ident.Sid.t;
}
and tdecl = private {
  1. td_node : tdecl_node;
  2. td_tag : int;
}
and tdecl_node =
  1. | Decl of Decl.decl
  2. | Use of theory
  3. | Clone of theory * symbol_map
  4. | Meta of meta * meta_arg list
and symbol_map = {
  1. sm_ty : Ty.ty Ty.Mts.t;
  2. sm_ts : Ty.tysymbol Ty.Mts.t;
  3. sm_ls : Term.lsymbol Term.Mls.t;
  4. sm_pr : Decl.prsymbol Decl.Mpr.t;
}
module Mtdecl : sig ... end
module Stdecl : sig ... end
module Htdecl : sig ... end
val td_equal : tdecl -> tdecl -> bool
val td_hash : tdecl -> int
type theory_uc = private {
  1. uc_name : Ident.ident;
  2. uc_path : string list;
  3. uc_decls : tdecl list;
  4. uc_ranges : tdecl Ty.Mts.t;
  5. uc_floats : tdecl Ty.Mts.t;
  6. uc_crcmap : Coercion.t;
  7. uc_prefix : string list;
  8. uc_import : namespace list;
  9. uc_export : namespace list;
  10. uc_known : Decl.known_map;
  11. uc_local : Ident.Sid.t;
  12. 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
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
val create_use : theory -> tdecl
val use_export : theory_uc -> theory -> theory_uc
type th_inst = {
  1. inst_ty : Ty.ty Ty.Mts.t;
  2. inst_ts : Ty.tysymbol Ty.Mts.t;
  3. inst_ls : Term.lsymbol Term.Mls.t;
  4. inst_pr : Decl.prop_kind Decl.Mpr.t;
  5. 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
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
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct