Module Mlw_ty

module Mlw_ty: sig .. end

Program Types


Individual types (first-order types w/o effects)

module T: sig .. end
module Mreg: sig .. end
module Sreg: sig .. end
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 Hreg: Exthtbl.S  with type key = region
module Wreg: Weakhtbl.S  with type key = region
val its_equal : T.itysymbol -> T.itysymbol -> bool
val ity_equal : T.ity -> T.ity -> bool
val its_hash : T.itysymbol -> int
val ity_hash : T.ity -> int
val reg_equal : T.region -> T.region -> bool
val reg_hash : T.region -> int
exception BadItyArity of T.itysymbol * int
exception BadRegArity of T.itysymbol * int
exception DuplicateRegion of T.region
exception UnboundRegion of T.region
val create_region : Ident.preid -> T.ity -> T.region
val create_itysymbol : Ident.preid ->
?abst:bool ->
?priv:bool ->
?inv:bool ->
?ghost_reg:Sreg.t ->
Ty.tvsymbol list ->
T.region list -> T.ity option -> T.itysymbol

creation of a symbol for type in programs

val restore_its : Ty.tysymbol -> T.itysymbol

raises Not_found if the argument is not a its_ts

val ity_var : Ty.tvsymbol -> T.ity
val ity_pur : Ty.tysymbol -> T.ity list -> T.ity
val ity_app : T.itysymbol ->
T.ity list -> T.region list -> T.ity
val ity_app_fresh : T.itysymbol -> T.ity list -> T.ity
val ty_of_ity : T.ity -> Ty.ty

all aliases expanded, all regions removed

val ity_of_ty : Ty.ty -> T.ity

replaces every Tyapp with Itypur

Generic traversal functions

val ity_map : (T.ity -> T.ity) -> T.ity -> T.ity
val ity_fold : ('a -> T.ity -> 'a) -> 'a -> T.ity -> 'a
val ity_all : (T.ity -> bool) -> T.ity -> bool
val ity_any : (T.ity -> bool) -> T.ity -> bool

Traversal functions on type symbols

val ity_s_fold : ('a -> T.itysymbol -> 'a) ->
('a -> Ty.tysymbol -> 'a) -> 'a -> T.ity -> 'a
val ity_s_all : (T.itysymbol -> bool) -> (Ty.tysymbol -> bool) -> T.ity -> bool
val ity_s_any : (T.itysymbol -> bool) -> (Ty.tysymbol -> bool) -> T.ity -> bool
val its_clone : Theory.symbol_map ->
T.itysymbol Mits.t * T.region Mreg.t
val ity_closed : T.ity -> bool
val ity_immutable : T.ity -> bool
val ity_has_inv : T.ity -> bool
val reg_fold : (T.region -> 'a -> 'a) -> T.varset -> 'a -> 'a
val reg_any : (T.region -> bool) -> T.varset -> bool
val reg_all : (T.region -> bool) -> T.varset -> bool
val reg_iter : (T.region -> unit) -> T.varset -> unit
val reg_occurs : T.region -> T.varset -> bool
val ity_nonghost_reg : Sreg.t -> T.ity -> Sreg.t
val lookup_nonghost_reg : Sreg.t -> T.ity -> bool

Built-in types

val ts_unit : Ty.tysymbol

the same as Ty.ts_tuple 0

val ty_unit : Ty.ty
val ity_int : T.ity
val ity_real : T.ity
val ity_bool : T.ity
val ity_unit : T.ity
type ity_subst = private {
   ity_subst_tv : T.ity Ty.Mtv.t;
   ity_subst_reg : T.region Mreg.t;
}
exception RegionMismatch of T.region * T.region * ity_subst
exception TypeMismatch of T.ity * T.ity * ity_subst
val ity_subst_empty : ity_subst
val ity_match : ity_subst -> T.ity -> T.ity -> ity_subst
val reg_match : ity_subst -> T.region -> T.region -> ity_subst
val ity_equal_check : T.ity -> T.ity -> unit
val reg_equal_check : T.region -> T.region -> unit
val ity_full_inst : ity_subst -> T.ity -> T.ity
val reg_full_inst : ity_subst -> T.region -> T.region

Varset manipulation

val vars_empty : T.varset
val vars_union : T.varset -> T.varset -> T.varset
val vars_freeze : T.varset -> ity_subst

Exception symbols

type xsymbol = private {
   xs_name : Ident.ident;
   xs_ity : T.ity; (*

closed and immutable

*)
}
val xs_equal : xsymbol -> xsymbol -> bool
exception PolymorphicException of Ident.ident * T.ity
exception MutableException of Ident.ident * T.ity
val create_xsymbol : Ident.preid -> T.ity -> xsymbol
module Mexn: Extmap.S  with type key = xsymbol
module Sexn: Extset.S  with module M = Mexn

Effects

type effect = private {
   eff_writes : Sreg.t;
   eff_raises : Sexn.t;
   eff_ghostw : Sreg.t; (*

ghost writes

*)
   eff_ghostx : Sexn.t; (*

ghost raises

*)
   eff_resets : T.region option Mreg.t;
   eff_compar : Ty.Stv.t;
   eff_diverg : bool;
}
val eff_empty : effect
val eff_equal : effect -> effect -> bool
val eff_union : effect -> effect -> effect
val eff_ghostify : bool -> effect -> effect
val eff_write : effect -> ?ghost:bool -> T.region -> effect
val eff_raise : effect -> ?ghost:bool -> xsymbol -> effect
val eff_reset : effect -> T.region -> effect
val eff_refresh : effect -> T.region -> T.region -> effect
val eff_assign : effect ->
?ghost:bool -> T.region -> T.ity -> effect
val eff_compare : effect -> Ty.tvsymbol -> effect
val eff_diverge : effect -> effect
val eff_remove_raise : effect -> xsymbol -> effect
val eff_stale_region : effect -> T.varset -> bool
exception IllegalAlias of T.region
exception IllegalCompar of Ty.tvsymbol * T.ity
exception GhostDiverg
val eff_full_inst : ity_subst -> effect -> effect
val eff_is_empty : effect -> bool

Specification

type pre = Term.term 

precondition: pre_fmla

type post = Term.term 

postcondition: eps result . post_fmla

type xpost = post Mexn.t 

exceptional postconditions

type variant = Term.term * Term.lsymbol option 

tau * (tau -> tau -> prop)

val create_post : Term.vsymbol -> Term.term -> post
val open_post : post -> Term.vsymbol * Term.term
val check_post : Ty.ty -> post -> unit
type spec = {
   c_pre : pre;
   c_post : post;
   c_xpost : xpost;
   c_effect : effect;
   c_variant : variant list;
   c_letrec : int;
}

Program variables

type pvsymbol = private {
   pv_vs : Term.vsymbol;
   pv_ity : T.ity;
   pv_ghost : bool;
}
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 pv_equal : pvsymbol -> pvsymbol -> bool
val create_pvsymbol : Ident.preid -> ?ghost:bool -> T.ity -> pvsymbol
val restore_pv : Term.vsymbol -> pvsymbol

raises Not_found if the argument is not a pv_vs

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

raises Not_found if the term contains non-pv variables

val spec_pvset : Spv.t -> spec -> Spv.t

raises Not_found if the spec contains non-pv variables

Program types

type vty = 
| VTvalue of T.ity
| VTarrow of aty
type aty = private {
   aty_args : pvsymbol list;
   aty_result : vty;
   aty_spec : spec;
}
exception UnboundException of xsymbol

every raised exception must have a postcondition in spec.c_xpost

val vty_arrow : pvsymbol list -> ?spec:spec -> vty -> aty
val aty_pvset : aty -> Spv.t

raises Not_found if the spec contains non-pv variables

val aty_vars_match : ity_subst ->
aty -> T.ity list -> T.ity -> ity_subst

this only compares the types of arguments and results, and ignores the spec. In other words, only the type variables and regions in aty_vars aty are matched. The caller should supply a "freezing" substitution that covers all external type variables and regions.

val aty_full_inst : ity_subst -> aty -> aty

the substitution must cover not only aty_vars aty but also every type variable and every region in aty_spec

val aty_filter : ?ghost:bool -> Spv.t -> aty -> aty

remove from the given arrow every effect that is covered neither by the arrow's arguments nor by the given pvset

val aty_app : aty -> pvsymbol -> spec * bool * vty

apply a function specification to a variable argument

val spec_check : ?full_xpost:bool -> spec -> vty -> unit

verify that the spec corresponds to the result type

val ity_of_vty : vty -> T.ity
val ty_of_vty : vty -> Ty.ty

convert arrows to the unit type

val aty_vars : aty -> T.varset
val vty_vars : vty -> T.varset

collect the type variables and regions in arguments and values, but ignores the spec