mlw_ty.ml 22.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    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
24
open Term
25

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

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

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

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

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

53
(** regions *)
54 55 56

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
68 69 70 71 72 73 74 75 76
(* 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). *)

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

80
(* value type symbols *)
81

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

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

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

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

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

101 102
  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
    | Ityvar n1, Ityvar n2 ->
103
        tv_equal n1 n2
104 105 106 107
    | 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
108
          && List.for_all2 reg_equal r1 r2
109 110
    | _ ->
        false
111

112 113 114 115
  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) ->
116
        Hashcons.combine_list reg_hash
117
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl
118

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

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

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

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

137 138 139
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)))
140 141 142

(* generic traversal functions *)

143 144 145 146
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
147

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

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

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

159 160 161 162 163 164 165 166 167
(* 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

168 169 170 171
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 =
172
  try ity_s_fold (any_fn pr) (any_fn pts) false ity with FoldSkip -> true
173

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

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

let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
  | Ityvar v ->
186
      fnv acc v
187 188 189 190
  | 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
191

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

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

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

201 202
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)
203

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

(* smart constructors *)

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

212 213
exception DuplicateRegion of region
exception UnboundRegion of region
214

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
224 225 226 227 228 229 230
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

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

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

241 242 243 244 245 246 247 248 249 250 251 252
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

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

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

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

and reg_match s r1 r2 =
  let is_new = ref false in
Andrei Paskevich's avatar
Andrei Paskevich committed
281
  let set = function (* must preserve ghost-ness of regions *)
Andrei Paskevich's avatar
Andrei Paskevich committed
282
    | None when r1.reg_ghost = r2.reg_ghost -> is_new := true; Some r2
283 284 285
    | Some r3 as r when reg_equal r3 r2 -> r
    | _ -> raise Exit
  in
286
  let reg_map = Mreg.change set r1 s.ity_subst_reg in
287 288
  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
289

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

294 295 296 297
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)
298

299 300 301
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)
302

303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
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
319 320
      let id = id_clone r.reg_name in
      let ghost = r.reg_ghost in
321 322 323 324 325 326 327 328 329 330 331
      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
332
  (* every top region in def is guaranteed to be in mr *)
333
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
334
  | Some ity -> ity_subst_unsafe mv mr ity
335 336
  | None -> ity_app s tl rl

337
let ity_app s tl rl =
338
  (* type variable map *)
339
  let add m v t = Mtv.add v t m in
340 341 342 343
  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
344 345
  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
346 347
    with Invalid_argument _ ->
      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
348
  (* every type var and top region in def are in its_args and its_regs *)
349
  match s.its_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
350
  | Some ity -> ity_full_inst sub ity
351
  | None -> ity_app s tl rl
352

353
let ity_pur s tl = match s.ts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
354 355 356
  | 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
357
      ity_subst_unsafe m Mreg.empty (ity_of_ty ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
358
  | None ->
359
      ity_pur s tl
Andrei Paskevich's avatar
Andrei Paskevich committed
360

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

(** computation types (with effects) *)

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

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

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

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

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

(* effects *)
type effect = {
410 411 412 413 414
  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;
415
}
416

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

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

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

434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
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
449
  ignore (Mreg.fold add_right sub.ity_subst_reg Sreg.empty);
450 451
  (* 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
452
  let reset = Mreg.fold add_right sub.ity_subst_reg Mreg.empty in
453 454
  (* ...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
455
  let reset = Mreg.fold add_left sub.ity_subst_reg reset in
456 457 458
  { 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 }
459

Andrei Paskevich's avatar
Andrei Paskevich committed
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482
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 }
483

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

494 495 496 497 498 499 500 501 502 503
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 = (==)

504 505 506 507 508 509
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
510 511 512 513
    | 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) ->
514
        raise (InvalidPVsymbol vs.vs_name)
515 516
    | _ ->
        ()
517
  end;
Andrei Paskevich's avatar
Andrei Paskevich committed
518 519 520 521 522 523 524 525 526 527
  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;
  }
528

Andrei Paskevich's avatar
Andrei Paskevich committed
529 530 531 532 533
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 }

534 535 536 537 538
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
539

540
(* value types *)
541

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

(* computation types *)
547
and vty_arrow = {
Andrei Paskevich's avatar
Andrei Paskevich committed
548 549 550 551 552
  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
553 554 555
  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
556 557 558 559 560 561 562
}

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
570 571 572 573 574 575 576 577
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

578
(* smart constructors *)
579

580
let vty_value pvs = VTvalue pvs
581

Andrei Paskevich's avatar
Andrei Paskevich committed
582 583 584 585 586 587 588 589 590 591 592
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
593

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

let vty_arrow
  x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
Andrei Paskevich's avatar
Andrei Paskevich committed
600
  (* check for clashes *)
Andrei Paskevich's avatar
Andrei Paskevich committed
601
(* let check_vs y = if vs_equal x.pv_vs y then raise (DuplicateVar y) in *)
Andrei Paskevich's avatar
Andrei Paskevich committed
602
  let check_pv y = if pv_equal x y then raise (DuplicateVar x.pv_vs) in
603
  let rec check = function
Andrei Paskevich's avatar
Andrei Paskevich committed
604
    | VTarrow a ->
Andrei Paskevich's avatar
Andrei Paskevich committed
605
     (* Mexn.iter (fun _ (y,_) -> check_vs y) a.a_xpost; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
606 607 608 609
        check_pv a.a_arg;
        check a.a_vty
    | VTvalue y ->
        check_pv y
610
  in
611
  check vty;
Andrei Paskevich's avatar
Andrei Paskevich committed
612 613 614 615 616 617 618 619 620 621 622 623
  (* 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
624 625
    (* check_vs vs; *)
    t_eps_close vs f
Andrei Paskevich's avatar
Andrei Paskevich committed
626 627 628 629 630
  in
  let post = match vty with
    | VTvalue pv -> t_eps_close pv.pv_vs post
    | VTarrow _  -> close_spec post
  in
631
  VTarrow {
Andrei Paskevich's avatar
Andrei Paskevich committed
632 633 634 635 636 637
    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
638 639
    a_tvs   = vty_freevars x.pv_tvs vty;
    a_regs  = vty_topregions x.pv_regs vty;
640 641
  }

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

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

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
655
  let xsubst e = open_spec (subst e) in
Andrei Paskevich's avatar
Andrei Paskevich committed
656 657 658 659 660 661
  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
662
    a_xpost = Mexn.map subst arr.a_xpost;
Andrei Paskevich's avatar
Andrei Paskevich committed
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677
  }
  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;
  }
678

Andrei Paskevich's avatar
Andrei Paskevich committed
679 680 681 682 683
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
684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708
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