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

open Why3
open Util
open Ident
open Ty
25
open Term
26

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

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

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

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

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

54
(** regions *)
55
56
57

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

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

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

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

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

81
(* value type symbols *)
82

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

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

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

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

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

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

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

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

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

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

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

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

(* generic traversal functions *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* smart constructors *)

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

213
214
exception DuplicateRegion of region
exception UnboundRegion of region
215

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(** computation types (with effects) *)

(* exception symbols *)
type xsymbol = {
  xs_name : ident;
389
  xs_ity  : ity; (* closed and pure *)
390
}
391

392
393
exception PolymorphicException of ident * ity
exception MutableException of ident * ity
394

395
396
397
398
399
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; }
400

401
402
403
404
module Exn = StructMake (struct
  type t = xsymbol
  let tag xs = Hashweak.tag_hash xs.xs_name.id_tag
end)
405

406
407
408
409
410
module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
type effect = {
411
412
413
414
415
  eff_reads  : Sreg.t;
  eff_writes : Sreg.t;
  (* if r1 -> Some r2 then r1 appears in ty(r2) *)
  eff_resets : region option Mreg.t;
  eff_raises : Sexn.t;
416
}
417

418
let eff_empty = {
419
420
421
422
  eff_reads  = Sreg.empty;
  eff_writes = Sreg.empty;
  eff_resets = Mreg.empty;
  eff_raises = Sexn.empty
423
}
424

425
426
427
let join_reset _key v1 v2 =
  Some (if option_eq reg_equal v1 v2 then v1 else None)

428
let eff_union x y =
429
  { eff_reads  = Sreg.union x.eff_reads  y.eff_reads;
430
    eff_writes = Sreg.union x.eff_writes y.eff_writes;
431
    eff_resets = Mreg.union join_reset x.eff_resets y.eff_resets;
Andrei Paskevich's avatar
Andrei Paskevich committed
432
433
    eff_raises = Sexn.union x.eff_raises y.eff_raises;
  }
434

435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
let eff_read  e r = { e with eff_reads  = Sreg.add r e.eff_reads }
let eff_write e r = { e with eff_writes = Sreg.add r e.eff_writes }
let eff_raise e x = { e with eff_raises = Sexn.add x e.eff_raises }
let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }

exception IllegalAlias of region

let eff_assign e r ty =
  let e = eff_write e r in
  let sub = ity_match ity_subst_empty r.reg_ity ty in
  (* assignment cannot instantiate type variables *)
  if not (Mtv.is_empty sub.ity_subst_tv) then
    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
450
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
451
452
  (* 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
453
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
454
455
  (* ...except those which occur on the lhs : they are preserved under r *)
  let add_left k v m = if reg_equal k v then m else Mreg.add v (Some r) m in
Andrei Paskevich's avatar
Andrei Paskevich committed
456
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
457
458
459
  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }

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

Andrei Paskevich's avatar
Andrei Paskevich committed
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
let eff_full_inst s e =
  let s = s.ity_subst_reg in
  (* modified or reset regions in e *)
  let wr = Mreg.map (Util.const ()) e.eff_resets in
  let wr = Sreg.union e.eff_writes wr in
  (* read-only regions in e *)
  let ro = Sreg.diff e.eff_reads wr in
  (* all modified or reset regions are instantiated into distinct regions *)
  let add_affected r acc =
    let r = Mreg.find r s in Sreg.add_new (IllegalAlias r) r acc in
  let wr = Sreg.fold add_affected wr Sreg.empty in
  (* all read-only regions are instantiated outside wr *)
  let add_readonly r =
    let r = Mreg.find r s in if Sreg.mem r wr then raise (IllegalAlias r) in
  Sreg.iter add_readonly ro;
  (* calculate instantiated effect *)
  let add_inst r acc = Sreg.add (Mreg.find r s) acc in
  let reads  = Sreg.fold add_inst e.eff_reads  Sreg.empty in
  let writes = Sreg.fold add_inst e.eff_writes Sreg.empty in
  let add_inst r v acc =
    Mreg.add (Mreg.find r s) (option_map (fun v -> Mreg.find v s) v) acc in
  let resets = Mreg.fold add_inst e.eff_resets Mreg.empty in
  { e with eff_reads = reads ; eff_writes = writes ; eff_resets = resets }
484

485
486
(* program variables *)
type pvsymbol = {
487
488
489
490
  pv_vs      : vsymbol;
  pv_ity     : ity;
  pv_ghost   : bool;
  pv_mutable : region option;
Andrei Paskevich's avatar
Andrei Paskevich committed
491
492
  pv_tvs     : Stv.t;
  pv_regs    : Sreg.t;
493
}
494

495
496
497
498
499
500
501
502
503
504
module Pv = StructMake (struct
  type t = pvsymbol
  let tag pv = Hashweak.tag_hash pv.pv_vs.vs_name.id_tag
end)

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

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

505
506
507
508
509
510
exception InvalidPVsymbol of ident

let create_pvsymbol id ?mut ?(ghost=false) ity =
  let ty = ty_of_ity ity in
  let vs = create_vsymbol id ty in
  begin match mut with
Andrei Paskevich's avatar
Andrei Paskevich committed
511
512
513
514
    | Some r when
      (* A ghost variable may contain a non-ghost region.
         No writes are allowed in such a ghost variable. *)
      not (ity_equal r.reg_ity ity) || (r.reg_ghost && not ghost) ->
515
        raise (InvalidPVsymbol vs.vs_name)
516
517
    | _ ->
        ()
518
  end;
Andrei Paskevich's avatar
Andrei Paskevich committed
519
520
521
522
523
524
525
526
527
528
  let tvs = ity_freevars Stv.empty ity in
  let regs = ity_topregions Sreg.empty ity in
  let regs = option_fold (fun s r -> Sreg.add r s) regs mut in
  { pv_vs      = vs;
    pv_ity     = ity;
    pv_ghost   = ghost;
    pv_mutable = mut;
    pv_tvs     = tvs;
    pv_regs    = regs;
  }
529

Andrei Paskevich's avatar
Andrei Paskevich committed
530
531
532
533
534
let pv_clone pv =
  let id = id_clone pv.pv_vs.vs_name in
  let vs = create_vsymbol id pv.pv_vs.vs_ty in
  { pv with pv_vs = vs }

535
536
537
538
539
let pv_full_inst s pv =
  let ghost = pv.pv_ghost in
  let mut = option_map (reg_full_inst s) pv.pv_mutable in
  let ity = ity_full_inst s pv.pv_ity in
  create_pvsymbol (id_clone pv.pv_vs.vs_name) ~ghost ?mut ity
540

541
(* value types *)
542

543
544
type vty =
  | VTvalue of pvsymbol
545
  | VTarrow of vty_arrow
546
547

(* computation types *)
548
and vty_arrow = {
Andrei Paskevich's avatar
Andrei Paskevich committed
549
550
551
552
553
  a_arg   : pvsymbol;
  a_vty   : vty;
  a_eff   : effect;
  a_pre   : term; (* epsilon under a dummy variable, to accumulate substs *)
  a_post  : term; (* epsilon under the value variable or under a dummy vs *)
Andrei Paskevich's avatar
Andrei Paskevich committed
554
555
556
  a_xpost : term Mexn.t; (* epsilon under the exception value variable *)
  a_tvs   : Stv.t; (* we do not count type variables in eff/pre/post/xpost *)
  a_regs  : Sreg.t; (* we do not count regions in eff/pre/post/xpost *)
Andrei Paskevich's avatar
Andrei Paskevich committed
557
558
559
560
561
562
563
}

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

type vty_comp = {
564
565
  c_vty   : vty;
  c_eff   : effect;
Andrei Paskevich's avatar
Andrei Paskevich committed
566
  c_pre   : pre;
567
  c_post  : post;
568
  c_xpost : xpost;
569
}
570

Andrei Paskevich's avatar
Andrei Paskevich committed
571
572
573
574
575
576
577
578
let vty_freevars s = function
  | VTvalue pv -> Stv.union s pv.pv_tvs
  | VTarrow a  -> Stv.union s a.a_tvs

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

579
(* smart constructors *)
580

581
let vty_value pvs = VTvalue pvs
582

Andrei Paskevich's avatar
Andrei Paskevich committed
583
584
585
586
587
588
589
590
591
592
593
exception InvalidExceptionPost of xsymbol

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
595
596
597
let open_spec = function
  | { t_node = Teps bf } -> t_open_bound bf
  | _ -> assert false
598
599
600

let vty_arrow
  x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
Andrei Paskevich's avatar
Andrei Paskevich committed
601
  (* check for clashes *)
Andrei Paskevich's avatar
Andrei Paskevich committed
602
(* let check_vs y = if vs_equal x.pv_vs y then raise (DuplicateVar y) in *)
Andrei Paskevich's avatar
Andrei Paskevich committed
603
  let check_pv y = if pv_equal x y then raise (DuplicateVar x.pv_vs) in
604
  let rec check = function
Andrei Paskevich's avatar
Andrei Paskevich committed
605
    | VTarrow a ->
Andrei Paskevich's avatar
Andrei Paskevich committed
606
     (* Mexn.iter (fun _ (y,_) -> check_vs y) a.a_xpost; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
607
608
609
610
        check_pv a.a_arg;
        check a.a_vty
    | VTvalue y ->
        check_pv y
611
  in
612
  check vty;
Andrei Paskevich's avatar
Andrei Paskevich committed
613
614
615
616
617
618
619
620
621
622
623
624
  (* check that every raised exception is mentioned in xpost *)
  if not (Mexn.set_submap effect.eff_raises xpost) then
    (let d = Mexn.set_diff xpost effect.eff_raises in
    raise (InvalidExceptionPost (fst (Mexn.choose d))));
  (* check that every exception mentioned in xpost is raised *)
  if not (Mexn.set_submap xpost effect.eff_raises) then
    (let d = Mexn.set_diff effect.eff_raises xpost in
    raise (InvalidExceptionPost (fst (Mexn.choose d))));
  (* check that vsymbols in xpost have valid types *)
  let conv_xpost xs (vs,f) =
    if not (ty_equal (ty_of_ity xs.xs_ity) vs.vs_ty)
    then raise (InvalidExceptionPost xs);
Andrei Paskevich's avatar
Andrei Paskevich committed
625
626
    (* check_vs vs; *)
    t_eps_close vs f
Andrei Paskevich's avatar
Andrei Paskevich committed
627
628
629
630
631
  in
  let post = match vty with
    | VTvalue pv -> t_eps_close pv.pv_vs post
    | VTarrow _  -> close_spec post
  in
632
  VTarrow {
Andrei Paskevich's avatar
Andrei Paskevich committed
633
634
635
636
637
638
    a_arg   = x;
    a_vty   = vty;
    a_eff   = effect;
    a_pre   = close_spec pre;
    a_post  = post;
    a_xpost = Mexn.mapi conv_xpost xpost;
Andrei Paskevich's avatar
Andrei Paskevich committed
639
640
    a_tvs   = vty_freevars x.pv_tvs vty;
    a_regs  = vty_topregions x.pv_regs vty;
641
642
  }

Andrei Paskevich's avatar
Andrei Paskevich committed
643
(*
644
645
646
647
648
exception NotAFunction

let get_arrow = function
  | VTvalue _ -> raise NotAFunction
  | VTarrow a -> a
Andrei Paskevich's avatar
Andrei Paskevich committed
649
650
651
652
653
654
655
*)

let vty_app_arrow arr x =
  ity_equal_check arr.a_arg.pv_ity x.pv_ity;
  let subst f = t_subst_single arr.a_arg.pv_vs (t_var x.pv_vs) f in
  let _,pre = open_spec (subst arr.a_pre) in
  let res,post = open_spec (subst arr.a_post) in
Andrei Paskevich's avatar
Andrei Paskevich committed
656
  let xsubst e = open_spec (subst e) in
Andrei Paskevich's avatar
Andrei Paskevich committed
657
658
659
660
661
662
  let rec arr_subst arr = { arr with
    a_vty   = (match arr.a_vty with
      | VTarrow a -> VTarrow (arr_subst a)
      | VTvalue _ -> arr.a_vty);
    a_pre   = subst arr.a_pre;
    a_post  = subst arr.a_post;
Andrei Paskevich's avatar
Andrei Paskevich committed
663
    a_xpost = Mexn.map subst arr.a_xpost;
Andrei Paskevich's avatar
Andrei Paskevich committed
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
  }
  in
  let vty = match arr.a_vty with
    (* here we make a new pvsymbol in a bad fashion. It should however
       be safe, since res comes from t_open_bound and is guaranteed to
       be fresh, so there can be no illegal sharing of idents *)
    | VTvalue pv -> VTvalue { pv with pv_vs = res }
    | VTarrow a  -> VTarrow (arr_subst a)
  in {
    c_vty   = vty;
    c_eff   = arr.a_eff;
    c_pre   = pre;
    c_post  = post;
    c_xpost = Mexn.map xsubst arr.a_xpost;
  }
679

Andrei Paskevich's avatar
Andrei Paskevich committed
680
681
682
683
684
let open_vty_arrow arr =
  let pv = pv_clone arr.a_arg in
  let c = vty_app_arrow arr pv in
  pv, c.c_vty

Andrei Paskevich's avatar
Andrei Paskevich committed
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
let vty_full_inst s vty =
  let subT = Mtv.map ty_of_ity s.ity_subst_tv in
  let rec inst subV = function
    | VTvalue pv ->
        (* this is not the same vsymbol anymore that is bound in
           the preceding post. However, this should not matter. *)
        VTvalue (pv_full_inst s pv)
    | VTarrow a ->
        let x = pv_full_inst s a.a_arg in
        let subV = Mvs.add a.a_arg.pv_vs (t_var x.pv_vs) subV in
        let subst = t_ty_subst subT subV in
        let vty = inst subV a.a_vty in
        VTarrow {
          a_arg   = x;
          a_vty   = vty;
          a_eff   = eff_full_inst s a.a_eff;
          a_pre   = subst a.a_pre;
          a_post  = subst a.a_post;
          a_xpost = Mexn.map subst a.a_xpost;
          a_tvs   = vty_freevars x.pv_tvs vty;
          a_regs  = vty_topregions x.pv_regs vty;
        }
  in
  inst Mvs.empty vty