mlw_ty.ml 31.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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
  eff_compar : Stv.t;
556
  eff_diverg : bool;
557
}
558

559
let eff_empty = {
560
561
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
562
563
564
565
  eff_raises = Sexn.empty;
  eff_ghostr = Sreg.empty;
  eff_ghostw = Sreg.empty;
  eff_ghostx = Sexn.empty;
566
  eff_resets = Mreg.empty;
567
  eff_compar = Stv.empty;
568
  eff_diverg = false;
569
}
570

571
572
573
574
575
576
577
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 &&
578
  Mreg.is_empty e.eff_resets &&
579
  (* eff_compar is not a side effect *)
580
581
582
583
584
585
586
587
588
589
  not e.eff_diverg

let eff_equal e1 e2 =
  Sreg.equal e1.eff_reads  e2.eff_reads  &&
  Sreg.equal e1.eff_writes e2.eff_writes &&
  Sexn.equal e1.eff_raises e2.eff_raises &&
  Sreg.equal e1.eff_ghostr e2.eff_ghostr &&
  Sreg.equal e1.eff_ghostw e2.eff_ghostw &&
  Sexn.equal e1.eff_ghostx e2.eff_ghostx &&
  Mreg.equal (Opt.equal reg_equal) e1.eff_resets e2.eff_resets &&
590
  Stv.equal e1.eff_compar e2.eff_compar &&
591
  e1.eff_diverg = e2.eff_diverg
592

593
594
595
596
597
598
599
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
600

601
602
603
604
605
606
607
608
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;
609
  eff_compar = Stv.union x.eff_compar y.eff_compar;
610
  eff_diverg = x.eff_diverg || y.eff_diverg;
611
612
}

613
614
exception GhostDiverg

615
616
617
618
619
620
621
622
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;
623
624
625
626
627
628
629
  eff_compar = e.eff_compar;
    (* from the code extraction point of view, we can allow comparing
       opaque types in the ghost code, as it is never extracted.
       However, if we consider Coq realisations, we have to treat
       some pure types (e.g., maps) as opaque, too, and never compare
       them even in pure formulas. Therefore, we play safe and forbid
       comparison of opaque types in the ghost code. *)
630
  eff_diverg = if e.eff_diverg then raise GhostDiverg else false;
631
632
}

633
634
let eff_ghostify gh e = if gh then eff_ghostify e else e

635
636
637
638
639
640
641
642
643
644
645
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 }
646

647
648
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

649
650
let eff_compare e tv = { e with eff_compar = Stv.add tv e.eff_compar }

651
652
let eff_diverge e = { e with eff_diverg = true }

653
exception IllegalAlias of region
654
exception IllegalCompar of tvsymbol * ity
655

656
657
658
659
660
661
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 }

662
663
let eff_assign e ?(ghost=false) r ty =
  let e = eff_write e ~ghost r in
664
665
  let sub = ity_match ity_subst_empty r.reg_ity ty in
  (* assignment cannot instantiate type variables *)
Andrei Paskevich's avatar
Andrei Paskevich committed
666
667
668
669
  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
670
    raise (TypeMismatch (r.reg_ity,ty,ity_subst_empty));
671
672
  (* 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
673
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
674
675
  (* 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
676
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
677
  (* ...except those which occur on the lhs : they are preserved under r *)
Andrei Paskevich's avatar
Andrei Paskevich committed
678
  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
679
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
680
681
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

682
683
684
685
let eff_remove_raise e x = { e with
  eff_raises = Sexn.remove x e.eff_raises;
  eff_ghostx = Sexn.remove x e.eff_ghostx;
}
686

687
688
let eff_full_inst sbs e =
  let s = sbs.ity_subst_reg in
Andrei Paskevich's avatar
Andrei Paskevich committed
689
690
691
  (* 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
692
  let wr = Sreg.union e.eff_ghostw wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
693
  (* read-only regions in e *)
Andrei Paskevich's avatar
Andrei Paskevich committed
694
  let ro = Sreg.diff (Mreg.map (Util.const ()) s) wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
695
696
697
698
699
700
701
702
703
  (* 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 *)
704
705
  let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
  let add_mreg r v acc =
706
    Mreg.add (Mreg.find r s) (Opt.map (fun v -> Mreg.find v s) v) acc in
707
708
709
710
711
712
  (* compute compared type variables *)
  let add_stv tv acc =
    let ity = Mtv.find tv sbs.ity_subst_tv in
    let check () _ = raise (IllegalCompar (tv,ity)) in
    ity_s_fold check (fun () _ -> ()) () ity;
    Stv.union acc ity.ity_vars.vars_tv in
713
714
715
716
717
718
  { 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;
719
    eff_compar = Stv.fold  add_stv  e.eff_compar Stv.empty;
720
  }
721

722
let eff_filter vars e =
723
  let check r = reg_occurs r vars in
724
725
726
727
728
729
730
731
732
733
734
  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;
735
    eff_compar = Stv.inter vars.vars_tv e.eff_compar;
736
737
  }

738
739
740
741
742
743
744
745
746
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

747
748
749
750
751
752
(** specification *)

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

753
754
type variant = term * lsymbol option (* tau * (tau -> tau -> prop) *)

755
756
757
758
759
760
761
762
763
764
765
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 = {
766
767
768
769
770
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
771
  c_letrec  : int;
772
773
774
}

let spec_empty ty = {
775
776
777
778
779
  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 = [];
780
  c_letrec  = 0;
781
782
783
784
}

let spec_full_inst sbs tvm vsm c =
  let subst = t_ty_subst tvm vsm in {
785
786
787
788
789
    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;
790
    c_letrec  = c.c_letrec;
791
792
793
794
  }

let spec_subst sbs c =
  let subst = t_subst sbs in {
795
796
797
798
799
    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;
800
    c_letrec  = c.c_letrec;
801
802
  }

803
let spec_filter ghost varm vars c =
804
805
806
807
  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
808
809
810
  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;
811
  { c with c_effect = eff_ghostify ghost (eff_filter vars c.c_effect) }
812
813
814

exception UnboundException of xsymbol

815
let spec_check ~full_xpost c ty =
816
817
818
819
  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;
820
821
  let check_variant (t,rel) = match rel with
    | Some ps -> ignore (ps_app ps [t;t])
822
    | None -> ignore (t_type t) in
823
  List.iter check_variant c.c_variant;
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
824
825
826
827
828
829
  if full_xpost && not (Mexn.set_submap c.c_effect.eff_raises c.c_xpost) then
    raise (UnboundException
      (Sexn.choose (Mexn.set_diff c.c_effect.eff_raises c.c_xpost)));
  if full_xpost && not (Mexn.set_submap c.c_effect.eff_ghostx c.c_xpost) then
    raise (UnboundException
      (Sexn.choose (Mexn.set_diff c.c_effect.eff_ghostx c.c_xpost)))
830
831

(** program variables *)
832

833
type pvsymbol = {
834
  pv_vs    : vsymbol;
835
  pv_ity   : ity;
836
  pv_ghost : bool;
837
838
}

839
module PVsym = MakeMSHW (struct
840
841
842
843
844
845
846
847
848
849
850
  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 = (==)

851
852
853
let create_pvsymbol id ghost ity = {
  pv_vs    = create_vsymbol id (ty_of_ity ity);
  pv_ity   = ity;
854
  pv_ghost = ghost;
855
856
}

857
858
let create_pvsymbol, restore_pv, restore_pv_by_id =
  let id_to_pv = Wid.create 17 in
859
860
  (fun id ?(ghost=false) ity ->
    let pv = create_pvsymbol id ghost ity in
861
    Wid.set id_to_pv pv.pv_vs.vs_name pv;
862
    pv),
863
864
  (fun vs -> Wid.find id_to_pv vs.vs_name),
  (fun id -> Wid.find id_to_pv id)
865
866
867
868

(** program types *)

type vty =
869
  | VTvalue of ity
870
  | VTarrow of aty
871

872
873
874
875
and aty = {
  aty_args   : pvsymbol list;
  aty_result : vty;
  aty_spec   : spec;
876
877
}

878
let rec aty_vars aty =
879
  let add_arg vars pv = vars_union vars pv.pv_ity.ity_vars in
880
  List.fold_left add_arg (vty_vars aty.aty_result) aty.aty_args
881
882

and vty_vars = function
883
  | VTvalue ity -> ity.ity_vars
884
  | VTarrow aty -> aty_vars aty
885
886

let ity_of_vty = function
887
  | VTvalue ity -> ity
888
889
890
  | VTarrow _   -> ity_unit

let ty_of_vty = function
891
  | VTvalue ity -> ty_of_ity ity
892
893
  | VTarrow _   -> ty_unit

894
895
let spec_check ?(full_xpost=true) spec vty =
  spec_check ~full_xpost spec (ty_of_vty vty)
896

897
let vty_arrow_unsafe argl spec vty = {
898
899
900
  aty_args   = argl;
  aty_result = vty;
  aty_spec   = spec;
901
}
902

903
let vty_arrow argl ?spec vty =
904
905
906
  let exn = Invalid_argument "Mlw.vty_arrow" in
  (* the arguments must be all distinct *)
  if argl = [] then raise exn;
907
  let add_arg pvs pv = Spv.add_new exn pv pvs in
908
909
910
911
  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
912
913
914
  (* 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 *)
915
  vty_arrow_unsafe argl spec vty
916
917

(* this only compares the types of arguments and results, and ignores
918
919
   the spec. In other words, only the type variables and regions in
   [aty_vars aty] are matched. The caller should supply a "freezing"
920
   substitution that covers all external type variables and regions. *)
921
let rec aty_vars_match s a argl res =
922
  let rec match_args s l1 l2 = match l1, l2 with
923
924
925
926
927
928
929
930
931
    | 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
932

933
934
935
(* 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 =
936
  let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
937
938
  let pv_inst {