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
  7. | MTid
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
  7. | MAid of Ident.ident
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
val meta_record : 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 restore_theory : Ident.ident -> theory
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
type bad_instance =
  1. | BadI of Ident.ident
  2. | BadI_ty_vars of Ty.tysymbol
  3. | BadI_ty_ner of Ty.tysymbol
  4. | BadI_ty_impure of Ty.tysymbol
  5. | BadI_ty_arity of Ty.tysymbol
  6. | BadI_ty_rec of Ty.tysymbol
  7. | BadI_ty_mut_lhs of Ty.tysymbol
  8. | BadI_ty_mut_rhs of Ty.tysymbol
  9. | BadI_ty_alias of Ty.tysymbol
  10. | BadI_field of Ty.tysymbol * Term.vsymbol
  11. | BadI_field_type of Ty.tysymbol * Term.vsymbol
  12. | BadI_field_ghost of Ty.tysymbol * Term.vsymbol
  13. | BadI_field_mut of Ty.tysymbol * Term.vsymbol
  14. | BadI_field_inv of Ty.tysymbol * Term.vsymbol
  15. | BadI_ls_type of Term.lsymbol
  16. | BadI_ls_kind of Term.lsymbol
  17. | BadI_ls_arity of Term.lsymbol
  18. | BadI_ls_rs of Term.lsymbol
  19. | BadI_rs_arity of Ident.ident
  20. | BadI_rs_type of Ident.ident
  21. | BadI_rs_kind of Ident.ident
  22. | BadI_rs_ghost of Ident.ident
  23. | BadI_rs_mask of Ident.ident
  24. | BadI_rs_reads of Ident.ident * Term.Svs.t
  25. | BadI_rs_writes of Ident.ident * Term.Svs.t
  26. | BadI_rs_taints of Ident.ident * Term.Svs.t
  27. | BadI_rs_covers of Ident.ident * Term.Svs.t
  28. | BadI_rs_resets of Ident.ident * Term.Svs.t
  29. | BadI_rs_raises of Ident.ident * Ident.Sid.t
  30. | BadI_rs_spoils of Ident.ident * Ty.Stv.t
  31. | BadI_rs_oneway of Ident.ident
  32. | BadI_xs_type of Ident.ident
  33. | 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 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