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