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

open Why3
22
open Stdlib
23
24
25
open Util
open Ident
open Ty
26
open Term
27

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

30
module rec T : sig
31

32
33
34
35
  type varset = {
    vars_tv  : Stv.t;
    vars_reg : Reg.S.t;
  }
36

37
38
  type varmap = varset Mid.t

39
40
41
  type itysymbol = {
    its_pure : tysymbol;
    its_args : tvsymbol list;
42
    its_regs : region list;
43
44
45
46
    its_def  : ity option;
    its_abst : bool;
    its_priv : bool;
  }
47

48
49
50
51
52
  and ity = {
    ity_node : ity_node;
    ity_vars : varset;
    ity_tag  : Hashweak.tag;
  }
53

54
55
56
57
  and ity_node =
    | Ityvar of tvsymbol
    | Itypur of tysymbol * ity list
    | Ityapp of itysymbol * ity list * region list
58

59
60
61
62
63
64
65
66
67
68
69
70
  and region = {
    reg_name  : ident;
    reg_ity   : ity;
  }

end = struct

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

71
72
  type varmap = varset Mid.t

73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
  type itysymbol = {
    its_pure : tysymbol;
    its_args : tvsymbol list;
    its_regs : region   list;
    its_def  : ity option;
    its_abst : bool;
    its_priv : bool;
  }

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

  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
  module H : Hashtbl.S with type key = T.region
  module W : Hashweak.S with type key = T.region
end = WeakStructMake (struct
  type t = T.region
  let tag r = r.T.reg_name.id_tag
108
109
end)

110
111
112
113
open T

(** regions *)

114
115
116
117
118
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W

119
let reg_equal : region -> region -> bool = (==)
120
let reg_hash r = id_hash r.reg_name
121

122
let create_region id ty = { reg_name = id_register id; reg_ity = ty }
123

124
125
126
127
128
129
130
131
132
(* 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;
}

133
134
let vars_merge = Mid.fold (fun _ -> vars_union)

Andrei Paskevich's avatar
Andrei Paskevich committed
135
136
137
138
139
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;
}

140
141
142
143
let rec reg_occurs r vars =
  let check r r' = reg_equal r r' || reg_occurs r r'.reg_ity.ity_vars in
  Sreg.exists (check r) vars.vars_reg

144
(* value type symbols *)
145

146
147
148
module Itsym = WeakStructMake (struct
  type t = itysymbol
  let tag its = its.its_pure.ts_name.id_tag
149
150
end)

151
152
153
154
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W
155

156
157
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
158

159
160
let its_hash its = id_hash its.its_pure.ts_name
let ity_hash ity = Hashweak.tag_hash ity.ity_tag
161

162
163
module Hsity = Hashcons.Make (struct
  type t = ity
164

165
166
  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
    | Ityvar n1, Ityvar n2 ->
167
        tv_equal n1 n2
168
169
170
171
    | 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
172
          && List.for_all2 reg_equal r1 r2
173
174
    | _ ->
        false
175

176
177
178
179
  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) ->
180
        Hashcons.combine_list reg_hash
181
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl
182

183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
  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;
    ity_tag  = Hashweak.create_tag n }

198
199
end)

200
201
202
module Ity = WeakStructMake (struct
  type t = ity
  let tag ity = ity.ity_tag
203
204
end)

205
206
207
208
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W
209

210
211
let mk_ity n = {
  ity_node = n;
212
  ity_vars = vars_empty;
213
  ity_tag  = Hashweak.dummy_tag;
214
215
}

216
217
218
let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
let ity_pur s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_app s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
219
220
221

(* generic traversal functions *)

222
223
224
225
let ity_map fn ity = match ity.ity_node with
  | Ityvar _ -> ity
  | Itypur (f,tl) -> ity_pur f (List.map fn tl)
  | Ityapp (f,tl,rl) -> ity_app f (List.map fn tl) rl
226

227
228
229
230
let ity_fold fn acc ity = match ity.ity_node with
  | Ityvar _ -> acc
  | Itypur (_,tl)
  | Ityapp (_,tl,_) -> List.fold_left fn acc tl
231

232
233
let ity_all pr ity =
  try ity_fold (all_fn pr) true ity with FoldSkip -> false
234

235
236
let ity_any pr ity =
  try ity_fold (any_fn pr) false ity with FoldSkip -> true
237

238
239
240
241
242
243
244
245
246
(* 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

247
248
249
250
let ity_s_all pr pts ity =
  try ity_s_fold (all_fn pr) (all_fn pts) true ity with FoldSkip -> false

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

253
254
(* traversal functions on type variables and regions *)

255
let rec ity_v_map fnv fnr ity = match ity.ity_node with
256
  | Ityvar v ->
257
      fnv v
258
  | Itypur (f,tl) ->
259
      ity_pur f (List.map (ity_v_map fnv fnr) tl)
260
  | Ityapp (f,tl,rl) ->
261
      ity_app f (List.map (ity_v_map fnv fnr) tl) (List.map fnr rl)
262
263
264

let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
  | Ityvar v ->
265
      fnv acc v
266
267
268
269
  | Itypur (_,tl) ->
      List.fold_left (ity_v_fold fnv fnr) acc tl
  | Ityapp (_,tl,rl) ->
      List.fold_left (ity_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
270

271
272
let ity_v_all prv prr ity =
  try ity_v_fold (all_fn prv) (all_fn prr) true ity with FoldSkip -> false
273

274
275
let ity_v_any prv prr ity =
  try ity_v_fold (any_fn prv) (any_fn prr) false ity with FoldSkip -> true
276

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

280
281
let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
282
283
284

(* smart constructors *)

285
286
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
287

288
289
exception DuplicateRegion of region
exception UnboundRegion of region
290

291
exception RegionMismatch of region * region
292
exception TypeMismatch of ity * ity
293

294
295
let ity_equal_check ty1 ty2 =
  if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
296

297
298
299
let reg_equal_check r1 r2 =
  if not (reg_equal r1 r2) then raise (RegionMismatch (r1, r2))

300
type ity_subst = {
301
  ity_subst_tv  : ity Mtv.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
302
  ity_subst_reg : region Mreg.t; (* must preserve ghost-ness *)
303
304
}

305
let ity_subst_empty = {
306
  ity_subst_tv  = Mtv.empty;
307
  ity_subst_reg = Mreg.empty;
308
309
}

310
311
312
313
314
315
let ity_subst_union s1 s2 =
  let check_ity _ ity1 ity2 = ity_equal_check ity1 ity2; Some ity1 in
  let check_reg _ r1 r2 = reg_equal_check r1 r2; Some r1 in
  { ity_subst_tv  = Mtv.union  check_ity s1.ity_subst_tv  s2.ity_subst_tv;
    ity_subst_reg = Mreg.union check_reg s1.ity_subst_reg s2.ity_subst_reg }

316
317
let tv_inst s v = Mtv.find_def (ity_var v) v s.ity_subst_tv
let reg_inst s r = Mreg.find_def r r s.ity_subst_reg
Andrei Paskevich's avatar
Andrei Paskevich committed
318
319
320
321

let ity_inst s ity =
  if ity_closed ity && ity_pure ity then ity
  else ity_v_map (tv_inst s) (reg_inst s) ity
322

323
let reg_full_inst s r = Mreg.find r s.ity_subst_reg
Andrei Paskevich's avatar
Andrei Paskevich committed
324
325
326
327

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
328

329
let rec ity_match s ity1 ity2 =
330
  let set = function
331
332
    | None -> Some ity2
    | Some ity3 as r when ity_equal ity3 ity2 -> r
333
334
    | _ -> raise Exit
  in
335
336
337
  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
338
      List.fold_left2 reg_match s r1 r2
339
340
341
  | Itypur (s1, l1), Itypur (s2, l2) when ts_equal s1 s2 ->
      List.fold_left2 ity_match s l1 l2
  | Ityvar tv1, _ ->
342
      { s with ity_subst_tv = Mtv.change set tv1 s.ity_subst_tv }
343
344
345
346
347
  | _ ->
      raise Exit

and reg_match s r1 r2 =
  let is_new = ref false in
348
349
  let set = function
    | None -> is_new := true; Some r2
350
351
352
    | Some r3 as r when reg_equal r3 r2 -> r
    | _ -> raise Exit
  in
353
  let reg_map = Mreg.change set r1 s.ity_subst_reg in
354
355
  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
356

357
358
359
let ity_match s ity1 ity2 =
  try ity_match s ity1 ity2
  with Exit -> raise (TypeMismatch (ity_inst s ity1, ity2))
360

361
362
363
364
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)
365

366
367
368
let rec ity_of_ty ty = match ty.ty_node with
  | Tyvar v -> ity_var v
  | Tyapp (s,tl) -> ity_pur s (List.map ity_of_ty tl)
369

370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
let rec ity_inst_fresh mv mr ity = match ity.ity_node with
  | Ityvar v ->
      mr, Mtv.find v mv
  | Itypur (s,tl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
      mr, ity_pur s tl
  | Ityapp (s,tl,rl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
      let mr,rl = Util.map_fold_left (reg_refresh mv) mr rl in
      mr, ity_app s tl rl

and reg_refresh mv mr r = match Mreg.find_opt r mr with
  | Some r ->
      mr, r
  | None ->
      let mr,ity = ity_inst_fresh mv mr r.reg_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
386
      let id = id_clone r.reg_name in
387
      let reg = create_region id ity in
388
389
390
391
392
393
394
395
396
397
      Mreg.add r reg mr, reg

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

403
let ity_app s tl rl =
404
  (* type variable map *)
405
  let add m v t = Mtv.add v t m in
406
407
408
409
  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
410
411
  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
412
413
    with Invalid_argument _ ->
      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  (* every type var and top region in def are in its_args and its_regs *)
415
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
416
  | Some ity -> ity_full_inst sub ity
417
  | None -> ity_app s tl rl
418

419
let ity_pur s tl = match s.ts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
420
421
  | Some ty ->
      let add m v t = Mtv.add v t m in
422
423
424
      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
425
      ity_subst_unsafe m Mreg.empty (ity_of_ty ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
426
  | None ->
427
      ity_pur s tl
Andrei Paskevich's avatar
Andrei Paskevich committed
428

429
let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
430
  let puredef = option_map ty_of_ity def in
Andrei Paskevich's avatar
Andrei Paskevich committed
431
  let purets = create_tysymbol name args puredef in
432
  (* all regions *)
433
  let add s v = Sreg.add_new (DuplicateRegion v) v s in
434
435
436
437
438
  let sregs = List.fold_left add Sreg.empty regs in
  (* all type variables *)
  let sargs = List.fold_right Stv.add args Stv.empty in
  (* all type variables in [regs] must be in [args] *)
  let check tv = Stv.mem tv sargs || raise (UnboundTypeVar tv) in
439
  List.iter (fun r -> ignore (ity_v_all check Util.ttrue r.reg_ity)) regs;
440
441
  (* all regions in [def] must be in [regs] *)
  let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
442
  ignore (option_map (ity_v_all Util.ttrue check) def);
443
  (* if a type is an alias then it cannot be abstract or private *)
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
444
445
  if abst && def <> None then Loc.errorm "A type alias cannot be abstract";
  if priv && def <> None then Loc.errorm "A type alias cannot be private";
446
447
448
  { its_pure  = purets;
    its_args  = args;
    its_regs  = regs;
449
450
451
    its_def   = def;
    its_abst  = abst;
    its_priv  = priv }
452

Andrei Paskevich's avatar
Andrei Paskevich committed
453
454
455
let ts_unit = ts_tuple 0
let ty_unit = ty_tuple []

Andrei Paskevich's avatar
Andrei Paskevich committed
456
457
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
458
let ity_unit = ity_of_ty ty_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
459

460
461
462
463
464
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

465
466
467
468
469
(** computation types (with effects) *)

(* exception symbols *)
type xsymbol = {
  xs_name : ident;
470
  xs_ity  : ity; (* closed and pure *)
471
}
472

473
474
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
475

476
477
let xs_equal : xsymbol -> xsymbol -> bool = (==)

478
479
480
481
482
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; }
483

484
485
486
487
module Exn = StructMake (struct
  type t = xsymbol
  let tag xs = Hashweak.tag_hash xs.xs_name.id_tag
end)
488

489
490
491
492
493
module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
type effect = {
494
495
  eff_reads  : Sreg.t;
  eff_writes : Sreg.t;
496
497
498
499
  eff_raises : Sexn.t;
  eff_ghostr : Sreg.t; (* ghost reads *)
  eff_ghostw : Sreg.t; (* ghost writes *)
  eff_ghostx : Sexn.t; (* ghost raises *)
500
501
  (* if r1 -> Some r2 then r1 appears in ty(r2) *)
  eff_resets : region option Mreg.t;
502
}
503

504
let eff_empty = {
505
506
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
507
508
509
510
  eff_raises = Sexn.empty;
  eff_ghostr = Sreg.empty;
  eff_ghostw = Sreg.empty;
  eff_ghostx = Sexn.empty;
511
  eff_resets = Mreg.empty;
512
}
513

514
515
516
517
518
519
520
521
522
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

523
524
525
526
527
528
529
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
530

531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
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 }
562

563
564
565
566
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

exception IllegalAlias of region

567
568
569
570
571
572
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 }

573
574
let eff_assign e ?(ghost=false) r ty =
  let e = eff_write e ~ghost r in
575
576
  let sub = ity_match ity_subst_empty r.reg_ity ty in
  (* assignment cannot instantiate type variables *)
Andrei Paskevich's avatar
Andrei Paskevich committed
577
578
579
580
  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
581
582
583
    raise (TypeMismatch (r.reg_ity,ty));
  (* r:t[r1,r2] <- t[r1,r1] introduces an alias *)
  let add_right _ v s = Sreg.add_new (IllegalAlias v) v s in
Andrei Paskevich's avatar
Andrei Paskevich committed
584
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
585
586
  (* 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
587
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
588
  (* ...except those which occur on the lhs : they are preserved under r *)
Andrei Paskevich's avatar
Andrei Paskevich committed
589
  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
590
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
591
592
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

593
594
595
596
let eff_remove_raise e x = { e with
  eff_raises = Sexn.remove x e.eff_raises;
  eff_ghostx = Sexn.remove x e.eff_ghostx;
}
597

Andrei Paskevich's avatar
Andrei Paskevich committed
598
599
600
601
602
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
603
  let wr = Sreg.union e.eff_ghostw wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
604
  (* read-only regions in e *)
605
  let ro = Sreg.diff (Sreg.union e.eff_reads e.eff_ghostr) wr in
Andrei Paskevich's avatar
Andrei Paskevich committed
606
607
608
609
610
611
612
613
614
  (* 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 *)
615
616
  let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
  let add_mreg r v acc =
Andrei Paskevich's avatar
Andrei Paskevich committed
617
    Mreg.add (Mreg.find r s) (option_map (fun v -> Mreg.find v s) v) acc in
618
619
620
621
622
623
624
  { 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;
  }
625

626
let eff_filter vars e =
627
  let check r = reg_occurs r vars in
628
629
630
631
632
633
634
635
636
637
638
639
640
  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;
  }

641
642
643
644
645
646
(** specification *)

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

647
648
type variant = term * lsymbol option (* tau * (tau -> tau -> prop) *)

649
650
651
652
653
654
655
656
657
658
659
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 = {
660
661
662
663
664
665
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
  c_letrec  : int;
666
667
668
}

let spec_empty ty = {
669
670
671
672
673
674
  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 = [];
  c_letrec  = 0;
675
676
677
678
}

let spec_full_inst sbs tvm vsm c =
  let subst = t_ty_subst tvm vsm in {
679
680
681
682
683
684
    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;
    c_letrec  = c.c_letrec;
685
686
687
688
  }

let spec_subst sbs c =
  let subst = t_subst sbs in {
689
690
691
692
693
694
    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;
    c_letrec  = c.c_letrec;
695
696
697
  }

let spec_filter varm vars c =
698
699
700
701
  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
702
703
704
705
706
707
708
709
710
711
712
713
  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;
714
715
716
717
  let check_variant (t,rel) = match rel with
    | Some ps -> ignore (ps_app ps [t;t])
    | None -> t_ty_check t (Some ty_int) in
  List.iter check_variant c.c_variant;
718
719
720
721
722
723
  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 *)
724
725
726
727
728
729
730
731

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

let vty_value ?(ghost=false) ?mut ity =
732
733
  Util.option_iter (fun r -> ity_equal_check ity r.reg_ity) mut;
  { vtv_ity   = ity;
734
    vtv_ghost = ghost;
735
736
737
738
739
    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
740

741
742
743
744
let vtv_unmut vtv =
  if vtv.vtv_mut = None then vtv else
    vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity

745
type pvsymbol = {
746
747
748
  pv_vs   : vsymbol;
  pv_vtv  : vty_value;
  pv_vars : varset;
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
}

module PVsym = WeakStructMake (struct
  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;
766
  pv_vars = vtv_vars vtv;
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
}

let create_pvsymbol, restore_pv =
  let vs_to_pv = Wvs.create 17 in
  (fun id vtv ->
    let pv = create_pvsymbol id vtv in
    Wvs.set vs_to_pv pv.pv_vs pv;
    pv),
  (fun vs -> try Wvs.find vs_to_pv vs with Not_found ->
    Loc.error ?loc:vs.vs_name.id_loc (Decl.UnboundVar vs))

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

791
let rec vta_vars vta =
792
  let add_arg vars pv = vars_union vars pv.pv_vars in
793
794
795
  List.fold_left add_arg (vty_vars vta.vta_result) vta.vta_args

and vty_vars = function
796
  | VTvalue vtv -> vtv_vars vtv
797
  | VTarrow vta -> vta_vars vta
798

799
800
801
802
let vty_ghost = function
  | VTvalue vtv -> vtv.vtv_ghost
  | VTarrow vta -> vta.vta_ghost

803
804
805
806
807
808
809
810
811
812
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)

813
814
815
816
817
818
let vty_arrow_unsafe argl ~spec ~ghost vty = {
  vta_args   = argl;
  vta_result = vty;
  vta_spec   = spec;
  vta_ghost  = ghost || vty_ghost vty;
}
819

820
let vty_arrow argl ?spec ?(ghost=false) vty =
821
822
823
  let exn = Invalid_argument "Mlw.vty_arrow" in
  (* the arguments must be all distinct *)
  if argl = [] then raise exn;
824
825
  let add_arg pvs pv =
    (* mutable arguments are rejected outright *)
826
827
    if pv.pv_vtv.vtv_mut <> None then raise exn;
    Spv.add_new exn pv pvs in
828
  ignore (List.fold_left add_arg Spv.empty argl);
829
830
831
832
833
  (* only projections may return mutable values *)
  begin match vty with
    | VTvalue { vtv_mut = Some _ } -> raise exn
    | _ -> ()
  end;
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
  let spec = match spec with
    | Some spec -> spec_check spec vty; spec
    | None -> spec_empty (ty_of_vty vty) in
  vty_arrow_unsafe argl ~spec ~ghost vty

(* 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 =
    let vsm, args = Util.map_fold_left add_arg vsm vta.vta_args in
    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
    vty_arrow_unsafe args ~ghost:vta.vta_ghost ~spec vty
  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 =
882
883
  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
884
885
886
887
888
889
890
891
892
  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
893
894
895
896
897
898
  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
899
900
901
902
903
  vty_arrow_unsafe vta.vta_args ~ghost:vta.vta_ghost ~spec vty

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

904
905
906
907
908
909
910
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)

911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
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
        VTarrow (vty_arrow_unsafe a.vta_args ~ghost:a.vta_ghost ~spec result)
    | vty -> vty in
  let result = vty_subst vta.vta_result in
  let spec = spec_subst sbs vta.vta_spec in
  let ghost = vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
  if rest = [] then spec, (if ghost then vty_ghostify result else result)
  else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest ~ghost ~spec result)