ity.mli 11.1 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
  its_ts      : tysymbol;       (** pure "snapshot" type symbol *)
  its_private : bool;           (** is a private/abstract type *)
  its_mutable : bool;           (** is a record with mutable fields *)
Andrei Paskevich's avatar
Andrei Paskevich committed
22
  its_mfields : pvsymbol list;  (** mutable fields *)
23
24
25
26
27
  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
  ity_tag  : Weakhtbl.tag;
}

and ity_node = private
37
  | Ityreg of region
38
39
40
41
42
43
44
45
    (** 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 *)

46
47
48
49
50
51
52
and region = private {
  reg_name : ident;
  reg_its  : itysymbol;
  reg_args : ity list;
  reg_regs : region list;
}

53
54
55
56
57
and pvsymbol = private {
  pv_vs    : vsymbol;
  pv_ity   : ity;
  pv_ghost : bool;
}
58
59
60
61
62
63
64
65
66
67
68

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

69
module Mreg : Extmap.S with type key = region
70
module Sreg : Extset.S with module M = Mreg
71
72
module Hreg : Exthtbl.S with type key = region
module Wreg : Weakhtbl.S with type key = region
73

74
75
76
77
78
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

79
80
81
82
83
val its_compare : itysymbol -> itysymbol -> int
val ity_compare : ity -> ity -> int
val reg_compare : region -> region -> int
val pv_compare  : pvsymbol -> pvsymbol -> int

84
85
val its_equal : itysymbol -> itysymbol -> bool
val ity_equal : ity -> ity -> bool
86
val reg_equal : region -> region -> bool
87
val pv_equal  : pvsymbol -> pvsymbol -> bool
88
89
90

val its_hash : itysymbol -> int
val ity_hash : ity -> int
91
val reg_hash : region -> int
92
val pv_hash  : pvsymbol -> int
93
94
95
96
97
98

exception DuplicateRegion of region
exception UnboundRegion of region

(** creation of a symbol for type in programs *)
val create_itysymbol :
99
  preid -> (tvsymbol * bool * bool) list ->
100
101
102
    bool -> bool -> (region * bool) list ->
    Spv.t -> ity option -> itysymbol

103
val restore_its : tysymbol -> itysymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
104
(** raises [Not_found] if the argument is not a [its_ts] *)
105

Andrei Paskevich's avatar
Andrei Paskevich committed
106
(** {2 Type constructors} *)
107

Andrei Paskevich's avatar
Andrei Paskevich committed
108
109
exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
110
111
exception NonUpdatable of itysymbol * ity

Andrei Paskevich's avatar
Andrei Paskevich committed
112
113
114
115
val create_region : preid -> itysymbol -> ity list -> region list -> region
(** the type symbol must be mutable, aliases are allowed *)

val ity_reg : region -> ity
116
val ity_var : tvsymbol -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
117

118
val ity_pur : itysymbol -> ity list -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
119
120
(** [ity_pur] may be applied to mutable type symbols to create a snapshot *)

121
val ity_app : itysymbol -> ity list -> region list -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
122
123
124
125
(** [ity_app s tl rl] creates
  - a fresh region and an [Ityreg] type if [s] is mutable
  - an [Itypur] type if [s] is not mutable and [rl] is empty
  - an [Ityapp] type otherwise *)
126

127
val ity_app_fresh : itysymbol -> ity list -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
128
(** [ity_app_fresh] creates fresh regions where needed *)
129
130
131
132
133

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

val ity_of_ty : ty -> ity
134
135
136
137
(** snapshot type, raises [Invalid_argument] for any non-its *)

val ity_purify : ity -> ity
(** snapshot type *)
138

139
140
(** {2 Generic traversal functions} *)

141
142
val ity_fold : ('a -> ity -> 'a) -> ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_fold : ('a -> ity -> 'a) -> ('a -> region -> 'a) -> 'a -> region -> 'a
143
144
145

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

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

149
(** {2 Traversal functions on type variables} *)
150
151

val ity_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ity -> 'a
152
val reg_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> region -> 'a
153

154
(** {2 Traversal functions on top regions} *)
155

156
157
val ity_r_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_r_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
158

159
(** {2 Miscellaneous type utilities} *)
160

161
val ity_freevars : Stv.t -> ity -> Stv.t
162

163
val ity_v_occurs : tvsymbol -> ity -> bool
164
165

val ity_r_occurs : region -> ity -> bool
166
167
val reg_r_occurs : region -> region -> bool

168
val ity_r_stale  : region -> Sreg.t -> ity -> bool
169
val reg_r_stale  : region -> Sreg.t -> region -> bool
170
171
172
173

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

174
(* detect non-ghost type variables and regions *)
175

176
177
val ity_r_visible : Sreg.t -> ity -> Sreg.t
val ity_v_visible : Stv.t  -> ity -> Stv.t
178
179
180
181
182
183

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

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

184
val its_int  : itysymbol
185
val its_real : itysymbol
186
187
val its_bool : itysymbol
val its_unit : itysymbol
188
189
val its_func : itysymbol
val its_pred : itysymbol
190
191

val ity_int  : ity
192
val ity_real : ity
193
194
val ity_bool : ity
val ity_unit : ity
195
196
val ity_func : ity -> ity -> ity
val ity_pred : ity -> ity (* ity_pred 'a == ity_func 'a ity_bool *)
197

198
199
200
val its_tuple : int -> itysymbol
val ity_tuple : ity list -> ity

201
(** {2 Type matching and instantiation} *)
202

203
type ity_subst = private {
204
205
  isb_tv  : ity Mtv.t;
  isb_reg : region Mreg.t;
206
207
208
209
210
}

exception TypeMismatch of ity * ity * ity_subst
exception RegionMismatch of region * region * ity_subst

211
val isb_empty : ity_subst
212

213
214
val ity_match : ity_subst -> ity -> ity -> ity_subst
val reg_match : ity_subst -> region -> region -> ity_subst
215

216
217
val ity_freeze : ity_subst -> ity -> ity_subst (* self-match *)
val reg_freeze : ity_subst -> region -> ity_subst (* self-match *)
218
219

val ity_equal_check : ity -> ity -> unit
220
val reg_equal_check : region -> region -> unit
221

222
223
val ity_full_inst : ity_subst -> ity -> ity
val reg_full_inst : ity_subst -> region -> region
224

Andrei Paskevich's avatar
Andrei Paskevich committed
225
226
227
228
229
230
231
(** {2 Program variables} *)

val create_pvsymbol : preid -> ?ghost:bool -> ity -> pvsymbol

val restore_pv : vsymbol -> pvsymbol
(** raises [Not_found] if the argument is not a [pv_vs] *)

232
233
234
235
val t_freepvs : Spv.t -> term -> Spv.t
(** raises [Not_found] if the term contains a free variable
    which is not a [pv_vs] *)

236
237
val pvs_of_vss : Spv.t -> Svs.t -> Spv.t

238
239
240
241
242
243
244
(** {2 Exception symbols} *)

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

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

248
val xs_compare : xsymbol -> xsymbol -> int
249
val xs_equal : xsymbol -> xsymbol -> bool
250
val xs_hash: xsymbol -> int
251
252
253
254
255
256
257
258
259

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

val create_xsymbol : preid -> ity -> xsymbol

(** {2 Effects} *)

type effect = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
260
  eff_writes : Spv.t Mreg.t;
261
  eff_resets : Sreg.t Mreg.t;
262
263
264
265
266
267
268
269
  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
270
val eff_is_empty : effect -> bool
271
val eff_is_pure  : effect -> bool
272

Andrei Paskevich's avatar
Andrei Paskevich committed
273
274
275
276
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
277
278
279

val eff_diverge : effect -> effect

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

282
val refresh_of_effect : effect -> effect
Andrei Paskevich's avatar
Andrei Paskevich committed
283

284
285
exception IllegalAlias of region

286
val eff_full_inst : ity_subst -> effect -> effect
287

288
val eff_stale_region : effect -> ity -> bool
289

290
(** {2 Computation types (higher-order types with effects)} *)
291

292
293
type pre = term   (** precondition: pre_fmla *)
type post = term  (** postcondition: eps result . post_fmla *)
294
295
296
297

val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term

298
299
300
301
302
303
304
305
306
type cty = private {
  cty_args   : pvsymbol list;
  cty_pre    : pre list;
  cty_post   : post list;
  cty_xpost  : post list Mexn.t;
  cty_reads  : Spv.t;
  cty_effect : effect;
  cty_result : ity;
  cty_freeze : ity_subst;
307
308
}

309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
val create_cty : pvsymbol list ->
  pre list -> post list -> post list Mexn.t -> Spv.t -> effect -> ity -> cty
(** [create_cty args pre post xpost reads effect result] creates a cty.
    The [cty_xpost] field does not have to cover all raised exceptions.
    The [cty_reads] field is the union of free variables in all arguments.
    The [cty_freeze] field freezes every pvsymbol in [cty_reads \ args].
    The [cty_effect] field is filtered with respect to [cty_reads], and
    fresh regions in [result] are reset. Every type variable in [pre],
    [post], and [xpost] must come from [cty_reads] or from [result]. *)

val cty_apply : cty -> pvsymbol list -> ity list -> ity -> bool * 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 ghost status and the computation type of the result.
    This is essentially [rest -> res], with every type variable and
    region in [pvl] freezed. The combined length of [pvl] and [rest]
    must be equal to the length of [cty.cty_args]. The instantiation
    must be compatible with [cty.cty_freeze]. *)
327
328
329
330
331
332
333
334
335
336
337
338

val cty_add_reads : cty -> Spv.t -> cty
(** [cty_add_reads cty pvs] adds variables in [pvs] to [cty.cty_reads].
    This function performs capture: if some variables in [pvs] occur
    in [cty.cty_args], no renaming is made, and the corresponding type
    variables and regions are not frozen. *)

val cty_add_pre : cty -> pre list -> cty
(** [cty_add_pre cty fl] 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_reads] and frozen. *)
339
340
341
342
343
344
345
346
347

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_reads] and frozen. *)

val cty_pop_post : cty -> cty
(** [cty_pop_post cty] removes the first post-condition from [cty.cty_post]. *)