package why3

  1. Overview
  2. Docs
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_regions : region list;
  8. its_arg_flg : its_flag list;
  9. its_reg_flg : its_flag list;
  10. 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 ts_unit : Ty.tysymbol
val ty_unit : Ty.ty
val its_int : itysymbol
val its_real : itysymbol
val its_bool : itysymbol
val its_unit : itysymbol
val its_func : itysymbol
val ity_int : ity
val ity_real : ity
val ity_bool : 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 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 : bool;
  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_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
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.