ity.mli 9.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
open Ident
13
open Ty
14
open Term
15 16 17 18

(** {2 Individual types (first-order types w/o effects)} *)

type itysymbol = private {
19 20 21 22 23 24 25 26 27
  its_ts      : tysymbol;       (** pure "snapshot" type symbol *)
  its_private : bool;           (** is a private/abstract type *)
  its_mutable : bool;           (** is a record with mutable fields *)
  its_mfields : pvsymbol Mvs.t; (** mutable fields *)
  its_regions : region list;    (** mutable shareable components *)
  its_reg_vis : bool list;      (** non-ghost shareable components *)
  its_arg_vis : bool list;      (** non-ghost type parameters *)
  its_arg_upd : bool list;      (** updatable type parameters *)
  its_def     : ity option;     (** is a type alias *)
28 29 30 31
}

and ity = private {
  ity_node : ity_node;
32
  ity_pure : bool;
33 34 35 36 37
  ity_tag  : Weakhtbl.tag;
}

and ity_node = private
  | Itymut of itysymbol * ity list * region list * tvsymbol
38 39 40 41 42 43 44 45 46 47 48 49 50
    (** record with mutable fields and shareable components *)
  | Ityapp of itysymbol * ity list * region list
    (** algebraic type with shareable components *)
  | Itypur of itysymbol * ity list
    (** immutable type or a snapshot of a mutable type *)
  | Ityvar of tvsymbol
    (** type variable *)

and pvsymbol = private {
  pv_vs    : vsymbol;
  pv_ity   : ity;
  pv_ghost : bool;
}
51

52
and region = ity (** regions are itys of the [Itymut] kind *)
53 54 55 56 57 58 59 60 61 62 63

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

64
module Mreg : Extmap.S with type key = region and type 'a t = 'a Mity.t
65
module Sreg : Extset.S with module M = Mreg
66 67
module Hreg : Exthtbl.S with type key = region and type 'a t = 'a Hity.t
module Wreg : Weakhtbl.S with type key = region and type 'a t = 'a Wity.t
68

69 70 71 72 73
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

74 75
val its_equal : itysymbol -> itysymbol -> bool
val ity_equal : ity -> ity -> bool
76
val pv_equal  : pvsymbol -> pvsymbol -> bool
77 78 79

val its_hash : itysymbol -> int
val ity_hash : ity -> int
80
val pv_hash  : pvsymbol -> int
81 82 83 84 85 86 87 88

exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
exception DuplicateRegion of region
exception UnboundRegion of region

(** creation of a symbol for type in programs *)
val create_itysymbol :
89
  preid -> (tvsymbol * bool * bool) list ->
90 91 92 93
    bool -> bool -> (region * bool) list ->
    Spv.t -> ity option -> itysymbol

val create_pvsymbol : preid -> ?ghost:bool -> ity -> pvsymbol
94 95 96 97

val restore_its : tysymbol -> itysymbol
  (** raises [Not_found] if the argument is not a its_ts *)

98 99 100 101 102 103 104
val restore_pv : vsymbol -> pvsymbol
(** raises [Not_found] if the argument is not a [pv_vs] *)

exception NonUpdatable of itysymbol * ity

val ity_var : tvsymbol  -> ity
val ity_pur : itysymbol -> ity list -> ity
105
val ity_app : itysymbol -> ity list -> region list -> ity
106 107
val ity_mut : itysymbol -> ity list -> region list -> tvsymbol -> ity

108 109 110 111 112 113
val ity_app_fresh : itysymbol -> ity list -> ity

val ty_of_ity : ity -> ty
(** all aliases expanded, all regions removed *)

val ity_of_ty : ty -> ity
114 115 116 117
(** snapshot type, raises [Invalid_argument] for any non-its *)

val ity_purify : ity -> ity
(** snapshot type *)
118 119

val tv_of_region : region -> tvsymbol
120 121 122 123 124 125 126 127 128

(** {2 Generic traversal functions} *)

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

(** {2 Traversal functions on type symbols} *)

129
val ity_s_fold : ('a -> itysymbol -> 'a) -> 'a -> ity -> 'a
130

131 132
val ity_s_all : (itysymbol -> bool) -> ity -> bool
val ity_s_any : (itysymbol -> bool) -> ity -> bool
133 134 135

val ity_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ity -> 'a

136 137
val ity_freevars : Stv.t -> ity -> Stv.t

138 139 140 141 142 143 144 145 146 147 148
val ity_v_all : (tvsymbol -> bool) -> ity -> bool
val ity_v_any : (tvsymbol -> bool) -> ity -> bool

val ity_v_occurs : tvsymbol -> ity -> bool

val ity_r_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a

val ity_r_all : (region -> bool) -> ity -> bool
val ity_r_any : (region -> bool) -> ity -> bool

val ity_r_occurs : region -> ity -> bool
149
val ity_r_stale  : region -> Sreg.t -> ity -> bool
150 151 152 153

val ity_closed    : ity -> bool
val ity_immutable : ity -> bool

154
(* detect non-ghost type variables and regions *)
155

156 157
val ity_r_visible : Sreg.t -> ity -> Sreg.t
val ity_v_visible : Stv.t  -> ity -> Stv.t
158 159 160 161 162 163

(** {2 Built-in types} *)

val ts_unit : tysymbol (** the same as [Ty.ts_tuple 0] *)
val ty_unit : ty

164
val its_int  : itysymbol
165
val its_real : itysymbol
166 167 168 169
val its_bool : itysymbol
val its_unit : itysymbol

val ity_int  : ity
170
val ity_real : ity
171 172 173
val ity_bool : ity
val ity_unit : ity

174 175 176
val its_tuple : int -> itysymbol
val ity_tuple : ity list -> ity

177
(** {2 Type matching and instantiation} *)
178

179
exception TypeMismatch of ity * ity * ity Mtv.t
180

181
val ity_match : ity Mtv.t -> ity -> ity -> ity Mtv.t
182

183
val ity_freeze : ity Mtv.t -> ity -> ity Mtv.t (* self-match *)
184 185 186

val ity_equal_check : ity -> ity -> unit

187
val ity_full_inst : ity Mtv.t -> ity -> ity
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208

(** {2 Exception symbols} *)

type xsymbol = private {
  xs_name : ident;
  xs_ity  : ity; (** closed and immutable *)
}

val xs_equal : xsymbol -> xsymbol -> bool

exception PolymorphicException of ident * ity
exception MutableException of ident * ity

val create_xsymbol : preid -> ity -> xsymbol

module Mexn: Extmap.S with type key = xsymbol
module Sexn: Extset.S with module M = Mexn

(** {2 Effects} *)

type effect = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
209
  eff_writes : Spv.t Mreg.t;
210
  eff_resets : Sreg.t Mreg.t;
211 212 213 214 215 216 217 218
  eff_raises : Sexn.t;
  eff_diverg : bool;
}

val eff_empty : effect
val eff_equal : effect -> effect -> bool
val eff_union : effect -> effect -> effect

Andrei Paskevich's avatar
Andrei Paskevich committed
219
val eff_is_empty : effect -> bool
220

Andrei Paskevich's avatar
Andrei Paskevich committed
221 222 223 224
val eff_write : effect -> region -> pvsymbol option -> effect
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
val eff_reset : effect -> region -> effect
225 226 227

val eff_diverge : effect -> effect

228
val eff_assign : effect -> (region * pvsymbol * ity) list -> effect
Andrei Paskevich's avatar
Andrei Paskevich committed
229

230
val refresh_of_effect : effect -> effect
Andrei Paskevich's avatar
Andrei Paskevich committed
231

232 233
exception IllegalAlias of region

234
val eff_full_inst : ity Mtv.t -> effect -> effect
235

Andrei Paskevich's avatar
Andrei Paskevich committed
236
(*
237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
(** {2 Specification} *)

type pre = term          (** precondition: pre_fmla *)
type post = term         (** postcondition: eps result . post_fmla *)
type xpost = post Mexn.t (** exceptional postconditions *)

type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)

val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
val check_post : ty -> post -> unit

type spec = {
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
  c_letrec  : int;
}

(** {2 Program variables} *)

val t_pvset : Spv.t -> 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 *)

(** {2 Program types} *)

type vty =
  | VTvalue of ity
  | VTarrow of aty

and 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 *)

286
val aty_vars_match : ity Mtv.t -> aty -> ity list -> ity -> ity Mtv.t
287 288 289 290 291
(** 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. *)

292
val aty_full_inst : ity Mtv.t -> aty -> aty
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314
(** 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 -> ity
val ty_of_vty  : vty -> ty
(** convert arrows to the unit type *)

val aty_vars : aty -> varset
val vty_vars : vty -> varset
(** collect the type variables and regions in arguments and values,
    but ignores the spec *)
*)