package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type itysymbol = private {
  1. its_ts : Ty.tysymbol;
  2. its_nonfree : bool;
  3. its_private : bool;
  4. its_mutable : bool;
  5. its_fragile : bool;
  6. its_mfields : pvsymbol list;
  7. its_ofields : pvsymbol list;
  8. its_regions : region list;
  9. its_arg_flg : its_flag list;
  10. its_reg_flg : its_flag list;
  11. its_def : ity Ty.type_def;
}
and its_flag = private {
  1. its_frozen : bool;
  2. its_exposed : bool;
  3. its_liable : bool;
  4. its_fixed : bool;
  5. its_visible : bool;
}
and ity = private {
  1. ity_node : ity_node;
  2. ity_pure : bool;
  3. ity_tag : Weakhtbl.tag;
}
and ity_node = private
  1. | Ityreg of region
  2. | Ityapp of itysymbol * ity list * ity list
  3. | Ityvar of Ty.tvsymbol
and region = private {
  1. reg_name : Ident.ident;
  2. reg_its : itysymbol;
  3. reg_args : ity list;
  4. reg_regs : ity list;
}
and pvsymbol = private {
  1. pv_vs : Term.vsymbol;
  2. pv_ity : ity;
  3. pv_ghost : bool;
}
module Mits : sig ... end
module Sits : sig ... end
module Hits : sig ... end
module Wits : sig ... end
module Mity : sig ... end
module Sity : sig ... end
module Hity : sig ... end
module Wity : sig ... end
module Mreg : sig ... end
module Sreg : sig ... end
module Hreg : sig ... end
module Wreg : sig ... end
module Mpv : sig ... end
module Spv : sig ... end
module Hpv : sig ... end
module Wpv : sig ... end
val its_compare : itysymbol -> itysymbol -> int
val ity_compare : ity -> ity -> int
val reg_compare : region -> region -> int
val pv_compare : pvsymbol -> pvsymbol -> int
val its_equal : itysymbol -> itysymbol -> bool
val ity_equal : ity -> ity -> bool
val reg_equal : region -> region -> bool
val pv_equal : pvsymbol -> pvsymbol -> bool
val its_hash : itysymbol -> int
val ity_hash : ity -> int
val reg_hash : region -> int
val pv_hash : pvsymbol -> int
exception DuplicateRegion of region
exception UnboundRegion of region
val create_plain_record_itysymbol : priv:bool -> mut:bool -> Ident.preid -> Ty.tvsymbol list -> bool Mpv.t -> Term.term list -> itysymbol
val create_plain_variant_itysymbol : Ident.preid -> Ty.tvsymbol list -> Spv.t list -> itysymbol
val create_rec_itysymbol : Ident.preid -> Ty.tvsymbol list -> itysymbol
val create_alias_itysymbol : Ident.preid -> Ty.tvsymbol list -> ity -> itysymbol
val create_range_itysymbol : Ident.preid -> Number.int_range -> itysymbol
val create_float_itysymbol : Ident.preid -> Number.float_format -> itysymbol
val restore_its : Ty.tysymbol -> itysymbol
val its_pure : itysymbol -> bool
val ity_closed : ity -> bool
val ity_fragile : ity -> bool
exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
val create_region : Ident.preid -> itysymbol -> ity list -> ity list -> region
val ity_app : itysymbol -> ity list -> ity list -> ity
val ity_app_pure : itysymbol -> ity list -> ity list -> ity
val ity_reg : region -> ity
val ity_var : Ty.tvsymbol -> ity
val ity_purify : ity -> ity
val ity_of_ty : Ty.ty -> ity
val ity_of_ty_pure : Ty.ty -> ity
val ty_of_ity : ity -> Ty.ty
val ity_fold : ('a -> ity -> 'a) -> 'a -> ity -> 'a
val reg_fold : ('a -> ity -> 'a) -> 'a -> region -> 'a
val ity_s_fold : ('a -> itysymbol -> 'a) -> 'a -> ity -> 'a
val reg_s_fold : ('a -> itysymbol -> 'a) -> 'a -> region -> 'a
val ity_v_fold : ('a -> Ty.tvsymbol -> 'a) -> 'a -> ity -> 'a
val reg_v_fold : ('a -> Ty.tvsymbol -> 'a) -> 'a -> region -> 'a
val ity_freevars : Ty.Stv.t -> ity -> Ty.Stv.t
val reg_freevars : Ty.Stv.t -> region -> Ty.Stv.t
val ity_v_occurs : Ty.tvsymbol -> ity -> bool
val reg_v_occurs : Ty.tvsymbol -> region -> bool
val ity_r_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_r_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
val ity_freeregs : Sreg.t -> ity -> Sreg.t
val reg_freeregs : Sreg.t -> region -> Sreg.t
val ity_r_occurs : region -> ity -> bool
val reg_r_occurs : region -> region -> bool
val ity_exp_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_exp_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
val ity_rch_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_rch_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
val ity_r_reachable : region -> ity -> bool
val reg_r_reachable : region -> region -> bool
val ity_r_stale : Sreg.t -> Sreg.t -> ity -> bool
val reg_r_stale : Sreg.t -> Sreg.t -> region -> bool
val ity_frz_regs : Sreg.t -> ity -> Sreg.t
val ts_unit : Ty.tysymbol
val ty_unit : Ty.ty
val its_int : itysymbol
val its_real : itysymbol
val its_bool : itysymbol
val its_str : itysymbol
val its_unit : itysymbol
val its_func : itysymbol
val ity_int : ity
val ity_real : ity
val ity_bool : ity
val ity_str : ity
val ity_unit : ity
val ity_func : ity -> ity -> ity
val ity_pred : ity -> ity
val its_tuple : int -> itysymbol
val ity_tuple : ity list -> ity
type ity_subst = private {
  1. isb_var : ity Ty.Mtv.t;
  2. isb_reg : ity Mreg.t;
}
exception TypeMismatch of ity * ity * ity_subst
val isb_empty : ity_subst
val ity_match : ity_subst -> ity -> ity -> ity_subst
val reg_match : ity_subst -> region -> ity -> ity_subst
val its_match_args : itysymbol -> ity list -> ity_subst
val its_match_regs : itysymbol -> ity list -> ity list -> ity_subst
val ity_freeze : ity_subst -> ity -> ity_subst
val reg_freeze : ity_subst -> region -> ity_subst
val ity_equal_check : ity -> ity -> unit
val reg_equal_check : region -> region -> unit
val ity_full_inst : ity_subst -> ity -> ity
val reg_full_inst : ity_subst -> region -> ity
val create_pvsymbol : Ident.preid -> ?ghost:bool -> ity -> pvsymbol
val restore_pv : Term.vsymbol -> pvsymbol
val t_freepvs : Spv.t -> Term.term -> Spv.t
val pvs_of_vss : Spv.t -> 'a Term.Mvs.t -> Spv.t
type mask =
  1. | MaskVisible
  2. | MaskTuple of mask list
  3. | MaskGhost
val mask_ghost : mask -> bool
val mask_of_pv : pvsymbol -> mask
val mask_union : mask -> mask -> mask
val mask_equal : mask -> mask -> bool
val mask_spill : mask -> mask -> bool
type xsymbol = private {
  1. xs_name : Ident.ident;
  2. xs_ity : ity;
  3. xs_mask : mask;
}
module Mxs : sig ... end
module Sxs : sig ... end
val xs_compare : xsymbol -> xsymbol -> int
val xs_equal : xsymbol -> xsymbol -> bool
val xs_hash : xsymbol -> int
val create_xsymbol : Ident.preid -> ?mask:mask -> ity -> xsymbol
exception IllegalSnapshot of ity
exception IllegalAlias of region
exception AssignPrivate of region
exception AssignSnapshot of ity
exception WriteImmutable of region * pvsymbol
exception IllegalUpdate of pvsymbol * region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception IllegalAssign of region * region * region
exception ImpureVariable of Ty.tvsymbol * ity
exception GhostDivergence
type oneway =
  1. | Total
  2. | Partial
  3. | Diverges
val total : oneway -> bool
val partial : oneway -> bool
val diverges : oneway -> bool
type effect = private {
  1. eff_reads : Spv.t;
  2. eff_writes : Spv.t Mreg.t;
  3. eff_taints : Sreg.t;
  4. eff_covers : Sreg.t;
  5. eff_resets : Sreg.t;
  6. eff_raises : Sxs.t;
  7. eff_spoils : Ty.Stv.t;
  8. eff_oneway : oneway;
  9. eff_ghost : bool;
}
val eff_empty : effect
val eff_equal : effect -> effect -> bool
val eff_pure : effect -> bool
val eff_read : Spv.t -> effect
val eff_write : Spv.t -> Spv.t Mreg.t -> effect
val eff_assign : (pvsymbol * pvsymbol * pvsymbol) list -> effect
val eff_read_pre : Spv.t -> effect -> effect
val eff_read_post : effect -> Spv.t -> effect
val eff_bind : Spv.t -> effect -> effect
val eff_read_single : pvsymbol -> effect
val eff_read_single_pre : pvsymbol -> effect -> effect
val eff_read_single_post : effect -> pvsymbol -> effect
val eff_bind_single : pvsymbol -> effect -> effect
val eff_reset : effect -> Sreg.t -> effect
val eff_reset_overwritten : effect -> effect
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
val eff_spoil : effect -> ity -> effect
val eff_partial : effect -> effect
val eff_diverge : effect -> effect
val eff_ghostify : bool -> effect -> effect
val eff_ghostify_weak : bool -> effect -> effect
val eff_union_seq : effect -> effect -> effect
val eff_union_par : effect -> effect -> effect
val mask_adjust : effect -> ity -> mask -> mask
val eff_escape : effect -> ity -> Sity.t
val ity_affected : 'a Mreg.t -> ity -> bool
val pv_affected : 'a Mreg.t -> pvsymbol -> bool
val pvs_affected : 'a Mreg.t -> Spv.t -> Spv.t
type pre = Term.term
type post = Term.term
val open_post : post -> Term.vsymbol * Term.term
val open_post_with : Term.term -> post -> Term.term
val clone_post_result : post -> Ident.preid
val create_post : Term.vsymbol -> Term.term -> post
val annot_attr : Ident.attribute
val break_attr : Ident.attribute
type cty = private {
  1. cty_args : pvsymbol list;
  2. cty_pre : pre list;
  3. cty_post : post list;
  4. cty_xpost : post list Mxs.t;
  5. cty_oldies : pvsymbol Mpv.t;
  6. cty_effect : effect;
  7. cty_result : ity;
  8. cty_mask : mask;
  9. cty_freeze : ity_subst;
}
val create_cty : ?mask:mask -> pvsymbol list -> pre list -> post list -> post list Mxs.t -> pvsymbol Mpv.t -> effect -> ity -> cty
val create_cty_defensive : ?mask:mask -> pvsymbol list -> pre list -> post list -> post list Mxs.t -> pvsymbol Mpv.t -> effect -> ity -> cty
val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty
val cty_tuple : pvsymbol list -> cty
val cty_exec : cty -> cty
val cty_exec_post : cty -> post list
val cty_ghost : cty -> bool
val cty_pure : cty -> bool
val cty_ghostify : bool -> cty -> cty
val cty_reads : cty -> Spv.t
val cty_read_pre : Spv.t -> cty -> cty
val cty_read_post : cty -> Spv.t -> cty
val cty_add_pre : pre list -> cty -> cty
val cty_add_post : cty -> post list -> cty
val forget_reg : region -> unit
val forget_pv : pvsymbol -> unit
val forget_xs : xsymbol -> unit
val forget_cty : cty -> unit
val print_its : Format.formatter -> itysymbol -> unit
val print_reg : Format.formatter -> region -> unit
val print_ity : Format.formatter -> ity -> unit
val print_ity_full : Format.formatter -> ity -> unit
val print_xs : Format.formatter -> xsymbol -> unit
val print_pv : Format.formatter -> pvsymbol -> unit
val print_pvty : Format.formatter -> pvsymbol -> unit
val print_cty : Format.formatter -> cty -> unit
val print_spec : pvsymbol list -> pre list -> post list -> post list Mxs.t -> pvsymbol Mpv.t -> effect -> Format.formatter -> ity option -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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