mlw_ty.ml 31 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
29
30
  type itysymbol = {
    its_pure : tysymbol;
    its_args : tvsymbol list;
31
    its_regs : region list;
32
    its_def  : ity option;
33
    its_inv  : bool;
34
35
36
    its_abst : bool;
    its_priv : bool;
  }
37

38
39
40
  and ity = {
    ity_node : ity_node;
    ity_vars : varset;
Andrei Paskevich's avatar
Andrei Paskevich committed
41
    ity_tag  : Weakhtbl.tag;
42
  }
43

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

49
50
51
52
53
54
55
56
57
58
59
60
  and region = {
    reg_name  : ident;
    reg_ity   : ity;
  }

end = struct

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

61
62
  type varmap = varset Mid.t

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

  and ity = {
    ity_node : ity_node;
    ity_vars : varset;
Andrei Paskevich's avatar
Andrei Paskevich committed
76
    ity_tag  : Weakhtbl.tag;
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
  }

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

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

end

and Reg : sig
  module M : Map.S with type key = T.region
  module S : M.Set
Andrei Paskevich's avatar
Andrei Paskevich committed
94
  module H : XHashtbl.S with type key = T.region
Andrei Paskevich's avatar
Andrei Paskevich committed
95
  module W : Weakhtbl.S with type key = T.region
96
end = MakeMSHW (struct
97
98
  type t = T.region
  let tag r = r.T.reg_name.id_tag
99
100
end)

101
102
103
104
open T

(** regions *)

105
106
107
108
109
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W

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

113
let create_region id ty = { reg_name = id_register id; reg_ity = ty }
114

115
116
117
118
119
120
121
122
123
(* 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;
}

124
125
let vars_merge = Mid.fold (fun _ -> vars_union)

Andrei Paskevich's avatar
Andrei Paskevich committed
126
127
128
129
130
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;
}

131
(* value type symbols *)
132

133
module Itsym = MakeMSHW (struct
134
135
  type t = itysymbol
  let tag its = its.its_pure.ts_name.id_tag
136
137
end)

138
139
140
141
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W
142

143
144
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
145

146
let its_hash its = id_hash its.its_pure.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
147
let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
148

149
150
module Hsity = Hashcons.Make (struct
  type t = ity
151

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

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

170
171
172
173
174
175
176
177
178
179
180
181
182
  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
183
    ity_tag  = Weakhtbl.create_tag n }
184

185
186
end)

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

192
193
194
195
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W
196

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

203
let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
204
205
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)))
206
207
208

(* generic traversal functions *)

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

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

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

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

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

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

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

242
243
(* traversal functions on type variables and regions *)

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

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

255
256
let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
257

258
259
260
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
261

262
263
264
265
266
267
268
269
270
271
272
273
274
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 =
275
  let on_reg r = fn r; reg_iter fn r.reg_ity.ity_vars in
276
277
278
279
  Sreg.iter on_reg vars.vars_reg

let reg_occurs r vars = reg_any (reg_equal r) vars

280
281
(* smart constructors *)

282
283
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
284

285
286
exception DuplicateRegion of region
exception UnboundRegion of region
287

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

293
let ity_subst_empty = {
294
  ity_subst_tv  = Mtv.empty;
295
  ity_subst_reg = Mreg.empty;
296
297
}

Andrei Paskevich's avatar
Andrei Paskevich committed
298
299
exception RegionMismatch of region * region * ity_subst
exception TypeMismatch of ity * ity * ity_subst
Andrei Paskevich's avatar
Andrei Paskevich committed
300

Andrei Paskevich's avatar
Andrei Paskevich committed
301
302
303
304
305
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))
306

307
let reg_full_inst s r = Mreg.find r s.ity_subst_reg
Andrei Paskevich's avatar
Andrei Paskevich committed
308
309
310
311

let ity_full_inst s ity =
  if ity_closed ity && ity_pure ity then ity
  else ity_subst_unsafe s.ity_subst_tv s.ity_subst_reg ity
312

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

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

341
342
let ity_match s ity1 ity2 =
  try ity_match s ity1 ity2
Andrei Paskevich's avatar
Andrei Paskevich committed
343
344
345
346
347
  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))
348

349
350
351
352
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)
353

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

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

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
374
      let id = id_clone r.reg_name in
375
      let reg = create_region id ity in
376
377
378
379
380
381
382
383
384
      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 *)
385
  let mr,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
Andrei Paskevich's avatar
Andrei Paskevich committed
386
  (* every top region in def is guaranteed to be in mr *)
387
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
388
  | Some ity -> ity_subst_unsafe mv mr ity
389
  | None -> ity_app_unsafe s tl rl
390

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

407
let ity_pur s tl = match s.ts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
408
409
  | Some ty ->
      let add m v t = Mtv.add v t m in
410
411
412
      let m = 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
Andrei Paskevich's avatar
Andrei Paskevich committed
413
      ity_subst_unsafe m Mreg.empty (ity_of_ty ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  | None ->
415
416
417
418
      ity_pur_unsafe s tl

let create_itysymbol_unsafe, restore_its =
  let ts_to_its = Wts.create 17 in
419
  (fun ts ~abst ~priv ~inv regs def ->
420
421
422
423
424
    let its = {
      its_pure  = ts;
      its_args  = ts.ts_args;
      its_regs  = regs;
      its_def   = def;
425
      its_inv   = inv;
426
427
428
429
430
431
      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
432

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

Andrei Paskevich's avatar
Andrei Paskevich committed
456
457
458
let ts_unit = ts_tuple 0
let ty_unit = ty_tuple []

Andrei Paskevich's avatar
Andrei Paskevich committed
459
460
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
461
let ity_unit = ity_of_ty ty_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
462

463
464
465
466
467
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

468
469
470
471
472
473
474
475
476
(** 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
477
      let inv  = oits.its_inv in
478
      let regs = List.map conv_reg oits.its_regs in
479
      let def = Opt.map conv_ity oits.its_def in
480
      create_itysymbol_unsafe nts ~abst ~priv ~inv regs def
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
    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 ->
      try add_ts its (Mts.find its.its_pure sm.Theory.sm_ts)
      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;
511
512
  Hits.fold Mits.add itsh Mits.empty,
  Hreg.fold Mreg.add regh Mreg.empty
513

514
515
516
517
518
(** computation types (with effects) *)

(* exception symbols *)
type xsymbol = {
  xs_name : ident;
519
  xs_ity  : ity; (* closed and pure *)
520
}
521

522
523
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
524

525
526
let xs_equal : xsymbol -> xsymbol -> bool = (==)

527
528
529
530
531
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; }
532

533
module Exn = MakeMSH (struct
534
  type t = xsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
535
  let tag xs = Weakhtbl.tag_hash xs.xs_name.id_tag
536
end)
537

538
539
540
541
542
module Sexn = Exn.S
module Mexn = Exn.M

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

553
let eff_empty = {
554
555
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
556
557
558
559
  eff_raises = Sexn.empty;
  eff_ghostr = Sreg.empty;
  eff_ghostw = Sreg.empty;
  eff_ghostx = Sexn.empty;
560
  eff_resets = Mreg.empty;
561
}
562

563
564
565
566
567
568
569
570
571
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

572
573
574
575
576
577
578
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
579

580
581
582
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
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;
}

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

612
613
614
615
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

exception IllegalAlias of region

616
617
618
619
620
621
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 }

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

642
643
644
645
let eff_remove_raise e x = { e with
  eff_raises = Sexn.remove x e.eff_raises;
  eff_ghostx = Sexn.remove x e.eff_ghostx;
}
646

Andrei Paskevich's avatar
Andrei Paskevich committed
647
648
649
650
651
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
652
  let wr = Sreg.union e.eff_ghostw wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
653
  (* read-only regions in e *)
Andrei Paskevich's avatar
Andrei Paskevich committed
654
  let ro = Sreg.diff (Mreg.map (Util.const ()) s) wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
655
656
657
658
659
660
661
662
663
  (* 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 *)
664
665
  let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
  let add_mreg r v acc =
666
    Mreg.add (Mreg.find r s) (Opt.map (fun v -> Mreg.find v s) v) acc in
667
668
669
670
671
672
673
  { 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;
  }
674

675
let eff_filter vars e =
676
  let check r = reg_occurs r vars in
677
678
679
680
681
682
683
684
685
686
687
688
689
  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;
  }

690
691
692
693
694
695
696
697
698
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

699
700
701
702
703
704
(** specification *)

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

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

707
708
709
710
711
712
713
714
715
716
717
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 = {
718
719
720
721
722
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
723
  c_letrec  : int;
724
725
726
}

let spec_empty ty = {
727
728
729
730
731
  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 = [];
732
  c_letrec  = 0;
733
734
735
736
}

let spec_full_inst sbs tvm vsm c =
  let subst = t_ty_subst tvm vsm in {
737
738
739
740
741
    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;
742
    c_letrec  = c.c_letrec;
743
744
745
746
  }

let spec_subst sbs c =
  let subst = t_subst sbs in {
747
748
749
750
751
    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;
752
    c_letrec  = c.c_letrec;
753
754
755
  }

let spec_filter varm vars c =
756
757
758
759
  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
760
761
762
763
764
765
766
767
768
769
770
771
  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;
772
773
  let check_variant (t,rel) = match rel with
    | Some ps -> ignore (ps_app ps [t;t])
774
    | None -> ignore (t_type t) in
775
  List.iter check_variant c.c_variant;
776
777
778
779
780
781
  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 *)
782
783
784
785
786
787
788
789

type vty_value = {
  vtv_ity   : ity;
  vtv_ghost : bool;
  vtv_mut   : region option;
}

let vty_value ?(ghost=false) ?mut ity =
790
  Opt.iter (fun r -> ity_equal_check ity r.reg_ity) mut;
791
  { vtv_ity   = ity;
792
    vtv_ghost = ghost;
793
794
795
796
797
    vtv_mut   = mut }

let vtv_vars {vtv_ity = {ity_vars = vars}; vtv_mut = mut} = match mut with
  | Some r -> { vars with vars_reg = Sreg.add r vars.vars_reg }
  | None   -> vars
798

799
800
801
802
let vtv_unmut vtv =
  if vtv.vtv_mut = None then vtv else
    vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity

803
type pvsymbol = {
804
805
806
  pv_vs   : vsymbol;
  pv_vtv  : vty_value;
  pv_vars : varset;
807
808
}

809
module PVsym = MakeMSHW (struct
810
811
812
813
814
815
816
817
818
819
820
821
822
823
  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 = (==)

let create_pvsymbol id vtv = {
  pv_vs   = create_vsymbol id (ty_of_ity vtv.vtv_ity);
  pv_vtv  = vtv;
824
  pv_vars = vtv_vars vtv;
825
826
}

827
828
let create_pvsymbol, restore_pv, restore_pv_by_id =
  let id_to_pv = Wid.create 17 in
829
830
  (fun id vtv ->
    let pv = create_pvsymbol id vtv in
831
    Wid.set id_to_pv pv.pv_vs.vs_name pv;
832
    pv),
833
834
  (fun vs -> Wid.find id_to_pv vs.vs_name),
  (fun id -> Wid.find id_to_pv id)
835
836
837
838
839
840
841
842
843
844
845
846
847
848

(** program types *)

type vty =
  | VTvalue of vty_value
  | VTarrow of vty_arrow

and vty_arrow = {
  vta_args   : pvsymbol list;
  vta_result : vty;
  vta_spec   : spec;
  vta_ghost  : bool;
}

849
let rec vta_vars vta =
850
  let add_arg vars pv = vars_union vars pv.pv_vars in
851
852
853
  List.fold_left add_arg (vty_vars vta.vta_result) vta.vta_args

and vty_vars = function
854
  | VTvalue vtv -> vtv_vars vtv
855
  | VTarrow vta -> vta_vars vta
856

857
858
859
860
let vty_ghost = function
  | VTvalue vtv -> vtv.vtv_ghost
  | VTarrow vta -> vta.vta_ghost

861
862
863
864
865
866
867
868
869
870
let ity_of_vty = function
  | VTvalue vtv -> vtv.vtv_ity
  | VTarrow _   -> ity_unit

let ty_of_vty = function
  | VTvalue vtv -> ty_of_ity vtv.vtv_ity
  | VTarrow _   -> ty_unit

let spec_check spec vty = spec_check spec (ty_of_vty vty)

871
let vty_arrow_unsafe argl spec ghost vty = {
872
873
874
875
876
  vta_args   = argl;
  vta_result = vty;
  vta_spec   = spec;
  vta_ghost  = ghost || vty_ghost vty;
}
877

878
let vty_arrow argl ?spec ?(ghost=false) vty =
879
880
881
  let exn = Invalid_argument "Mlw.vty_arrow" in
  (* the arguments must be all distinct *)
  if argl = [] then raise exn;
882
883
  let add_arg pvs pv =
    (* mutable arguments are rejected outright *)
884
885
    if pv.pv_vtv.vtv_mut <> None then raise exn;
    Spv.add_new exn pv pvs in
886
  ignore (List.fold_left add_arg Spv.empty argl);
887
888
889
890
891
  (* only projections may return mutable values *)
  begin match vty with
    | VTvalue { vtv_mut = Some _ } -> raise exn
    | _ -> ()
  end;
892
893
894
  let spec = match spec with
    | Some spec -> spec_check spec vty; spec
    | None -> spec_empty (ty_of_vty vty) in
895
896
897
  (* 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 *)
898
  vty_arrow_unsafe argl spec ghost vty
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930

(* this only compares the types of arguments and results, and ignores
   the spec. In other words, only the type variables and regions
   in .vta_vars are matched. The caller should supply a "freezing"
   substitution that covers all external type variables and regions. *)
let rec vta_vars_match s a1 a2 =
  let vtv_match s v1 v2 = ity_match s v1.vtv_ity v2.vtv_ity in
  let rec match_args s l1 l2 = match l1, l2 with
    | [],[] -> s, a1.vta_result, a2.vta_result
    | [], _ -> s, a1.vta_result, VTarrow { a2 with vta_args = l2 }
    | _, [] -> s, VTarrow { a1 with vta_args = l1 }, a2.vta_result
    | {pv_vtv = v1}::l1, {pv_vtv = v2}::l2 ->
        match_args (vtv_match s v1 v2) l1 l2
  in
  let s, vty1, vty2 = match_args s a1.vta_args a2.vta_args in
  match vty1, vty2 with
  | VTarrow a1, VTarrow a2 -> vta_vars_match s a1 a2
  | VTvalue v1, VTvalue v2 -> vtv_match s v1 v2
  | _ -> invalid_arg "Mlw_ty.vta_vars_match"

(* the substitution must cover not only vta.vta_tvs and vta.vta_regs
   but also every type variable and every region in vta_spec *)
let vta_full_inst sbs vta =
  let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
  let vtv_inst { vtv_ity = ity; vtv_ghost = ghost } =
    vty_value ~ghost (ity_full_inst sbs ity) in
  let pv_inst { pv_vs = vs; pv_vtv = vtv } =
    create_pvsymbol (id_clone vs.vs_name) (vtv_inst vtv) in
  let add_arg vsm pv =
    let nv = pv_inst pv in
    Mvs.add pv.pv_vs (t_var nv.pv_vs) vsm, nv in
  let rec vta_inst vsm vta =
931
    let vsm, args = Lists.map_fold_left add_arg vsm vta.vta_args in
932
933
934
935
    let spec = spec_full_inst sbs tvm vsm vta.vta_spec in
    let vty = match vta.vta_result with
      | VTarrow vta -> VTarrow (vta_inst vsm vta)
      | VTvalue vtv -> VTvalue (vtv_inst vtv) in
936
    vty_arrow_unsafe args spec vta.vta_ghost vty
937
938
939
940
941
942
  in
  vta_inst Mvs.empty vta

(* remove from the given arrow every effect that is covered
   neither by the arrow's vta_vars nor by the given varmap *)
let rec vta_filter varm vars vta =
943
944
  let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_vars m in
  let add_s pv s = vars_union pv.pv_vars s in
945
946
947
948
949
950
951
952
953
  let varm = List.fold_right add_m vta.vta_args varm in
  let vars = List.fold_right add_s vta.vta_args vars in
  let vty = match vta.vta_result with
    | VTarrow a -> VTarrow (vta_filter varm vars a)
    | VTvalue _ -> vta.vta_result in
  (* reads and writes must come from the context,
     resets may affect the regions in the result *)
  let spec = spec_filter varm vars vta.vta_spec in
  let rst = vta.vta_spec.c_effect.eff_resets in
954
955
956
957
958
959
  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
960
961
962
963
964
965
966
  (* we must also reset every fresh region in the value *)
  let spec = match vta.vta_result with
    | VTvalue v ->
        let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
        let eff = reg_fold on_reg v.vtv_ity.ity_vars spec.c_effect in
        { spec with c_effect = eff }
    | VTarrow _ -> spec in
967
  vty_arrow_unsafe vta.vta_args spec vta.vta_ghost vty
968
969
970
971

let vta_filter varm vta =
  vta_filter varm (vars_merge varm vars_empty) vta

972
973
974
975
976
977
978
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)

979
980
981
982
983
984
985
986
987
988
let vta_app vta pv =
  let vtv = pv.pv_vtv in
  let arg, rest = match vta.vta_args with
    | arg::rest -> arg,rest | _ -> assert false in
  ity_equal_check arg.pv_vtv.vtv_ity vtv.vtv_ity;
  let sbs = Mvs.singleton arg.pv_vs (t_var pv.pv_vs) in
  let rec vty_subst = function
    | VTarrow a when not (List.exists (pv_equal arg) a.vta_args) ->
        let result = vty_subst a.vta_result in
        let spec = spec_subst sbs a.vta_spec in
989
        VTarrow (vty_arrow_unsafe a.vta_args spec a.vta_ghost result)
990
991
992
    | vty -> vty in
  let result = vty_subst vta.vta_result in
  let spec = spec_subst sbs vta.vta_spec in
993
994
  if not vtv.vtv_ghost && arg.pv_vtv.vtv_ghost then
    Loc.errorm "non-ghost value passed as a ghost argument";
995
996
  let ghost =
    vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
997
998
  if rest = [] then spec, (if ghost then vty_ghostify result else result)
  else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest spec ghost result)