mlw_ty.ml 26.2 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 Util
open Ident
open Ty
25
open Term
26

27
(** value types (w/o effects) *)
28

29
type itysymbol = {
30
31
32
33
34
35
  its_pure : tysymbol;
  its_args : tvsymbol list;
  its_regs : region   list;
  its_def  : ity option;
  its_abst : bool;
  its_priv : bool;
36
37
}

38
39
40
and ity = {
  ity_node : ity_node;
  ity_tag  : Hashweak.tag;
41
42
}

43
44
45
46
and ity_node =
  | Ityvar of tvsymbol
  | Itypur of tysymbol * ity list
  | Ityapp of itysymbol * ity list * region list
47

48
and region = {
49
50
51
  reg_name  : ident;
  reg_ity   : ity;
  reg_ghost : bool;
52
53
}

54
(** regions *)
55
56
57

module Reg = WeakStructMake (struct
  type t = region
58
  let tag r = r.reg_name.id_tag
59
60
61
62
63
64
65
end)

module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W

66
let reg_equal : region -> region -> bool = (==)
67
let reg_hash r = id_hash r.reg_name
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69
70
71
72
73
74
75
76
77
(* a region is ghost if and only if it corresponds to a ghost mutable field
   in a record. The "contents" region of an ordinary reference is not ghost
   even if the reference itself is ghost. This is because we can alias
   a non-ghost reference with a ghost reference as follows:
     let ghost_ref<ro> = K nonghost_ref<ro> ghost_value
   Here, ghost_ref is ghost by contamination, but it shares <ro> with
   a non-ghost reference. Notice that any write in ghost_ref is forbidden
   (such a write would be a ghost expression touching a non-ghost region). *)

78
79
let create_region id ?(ghost=false) ty =
  { reg_name = id_register id; reg_ity = ty; reg_ghost = ghost }
80

81
(* value type symbols *)
82

83
84
85
module Itsym = WeakStructMake (struct
  type t = itysymbol
  let tag its = its.its_pure.ts_name.id_tag
86
87
end)

88
89
90
91
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W
92

93
94
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
95

96
97
let its_hash its = id_hash its.its_pure.ts_name
let ity_hash ity = Hashweak.tag_hash ity.ity_tag
98

99
100
module Hsity = Hashcons.Make (struct
  type t = ity
101

102
103
  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
    | Ityvar n1, Ityvar n2 ->
104
        tv_equal n1 n2
105
106
107
108
    | Itypur (s1,l1), Itypur (s2,l2) ->
        ts_equal s1 s2 && List.for_all2 ity_equal l1 l2
    | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) ->
        its_equal s1 s2 && List.for_all2 ity_equal l1 l2
109
          && List.for_all2 reg_equal r1 r2
110
111
    | _ ->
        false
112

113
114
115
116
  let hash ity = match ity.ity_node with
    | Ityvar v -> tv_hash v
    | Itypur (s,tl) -> Hashcons.combine_list ity_hash (ts_hash s) tl
    | Ityapp (s,tl,rl) ->
117
        Hashcons.combine_list reg_hash
118
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl
119

120
  let tag n ity = { ity with ity_tag = Hashweak.create_tag n }
121
122
end)

123
124
125
module Ity = WeakStructMake (struct
  type t = ity
  let tag ity = ity.ity_tag
126
127
end)

128
129
130
131
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W
132

133
134
135
let mk_ity n = {
  ity_node = n;
  ity_tag  = Hashweak.dummy_tag;
136
137
}

138
139
140
let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
let ity_pur s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_app s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
141
142
143

(* generic traversal functions *)

144
145
146
147
let ity_map fn ity = match ity.ity_node with
  | Ityvar _ -> ity
  | Itypur (f,tl) -> ity_pur f (List.map fn tl)
  | Ityapp (f,tl,rl) -> ity_app f (List.map fn tl) rl
148

149
150
151
152
let ity_fold fn acc ity = match ity.ity_node with
  | Ityvar _ -> acc
  | Itypur (_,tl)
  | Ityapp (_,tl,_) -> List.fold_left fn acc tl
153

154
155
let ity_all pr ity =
  try ity_fold (all_fn pr) true ity with FoldSkip -> false
156

157
158
let ity_any pr ity =
  try ity_fold (any_fn pr) false ity with FoldSkip -> true
159

160
161
162
163
164
165
166
167
168
(* symbol-wise map/fold *)

let rec ity_s_fold fn fts acc ity = match ity.ity_node with
  | Ityvar _ -> acc
  | Itypur (ts, tl) -> List.fold_left (ity_s_fold fn fts) (fts acc ts) tl
  | Ityapp (f, tl, rl) ->
      let acc = List.fold_left (ity_s_fold fn fts) (fn acc f) tl in
      List.fold_left (fun acc r -> ity_s_fold fn fts acc r.reg_ity) acc rl

169
170
171
172
let ity_s_all pr pts ity =
  try ity_s_fold (all_fn pr) (all_fn pts) true ity with FoldSkip -> false

let ity_s_any pr pts ity =
173
  try ity_s_fold (any_fn pr) (any_fn pts) false ity with FoldSkip -> true
174

175
176
(* traversal functions on type variables and regions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
177
let rec ity_v_map_unsafe fnv fnr ity = match ity.ity_node with
178
  | Ityvar v ->
179
      fnv v
180
  | Itypur (f,tl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
181
      ity_pur f (List.map (ity_v_map_unsafe fnv fnr) tl)
182
  | Ityapp (f,tl,rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
183
      ity_app f (List.map (ity_v_map_unsafe fnv fnr) tl) (List.map fnr rl)
184
185
186

let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
  | Ityvar v ->
187
      fnv acc v
188
189
190
191
  | Itypur (_,tl) ->
      List.fold_left (ity_v_fold fnv fnr) acc tl
  | Ityapp (_,tl,rl) ->
      List.fold_left (ity_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
192

193
194
let ity_v_all prv prr ity =
  try ity_v_fold (all_fn prv) (all_fn prr) true ity with FoldSkip -> false
195

196
197
let ity_v_any prv prr ity =
  try ity_v_fold (any_fn prv) (any_fn prr) false ity with FoldSkip -> true
198

Andrei Paskevich's avatar
Andrei Paskevich committed
199
200
let ity_subst_unsafe mv mr ity =
  ity_v_map_unsafe (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
201

202
203
let ity_freevars = ity_v_fold (fun s v -> Stv.add v s) Util.const
let ity_topregions = ity_v_fold Util.const (fun s r -> Sreg.add r s)
204

205
206
let ity_closed = ity_v_all Util.ffalse Util.ttrue
let ity_pure = ity_v_all Util.ttrue Util.ffalse
207
208
209

(* smart constructors *)

210
211
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
212

213
214
exception DuplicateRegion of region
exception UnboundRegion of region
215

216
exception RegionMismatch of region * region
217
exception TypeMismatch of ity * ity
218

219
220
let ity_equal_check ty1 ty2 =
  if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
221

222
223
224
let reg_equal_check r1 r2 =
  if not (reg_equal r1 r2) then raise (RegionMismatch (r1, r2))

Andrei Paskevich's avatar
Andrei Paskevich committed
225
226
227
228
229
230
231
let reg_protect fn r =
  let nr = fn r in
  if nr.reg_ghost <> r.reg_ghost then raise (RegionMismatch (r, nr));
  nr

let ity_v_map fnv fnr ity = ity_v_map_unsafe fnv (reg_protect fnr) ity

232
type ity_subst = {
233
  ity_subst_tv  : ity Mtv.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
234
  ity_subst_reg : region Mreg.t; (* must preserve ghost-ness *)
235
236
}

237
238
239
let ity_subst_empty = {
  ity_subst_tv = Mtv.empty;
  ity_subst_reg = Mreg.empty;
240
241
}

242
243
244
245
246
247
248
249
250
251
252
253
let ity_subst_union s1 s2 =
  let check_ity _ ity1 ity2 = ity_equal_check ity1 ity2; Some ity1 in
  let check_reg _ r1 r2 = reg_equal_check r1 r2; Some r1 in
  { ity_subst_tv  = Mtv.union  check_ity s1.ity_subst_tv  s2.ity_subst_tv;
    ity_subst_reg = Mreg.union check_reg s1.ity_subst_reg s2.ity_subst_reg }

let reg_inst s r =
  Mreg.find_def r r s.ity_subst_reg

let reg_full_inst s r =
  Mreg.find r s.ity_subst_reg

254
let ity_inst s ity =
Andrei Paskevich's avatar
Andrei Paskevich committed
255
  ity_v_map_unsafe
256
257
    (fun v -> Mtv.find_def (ity_var v) v s.ity_subst_tv)
    (fun r -> Mreg.find_def r r s.ity_subst_reg)
258
    ity
259

260
let ity_full_inst s ity =
Andrei Paskevich's avatar
Andrei Paskevich committed
261
  ity_subst_unsafe s.ity_subst_tv s.ity_subst_reg ity
262

263
let rec ity_match s ity1 ity2 =
264
  let set = function
265
266
    | None -> Some ity2
    | Some ity3 as r when ity_equal ity3 ity2 -> r
267
268
    | _ -> raise Exit
  in
269
270
271
  match ity1.ity_node, ity2.ity_node with
  | Ityapp (s1, l1, r1), Ityapp (s2, l2, r2) when its_equal s1 s2 ->
      let s = List.fold_left2 ity_match s l1 l2 in
272
      List.fold_left2 reg_match s r1 r2
273
274
275
  | Itypur (s1, l1), Itypur (s2, l2) when ts_equal s1 s2 ->
      List.fold_left2 ity_match s l1 l2
  | Ityvar tv1, _ ->
276
      { s with ity_subst_tv = Mtv.change set tv1 s.ity_subst_tv }
277
278
279
280
281
  | _ ->
      raise Exit

and reg_match s r1 r2 =
  let is_new = ref false in
Andrei Paskevich's avatar
Andrei Paskevich committed
282
  let set = function (* must preserve ghost-ness of regions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
283
    | None when r1.reg_ghost = r2.reg_ghost -> is_new := true; Some r2
284
285
286
    | Some r3 as r when reg_equal r3 r2 -> r
    | _ -> raise Exit
  in
287
  let reg_map = Mreg.change set r1 s.ity_subst_reg in
288
289
  let s = { s with ity_subst_reg = reg_map } in
  if !is_new then ity_match s r1.reg_ity r2.reg_ity else s
290

291
292
293
let ity_match s ity1 ity2 =
  try ity_match s ity1 ity2
  with Exit -> raise (TypeMismatch (ity_inst s ity1, ity2))
294

295
296
297
298
let rec ty_of_ity ity = match ity.ity_node with
  | Ityvar v -> ty_var v
  | Itypur (s,tl) -> ty_app s (List.map ty_of_ity tl)
  | Ityapp (s,tl,_) -> ty_app s.its_pure (List.map ty_of_ity tl)
299

300
301
302
let rec ity_of_ty ty = match ty.ty_node with
  | Tyvar v -> ity_var v
  | Tyapp (s,tl) -> ity_pur s (List.map ity_of_ty tl)
303

304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
let rec ity_inst_fresh mv mr ity = match ity.ity_node with
  | Ityvar v ->
      mr, Mtv.find v mv
  | Itypur (s,tl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
      mr, ity_pur s tl
  | Ityapp (s,tl,rl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
      let mr,rl = Util.map_fold_left (reg_refresh mv) mr rl in
      mr, ity_app s tl rl

and reg_refresh mv mr r = match Mreg.find_opt r mr with
  | Some r ->
      mr, r
  | None ->
      let mr,ity = ity_inst_fresh mv mr r.reg_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
320
321
      let id = id_clone r.reg_name in
      let ghost = r.reg_ghost in
322
323
324
325
326
327
328
329
330
331
332
      let reg = create_region id ~ghost ity in
      Mreg.add r reg mr, reg

let ity_app_fresh s tl =
  (* type variable map *)
  let add m v t = Mtv.add v t m in
  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
    with Invalid_argument _ ->
      raise (BadItyArity (s, List.length s.its_args, List.length tl)) in
  (* refresh regions *)
  let mr,rl = Util.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
Andrei Paskevich's avatar
Andrei Paskevich committed
333
  (* every top region in def is guaranteed to be in mr *)
334
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
335
  | Some ity -> ity_subst_unsafe mv mr ity
336
337
  | None -> ity_app s tl rl

338
let ity_app s tl rl =
339
  (* type variable map *)
340
  let add m v t = Mtv.add v t m in
341
342
343
344
  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
    with Invalid_argument _ ->
      raise (BadItyArity (s, List.length s.its_args, List.length tl)) in
  (* region map *)
Andrei Paskevich's avatar
Andrei Paskevich committed
345
346
  let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
  let sub = try List.fold_left2 reg_match sub s.its_regs rl
347
348
    with Invalid_argument _ ->
      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
349
  (* every type var and top region in def are in its_args and its_regs *)
350
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
351
  | Some ity -> ity_full_inst sub ity
352
  | None -> ity_app s tl rl
353

354
let ity_pur s tl = match s.ts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
355
356
357
  | Some ty ->
      let add m v t = Mtv.add v t m in
      let m = List.fold_left2 add Mtv.empty s.ts_args tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
358
      ity_subst_unsafe m Mreg.empty (ity_of_ty ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
359
  | None ->
360
      ity_pur s tl
Andrei Paskevich's avatar
Andrei Paskevich committed
361

362
let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
363
  let puredef = option_map ty_of_ity def in
Andrei Paskevich's avatar
Andrei Paskevich committed
364
  let purets = create_tysymbol name args puredef in
365
  (* all regions *)
366
  let add s v = Sreg.add_new (DuplicateRegion v) v s in
367
368
369
370
371
  let sregs = List.fold_left add Sreg.empty regs in
  (* all type variables *)
  let sargs = List.fold_right Stv.add args Stv.empty in
  (* all type variables in [regs] must be in [args] *)
  let check tv = Stv.mem tv sargs || raise (UnboundTypeVar tv) in
372
  List.iter (fun r -> ignore (ity_v_all check Util.ttrue r.reg_ity)) regs;
373
374
  (* all regions in [def] must be in [regs] *)
  let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
375
  ignore (option_map (ity_v_all Util.ttrue check) def);
376
  (* if a type is an alias then abst and priv will be ignored *)
377
378
379
  { its_pure  = purets;
    its_args  = args;
    its_regs  = regs;
380
381
382
    its_def   = def;
    its_abst  = abst;
    its_priv  = priv }
383

Andrei Paskevich's avatar
Andrei Paskevich committed
384
385
let ity_int  = ity_of_ty Ty.ty_int
let ity_bool = ity_of_ty Ty.ty_bool
Andrei Paskevich's avatar
Andrei Paskevich committed
386
let ity_unit = ity_of_ty (Ty.ty_tuple [])
Andrei Paskevich's avatar
Andrei Paskevich committed
387

388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
type varset = {
  vars_tv  : Stv.t;
  vars_reg : Sreg.t;
}

let vars_empty = { vars_tv = Stv.empty ; vars_reg = Sreg.empty }

let ity_vars s ity = {
  vars_tv  = ity_freevars s.vars_tv ity;
  vars_reg = ity_topregions s.vars_reg ity;
}

let vs_vars s vs = {
  vars_tv  = ty_freevars s.vars_tv vs.vs_ty;
  vars_reg = s.vars_reg;
}

let vars_union s1 s2 = {
  vars_tv  = Stv.union s1.vars_tv s2.vars_tv;
  vars_reg = Sreg.union s1.vars_reg s2.vars_reg;
}

let vars_freeze s =
  let sbs = Stv.fold (fun v -> Mtv.add v (ity_var v)) s.vars_tv Mtv.empty in
  let sbs = { ity_subst_tv = sbs ; ity_subst_reg = Mreg.empty } in
  Sreg.fold (fun r s -> reg_match s r r) s.vars_reg sbs

415
416
417
418
419
(** computation types (with effects) *)

(* exception symbols *)
type xsymbol = {
  xs_name : ident;
420
  xs_ity  : ity; (* closed and pure *)
421
}
422

423
424
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
425

426
427
428
429
430
let create_xsymbol id ity =
  let id = id_register id in
  if not (ity_closed ity) then raise (PolymorphicException (id, ity));
  if not (ity_pure ity) then raise (MutableException (id, ity));
  { xs_name = id; xs_ity = ity; }
431

432
433
434
435
module Exn = StructMake (struct
  type t = xsymbol
  let tag xs = Hashweak.tag_hash xs.xs_name.id_tag
end)
436

437
438
439
440
441
module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
type effect = {
442
443
444
445
446
  eff_reads  : Sreg.t;
  eff_writes : Sreg.t;
  (* if r1 -> Some r2 then r1 appears in ty(r2) *)
  eff_resets : region option Mreg.t;
  eff_raises : Sexn.t;
447
}
448

449
let eff_empty = {
450
451
452
453
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
  eff_resets = Mreg.empty;
  eff_raises = Sexn.empty
454
}
455

456
457
458
let join_reset _key v1 v2 =
  Some (if option_eq reg_equal v1 v2 then v1 else None)

459
let eff_union x y =
460
  { eff_reads  = Sreg.union x.eff_reads  y.eff_reads;
461
    eff_writes = Sreg.union x.eff_writes y.eff_writes;
462
    eff_resets = Mreg.union join_reset x.eff_resets y.eff_resets;
Andrei Paskevich's avatar
Andrei Paskevich committed
463
464
    eff_raises = Sexn.union x.eff_raises y.eff_raises;
  }
465

466
467
468
469
470
471
472
473
474
475
476
let eff_read  e r = { e with eff_reads  = Sreg.add r e.eff_reads }
let eff_write e r = { e with eff_writes = Sreg.add r e.eff_writes }
let eff_raise e x = { e with eff_raises = Sexn.add x e.eff_raises }
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

exception IllegalAlias of region

let eff_assign e r ty =
  let e = eff_write e r in
  let sub = ity_match ity_subst_empty r.reg_ity ty in
  (* assignment cannot instantiate type variables *)
Andrei Paskevich's avatar
Andrei Paskevich committed
477
478
479
480
  let check tv ity = match ity.ity_node with
    | Ityvar tv' -> tv_equal tv tv'
    | _ -> false in
  if not (Mtv.for_all check sub.ity_subst_tv) then
481
482
483
    raise (TypeMismatch (r.reg_ity,ty));
  (* r:t[r1,r2] <- t[r1,r1] introduces an alias *)
  let add_right _ v s = Sreg.add_new (IllegalAlias v) v s in
Andrei Paskevich's avatar
Andrei Paskevich committed
484
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
485
486
  (* every region on the rhs must be erased *)
  let add_right k v m = if reg_equal k v then m else Mreg.add v None m in
Andrei Paskevich's avatar
Andrei Paskevich committed
487
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
488
  (* ...except those which occur on the lhs : they are preserved under r *)
Andrei Paskevich's avatar
Andrei Paskevich committed
489
  let add_left k v m = if reg_equal k v then m else Mreg.add k (Some r) m in
Andrei Paskevich's avatar
Andrei Paskevich committed
490
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
491
492
493
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

let eff_remove_raise e x = { e with eff_raises = Sexn.remove x e.eff_raises }
494

Andrei Paskevich's avatar
Andrei Paskevich committed
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
let eff_full_inst s e =
  let s = s.ity_subst_reg in
  (* modified or reset regions in e *)
  let wr = Mreg.map (Util.const ()) e.eff_resets in
  let wr = Sreg.union e.eff_writes wr in
  (* read-only regions in e *)
  let ro = Sreg.diff e.eff_reads wr in
  (* all modified or reset regions are instantiated into distinct regions *)
  let add_affected r acc =
    let r = Mreg.find r s in Sreg.add_new (IllegalAlias r) r acc in
  let wr = Sreg.fold add_affected wr Sreg.empty in
  (* all read-only regions are instantiated outside wr *)
  let add_readonly r =
    let r = Mreg.find r s in if Sreg.mem r wr then raise (IllegalAlias r) in
  Sreg.iter add_readonly ro;
  (* calculate instantiated effect *)
  let add_inst r acc = Sreg.add (Mreg.find r s) acc in
  let reads  = Sreg.fold add_inst e.eff_reads  Sreg.empty in
  let writes = Sreg.fold add_inst e.eff_writes Sreg.empty in
  let add_inst r v acc =
    Mreg.add (Mreg.find r s) (option_map (fun v -> Mreg.find v s) v) acc in
  let resets = Mreg.fold add_inst e.eff_resets Mreg.empty in
  { e with eff_reads = reads ; eff_writes = writes ; eff_resets = resets }
518

519
520
521
522
523
524
(* program types *)

type vty_value = {
  vtv_ity   : ity;
  vtv_ghost : bool;
  vtv_mut   : region option;
525
  vtv_vars  : varset;
526
527
528
529
530
531
532
533
534
535
536
}

type vty =
  | VTvalue of vty_value
  | VTarrow of vty_arrow

and vty_arrow = {
  vta_arg    : vty_value;
  vta_result : vty;
  vta_effect : effect;
  vta_ghost  : bool;
537
538
  vta_vars   : varset;
  (* this varset covers every type variable and region in vta_arg
539
540
541
542
543
544
     and vta_result, but may skip some type variables and regions
     in vta_effect *)
}

(* smart constructors *)

545
546
547
let vty_vars s = function
  | VTvalue vtv -> vars_union s vtv.vtv_vars
  | VTarrow vta -> vars_union s vta.vta_vars
548
549

let vty_value ?(ghost=false) ?mut ity =
550
551
  let vars = ity_vars vars_empty ity in
  let vars = match mut with
552
553
554
555
    | Some r ->
        if r.reg_ghost && not ghost then
          Loc.errorm "Ghost region in a non-ghost vty_value";
        ity_equal_check ity r.reg_ity;
556
        { vars with vars_reg = Sreg.add r vars.vars_reg }
557
    | None ->
558
        vars
559
560
561
562
  in {
    vtv_ity   = ity;
    vtv_ghost = ghost;
    vtv_mut   = mut;
563
    vtv_vars  = vars;
564
565
566
  }

let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
Andrei Paskevich's avatar
Andrei Paskevich committed
567
  (* mutable arguments are rejected outright *)
568
  if vtv.vtv_mut <> None then
Andrei Paskevich's avatar
Andrei Paskevich committed
569
570
571
572
    Loc.errorm "Mutable arguments are not allowed in vty_arrow";
  (* we accept a mutable vty_value for the result to simplify Mlw_expr,
     but erase it in the signature: only projections return mutables *)
  let vty = match vty with
573
574
575
    | VTvalue ({ vtv_mut = Some r ; vtv_vars = vars } as vtv) ->
        let vars = { vars with vars_reg = Sreg.remove r vars.vars_reg } in
        VTvalue { vtv with vtv_mut = None ; vtv_vars = vars }
Andrei Paskevich's avatar
Andrei Paskevich committed
576
577
    | _ -> vty
  in {
578
579
580
581
    vta_arg    = vtv;
    vta_result = vty;
    vta_effect = effect;
    vta_ghost  = ghost;
582
    vta_vars   = vty_vars vtv.vtv_vars vty;
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
  }

let vty_ghost = function
  | VTvalue vtv -> vtv.vtv_ghost
  | VTarrow vta -> vta.vta_ghost

let vtv_ghostify vtv = { vtv with vtv_ghost = true }
let vta_ghostify vta = { vta with vta_ghost = true }

let vty_ghostify = function
  | VTvalue vtv -> VTvalue (vtv_ghostify vtv)
  | VTarrow vta -> VTarrow (vta_ghostify vta)

let vty_app_arrow vta vtv =
  ity_equal_check vta.vta_arg.vtv_ity vtv.vtv_ity;
  let ghost = vta.vta_ghost || (vtv.vtv_ghost && not vta.vta_arg.vtv_ghost) in
  let result = if ghost then vty_ghostify vta.vta_result else vta.vta_result in
  vta.vta_effect, result

(* vty instantiation *)

let vtv_full_inst s vtv =
  vty_value ~ghost:vtv.vtv_ghost (ity_full_inst s vtv.vtv_ity)

(* the substitution must cover not only vta.vta_tvs and vta.vta_regs
   but also every type variable and every region in vta_effect *)
let rec vta_full_inst s vta =
  let vtv = vtv_full_inst s vta.vta_arg in
  let vty = vty_full_inst s vta.vta_result in
  let eff = eff_full_inst s vta.vta_effect in
  vty_arrow ~ghost:vta.vta_ghost ~effect:eff vtv vty

and vty_full_inst s = function
  | VTvalue vtv -> VTvalue (vtv_full_inst s vtv)
  | VTarrow vta -> VTarrow (vta_full_inst s vta)

(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
621
622
(* program variables *)
type pvsymbol = {
623
624
625
626
  pv_vs      : vsymbol;
  pv_ity     : ity;
  pv_ghost   : bool;
  pv_mutable : region option;
Andrei Paskevich's avatar
Andrei Paskevich committed
627
628
  pv_tvs     : Stv.t;
  pv_regs    : Sreg.t;
629
}
630

631
632
633
634
635
636
637
638
639
640
module Pv = StructMake (struct
  type t = pvsymbol
  let tag pv = Hashweak.tag_hash pv.pv_vs.vs_name.id_tag
end)

module Spv = Pv.S
module Mpv = Pv.M

let pv_equal : pvsymbol -> pvsymbol -> bool = (==)

641
642
643
644
645
646
exception InvalidPVsymbol of ident

let create_pvsymbol id ?mut ?(ghost=false) ity =
  let ty = ty_of_ity ity in
  let vs = create_vsymbol id ty in
  begin match mut with
Andrei Paskevich's avatar
Andrei Paskevich committed
647
648
649
650
    | Some r when
      (* A ghost variable may contain a non-ghost region.
         No writes are allowed in such a ghost variable. *)
      not (ity_equal r.reg_ity ity) || (r.reg_ghost && not ghost) ->
651
        raise (InvalidPVsymbol vs.vs_name)
652
653
    | _ ->
        ()
654
  end;
Andrei Paskevich's avatar
Andrei Paskevich committed
655
656
657
658
659
660
661
662
663
664
  let tvs = ity_freevars Stv.empty ity in
  let regs = ity_topregions Sreg.empty ity in
  let regs = option_fold (fun s r -> Sreg.add r s) regs mut in
  { pv_vs      = vs;
    pv_ity     = ity;
    pv_ghost   = ghost;
    pv_mutable = mut;
    pv_tvs     = tvs;
    pv_regs    = regs;
  }
665

Andrei Paskevich's avatar
Andrei Paskevich committed
666
667
668
669
670
let pv_clone pv =
  let id = id_clone pv.pv_vs.vs_name in
  let vs = create_vsymbol id pv.pv_vs.vs_ty in
  { pv with pv_vs = vs }

671
672
673
674
675
let pv_full_inst s pv =
  let ghost = pv.pv_ghost in
  let mut = option_map (reg_full_inst s) pv.pv_mutable in
  let ity = ity_full_inst s pv.pv_ity in
  create_pvsymbol (id_clone pv.pv_vs.vs_name) ~ghost ?mut ity
676

677
(* value types *)
678

679
680
type vty =
  | VTvalue of pvsymbol
681
  | VTarrow of vty_arrow
682
683

(* computation types *)
684
and vty_arrow = {
Andrei Paskevich's avatar
Andrei Paskevich committed
685
686
687
688
689
  a_arg   : pvsymbol;
  a_vty   : vty;
  a_eff   : effect;
  a_pre   : term; (* epsilon under a dummy variable, to accumulate substs *)
  a_post  : term; (* epsilon under the value variable or under a dummy vs *)
Andrei Paskevich's avatar
Andrei Paskevich committed
690
691
692
  a_xpost : term Mexn.t; (* epsilon under the exception value variable *)
  a_tvs   : Stv.t; (* we do not count type variables in eff/pre/post/xpost *)
  a_regs  : Sreg.t; (* we do not count regions in eff/pre/post/xpost *)
Andrei Paskevich's avatar
Andrei Paskevich committed
693
694
695
696
697
698
699
}

type pre = term
type post = term
type xpost = (vsymbol * post) Mexn.t

type vty_comp = {
700
701
  c_vty   : vty;
  c_eff   : effect;
Andrei Paskevich's avatar
Andrei Paskevich committed
702
  c_pre   : pre;
703
  c_post  : post;
704
  c_xpost : xpost;
705
}
706

Andrei Paskevich's avatar
Andrei Paskevich committed
707
708
709
710
711
712
713
714
let vty_freevars s = function
  | VTvalue pv -> Stv.union s pv.pv_tvs
  | VTarrow a  -> Stv.union s a.a_tvs

let vty_topregions s = function
  | VTvalue pv -> Sreg.union s pv.pv_regs
  | VTarrow a  -> Sreg.union s a.a_regs

715
(* smart constructors *)
716

717
let vty_value pvs = VTvalue pvs
718

Andrei Paskevich's avatar
Andrei Paskevich committed
719
720
721
722
723
724
725
726
727
728
729
exception InvalidExceptionPost of xsymbol

(* this vs is used to close pre- and post-conditions in order
   to accumulate substitutions into a_arg pvsymbols *)

let close_spec =
  let dummy = create_vsymbol (id_fresh "dummy") ty_int in
  let dumbf = t_eps_close dummy t_true in
  function
    | { t_node = Ttrue } -> dumbf
    | f -> t_eps_close dummy f
730

Andrei Paskevich's avatar
Andrei Paskevich committed
731
732
733
let open_spec = function
  | { t_node = Teps bf } -> t_open_bound bf
  | _ -> assert false
734
735
736

let vty_arrow
  x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
Andrei Paskevich's avatar
Andrei Paskevich committed
737
  (* check for clashes *)
Andrei Paskevich's avatar
Andrei Paskevich committed
738
(* let check_vs y = if vs_equal x.pv_vs y then raise (DuplicateVar y) in *)
Andrei Paskevich's avatar
Andrei Paskevich committed
739
  let check_pv y = if pv_equal x y then raise (DuplicateVar x.pv_vs) in
740
  let rec check = function
Andrei Paskevich's avatar
Andrei Paskevich committed
741
    | VTarrow a ->
Andrei Paskevich's avatar
Andrei Paskevich committed
742
     (* Mexn.iter (fun _ (y,_) -> check_vs y) a.a_xpost; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
743
744
745
746
        check_pv a.a_arg;
        check a.a_vty
    | VTvalue y ->
        check_pv y
747
  in
748
  check vty;
Andrei Paskevich's avatar
Andrei Paskevich committed
749
750
751
752
753
754
755
756
757
758
759
760
  (* check that every raised exception is mentioned in xpost *)
  if not (Mexn.set_submap effect.eff_raises xpost) then
    (let d = Mexn.set_diff xpost effect.eff_raises in
    raise (InvalidExceptionPost (fst (Mexn.choose d))));
  (* check that every exception mentioned in xpost is raised *)
  if not (Mexn.set_submap xpost effect.eff_raises) then
    (let d = Mexn.set_diff effect.eff_raises xpost in
    raise (InvalidExceptionPost (fst (Mexn.choose d))));
  (* check that vsymbols in xpost have valid types *)
  let conv_xpost xs (vs,f) =
    if not (ty_equal (ty_of_ity xs.xs_ity) vs.vs_ty)
    then raise (InvalidExceptionPost xs);
Andrei Paskevich's avatar
Andrei Paskevich committed
761
762
    (* check_vs vs; *)
    t_eps_close vs f
Andrei Paskevich's avatar
Andrei Paskevich committed
763
764
765
766
767
  in
  let post = match vty with
    | VTvalue pv -> t_eps_close pv.pv_vs post
    | VTarrow _  -> close_spec post
  in
768
  VTarrow {
Andrei Paskevich's avatar
Andrei Paskevich committed
769
770
771
772
773
774
    a_arg   = x;
    a_vty   = vty;
    a_eff   = effect;
    a_pre   = close_spec pre;
    a_post  = post;
    a_xpost = Mexn.mapi conv_xpost xpost;
Andrei Paskevich's avatar
Andrei Paskevich committed
775
776
    a_tvs   = vty_freevars x.pv_tvs vty;
    a_regs  = vty_topregions x.pv_regs vty;
777
778
  }

Andrei Paskevich's avatar
Andrei Paskevich committed
779
(*
780
781
782
783
784
exception NotAFunction

let get_arrow = function
  | VTvalue _ -> raise NotAFunction
  | VTarrow a -> a
Andrei Paskevich's avatar
Andrei Paskevich committed
785
786
787
788
789
790
791
*)

let vty_app_arrow arr x =
  ity_equal_check arr.a_arg.pv_ity x.pv_ity;
  let subst f = t_subst_single arr.a_arg.pv_vs (t_var x.pv_vs) f in
  let _,pre = open_spec (subst arr.a_pre) in
  let res,post = open_spec (subst arr.a_post) in
Andrei Paskevich's avatar
Andrei Paskevich committed
792
  let xsubst e = open_spec (subst e) in
Andrei Paskevich's avatar
Andrei Paskevich committed
793
794
795
796
797
798
  let rec arr_subst arr = { arr with
    a_vty   = (match arr.a_vty with
      | VTarrow a -> VTarrow (arr_subst a)
      | VTvalue _ -> arr.a_vty);
    a_pre   = subst arr.a_pre;
    a_post  = subst arr.a_post;
Andrei Paskevich's avatar
Andrei Paskevich committed
799
    a_xpost = Mexn.map subst arr.a_xpost;
Andrei Paskevich's avatar
Andrei Paskevich committed
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
  }
  in
  let vty = match arr.a_vty with
    (* here we make a new pvsymbol in a bad fashion. It should however
       be safe, since res comes from t_open_bound and is guaranteed to
       be fresh, so there can be no illegal sharing of idents *)
    | VTvalue pv -> VTvalue { pv with pv_vs = res }
    | VTarrow a  -> VTarrow (arr_subst a)
  in {
    c_vty   = vty;
    c_eff   = arr.a_eff;
    c_pre   = pre;
    c_post  = post;
    c_xpost = Mexn.map xsubst arr.a_xpost;
  }
815

Andrei Paskevich's avatar
Andrei Paskevich committed
816
817
818
819
820
let open_vty_arrow arr =
  let pv = pv_clone arr.a_arg in
  let c = vty_app_arrow arr pv in
  pv, c.c_vty

Andrei Paskevich's avatar
Andrei Paskevich committed
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
let vty_full_inst s vty =
  let subT = Mtv.map ty_of_ity s.ity_subst_tv in
  let rec inst subV = function
    | VTvalue pv ->
        (* this is not the same vsymbol anymore that is bound in
           the preceding post. However, this should not matter. *)
        VTvalue (pv_full_inst s pv)
    | VTarrow a ->
        let x = pv_full_inst s a.a_arg in
        let subV = Mvs.add a.a_arg.pv_vs (t_var x.pv_vs) subV in
        let subst = t_ty_subst subT subV in
        let vty = inst subV a.a_vty in
        VTarrow {
          a_arg   = x;
          a_vty   = vty;
          a_eff   = eff_full_inst s a.a_eff;
          a_pre   = subst a.a_pre;
          a_post  = subst a.a_post;
          a_xpost = Mexn.map subst a.a_xpost;
          a_tvs   = vty_freevars x.pv_tvs vty;
          a_regs  = vty_topregions x.pv_regs vty;
        }
  in
  inst Mvs.empty vty
845
*)