mlw_ty.ml 29.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
14
open Ident
open Ty
15
open Term
16

17
(** value types (w/o effects) *)
18

19
module rec T : sig
20

21
22
23
24
  type varset = {
    vars_tv  : Stv.t;
    vars_reg : Reg.S.t;
  }
25

26
27
  type varmap = varset Mid.t

28
  type itysymbol = {
29
    its_ts   : tysymbol;
30
    its_regs : region list;
31
    its_def  : ity option;
32
    its_inv  : bool;
33
34
35
    its_abst : bool;
    its_priv : bool;
  }
36

37
38
39
  and ity = {
    ity_node : ity_node;
    ity_vars : varset;
Andrei Paskevich's avatar
Andrei Paskevich committed
40
    ity_tag  : Weakhtbl.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
    reg_name : ident;
    reg_ity  : ity;
51
52
53
54
55
56
57
58
59
  }

end = struct

  type varset = {
    vars_tv  : Stv.t;
    vars_reg : Reg.S.t;
  }

60
61
  type varmap = varset Mid.t

62
  type itysymbol = {
63
64
    its_ts   : tysymbol;
    its_regs : region list;
65
    its_def  : ity option;
66
    its_inv  : bool;
67
68
69
70
71
72
73
    its_abst : bool;
    its_priv : bool;
  }

  and ity = {
    ity_node : ity_node;
    ity_vars : varset;
Andrei Paskevich's avatar
Andrei Paskevich committed
74
    ity_tag  : Weakhtbl.tag;
75
76
77
78
79
80
81
82
  }

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

  and region = {
83
84
    reg_name : ident;
    reg_ity  : ity;
85
86
87
88
89
  }

end

and Reg : sig
90
91
92
  module M : Extmap.S with type key = T.region
  module S : Extset.S with module M = M
  module H : Exthtbl.S with type key = T.region
Andrei Paskevich's avatar
Andrei Paskevich committed
93
  module W : Weakhtbl.S with type key = T.region
94
end = MakeMSHW (struct
95
96
  type t = T.region
  let tag r = r.T.reg_name.id_tag
97
98
end)

99
100
101
102
open T

(** regions *)

103
104
105
106
107
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W

108
let reg_equal : region -> region -> bool = (==)
109
let reg_hash r = id_hash r.reg_name
110

111
let create_region id ty = { reg_name = id_register id; reg_ity = ty }
112

113
114
115
116
117
118
119
120
121
(* variable sets *)

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

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;
}

122
123
let vars_merge = Mid.fold (fun _ -> vars_union)

Andrei Paskevich's avatar
Andrei Paskevich committed
124
125
126
127
128
let create_varset tvs regs = {
  vars_tv = Sreg.fold (fun r -> Stv.union r.reg_ity.ity_vars.vars_tv) regs tvs;
  vars_reg = regs;
}

129
(* value type symbols *)
130

131
module Itsym = MakeMSHW (struct
132
  type t = itysymbol
133
  let tag its = its.its_ts.ts_name.id_tag
134
135
end)

136
137
138
139
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W
140

141
142
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
143

144
let its_hash its = id_hash its.its_ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
145
let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
146

147
148
module Hsity = Hashcons.Make (struct
  type t = ity
149

150
151
  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
    | Ityvar n1, Ityvar n2 ->
152
        tv_equal n1 n2
153
154
155
156
    | 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
157
          && List.for_all2 reg_equal r1 r2
158
159
    | _ ->
        false
160

161
162
163
164
  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) ->
165
        Hashcons.combine_list reg_hash
166
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl
167

168
169
170
171
172
173
174
175
176
177
178
179
180
  let ity_vars s ity = vars_union s ity.ity_vars
  let reg_vars s r = { s with vars_reg = Sreg.add r s.vars_reg }

  let vars s ity = match ity.ity_node with
    | Ityvar v ->
        { s with vars_tv = Stv.add v s.vars_tv }
    | Itypur (_,tl) ->
        List.fold_left ity_vars s tl
    | Ityapp (_,tl,rl) ->
        List.fold_left reg_vars (List.fold_left ity_vars s tl) rl

  let tag n ity = { ity with
    ity_vars = vars vars_empty ity;
Andrei Paskevich's avatar
Andrei Paskevich committed
181
    ity_tag  = Weakhtbl.create_tag n }
182

183
184
end)

185
module Ity = MakeMSHW (struct
186
187
  type t = ity
  let tag ity = ity.ity_tag
188
189
end)

190
191
192
193
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W
194

195
196
let mk_ity n = {
  ity_node = n;
197
  ity_vars = vars_empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
198
  ity_tag  = Weakhtbl.dummy_tag;
199
200
}

201
let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
202
203
let ity_pur_unsafe s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
204
205
206

(* generic traversal functions *)

207
208
let ity_map fn ity = match ity.ity_node with
  | Ityvar _ -> ity
209
210
  | Itypur (f,tl) -> ity_pur_unsafe f (List.map fn tl)
  | Ityapp (f,tl,rl) -> ity_app_unsafe f (List.map fn tl) rl
211

212
213
214
215
let ity_fold fn acc ity = match ity.ity_node with
  | Ityvar _ -> acc
  | Itypur (_,tl)
  | Ityapp (_,tl,_) -> List.fold_left fn acc tl
216

217
let ity_all pr ity =
218
  try ity_fold (Util.all_fn pr) true ity with Util.FoldSkip -> false
219

220
let ity_any pr ity =
221
  try ity_fold (Util.any_fn pr) false ity with Util.FoldSkip -> true
222

223
224
225
226
227
228
229
230
231
(* 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

232
let ity_s_all pr pts ity =
233
234
  try ity_s_fold (Util.all_fn pr) (Util.all_fn pts) true ity
  with Util.FoldSkip -> false
235
236

let ity_s_any pr pts ity =
237
238
  try ity_s_fold (Util.any_fn pr) (Util.any_fn pts) false ity
  with Util.FoldSkip -> true
239

240
241
(* traversal functions on type variables and regions *)

242
let rec ity_v_map fnv fnr ity = match ity.ity_node with
243
  | Ityvar v ->
244
      fnv v
245
  | Itypur (f,tl) ->
246
      ity_pur_unsafe f (List.map (ity_v_map fnv fnr) tl)
247
  | Ityapp (f,tl,rl) ->
248
      ity_app_unsafe f (List.map (ity_v_map fnv fnr) tl) (List.map fnr rl)
249

Andrei Paskevich's avatar
Andrei Paskevich committed
250
let ity_subst_unsafe mv mr ity =
251
  ity_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
252

253
let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
254
let ity_immutable ity = Sreg.is_empty ity.ity_vars.vars_reg
255

256
257
258
let rec ity_has_inv ity = match ity.ity_node with
  | Ityapp (its,_,_) -> its.its_inv || ity_any ity_has_inv ity
  | _ -> ity_any ity_has_inv ity
259

260
261
262
263
264
265
266
267
268
269
270
271
272
let rec reg_fold fn vars acc =
  let on_reg r acc = reg_fold fn r.reg_ity.ity_vars (fn r acc) in
  Sreg.fold on_reg vars.vars_reg acc

let rec reg_all fn vars =
  let on_reg r = fn r && reg_all fn r.reg_ity.ity_vars in
  Sreg.for_all on_reg vars.vars_reg

let rec reg_any fn vars =
  let on_reg r = fn r || reg_any fn r.reg_ity.ity_vars in
  Sreg.exists on_reg vars.vars_reg

let rec reg_iter fn vars =
273
  let on_reg r = fn r; reg_iter fn r.reg_ity.ity_vars in
274
275
276
277
  Sreg.iter on_reg vars.vars_reg

let reg_occurs r vars = reg_any (reg_equal r) vars

278
279
(* smart constructors *)

280
281
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
282

283
284
exception DuplicateRegion of region
exception UnboundRegion of region
285

286
type ity_subst = {
287
  ity_subst_tv  : ity Mtv.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
288
  ity_subst_reg : region Mreg.t; (* must preserve ghost-ness *)
289
290
}

291
let ity_subst_empty = {
292
  ity_subst_tv  = Mtv.empty;
293
  ity_subst_reg = Mreg.empty;
294
295
}

Andrei Paskevich's avatar
Andrei Paskevich committed
296
297
exception RegionMismatch of region * region * ity_subst
exception TypeMismatch of ity * ity * ity_subst
Andrei Paskevich's avatar
Andrei Paskevich committed
298

Andrei Paskevich's avatar
Andrei Paskevich committed
299
300
301
302
303
let ity_equal_check ty1 ty2 =
  if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1,ty2,ity_subst_empty))

let reg_equal_check r1 r2 =
  if not (reg_equal r1 r2) then raise (RegionMismatch (r1,r2,ity_subst_empty))
304

305
let reg_full_inst s r = Mreg.find r s.ity_subst_reg
Andrei Paskevich's avatar
Andrei Paskevich committed
306
307

let ity_full_inst s ity =
308
  if ity_closed ity && ity_immutable ity then ity
Andrei Paskevich's avatar
Andrei Paskevich committed
309
  else ity_subst_unsafe s.ity_subst_tv s.ity_subst_reg ity
310

311
let rec ity_match s ity1 ity2 =
312
  let set = function
313
314
    | None -> Some ity2
    | Some ity3 as r when ity_equal ity3 ity2 -> r
315
316
    | _ -> raise Exit
  in
317
318
319
  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
320
      List.fold_left2 reg_match s r1 r2
321
322
323
  | Itypur (s1, l1), Itypur (s2, l2) when ts_equal s1 s2 ->
      List.fold_left2 ity_match s l1 l2
  | Ityvar tv1, _ ->
324
      { s with ity_subst_tv = Mtv.change set tv1 s.ity_subst_tv }
325
326
327
328
329
  | _ ->
      raise Exit

and reg_match s r1 r2 =
  let is_new = ref false in
330
331
  let set = function
    | None -> is_new := true; Some r2
332
333
334
    | Some r3 as r when reg_equal r3 r2 -> r
    | _ -> raise Exit
  in
335
  let reg_map = Mreg.change set r1 s.ity_subst_reg in
336
337
  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
338

339
340
let ity_match s ity1 ity2 =
  try ity_match s ity1 ity2
Andrei Paskevich's avatar
Andrei Paskevich committed
341
342
343
344
345
  with Exit -> raise (TypeMismatch (ity1,ity2,s))

let reg_match s r1 r2 =
  try reg_match s r1 r2
  with Exit -> raise (RegionMismatch (r1,r2,s))
346

347
348
349
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)
350
  | Ityapp (s,tl,_) -> ty_app s.its_ts (List.map ty_of_ity tl)
351

352
353
let rec ity_of_ty ty = match ty.ty_node with
  | Tyvar v -> ity_var v
354
  | Tyapp (s,tl) -> ity_pur_unsafe s (List.map ity_of_ty tl)
355

356
357
358
359
let rec ity_inst_fresh mv mr ity = match ity.ity_node with
  | Ityvar v ->
      mr, Mtv.find v mv
  | Itypur (s,tl) ->
360
      let mr,tl = Lists.map_fold_left (ity_inst_fresh mv) mr tl in
361
      mr, ity_pur_unsafe s tl
362
  | Ityapp (s,tl,rl) ->
363
364
      let mr,tl = Lists.map_fold_left (ity_inst_fresh mv) mr tl in
      let mr,rl = Lists.map_fold_left (reg_refresh mv) mr rl in
365
      mr, ity_app_unsafe s tl rl
366
367
368
369
370
371

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
372
      let id = id_clone r.reg_name in
373
      let reg = create_region id ity in
374
375
376
377
378
      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
379
  let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
380
    with Invalid_argument _ ->
381
      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
382
  (* refresh regions *)
383
  let mr,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
384
  let sub = { ity_subst_tv = mv; ity_subst_reg = mr } in
Andrei Paskevich's avatar
Andrei Paskevich committed
385
  (* every top region in def is guaranteed to be in mr *)
386
  match s.its_def with
387
  | Some ity -> ity_full_inst sub ity
388
  | None -> ity_app_unsafe s tl rl
389

390
let ity_app s tl rl =
391
  (* type variable map *)
392
  let add m v t = Mtv.add v t m in
393
  let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
394
    with Invalid_argument _ ->
395
      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
396
  (* region map *)
Andrei Paskevich's avatar
Andrei Paskevich committed
397
398
  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
399
400
    with Invalid_argument _ ->
      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
401
  (* every type var and top region in def are in its_ts.ts_args and its_regs *)
402
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
403
  | Some ity -> ity_full_inst sub ity
404
  | None -> ity_app_unsafe s tl rl
405

406
407
408
409
410
411
412
413
414
415
416
417
418
let ity_pur 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.ts_args tl
    with Invalid_argument _ ->
      raise (Ty.BadTypeArity (s, List.length s.ts_args, List.length tl)) in
  let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
  (* every top region in def is guaranteed to be in mr *)
  match s.ts_def with
  | Some ty -> ity_full_inst sub (ity_of_ty ty)
  | None -> ity_pur_unsafe s tl

(* itysymbol creation *)
419
420
421

let create_itysymbol_unsafe, restore_its =
  let ts_to_its = Wts.create 17 in
422
  (fun ts ~abst ~priv ~inv regs def ->
423
    let its = {
424
      its_ts    = ts;
425
426
      its_regs  = regs;
      its_def   = def;
427
      its_inv   = inv;
428
429
430
431
432
433
      its_abst  = abst;
      its_priv  = priv;
    } in
    Wts.set ts_to_its ts its;
    its),
  Wts.find ts_to_its
Andrei Paskevich's avatar
Andrei Paskevich committed
434

435
436
let create_itysymbol
      name ?(abst=false) ?(priv=false) ?(inv=false) args regs def =
437
  let puredef = Opt.map ty_of_ity def in
Andrei Paskevich's avatar
Andrei Paskevich committed
438
  let purets = create_tysymbol name args puredef in
439
  (* all regions *)
440
  let add s v = Sreg.add_new (DuplicateRegion v) v s in
441
442
443
444
  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] *)
445
446
447
  let check dtvs = if not (Stv.subset dtvs sargs) then
    raise (UnboundTypeVar (Stv.choose (Stv.diff dtvs sargs))) in
  List.iter (fun r -> check r.reg_ity.ity_vars.vars_tv) regs;
448
  (* all regions in [def] must be in [regs] *)
449
450
  let check dregs = if not (Sreg.subset dregs sregs) then
    raise (UnboundRegion (Sreg.choose (Sreg.diff dregs sregs))) in
451
  Opt.iter (fun d -> check d.ity_vars.vars_reg) def;
452
  (* if a type is an alias then it cannot be abstract or private *)
453
454
455
456
457
  if def <> None then begin
    if abst then Loc.errorm "Type aliases cannot be abstract";
    if priv then Loc.errorm "Type aliases cannot be private";
    if inv  then Loc.errorm "Type aliases cannot have invariants"
  end;
458
  create_itysymbol_unsafe purets ~abst ~priv ~inv regs def
459

Andrei Paskevich's avatar
Andrei Paskevich committed
460
461
462
let ts_unit = ts_tuple 0
let ty_unit = ty_tuple []

Andrei Paskevich's avatar
Andrei Paskevich committed
463
464
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
465
let ity_unit = ity_of_ty ty_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
466

467
468
469
470
471
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

472
473
474
475
476
477
478
479
480
(** cloning *)

let its_clone sm =
  let itsh = Hits.create 3 in
  let regh = Hreg.create 3 in
  let rec add_ts oits nts =
    let nits = try restore_its nts with Not_found ->
      let abst = oits.its_abst in
      let priv = oits.its_priv in
481
      let inv  = oits.its_inv in
482
      let regs = List.map conv_reg oits.its_regs in
483
      let def  = Opt.map conv_ity oits.its_def in
484
      create_itysymbol_unsafe nts ~abst ~priv ~inv regs def
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
    in
    Hits.replace itsh oits nits;
    nits
  and conv_reg r =
    try Hreg.find regh r with Not_found ->
      let ity = conv_ity r.reg_ity in
      let nr = create_region (id_clone r.reg_name) ity in
      Hreg.replace regh r nr;
      nr
  and conv_ity ity = match ity.ity_node with
    | Ityapp (its,tl,rl) ->
        let tl = List.map conv_ity tl in
        let rl = List.map conv_reg rl in
        ity_app_unsafe (conv_its its) tl rl
    | Itypur (ts,tl) ->
        let tl = List.map conv_ity tl in
        ity_pur_unsafe (conv_ts ts) tl
    | Ityvar _ -> ity
  and conv_its its =
    try Hits.find itsh its with Not_found ->
505
      try add_ts its (Mts.find its.its_ts sm.Theory.sm_ts)
506
507
508
509
510
511
512
513
514
      with Not_found -> its
  and conv_ts ts =
    Mts.find_def ts ts sm.Theory.sm_ts
  in
  let add_ts ots nts =
    try ignore (add_ts (restore_its ots) nts)
    with Not_found -> ()
  in
  Mts.iter add_ts sm.Theory.sm_ts;
515
516
  Hits.fold Mits.add itsh Mits.empty,
  Hreg.fold Mreg.add regh Mreg.empty
517

518
519
520
521
522
(** computation types (with effects) *)

(* exception symbols *)
type xsymbol = {
  xs_name : ident;
523
  xs_ity  : ity; (* closed and pure *)
524
}
525

526
527
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
528

529
530
let xs_equal : xsymbol -> xsymbol -> bool = (==)

531
532
533
let create_xsymbol id ity =
  let id = id_register id in
  if not (ity_closed ity) then raise (PolymorphicException (id, ity));
534
  if not (ity_immutable ity) then raise (MutableException (id, ity));
535
  { xs_name = id; xs_ity = ity; }
536

537
module Exn = MakeMSH (struct
538
  type t = xsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
539
  let tag xs = Weakhtbl.tag_hash xs.xs_name.id_tag
540
end)
541

542
543
544
545
546
module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
type effect = {
547
548
  eff_reads  : Sreg.t;
  eff_writes : Sreg.t;
549
550
551
552
  eff_raises : Sexn.t;
  eff_ghostr : Sreg.t; (* ghost reads *)
  eff_ghostw : Sreg.t; (* ghost writes *)
  eff_ghostx : Sexn.t; (* ghost raises *)
553
554
  (* if r1 -> Some r2 then r1 appears in ty(r2) *)
  eff_resets : region option Mreg.t;
555
}
556

557
let eff_empty = {
558
559
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
560
561
562
563
  eff_raises = Sexn.empty;
  eff_ghostr = Sreg.empty;
  eff_ghostw = Sreg.empty;
  eff_ghostx = Sexn.empty;
564
  eff_resets = Mreg.empty;
565
}
566

567
568
569
570
571
572
573
574
575
let eff_is_empty e =
  Sreg.is_empty e.eff_reads &&
  Sreg.is_empty e.eff_writes &&
  Sexn.is_empty e.eff_raises &&
  Sreg.is_empty e.eff_ghostr &&
  Sreg.is_empty e.eff_ghostw &&
  Sexn.is_empty e.eff_ghostx &&
  Mreg.is_empty e.eff_resets

576
577
578
579
580
581
582
let join_reset _key v1 v2 = match v1, v2 with
  | Some r1, Some r2 ->
      if reg_equal r1 r2 then Some v1 else
      if reg_occurs r1 r2.reg_ity.ity_vars then Some v2 else
      if reg_occurs r2 r1.reg_ity.ity_vars then Some v1 else
      Some None
  | _ -> Some None
583

584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
let eff_union x y = {
  eff_reads  = Sreg.union x.eff_reads  y.eff_reads;
  eff_writes = Sreg.union x.eff_writes y.eff_writes;
  eff_raises = Sexn.union x.eff_raises y.eff_raises;
  eff_ghostr = Sreg.union x.eff_ghostr y.eff_ghostr;
  eff_ghostw = Sreg.union x.eff_ghostw y.eff_ghostw;
  eff_ghostx = Sexn.union x.eff_ghostx y.eff_ghostx;
  eff_resets = Mreg.union join_reset x.eff_resets y.eff_resets;
}

let eff_ghostify e = {
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
  eff_raises = Sexn.empty;
  eff_ghostr = Sreg.union e.eff_reads  e.eff_ghostr;
  eff_ghostw = Sreg.union e.eff_writes e.eff_ghostw;
  eff_ghostx = Sexn.union e.eff_raises e.eff_ghostx;
  eff_resets = e.eff_resets;
}

604
605
let eff_ghostify gh e = if gh then eff_ghostify e else e

606
607
608
609
610
611
612
613
614
615
616
let eff_read e ?(ghost=false) r = if ghost
  then { e with eff_ghostr = Sreg.add r e.eff_ghostr }
  else { e with eff_reads  = Sreg.add r e.eff_reads  }

let eff_write e ?(ghost=false) r = if ghost
  then { e with eff_ghostw = Sreg.add r e.eff_ghostw }
  else { e with eff_writes = Sreg.add r e.eff_writes }

let eff_raise e ?(ghost=false) x = if ghost
  then { e with eff_ghostx = Sexn.add x e.eff_ghostx }
  else { e with eff_raises = Sexn.add x e.eff_raises }
617

618
619
620
621
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

exception IllegalAlias of region

622
623
624
625
626
627
let eff_refresh e r u =
  if not (reg_occurs r u.reg_ity.ity_vars) then
    invalid_arg "Mlw_ty.eff_refresh";
  let reset = Mreg.singleton r (Some u) in
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

628
629
let eff_assign e ?(ghost=false) r ty =
  let e = eff_write e ~ghost r in
630
631
  let sub = ity_match ity_subst_empty r.reg_ity ty in
  (* assignment cannot instantiate type variables *)
Andrei Paskevich's avatar
Andrei Paskevich committed
632
633
634
635
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
636
    raise (TypeMismatch (r.reg_ity,ty,ity_subst_empty));
637
638
  (* 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
639
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
640
641
  (* 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
642
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
643
  (* ...except those which occur on the lhs : they are preserved under r *)
Andrei Paskevich's avatar
Andrei Paskevich committed
644
  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
645
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
646
647
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

648
649
650
651
let eff_remove_raise e x = { e with
  eff_raises = Sexn.remove x e.eff_raises;
  eff_ghostx = Sexn.remove x e.eff_ghostx;
}
652

Andrei Paskevich's avatar
Andrei Paskevich committed
653
654
655
656
657
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
658
  let wr = Sreg.union e.eff_ghostw wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
659
  (* read-only regions in e *)
Andrei Paskevich's avatar
Andrei Paskevich committed
660
  let ro = Sreg.diff (Mreg.map (Util.const ()) s) wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
661
662
663
664
665
666
667
668
669
  (* 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 *)
670
671
  let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
  let add_mreg r v acc =
672
    Mreg.add (Mreg.find r s) (Opt.map (fun v -> Mreg.find v s) v) acc in
673
674
675
676
677
678
679
  { e with
    eff_reads  = Sreg.fold add_sreg e.eff_reads  Sreg.empty;
    eff_writes = Sreg.fold add_sreg e.eff_writes Sreg.empty;
    eff_ghostr = Sreg.fold add_sreg e.eff_ghostr Sreg.empty;
    eff_ghostw = Sreg.fold add_sreg e.eff_ghostw Sreg.empty;
    eff_resets = Mreg.fold add_mreg e.eff_resets Mreg.empty;
  }
680

681
let eff_filter vars e =
682
  let check r = reg_occurs r vars in
683
684
685
686
687
688
689
690
691
692
693
694
695
  let reset r = function
    | _ when not (check r) -> None
    | Some u as v when check u -> Some v
    | _ -> Some None
  in
  { e with
    eff_reads  = Sreg.filter check e.eff_reads;
    eff_writes = Sreg.filter check e.eff_writes;
    eff_ghostr = Sreg.filter check e.eff_ghostr;
    eff_ghostw = Sreg.filter check e.eff_ghostw;
    eff_resets = Mreg.mapi_filter reset e.eff_resets;
  }

696
697
698
699
700
701
702
703
704
let eff_stale_region eff vars =
  let check_reset r u =
    let rec check_reg reg =
      reg_equal r reg || match u with
        | Some u when reg_equal u reg -> false
        | _ -> Sreg.exists check_reg reg.reg_ity.ity_vars.vars_reg in
    Sreg.exists check_reg vars.vars_reg in
  Mreg.exists check_reset eff.eff_resets

705
706
707
708
709
710
(** specification *)

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

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

713
714
715
716
717
718
719
720
721
722
723
let create_post vs f = t_eps_close vs f

let open_post f = match f.t_node with
  | Teps bf -> t_open_bound bf
  | _ -> Loc.errorm "invalid post-condition"

let check_post ty f = match f.t_node with
  | Teps _ -> Ty.ty_equal_check ty (t_type f)
  | _ -> Loc.errorm "invalid post-condition"

type spec = {
724
725
726
727
728
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
729
  c_letrec  : int;
730
731
732
}

let spec_empty ty = {
733
734
735
736
737
  c_pre     = t_true;
  c_post    = create_post (create_vsymbol (id_fresh "dummy") ty) t_true;
  c_xpost   = Mexn.empty;
  c_effect  = eff_empty;
  c_variant = [];
738
  c_letrec  = 0;
739
740
741
742
}

let spec_full_inst sbs tvm vsm c =
  let subst = t_ty_subst tvm vsm in {
743
744
745
746
747
    c_pre     = subst c.c_pre;
    c_post    = subst c.c_post;
    c_xpost   = Mexn.map subst c.c_xpost;
    c_effect  = eff_full_inst sbs c.c_effect;
    c_variant = List.map (fun (t,rel) -> subst t, rel) c.c_variant;
748
    c_letrec  = c.c_letrec;
749
750
751
752
  }

let spec_subst sbs c =
  let subst = t_subst sbs in {
753
754
755
756
757
    c_pre     = subst c.c_pre;
    c_post    = subst c.c_post;
    c_xpost   = Mexn.map subst c.c_xpost;
    c_effect  = c.c_effect;
    c_variant = List.map (fun (t,rel) -> subst t, rel) c.c_variant;
758
    c_letrec  = c.c_letrec;
759
760
761
  }

let spec_filter varm vars c =
762
763
764
765
  let add f s = Mvs.set_union f.t_vars s in
  let vss = add c.c_pre c.c_post.t_vars in
  let vss = Mexn.fold (fun _ -> add) c.c_xpost vss in
  let vss = List.fold_right (fun (t,_) -> add t) c.c_variant vss in
766
767
768
769
770
771
772
773
774
775
776
777
  let check { vs_name = id } _ = if not (Mid.mem id varm) then
    Loc.errorm "Local variable %s escapes from its scope" id.id_string in
  Mvs.iter check vss;
  { c with c_effect = eff_filter vars c.c_effect }

exception UnboundException of xsymbol

let spec_check c ty =
  if c.c_pre.t_ty <> None then
    Loc.error ?loc:c.c_pre.t_loc (Term.FmlaExpected c.c_pre);
  check_post ty c.c_post;
  Mexn.iter (fun xs q -> check_post (ty_of_ity xs.xs_ity) q) c.c_xpost;
778
779
  let check_variant (t,rel) = match rel with
    | Some ps -> ignore (ps_app ps [t;t])
780
    | None -> ignore (t_type t) in
781
  List.iter check_variant c.c_variant;
782
783
784
785
786
787
  let sexn = Sexn.union c.c_effect.eff_raises c.c_effect.eff_ghostx in
  let sexn = Mexn.set_diff sexn c.c_xpost in
  if not (Sexn.is_empty sexn) then
    raise (UnboundException (Sexn.choose sexn))

(** program variables *)
788

789
type pvsymbol = {
790
  pv_vs    : vsymbol;
791
  pv_ity   : ity;
792
  pv_ghost : bool;
793
794
}

795
module PVsym = MakeMSHW (struct
796
797
798
799
800
801
802
803
804
805
806
  type t = pvsymbol
  let tag pv = pv.pv_vs.vs_name.id_tag
end)

module Spv = PVsym.S
module Mpv = PVsym.M
module Hpv = PVsym.H
module Wpv = PVsym.W

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

807
808
809
let create_pvsymbol id ghost ity = {
  pv_vs    = create_vsymbol id (ty_of_ity ity);
  pv_ity   = ity;
810
  pv_ghost = ghost;
811
812
}

813
814
let create_pvsymbol, restore_pv, restore_pv_by_id =
  let id_to_pv = Wid.create 17 in
815
816
  (fun id ?(ghost=false) ity ->
    let pv = create_pvsymbol id ghost ity in
817
    Wid.set id_to_pv pv.pv_vs.vs_name pv;
818
    pv),
819
820
  (fun vs -> Wid.find id_to_pv vs.vs_name),
  (fun id -> Wid.find id_to_pv id)
821
822
823
824

(** program types *)

type vty =
825
  | VTvalue of ity
826
  | VTarrow of aty
827

828
829
830
831
and aty = {
  aty_args   : pvsymbol list;
  aty_result : vty;
  aty_spec   : spec;
832
833
}

834
let rec aty_vars aty =
835
  let add_arg vars pv = vars_union vars pv.pv_ity.ity_vars in
836
  List.fold_left add_arg (vty_vars aty.aty_result) aty.aty_args
837
838

and vty_vars = function
839
  | VTvalue ity -> ity.ity_vars
840
  | VTarrow aty -> aty_vars aty
841
842

let ity_of_vty = function
843
  | VTvalue ity -> ity
844
845
846
  | VTarrow _   -> ity_unit

let ty_of_vty = function
847
  | VTvalue ity -> ty_of_ity ity
848
849
850
851
  | VTarrow _   -> ty_unit

let spec_check spec vty = spec_check spec (ty_of_vty vty)

852
let vty_arrow_unsafe argl spec vty = {
853
854
855
  aty_args   = argl;
  aty_result = vty;
  aty_spec   = spec;
856
}
857

858
let vty_arrow argl ?spec vty =
859
860
861
  let exn = Invalid_argument "Mlw.vty_arrow" in
  (* the arguments must be all distinct *)
  if argl = [] then raise exn;
862
  let add_arg pvs pv = Spv.add_new exn pv pvs in
863
864
865
866
  ignore (List.fold_left add_arg Spv.empty argl);
  let spec = match spec with
    | Some spec -> spec_check spec vty; spec
    | None -> spec_empty (ty_of_vty vty) in
867
868
869
  (* we admit non-empty variant list even for null letrec,
     so that we can store there external variables from
     user-written effects to save them from spec_filter *)
870
  vty_arrow_unsafe argl spec vty
871
872

(* this only compares the types of arguments and results, and ignores
873
874
   the spec. In other words, only the type variables and regions in
   [aty_vars aty] are matched. The caller should supply a "freezing"
875
   substitution that covers all external type variables and regions. *)
876
let rec aty_vars_match s a argl res =
877
  let rec match_args s l1 l2 = match l1, l2 with
878
879
880
881
882
883
884
885
886
    | v1::l1, v2::l2 -> match_args (ity_match s v1.pv_ity v2) l1 l2
    | [], l -> s, l
    | _, [] -> invalid_arg "Mlw_ty.aty_vars_match" in
  let s, argl = match_args s a.aty_args argl in
  match a.aty_result, argl with
  | VTvalue v, [] -> ity_match s v res
  | VTvalue _, _
  | VTarrow _, [] -> invalid_arg "Mlw_ty.aty_vars_match"
  | VTarrow a, _  -> aty_vars_match s a argl res
887

888
889
890
(* the substitution must cover not only [aty_vars aty] but
   also every type variable and every region in [aty_spec] *)
let aty_full_inst sbs aty =
891
  let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
892
893
  let pv_inst { pv_vs = vs; pv_ity = ity; pv_ghost = ghost } =
    create_pvsymbol (id_clone vs.vs_name) ~ghost (ity_full_inst sbs ity) in
894
895
896
  let add_arg vsm pv =
    let nv = pv_inst pv in
    Mvs.add pv.pv_vs (t_var nv.pv_vs) vsm, nv in
897
898
899
900
901
  let rec aty_inst vsm aty =
    let vsm, args = Lists.map_fold_left add_arg vsm aty.aty_args in
    let spec = spec_full_inst sbs tvm vsm aty.aty_spec in
    let vty = match aty.aty_result with
      | VTarrow aty -> VTarrow (aty_inst vsm aty)
902
      | VTvalue ity -> VTvalue (ity_full_inst sbs ity) in
903
    vty_arrow_unsafe args spec vty
904
  in
905
  aty_inst Mvs.empty aty
906
907

(* remove from the given arrow every effect that is covered
908
909
   neither by the arrow's aty_vars nor by the given varmap *)
let rec aty_filter varm vars aty =
910
911
  let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_ity.ity_vars m in
  let add_s pv s = vars_union pv.pv_ity.ity_vars s in
912
913
914
915
916
  let varm = List.fold_right add_m aty.aty_args varm in
  let vars = List.fold_right add_s aty.aty_args vars in
  let vty = match aty.aty_result with
    | VTarrow a -> VTarrow (aty_filter varm vars a)
    | VTvalue _ -> aty.aty_result in
917
918
  (* reads and writes must come from the context,
     resets may affect the regions in the result *)
919
920
  let spec = spec_filter varm vars aty.aty_spec in
  let rst = aty.aty_spec.c_effect.eff_resets in
921
922
923
924
925
926
  let spec = if Mreg.is_empty rst then spec else
    let vars = vars_union vars (vty_vars vty) in
    let rst = { eff_empty with eff_resets = rst } in
    let rst = (eff_filter vars rst).eff_resets in
    let eff = { spec.c_effect with eff_resets = rst } in
    { spec with c_effect = eff } in
927
  (* we must also reset every fresh region in the value *)
928
  let spec = match aty.aty_result with
929
930
    | VTvalue v ->
        let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
931
        let eff = reg_fold on_reg v.ity_vars spec.c_effect in
932
933
        { spec with c_effect = eff }
    | VTarrow _ -> spec in
934
  vty_arrow_unsafe aty.aty_args spec vty
935

936
937
let aty_filter varm aty =
  aty_filter varm (vars_merge varm vars_empty) aty
938

939
940
let aty_app aty pv =
  let arg, rest = match aty.aty_args with
941
    | arg::rest -> arg,rest | _ -> assert false in
942
  ity_equal_check arg.pv_ity pv.pv_ity;
943
944
  let sbs = Mvs.singleton arg.pv_vs (t_var pv.pv_vs) in
  let rec vty_subst = function
945
946
947
948
    | VTarrow a when not (List.exists (pv_equal arg) a.aty_args) ->
        let result = vty_subst a.aty_result in
        let spec = spec_subst sbs a.aty_spec in
        VTarrow (vty_arrow_unsafe a.aty_args spec result)
949
    | vty -> vty in
950
951
  let result = vty_subst aty.aty_result in
  let spec = spec_subst sbs aty.aty_spec in
952
  if not pv.pv_ghost && arg.pv_ghost then
953
    Loc.errorm "non-ghost value passed as a ghost argument";
954
  let ghost = pv.pv_ghost && not arg.pv_ghost in