mlw_ty.mli 9.34 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Stdlib
open Ident
open Ty
25
open Term
26

27
(** individual types (first-order types w/o effects) *)
28

29
30
31
32
33
34
35
module rec T : sig

  type varset = private {
    vars_tv  : Stv.t;
    vars_reg : Mreg.Set.t;
  }

36
37
  type varmap = varset Mid.t

38
39
40
  type itysymbol = private {
    its_pure : tysymbol;
    its_args : tvsymbol list;
41
    its_regs : region list;
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
    its_def  : ity option;
    its_abst : bool;
    its_priv : bool;
  }

  and ity = private {
    ity_node : ity_node;
    ity_vars : varset;
    ity_tag  : Hashweak.tag;
  }

  and ity_node = private
    | Ityvar of tvsymbol
    | Itypur of tysymbol * ity list
    | Ityapp of itysymbol * ity list * region list

  and region = private {
    reg_name  : ident;
    reg_ity   : ity;
  }

end
and Mreg : sig include Map.S with type key = T.region end

open T
67

68
69
70
71
module Mits : Map.S with type key = itysymbol
module Sits : Mits.Set
module Hits : Hashtbl.S with type key = itysymbol
module Wits : Hashweak.S with type key = itysymbol
72

73
74
75
76
module Mity : Map.S with type key = ity
module Sity : Mity.Set
module Hity : Hashtbl.S with type key = ity
module Wity : Hashweak.S with type key = ity
77

78
79
80
81
module Sreg : Mreg.Set
module Hreg : Hashtbl.S with type key = region
module Wreg : Hashweak.S with type key = region

82
83
val its_equal : itysymbol -> itysymbol -> bool
val ity_equal : ity -> ity -> bool
84

85
86
val its_hash : itysymbol -> int
val ity_hash : ity -> int
87

88
89
90
val reg_equal : region -> region -> bool
val reg_hash : region -> int

91
92
val reg_occurs : region -> varset -> bool

93
94
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
95
96
exception DuplicateRegion of region
exception UnboundRegion of region
97

98
val create_region : preid -> ity -> region
99

100
101
val create_itysymbol : preid -> ?abst:bool -> ?priv:bool ->
  tvsymbol list -> region list -> ity option -> itysymbol
102

103
104
val ity_var : tvsymbol -> ity
val ity_pur : tysymbol -> ity list -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
105

106
val ity_app : itysymbol -> ity list -> region list -> ity
107
val ity_app_fresh : itysymbol -> ity list -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
108
109

(* all aliases expanded, all regions removed *)
110
val ty_of_ity : ity -> ty
Andrei Paskevich's avatar
Andrei Paskevich committed
111

112
113
(* replaces every [Tyapp] with [Itypur] *)
val ity_of_ty : ty -> ity
Andrei Paskevich's avatar
Andrei Paskevich committed
114

115
116
(* generic traversal functions *)

117
118
119
120
val ity_map : (ity -> ity) -> ity -> ity
val ity_fold : ('a -> ity -> 'a) -> 'a -> ity -> 'a
val ity_all : (ity -> bool) -> ity -> bool
val ity_any : (ity -> bool) -> ity -> bool
121

122
123
124
125
126
127
128
129
(* traversal functions on type symbols *)

val ity_s_fold :
  ('a -> itysymbol -> 'a) -> ('a -> tysymbol -> 'a) -> 'a -> ity -> 'a

val ity_s_all : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool
val ity_s_any : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool

130
131
(* traversal functions on type variables and regions *)

132
val ity_v_map : (tvsymbol -> ity) -> (region -> region) -> ity -> ity
133

134
135
val ity_v_fold :
  ('a -> tvsymbol -> 'a) -> ('a -> region -> 'a) -> 'a -> ity -> 'a
136

137
138
val ity_v_all : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
val ity_v_any : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
139

140
val ity_closed : ity -> bool
141
val ity_pure : ity -> bool
142

Andrei Paskevich's avatar
Andrei Paskevich committed
143
144
145
val ts_unit : tysymbol
val ty_unit : ty

Andrei Paskevich's avatar
Andrei Paskevich committed
146
147
val ity_int : ity
val ity_bool : ity
Andrei Paskevich's avatar
Andrei Paskevich committed
148
val ity_unit : ity
Andrei Paskevich's avatar
Andrei Paskevich committed
149

150
exception RegionMismatch of region * region
151
exception TypeMismatch of ity * ity
152

153
type ity_subst = private {
154
155
  ity_subst_tv  : ity Mtv.t;
  ity_subst_reg : region Mreg.t;
156
157
}

158
val ity_subst_empty : ity_subst
159

160
val ity_match : ity_subst -> ity -> ity -> ity_subst
161

Andrei Paskevich's avatar
Andrei Paskevich committed
162
163
val reg_match : ity_subst -> region -> region -> ity_subst

164
val ity_equal_check : ity -> ity -> unit
165

Andrei Paskevich's avatar
Andrei Paskevich committed
166
167
val ity_subst_union : ity_subst -> ity_subst -> ity_subst

Andrei Paskevich's avatar
Andrei Paskevich committed
168
169
170
171
val ity_full_inst : ity_subst -> ity -> ity

val reg_full_inst : ity_subst -> region -> region

172
173
174
175
val vars_empty : varset

val vars_union : varset -> varset -> varset

176
177
val vars_merge : varmap -> varset -> varset

178
179
val vars_freeze : varset -> ity_subst

Andrei Paskevich's avatar
Andrei Paskevich committed
180
181
val create_varset : Stv.t -> Sreg.t -> varset

182
183
(* exception symbols *)
type xsymbol = private {
184
  xs_name : ident;
185
  xs_ity  : ity; (* closed and pure *)
186
187
}

188
189
val xs_equal : xsymbol -> xsymbol -> bool

190
191
192
exception PolymorphicException of ident * ity
exception MutableException of ident * ity

193
val create_xsymbol : preid -> ity -> xsymbol
194
195
196
197

module Mexn: Map.S with type key = xsymbol
module Sexn: Mexn.Set

198
199
(** effects *)

200
type effect = private {
201
202
  eff_reads  : Sreg.t;
  eff_writes : Sreg.t;
203
204
205
206
  eff_raises : Sexn.t;
  eff_ghostr : Sreg.t; (* ghost reads *)
  eff_ghostw : Sreg.t; (* ghost writes *)
  eff_ghostx : Sexn.t; (* ghost raises *)
207
208
  (* if r1 -> Some r2 then r1 appears in ty(r2) *)
  eff_resets : region option Mreg.t;
209
210
}

211
212
val eff_empty : effect
val eff_union : effect -> effect -> effect
213
val eff_ghostify : effect -> effect
214

215
216
217
val eff_read  : effect -> ?ghost:bool -> region -> effect
val eff_write : effect -> ?ghost:bool -> region -> effect
val eff_raise : effect -> ?ghost:bool -> xsymbol -> effect
218
val eff_reset : effect -> region -> effect
219

220
val eff_refresh : effect -> region -> region -> effect
221
val eff_assign : effect -> ?ghost:bool -> region -> ity -> effect
222
223

val eff_remove_raise : effect -> xsymbol -> effect
224

225
226
exception IllegalAlias of region

Andrei Paskevich's avatar
Andrei Paskevich committed
227
228
val eff_full_inst : ity_subst -> effect -> effect

229
230
val eff_filter : varset -> effect -> effect

231
232
val eff_is_empty : effect -> bool

233
234
235
236
237
238
(** specification *)

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

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

241
242
243
244
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term

type spec = {
245
246
247
248
249
250
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
  c_letrec  : int;
251
252
253
}

(** program variables *)
254
255
256
257
258

type vty_value = private {
  vtv_ity   : ity;
  vtv_ghost : bool;
  vtv_mut   : region option;
259
  vtv_vars  : varset;
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
val vty_value : ?ghost:bool -> ?mut:region -> ity -> vty_value

val vtv_unmut : vty_value -> vty_value (* remove mutability *)

type pvsymbol = private {
  pv_vs  : vsymbol;
  pv_vtv : vty_value;
}

module Mpv : Map.S with type key = pvsymbol
module Spv : Mpv.Set
module Hpv : Hashtbl.S with type key = pvsymbol
module Wpv : Hashweak.S with type key = pvsymbol

val pv_equal : pvsymbol -> pvsymbol -> bool

val create_pvsymbol : preid -> vty_value -> pvsymbol

val restore_pv : vsymbol -> pvsymbol
  (* raises Decl.UnboundVar if the argument is not a pv_vs *)

(** program types *)

285
286
287
288
289
type vty =
  | VTvalue of vty_value
  | VTarrow of vty_arrow

and vty_arrow = private {
290
  vta_args   : pvsymbol list;
291
  vta_result : vty;
292
  vta_spec   : spec;
293
294
295
  vta_ghost  : bool;
}

296
exception UnboundException of xsymbol
297

298
299
(* every raised exception must have a postcondition in spec.c_xpost *)
val vty_arrow : pvsymbol list -> ?spec:spec -> ?ghost:bool -> vty -> vty_arrow
300

301
(* this only compares the types of arguments and results, and ignores
302
303
   the spec. In other words, only the type variables and regions in
   [vta_vars vta] are matched. The caller should supply a "freezing"
304
305
306
   substitution that covers all external type variables and regions. *)
val vta_vars_match : ity_subst -> vty_arrow -> vty_arrow -> ity_subst

307
308
(* the substitution must cover not only [vta_vars vta] but
   also every type variable and every region in vta_spec *)
309
310
val vta_full_inst : ity_subst -> vty_arrow -> vty_arrow

311
(* remove from the given arrow every effect that is covered
312
   neither by the arrow's arguments nor by the given varmap *)
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
val vta_filter : varmap -> vty_arrow -> vty_arrow

(* apply a function specification to a variable argument *)
val vta_app : vty_arrow -> pvsymbol -> spec * vty

(* test for ghostness and convert to ghost *)
val vty_ghost : vty -> bool
val vty_ghostify : vty -> vty

(* verify that the spec corresponds to the result type *)
val spec_check : spec -> vty -> unit

(* convert arrows to the unit type *)
val ity_of_vty : vty -> ity
val ty_of_vty  : vty -> ty

329
330
331
(* collects the type variables and regions in arguments and values,
   but ignores the spec *)
val vta_vars : vty_arrow -> varset
332
val vty_vars : vty -> varset