Previous  Up  Next

Module Ity

module Ity: sig .. end

Types in WhyML programs

Individual types are first-order types without effects.

Computation types are higher-order types with effects.

Individual types (first-order types without effects)

type itysymbol = private {
   its_ts : Ty.tysymbol; (*

logical type symbol

*)
   its_nonfree : bool; (*

has no constructors

*)
   its_private : bool; (*

private type

*)
   its_mutable : bool; (*

mutable type

*)
   its_fragile : bool; (*

breakable invariant

*)
   its_mfields : pvsymbol list; (*

mutable record fields

*)
   its_ofields : pvsymbol list; (*

non-mutable fields

*)
   its_regions : region list; (*

shareable components

*)
   its_arg_flg : its_flag list; (*

flags for type args

*)
   its_reg_flg : its_flag list; (*

flags for regions

*)
   its_def : ity Ty.type_def; (*

type definition

*)
} 
type its_flag = private {
   its_frozen : bool; (*

cannot be updated

*)
   its_exposed : bool; (*

directly reachable from a field

*)
   its_liable : bool; (*

exposed in the type invariant

*)
   its_fixed : bool; (*

exposed in a non-mutable field

*)
   its_visible : bool; (*

visible from the non-ghost code

*)
} 
type ity = private {
   ity_node : ity_node;
   ity_pure : bool;
   ity_tag : Weakhtbl.tag;
} 
type ity_node = private
| Ityreg of region (*

record with mutable fields and shareable components

*)
| Ityapp of itysymbol * ity list * ity list (*

immutable type with shareable components

*)
| Ityvar of Ty.tvsymbol (*

type variable

*) 
type region = private {
   reg_name : Ident.ident;
   reg_its : itysymbol;
   reg_args : ity list;
   reg_regs : ity list;
} 
type pvsymbol = private {
   pv_vs : Term.vsymbol;
   pv_ity : ity;
   pv_ghost : bool;
} 
module Mits: Extmap.S  with type key = itysymbol
module Sits: Extset.S  with module M = Mits
module Hits: Exthtbl.S  with type key = itysymbol
module Wits: Weakhtbl.S  with type key = itysymbol
module Mity: Extmap.S  with type key = ity
module Sity: Extset.S  with module M = Mity
module Hity: Exthtbl.S  with type key = ity
module Wity: Weakhtbl.S  with type key = ity
module Mreg: Extmap.S  with type key = region
module Sreg: Extset.S  with module M = Mreg
module Hreg: Exthtbl.S  with type key = region
module Wreg: Weakhtbl.S  with type key = region
module Mpv: Extmap.S  with type key = pvsymbol
module Spv: Extset.S  with module M = Mpv
module Hpv: Exthtbl.S  with type key = pvsymbol
module Wpv: Weakhtbl.S  with type key = pvsymbol
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

creation of a type symbol in programs

val create_plain_record_itysymbol : priv:bool ->
       mut:bool ->
       Ident.preid ->
       Ty.tvsymbol list -> bool Mpv.t -> Term.term list -> itysymbol

create_plain_record_itysymbol ~priv ~mut id args fields invl creates a new type symbol for a non-recursive record type, possibly private or mutable. Every known field is represented by a pvsymbol mapped to its mutability status in fields. Variables corresponding to mutable fields are stored in the created type symbol and used in effects. The priv flag should be set to true for private records. The mut flag should be set to true to mark the new type as mutable even if it does not have known mutable fields. The invl parameter contains the list of invariant formulas that may only depend on variables from fields. Abstract types are considered to be private immutable records with no fields.

val create_plain_variant_itysymbol : Ident.preid -> Ty.tvsymbol list -> Spv.t list -> itysymbol

create_plain_variant_itysymbol id args fields creates a new type symbol for a non-recursive algebraic type.

val create_rec_itysymbol : Ident.preid -> Ty.tvsymbol list -> itysymbol

create_rec_itysymbol id args creates a new type symbol for a recursively defined type.

val create_alias_itysymbol : Ident.preid -> Ty.tvsymbol list -> ity -> itysymbol

create_alias_itysymbol id args def creates a new type alias.

val create_range_itysymbol : Ident.preid -> Number.int_range -> itysymbol

create_range_itysymbol id r creates a new range type.

val create_float_itysymbol : Ident.preid -> Number.float_format -> itysymbol

create_float_itysymbol id f creates a new float type.

val restore_its : Ty.tysymbol -> itysymbol

raises Not_found if the argument is not a its_ts

val its_pure : itysymbol -> bool

a pure type symbol is immutable and has no mutable components

val ity_closed : ity -> bool

a closed type contains no type variables

val ity_fragile : ity -> bool

a fragile type may contain a component with a broken invariant

Type constructors

exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
val create_region : Ident.preid -> itysymbol -> ity list -> ity list -> region

create_region id s tl rl creates a fresh region. Type symbol s must be a mutable record or an alias for one. If rl is empty, fresh subregions are created when needed.

val ity_app : itysymbol -> ity list -> ity list -> ity

ity_app s tl rl creates

val ity_app_pure : itysymbol -> ity list -> ity list -> ity

ity_app s tl rl creates an Ityapp type. If rl is empty, pure snapshots are substituted when needed.

val ity_reg : region -> ity
val ity_var : Ty.tvsymbol -> ity
val ity_purify : ity -> ity

replaces regions with pure snapshots

val ity_of_ty : Ty.ty -> ity

fresh regions are created when needed. Raises Invalid_argument for any non-its tysymbol.

val ity_of_ty_pure : Ty.ty -> ity

pure snapshots are substituted when needed. Raises Invalid_argument for any non-its tysymbol.

val ty_of_ity : ity -> Ty.ty

Generic traversal functions

val ity_fold : ('a -> ity -> 'a) -> 'a -> ity -> 'a
val reg_fold : ('a -> ity -> 'a) -> 'a -> region -> 'a

Traversal functions on type symbols

val ity_s_fold : ('a -> itysymbol -> 'a) -> 'a -> ity -> 'a
val reg_s_fold : ('a -> itysymbol -> 'a) -> 'a -> region -> 'a

Traversal functions on type variables

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

Traversal functions on top regions

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

Traversal functions on exposed and reachable regions

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

Built-in types

val ts_unit : Ty.tysymbol

Same as Ty.ts_tuple 0.

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 matching and instantiation

type ity_subst = private {
   isb_var : ity Ty.Mtv.t;
   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

Program variables

val create_pvsymbol : Ident.preid -> ?ghost:bool -> ity -> pvsymbol
val restore_pv : Term.vsymbol -> pvsymbol

raises Not_found if the argument is not a pv_vs

val t_freepvs : Spv.t -> Term.term -> Spv.t

raises Not_found if the term contains a free variable which is not a pv_vs

val pvs_of_vss : Spv.t -> 'a Term.Mvs.t -> Spv.t

Exception symbols

A mask is a generalized ghost information allowing to handle tuples where some components can be ghost and others are not.

They are used for expressions, including results of programs, and for exceptions

type mask =
| MaskVisible (*

fully non-ghost

*)
| MaskTuple of mask list (*

decomposed ghst status for tuples

*)
| MaskGhost (*

fully ghost

*) 
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 {
   xs_name : Ident.ident;
   xs_ity : ity; (*

closed and immutable

*)
   xs_mask : mask;
} 
module Mxs: Extmap.S  with type key = xsymbol
module Sxs: Extset.S  with module M = Mxs
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

Effects

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 =
| Total
| Partial
| Diverges 
val total : oneway -> bool
val partial : oneway -> bool
val diverges : oneway -> bool
type effekt = private {
   eff_reads : Spv.t;
   eff_writes : Spv.t Mreg.t;
   eff_taints : Sreg.t;
   eff_covers : Sreg.t;
   eff_resets : Sreg.t;
   eff_raises : Sxs.t;
   eff_spoils : Ty.Stv.t;
   eff_oneway : oneway;
   eff_ghost : bool;
} 
val eff_empty : effekt

Effect of a non-ghost total function without any observational effect of any kinds

val eff_equal : effekt -> effekt -> bool
val eff_pure : effekt -> bool
val eff_read : Spv.t -> effekt
val eff_write : Spv.t -> Spv.t Mreg.t -> effekt
val eff_assign : (pvsymbol * pvsymbol * pvsymbol) list -> effekt
val eff_read_pre : Spv.t -> effekt -> effekt
val eff_read_post : effekt -> Spv.t -> effekt
val eff_bind : Spv.t -> effekt -> effekt
val eff_read_single : pvsymbol -> effekt
val eff_read_single_pre : pvsymbol -> effekt -> effekt
val eff_read_single_post : effekt -> pvsymbol -> effekt
val eff_bind_single : pvsymbol -> effekt -> effekt
val eff_reset : effekt -> Sreg.t -> effekt
val eff_reset_overwritten : effekt -> effekt
val eff_raise : effekt -> xsymbol -> effekt
val eff_catch : effekt -> xsymbol -> effekt
val eff_spoil : effekt -> ity -> effekt
val eff_partial : effekt -> effekt
val eff_diverge : effekt -> effekt
val eff_ghostify : bool -> effekt -> effekt
val eff_ghostify_weak : bool -> effekt -> effekt
val eff_union_seq : effekt -> effekt -> effekt
val eff_union_par : effekt -> effekt -> effekt
val eff_fusion : effekt -> effekt -> effekt
val mask_adjust : effekt -> ity -> mask -> mask
val eff_escape : effekt -> ity -> Sity.t
val ity_affected : 'a Mreg.t -> ity -> bool

ity_affected wr ity returns true if the regions of ity are contained in the effect described by wr.

val pv_affected : 'a Mreg.t -> pvsymbol -> bool

pv_affected wr pv returns true if the regions of pv are contained in the effect described by wr.

val pvs_affected : 'a Mreg.t -> Spv.t -> Spv.t

pvs_affected wr pvs returns the set of pvsymbols from pvs whose regions are contained in the effect described by wr.

Computation types (higher-order types with effects)

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 : ?loc:Loc.position -> ?attrs:Ident.Sattr.t -> post -> Ident.preid
val result_id : ?loc:Loc.position ->
       ?attrs:Ident.Sattr.t -> ?ql:post list -> unit -> Ident.preid

result_id ?loc ?ql () returns a fresh pre-identifier whose name is appropriately chosen with respect to the optionally given list of post-conditions ("result" by default, as hard-coded in this module implementation).

val create_post : Term.vsymbol -> Term.term -> post
val annot_attr : Ident.attribute
val break_attr : Ident.attribute
type cty = private {
   cty_args : pvsymbol list;
   cty_pre : pre list;
   cty_post : post list;
   cty_xpost : post list Mxs.t;
   cty_oldies : pvsymbol Mpv.t;
   cty_effect : effekt;
   cty_result : ity;
   cty_mask : mask;
   cty_freeze : ity_subst;
} 
val create_cty : ?mask:mask ->
       pvsymbol list ->
       pre list ->
       post list ->
       post list Mxs.t ->
       pvsymbol Mpv.t -> effekt -> ity -> cty

create_cty ?mask ?defensive args pre post xpost oldies effect result creates a new cty. post and mask must be consistent with result. The cty_xpost field does not have to cover all raised exceptions. cty_effect.eff_reads is completed wrt the specification and args. cty_freeze freezes every unbound pvsymbol in cty_effect.eff_reads. All effects on regions outside cty_effect.eff_reads are removed. Fresh regions in result are reset. Every type variable in pre, post, and xpost must come from cty_reads, args or result. oldies maps ghost pure snapshots of the parameters and external reads to the original pvsymbols: these snapshots are removed from cty_effect.eff_reads and replaced with the originals.

val create_cty_defensive : ?mask:mask ->
       pvsymbol list ->
       pre list ->
       post list ->
       post list Mxs.t ->
       pvsymbol Mpv.t -> effekt -> ity -> cty

same as create_cty, except that type variables in the result and exceptional results are spoiled and fresh regions in the result and exceptional results are reset.

val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty

cty_apply cty pvl rest res instantiates cty up to the types in pvl, rest, and res, then applies it to the arguments in pvl, and returns the computation type of the result, rest -> res, with every type variable and region in pvl being frozen.

val cty_tuple : pvsymbol list -> cty

cty_tuple pvl returns a nullary tuple-valued cty with an appropriate cty_mask.

val cty_exec : cty -> cty

cty_exec cty converts a cty of a partial application into a cty of a fully applied application, returning a mapping. The original cty must be effectless.

val cty_exec_post : cty -> post list

cty_exec_post cty returns a post-condition appropriate for use with local let-functions in VC generation.

val cty_ghost : cty -> bool

cty_ghost cty returns cty.cty_effect.eff_ghost

val cty_pure : cty -> bool

cty_pure cty verifies that cty has no side effects except allocations.

val cty_ghostify : bool -> cty -> cty

cty_ghostify ghost cty ghostifies the effect of cty.

val cty_reads : cty -> Spv.t

cty_reads cty returns the set of external dependencies of cty.

val cty_read_pre : Spv.t -> cty -> cty

cty_read_pre pvs cty adds pvs to cty.cty_effect.eff_reads. This function performs capture: if some variables in pvs occur in cty.cty_args, they are not frozen.

val cty_read_post : cty -> Spv.t -> cty

cty_read_post cty pvs adds pvs to cty.cty_effect.eff_reads. This function performs capture: if some variables in pvs occur in cty.cty_args, they are not frozen.

val cty_add_pre : pre list -> cty -> cty

cty_add_pre fl cty appends pre-conditions in fl to cty.cty_pre. This function performs capture: the formulas in fl may refer to the variables in cty.cty_args. Only the new external dependencies in fl are added to cty.cty_effect.eff_reads and frozen.

val cty_add_post : cty -> post list -> cty

cty_add_post cty fl appends post-conditions in fl to cty.cty_post. This function performs capture: the formulas in fl may refer to the variables in cty.cty_args. Only the new external dependencies in fl are added to cty.cty_effect.eff_reads and frozen.

Pretty-printing

val forget_reg : region -> unit
val forget_pv : pvsymbol -> unit
val forget_xs : xsymbol -> unit
val forget_cty : cty -> unit
val print_its : Stdlib.Format.formatter -> itysymbol -> unit
val print_reg : Stdlib.Format.formatter -> region -> unit
val print_reg_name : Stdlib.Format.formatter -> region -> unit
val print_ity : Stdlib.Format.formatter -> ity -> unit
val print_ity_full : Stdlib.Format.formatter -> ity -> unit
val print_xs : Stdlib.Format.formatter -> xsymbol -> unit
val print_pv : Stdlib.Format.formatter -> pvsymbol -> unit
val print_pvty : Stdlib.Format.formatter -> pvsymbol -> unit
val print_cty : Stdlib.Format.formatter -> cty -> unit
val print_spec : pvsymbol list ->
       pre list ->
       post list ->
       post list Mxs.t ->
       pvsymbol Mpv.t ->
       effekt -> Stdlib.Format.formatter -> ity option -> unit