ity.ml 34.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
open Ident
open Ty
15
open Term
16 17 18 19

(** {2 Individual types (first-order types w/o effects)} *)

type itysymbol = {
20 21 22 23 24 25 26 27 28
  its_ts      : tysymbol;       (** pure "snapshot" type symbol *)
  its_private : bool;           (** is a private/abstract type *)
  its_mutable : bool;           (** is a record with mutable fields *)
  its_mfields : pvsymbol Mvs.t; (** mutable fields *)
  its_regions : region list;    (** mutable shareable components *)
  its_reg_vis : bool list;      (** non-ghost shareable components *)
  its_arg_vis : bool list;      (** non-ghost type parameters *)
  its_arg_upd : bool list;      (** updatable type parameters *)
  its_def     : ity option;     (** is a type alias *)
29 30 31 32
}

and ity = {
  ity_node : ity_node;
33
  ity_pure : bool;
34 35 36 37 38
  ity_tag  : Weakhtbl.tag;
}

and ity_node =
  | Itymut of itysymbol * ity list * region list * tvsymbol
39 40 41 42 43 44 45
    (** record with mutable fields and shareable components *)
  | Ityapp of itysymbol * ity list * region list
    (** algebraic type with shareable components *)
  | Itypur of itysymbol * ity list
    (** immutable type or a snapshot of a mutable type *)
  | Ityvar of tvsymbol
    (** type variable *)
46

47 48 49 50 51
and pvsymbol = {
  pv_vs    : vsymbol;
  pv_ity   : ity;
  pv_ghost : bool;
}
52

53
and region = ity (** regions are itys of the [Itymut] kind *)
54 55 56 57 58 59

module Itsym = MakeMSHW (struct
  type t = itysymbol
  let tag its = its.its_ts.ts_name.id_tag
end)

60 61 62 63 64 65 66 67 68 69
module Ity = MakeMSHW (struct
  type t = ity
  let tag ity = ity.ity_tag
end)

module PVsym = MakeMSHW (struct
  type t = pvsymbol
  let tag pv = pv.pv_vs.vs_name.id_tag
end)

70 71 72 73 74
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W

75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W

module Sreg = Sity
module Mreg = Mity
module Hreg = Hity
module Wreg = Wity

module Spv = PVsym.S
module Mpv = PVsym.M
module Hpv = PVsym.H
module Wpv = PVsym.W

(* value type symbols *)

92 93
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
94
let pv_equal  : pvsymbol  -> pvsymbol  -> bool = (==)
95 96 97

let its_hash its = id_hash its.its_ts.ts_name
let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
98 99 100
let pv_hash  pv  = id_hash pv.pv_vs.vs_name

exception NonUpdatable of itysymbol * ity
101 102 103 104 105 106

module Hsity = Hashcons.Make (struct
  type t = ity

  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
    | Itypur (s1,l1), Itypur (s2,l2) ->
107
        its_equal s1 s2 &&
108 109 110 111 112
        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 &&
        List.for_all2 ity_equal r1 r2
113 114
    | (Ityvar v1 | Itymut (_,_,_,v1)),
      (Ityvar v2 | Itymut (_,_,_,v2)) ->
115 116 117 118 119
        tv_equal v1 v2
    | _ -> false

  let hash ity = match ity.ity_node with
    | Itypur (s,tl) ->
120
        Hashcons.combine_list ity_hash (its_hash s) tl
121 122 123 124 125 126
    | Ityapp (s,tl,rl) ->
        Hashcons.combine_list ity_hash
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl
    | Ityvar v | Itymut (_,_,_,v) ->
        tv_hash v

127 128 129
  let check_upd s acc upd ity =
    if not (upd || ity.ity_pure) then raise (NonUpdatable (s,ity));
    acc && ity.ity_pure
130

131 132 133 134 135 136
  let pure ity = match ity.ity_node with
    | Ityvar _ -> true
    | Itypur (s,tl) -> List.fold_left2 (check_upd s) true s.its_arg_upd tl
    | Ityapp (_,_,[]) -> assert false
    | Ityapp (s,tl,_) -> List.fold_left2 (check_upd s) false s.its_arg_upd tl
    | Itymut (s,tl,_,_) -> List.fold_left2 (check_upd s) false s.its_arg_upd tl
137

138 139 140 141
  let tag n ity = { ity with
    ity_pure = pure ity;
    ity_tag  = Weakhtbl.create_tag n }
end)
142 143 144

let mk_ity n = {
  ity_node = n;
145
  ity_pure = true;
146 147 148
  ity_tag  = Weakhtbl.dummy_tag;
}

149
let ity_var_unsafe n = Hsity.hashcons (mk_ity (Ityvar n))
150 151 152 153
let ity_pur_unsafe s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
let ity_mut_unsafe s tl rl v = Hsity.hashcons (mk_ity (Itymut (s,tl,rl,v)))

154 155 156 157 158 159 160 161 162 163 164 165 166
let tv_of_region reg = match reg.ity_node with
  | Itymut (_,_,_,tv) -> tv
  | _ -> invalid_arg "Ity.tv_of_region"

let open_region reg = match reg.ity_node with
  | Itymut (s,tl,rl,tv) -> s,tl,rl,tv
  | _ -> invalid_arg "Ity.open_region"

let ity_mut_fresh_unsafe s tl rl =
  ity_mut_unsafe s tl rl (create_tvsymbol (id_fresh "rho"))

let ity_mut_known_unsafe s tl rl v =
  let ity = ity_mut_unsafe s tl rl v in
167 168 169 170 171 172
  match ity.ity_node with
  | Itymut (s',tl',rl',_)
    when its_equal s s' &&
         Lists.equal ity_equal tl tl' &&
         Lists.equal ity_equal rl rl' -> ity
  | _ -> invalid_arg "Ity.ity_mut"
173

174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
(* generic traversal functions *)

let ity_fold fn acc ity = match ity.ity_node with
  | Ityvar _ -> acc
  | Itypur (_,tl)
  | Ityapp (_,tl,_)
  | Itymut (_,tl,_,_) -> List.fold_left fn acc tl

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

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

(* symbol-wise map/fold *)

190 191
let rec ity_s_fold fits acc ity =
  let fold acc ity = ity_s_fold fits acc ity in
192 193
  let fold acc ityl = List.fold_left fold acc ityl in
  match ity.ity_node with
194 195
  | Itymut (s,tl,rl,_) | Ityapp (s,tl,rl) -> fold (fold (fits acc s) tl) rl
  | Itypur (s,tl) -> fold (fits acc s) tl
196 197
  | Ityvar _ -> acc

198 199
let ity_s_all pits ity =
  try ity_s_fold (Util.all_fn pits) true ity with Util.FoldSkip -> false
200

201 202
let ity_s_any pits ity =
  try ity_s_fold (Util.any_fn pits) false ity with Util.FoldSkip -> true
203 204 205 206 207 208 209

(* traversal functions on type variables and regions *)

let rec ity_v_fold fn acc ity = match ity.ity_node with
  | Ityvar v -> fn acc v
  | _ -> ity_fold (ity_v_fold fn) acc ity

210 211
let ity_freevars s ity = ity_v_fold (fun s v -> Stv.add v s) s ity

212 213 214 215 216 217 218 219 220 221 222 223 224 225
let ity_v_all pr ity =
  try ity_v_fold (Util.all_fn pr) true ity with Util.FoldSkip -> false

let ity_v_any pr ity =
  try ity_v_fold (Util.any_fn pr) false ity with Util.FoldSkip -> true

let ity_v_occurs tv ity = ity_v_any (tv_equal tv) ity

let ity_closed ity = ity_v_all (fun _ -> false) ity

let rec ity_r_fold fn acc ity =
  let ffn acc ity = ity_r_fold fn acc ity in
  match ity.ity_node with
  | Ityvar _ -> acc
226 227 228
  | Itypur (_,tl) -> List.fold_left ffn acc tl
  | Ityapp (_,tl,rl) -> List.fold_left ffn (List.fold_left fn acc rl) tl
  | Itymut _ -> fn acc ity
229 230 231 232 233 234 235

let ity_r_all pr ity =
  try ity_r_fold (Util.all_fn pr) true ity with Util.FoldSkip -> false

let ity_r_any pr ity =
  try ity_r_fold (Util.any_fn pr) false ity with Util.FoldSkip -> true

236 237
let ity_r_occurs reg ity =
  let rec check r = ity_equal r reg ||
238
    let _,tl,rl,_ = open_region r in
239
    List.exists (ity_r_any check) tl ||
240 241 242 243 244 245 246 247 248
    List.exists check rl in
  ity_r_any check ity

let ity_r_stale reg sreg ity =
  let rec check r = ity_equal r reg ||
    if Sreg.mem r sreg then false else
    let _,tl,rl,_ = open_region r in
    List.exists (ity_r_any check) tl ||
    List.exists check rl in
249
  ity_r_any check ity
250

251
let ity_immutable ity = not ity.ity_pure
252 253 254

(* detect non-ghost type variables and regions *)

255 256
let rec fold_visible on_var on_reg acc ity =
  let fnt acc ity = fold_visible on_var on_reg acc ity in
257 258
  let fnr acc vis ity = if vis then fnt acc ity else acc in
  match ity.ity_node with
259
  | Ityvar tv ->
260
      on_var acc tv
261 262 263 264 265 266
  | Itypur (s,tl) ->
      List.fold_left2 fnr acc s.its_arg_vis tl
  | Ityapp (s,tl,rl) ->
      let acc = List.fold_left2 fnr acc s.its_reg_vis rl in
      List.fold_left2 fnr acc s.its_arg_vis tl
  | Itymut (s,tl,rl,_) ->
267
      let acc = on_reg acc ity in
268 269
      let acc = List.fold_left2 fnr acc s.its_reg_vis rl in
      List.fold_left2 fnr acc s.its_arg_vis tl
270

271
let ity_r_visible regs ity =
272
  fold_visible (fun s _ -> s) (fun s r -> Sreg.add r s) regs ity
273

274
let ity_v_visible vars ity =
275
  fold_visible (fun s v -> Stv.add v s) (fun s _ -> s) vars ity
276 277 278 279 280 281 282 283 284

(* smart constructors *)

exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int

exception DuplicateRegion of region
exception UnboundRegion of region

285
exception TypeMismatch of ity * ity * ity Mtv.t
286 287

let ity_equal_check ty1 ty2 =
288
  if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1,ty2,Mtv.empty))
289 290 291 292 293 294 295 296 297

let ity_full_inst s ity =
  if Mtv.is_empty s then ity else
  let rec inst ity = match ity.ity_node with
    | Ityapp (f,tl,rl) -> ity_app_unsafe f (List.map inst tl) (List.map inst rl)
    | Itypur (f,tl) -> ity_pur_unsafe f (List.map inst tl)
    | Ityvar v | Itymut (_,_,_,v) -> Mtv.find v s in
  inst ity

298 299 300 301 302 303 304 305 306 307
let rec ity_match sbs ity1 ity2 = match ity1.ity_node, ity2.ity_node with
  | (Itymut (_,_,_,v1)| Ityvar v1), _ when Mtv.mem v1 sbs ->
      if ity_equal (Mtv.find v1 sbs) ity2 then sbs else raise Exit
  | Itymut (s1,l1,r1,v1), Itymut (s2,l2,r2,_) when its_equal s1 s2 ->
      let sbs = List.fold_left2 ity_match sbs l1 l2 in
      let sbs = List.fold_left2 ity_match sbs r1 r2 in
      Mtv.add v1 ity2 sbs
  | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) when its_equal s1 s2 ->
      let sbs = List.fold_left2 ity_match sbs l1 l2 in
      List.fold_left2 ity_match sbs r1 r2
308
  | Itypur (s1, l1), Itypur (s2, l2) when its_equal s1 s2 ->
309 310 311 312
      List.fold_left2 ity_match sbs l1 l2
  | Ityvar v1, _ ->
      Mtv.add v1 ity2 sbs
  | _ -> raise Exit
313

314 315 316
let ity_match sbs ity1 ity2 =
  try ity_match sbs ity1 ity2
  with Exit -> raise (TypeMismatch (ity1,ity2,sbs))
317

318
let ity_freeze sbs ity = ity_match sbs ity ity
319 320 321

let rec ty_of_ity ity = match ity.ity_node with
  | Ityvar v -> ty_var v
322
  | Itypur (s,tl) | Ityapp (s,tl,_) | Itymut (s,tl,_,_) ->
323
      ty_app s.its_ts (List.map ty_of_ity tl)
324

325 326 327 328
let rec ity_purify ity = match ity.ity_node with
  | Ityvar _ -> ity
  | Itypur (s,tl) | Ityapp (s,tl,_) | Itymut (s,tl,_,_) ->
      ity_pur_unsafe s (List.map ity_purify tl)
329

330 331 332 333 334 335
let ity_var v =
  let ity = ity_var_unsafe v in
  match ity.ity_node with
  | Ityvar _ -> ity
  | _ -> invalid_arg "Ity.ity_var"

336
let ity_pur s tl =
337 338 339 340 341 342
  if List.length s.its_ts.ts_args <> List.length tl then
    raise (BadItyArity (s, List.length tl));
  match s.its_def with
  | Some ity ->
      let sbs = List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty in
      ity_full_inst sbs (ity_purify ity)
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
  | None ->
      ity_pur_unsafe s tl

let ity_mut s tl rl v =
  (* compute the substitution even for non-aliases to verify regions *)
  let sbs = try List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty
    with Invalid_argument _ -> raise (BadItyArity (s, List.length tl)) in
  let sbs = try List.fold_left2 ity_match sbs s.its_regions rl
    with Invalid_argument _ -> raise (BadRegArity (s, List.length rl)) in
  match s.its_def with
  | Some { ity_node = Itymut (s,tl,rl,_) } ->
      let tl = List.map (ity_full_inst sbs) tl in
      let rl = List.map (ity_full_inst sbs) rl in
      ity_mut_known_unsafe s tl rl v
  | None when s.its_mutable ->
      ity_mut_known_unsafe s tl rl v
  | _ -> invalid_arg "Ity.ity_mut"

let ity_app sbs s tl rl = match s.its_def with
  | Some { ity_node = Itymut (s,tl,rl,_) } ->
      let tl = List.map (ity_full_inst sbs) tl in
      let rl = List.map (ity_full_inst sbs) rl in
      ity_mut_fresh_unsafe s tl rl
  | None when s.its_mutable ->
      ity_mut_fresh_unsafe s tl rl
  | Some ity ->
      ity_full_inst sbs ity
370 371
  | None when rl = [] ->
      ity_pur_unsafe s tl
372 373 374 375
  | None ->
      ity_app_unsafe s tl rl

let rec ity_inst_fresh sbs ity = match ity.ity_node with
376
  | Ityvar v ->
377
      sbs, Mtv.find v sbs
378
  | Itypur (s,tl) ->
379 380
      let sbs,tl = Lists.map_fold_left ity_inst_fresh sbs tl in
      sbs, ity_pur_unsafe s tl
381
  | Ityapp (s,tl,rl) ->
382 383 384 385 386 387 388 389 390 391
      let sbs,tl = Lists.map_fold_left ity_inst_fresh sbs tl in
      let sbs,rl = Lists.map_fold_left ity_inst_fresh sbs rl in
      sbs, ity_app_unsafe s tl rl
  | Itymut (_,_,_,v) when Mtv.mem v sbs ->
      sbs, Mtv.find v sbs
  | Itymut (s,tl,rl,v) ->
      let sbs,tl = Lists.map_fold_left ity_inst_fresh sbs tl in
      let sbs,rl = Lists.map_fold_left ity_inst_fresh sbs rl in
      let ity = ity_mut_unsafe s tl rl (create_tvsymbol (id_clone v.tv_name)) in
      Mtv.add v ity sbs, ity
392 393

let ity_app_fresh s tl =
394 395 396 397
  let sbs = try List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty
    with Invalid_argument _ -> raise (BadItyArity (s, List.length tl)) in
  let sbs,rl = Lists.map_fold_left ity_inst_fresh sbs s.its_regions in
  ity_app sbs s tl rl
398 399

let ity_app s tl rl =
400 401 402 403 404 405
  (* compute the substitution even for non-aliases to verify regions *)
  let sbs = try List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty
    with Invalid_argument _ -> raise (BadItyArity (s, List.length tl)) in
  let sbs = try List.fold_left2 ity_match sbs s.its_regions rl
    with Invalid_argument _ -> raise (BadRegArity (s, List.length rl)) in
  ity_app sbs s tl rl
406 407 408 409 410

(* itysymbol creation *)

let create_itysymbol_unsafe, restore_its =
  let ts_to_its = Wts.create 17 in
411
  (fun ~ts ~pri ~mut ~fld ~regs ~rvis ~avis ~aupd ~def ->
412
    let its = {
413
      its_ts      = ts;
414
      its_private = pri;
415
      its_mutable = mut;
416
      its_mfields = fld;
417
      its_regions = regs;
418 419 420
      its_reg_vis = rvis;
      its_arg_vis = avis;
      its_arg_upd = aupd;
421
      its_def     = def;
422 423 424 425 426
    } in
    Wts.set ts_to_its ts its;
    its),
  Wts.find ts_to_its

427 428
let create_itysymbol name args pri mut regs fld def =
  (* prepare arguments *)
429 430 431
  let args, avis, aupd = List.fold_right
    (fun (tv,v,u) (args,avis,aupd) ->
      tv::args, v::avis, u::aupd) args ([],[],[]) in
432 433 434 435 436
  let regs, rvis = List.split regs in
  let fld = Spv.fold (fun pv acc ->
    Mvs.add pv.pv_vs pv acc) fld Mvs.empty in
  (* create_tysymbol checks that args contains no duplicates
     and covers every type variable in def *)
437
  let puredef = Opt.map ty_of_ity def in
438
  let ts = create_tysymbol name args puredef in
439
  (* all regions *)
440 441 442 443
  let add_r s r = match r.ity_node with
    | Itymut _ -> Sreg.add_new (DuplicateRegion r) r s
    | _ -> invalid_arg "Ity.create_itysymbol" in
  let sregs = List.fold_left add_r Sreg.empty regs in
444 445
  (* all type variables *)
  let sargs = List.fold_right Stv.add args Stv.empty in
446
  (* each type variable in [regs] and [fld] must be in [args] *)
447
  let check_v () v =
448 449 450 451 452
    if not (Stv.mem v sargs) then raise (Ty.UnboundTypeVar v) in
  let check_var ity = ity_v_fold check_v () ity in
  List.iter check_var regs;
  Mvs.iter (fun _ pv -> check_var pv.pv_ity) fld;
  (* each surface region in [fld] must be in [regs] *)
453
  let check_r () r =
454
    if not (Sreg.mem r sregs) then raise (UnboundRegion r) in
455
  let check_reg ity = ity_r_fold check_r () ity in
456 457 458 459
  Mvs.iter (fun _ pv -> check_reg pv.pv_ity) fld;
  (* each lower surface region in [def] must be in [regs] *)
  let check_reg () ity = match ity.ity_node with
    | Itymut (_,tl,rl,_) ->
460
        List.iter check_reg rl;
461 462 463
        List.iter check_reg tl
    | _ -> check_reg ity in
  Opt.fold check_reg () def;
464 465
  (* the alias is mutable if and only if the symbol is *)
  let check = function
466
    | Some {ity_node = Itymut _} -> mut
467 468 469
    | Some _ -> not mut
    | None -> true in
  if not (check def) then invalid_arg "Ity.create_itysymbol";
470 471 472 473 474 475
  (* if we have mutable fields then we are mutable *)
  if not (mut || Mvs.is_empty fld) then
    invalid_arg "Ity.create_itysymbol";
  (* if we are an alias then we are not private and have no fields *)
  if def <> None && (pri || not (Mvs.is_empty fld)) then
    invalid_arg "Ity.create_itysymbol";
476 477 478
  (* if we are private, we have no subregions and all args are non-updateble *)
  if pri && (regs <> [] || List.exists (fun u -> u) aupd) then
    invalid_arg "Ity.create_itysymbol";
479 480 481
  (* each invisible type variable and region must be invisible in [def] *)
  let v_visible = Opt.fold ity_v_visible Stv.empty def in
  let r_visible = Opt.fold ity_r_visible Sreg.empty def in
482 483 484 485
  let check_v vis v = if not vis && Stv.mem v v_visible then
      invalid_arg "Ity.create_itysymbol" in
  let check_r vis r = if not vis && Sreg.mem r r_visible then
      invalid_arg "Ity.create_itysymbol" in
486 487
  List.iter2 check_v avis args;
  List.iter2 check_r rvis regs;
488 489 490 491 492 493 494 495 496 497 498 499
  (* each updatable type variable is updatable in [regs], [fld], and [def] *)
  let rec nonupd acc upd ity = match ity.ity_node with
    | _ when not upd -> ity_freevars acc ity
    | Itypur (s,tl) | Ityapp (s,tl,_) | Itymut (s,tl,_,_) ->
        List.fold_left2 nonupd acc s.its_arg_upd tl
    | Ityvar _ -> acc in
  let nonupd acc ity = nonupd acc true ity in
  let nu = List.fold_left nonupd Stv.empty regs in
  let nu = Mvs.fold (fun _ pv s -> nonupd s pv.pv_ity) fld nu in
  let nu = Opt.fold nonupd nu def in
  List.iter2 (fun upd v -> if upd && Stv.mem v nu then
    invalid_arg "Ity.create_itysymbol") aupd args;
Andrei Paskevich's avatar
Andrei Paskevich committed
500 501 502
  (* NOTE: record/constructor fields must be pairwise separated,
     but this should be checked during the type declaration, [fld]
     is not enough *)
503
  (* create the type symbol *)
504 505 506 507 508 509 510 511
  create_itysymbol_unsafe ~ts ~pri ~mut ~fld ~regs ~rvis ~avis ~aupd ~def

let rec ity_of_ty ty = match ty.ty_node with
  | Tyvar v -> ity_var v
  | Tyapp (s,tl) ->
      let s = try restore_its s with Not_found ->
        invalid_arg "Ity.ity_of_ty" in
      ity_pur_unsafe s (List.map ity_of_ty tl)
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532

(** pvsymbol creation *)

let create_pvsymbol id ghost ity = {
  pv_vs    = create_vsymbol id (ty_of_ity ity);
  pv_ity   = ity;
  pv_ghost = ghost;
}

let create_pvsymbol, restore_pv =
  let vs_to_pv = Wvs.create 17 in
  (fun id ?(ghost=false) ity ->
    let pv = create_pvsymbol id ghost ity in
    Wvs.set vs_to_pv pv.pv_vs pv;
    pv),
  (fun vs -> Wvs.find vs_to_pv vs)

(** builtin symbols *)

let its_int = create_itysymbol_unsafe
    ~ts:ts_int ~pri:false ~mut:false ~fld:Mvs.empty
533 534 535 536 537
    ~regs:[] ~rvis:[] ~avis:[] ~aupd:[] ~def:None

let its_real = create_itysymbol_unsafe
    ~ts:ts_real ~pri:false ~mut:false ~fld:Mvs.empty
    ~regs:[] ~rvis:[] ~avis:[] ~aupd:[] ~def:None
538 539 540

let its_bool = create_itysymbol_unsafe
    ~ts:ts_bool ~pri:false ~mut:false ~fld:Mvs.empty
541 542 543 544 545 546 547 548 549 550 551 552 553 554
    ~regs:[] ~rvis:[] ~avis:[] ~aupd:[] ~def:None

let ity_int  = ity_pur its_int  []
let ity_real = ity_pur its_real []
let ity_bool = ity_pur its_bool []

let its_tuple = Hint.memo 17 (fun n ->
  let ts = ts_tuple n in
  let ll = List.map (fun _ -> true) ts.ts_args in
  create_itysymbol_unsafe
    ~ts:ts ~pri:false ~mut:false ~fld:Mvs.empty
    ~regs:[] ~rvis:[] ~avis:ll ~aupd:ll ~def:None)

let ity_tuple tl = ity_pur (its_tuple (List.length tl)) tl
555

556 557
let ts_unit  = ts_tuple  0
let its_unit = its_tuple 0
558

559 560
let ty_unit  = ty_tuple  []
let ity_unit = ity_tuple []
561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590

(** computation types (with effects) *)

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

exception PolymorphicException of ident * ity
exception MutableException of ident * ity

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

let create_xsymbol id ity =
  let id = id_register id in
  if not (ity_closed ity) then raise (PolymorphicException (id, ity));
  if not (ity_immutable ity) then raise (MutableException (id, ity));
  { xs_name = id; xs_ity = ity; }

module Exn = MakeMSH (struct
  type t = xsymbol
  let tag xs = Weakhtbl.tag_hash xs.xs_name.id_tag
end)

module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
type effect = {
Andrei Paskevich's avatar
Andrei Paskevich committed
591
  eff_writes : Spv.t Mreg.t;
592
  eff_resets : Sreg.t Mreg.t;
593 594 595 596 597
  eff_raises : Sexn.t;
  eff_diverg : bool;
}

let eff_empty = {
Andrei Paskevich's avatar
Andrei Paskevich committed
598
  eff_writes = Mreg.empty;
599
  eff_resets = Mreg.empty;
600 601 602 603 604
  eff_raises = Sexn.empty;
  eff_diverg = false;
}

let eff_is_empty e =
Andrei Paskevich's avatar
Andrei Paskevich committed
605
  Mreg.is_empty e.eff_writes &&
606
  Mreg.is_empty e.eff_resets &&
607 608 609 610
  Sexn.is_empty e.eff_raises &&
  not e.eff_diverg

let eff_equal e1 e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
611
  Mreg.equal Spv.equal e1.eff_writes e2.eff_writes &&
612
  Mreg.equal Sreg.equal e1.eff_resets e2.eff_resets &&
613 614 615
  Sexn.equal e1.eff_raises e2.eff_raises &&
  e1.eff_diverg = e2.eff_diverg

616 617 618 619 620
let merge_fields _ f1 f2 = Some (Spv.union f1 f2)

let merge_covers reg c1 c2 = Some (Sreg.union
  (Sreg.filter (fun r -> not (ity_r_stale reg c1 r)) c2)
  (Sreg.filter (fun r -> not (ity_r_stale reg c2 r)) c1))
621 622

let eff_union x y = {
623 624
  eff_writes = Mreg.union merge_fields x.eff_writes y.eff_writes;
  eff_resets = Mreg.union merge_covers x.eff_resets y.eff_resets;
625 626 627 628
  eff_raises = Sexn.union x.eff_raises y.eff_raises;
  eff_diverg = x.eff_diverg || y.eff_diverg;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645
let eff_write e r f =
  begin match r.ity_node, f with
    | Itymut (s,_,_,_), Some f when Mvs.mem f.pv_vs s.its_mfields -> ()
    | Itymut _, None -> ()
    | _, _ -> invalid_arg "Ity.eff_write"
  end;
  let add fs = match f, fs with
    | Some f, Some fs -> Some (Spv.add f fs)
    | Some f, None    -> Some (Spv.singleton f)
    | None,   Some fs -> Some fs
    | None,   None    -> Some Spv.empty in
  { e with eff_writes = Mreg.change add r e.eff_writes }

let eff_raise e x = { e with eff_raises = Sexn.add x e.eff_raises }
let eff_catch e x = { e with eff_raises = Sexn.remove x e.eff_raises }

let eff_reset e r = match r.ity_node with
646
  | Itymut _ -> { e with eff_resets = Mreg.add r Sreg.empty e.eff_resets }
Andrei Paskevich's avatar
Andrei Paskevich committed
647
  | _ -> invalid_arg "Ity.eff_reset"
648 649 650

let eff_diverge e = { e with eff_diverg = true }

Andrei Paskevich's avatar
Andrei Paskevich committed
651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
exception AssignPrivate of ity

(* freeze type variables and regions outside modified fields *)
let freeze_of_writes wr =
  let freeze_of_write r fs frz =
    let s,tl,rl,_ = open_region r in
    let frz = List.fold_left ity_freeze frz tl in
    let freeze_unhit frz r reg =
      (* fields are unaliased in [s], therefore if region [r] from
          [s.its_regions] occurs in [f.pv_ity], it cannot occur in
          any other field of [s], and therefore [reg] doesn't need
          to be frozen. If [reg] or subregions of [reg] are aliased
          with other fields of the modified value, they will occur
          in the instances of other regions in [s.its_regions], and
          will be frozen there. *)
      let hit f _ = ity_r_occurs r f.pv_ity in
      if Mpv.exists hit fs then frz else ity_freeze frz reg in
    List.fold_left2 freeze_unhit frz s.its_regions rl in
  Mreg.fold freeze_of_write wr Mtv.empty

let eff_assign e asl =
  let seen,e = List.fold_left (fun (seen,e) (r,f,ity) ->
    begin match r.ity_node with
      | Itymut (s,_,_,_) when s.its_private -> raise (AssignPrivate r)
      | Itymut (s,_,_,_) when Mvs.mem f.pv_vs s.its_mfields -> ()
      | _ -> invalid_arg "Ity.eff_assign"
    end;
    let seen = Mreg.change (fun fs -> Some (match fs with
      | Some fs -> Mpv.add_new (Invalid_argument "Ity.eff_assign") f ity fs
      | None    -> Mpv.singleton f ity)) r seen in
    seen, eff_write e r (Some f)) (Mreg.empty,e) asl in
  (* type variables and regions outside modified fields are frozen *)
  let frz = freeze_of_writes seen in
  (* non-frozen regions are allowed to be renamed, preserving aliases *)
  let sbst, sbsf = Mreg.fold (fun r fs acc ->
    let s,tl,rl,_ = open_region r in
    let sbs = List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty in
    let sbs = List.fold_left2 ity_match sbs s.its_regions rl in
689 690
    (* TODO: catch the TypeMismatch exception and produce a reasonable
       error message *)
Andrei Paskevich's avatar
Andrei Paskevich committed
691 692 693 694 695
    Mpv.fold (fun pv ity (sbst,sbsf) ->
      let fity = ity_full_inst sbs pv.pv_ity in
      ity_match sbst fity ity,
      ity_match sbsf ity fity) fs acc) seen (frz,frz) in
  (* every RHS region is reset unless it is preserved *)
Andrei Paskevich's avatar
Andrei Paskevich committed
696
  let rst = Mtv.set_diff sbsf sbst in
697 698 699 700 701
  let e = Mtv.fold (fun v _ e ->
    (* since type variables are frozen, they can't appear in [rst].
       Thus, [v] has to be a region variable, and [ity_var_unsafe]
       will restore the corresponging region via hash-consing. *)
    eff_reset e (ity_var_unsafe v)) rst e in
Andrei Paskevich's avatar
Andrei Paskevich committed
702
  (* every region not instantiated to itself is refreshed *)
Andrei Paskevich's avatar
Andrei Paskevich committed
703 704 705
  let rfr = Mreg.fold (fun r _ rfr ->
    let sbst = Mtv.inter (fun v reg i -> match i.ity_node with
      | Itymut (_,_,_,u) when not (tv_equal u v) -> Some reg
706
      | _ -> None) (ity_freeze Mtv.empty r) sbst in
Andrei Paskevich's avatar
Andrei Paskevich committed
707
    let add_rfr _ reg rfr = Mreg.change (function
708 709
      | Some cvr -> Some (Sreg.add r cvr)
      | None     -> Some (Sreg.singleton r)) reg rfr in
Andrei Paskevich's avatar
Andrei Paskevich committed
710
    Mtv.fold add_rfr sbst rfr) seen Mreg.empty in
711
  { e with eff_resets = Mreg.union merge_covers e.eff_resets rfr }
Andrei Paskevich's avatar
Andrei Paskevich committed
712 713 714

let refresh_of_effect e =
  let frz = freeze_of_writes e.eff_writes in
715 716
  let rfr = Mreg.fold (fun r _ rfr ->
    let sbst = Mtv.set_diff (ity_freeze Mtv.empty r) frz in
Andrei Paskevich's avatar
Andrei Paskevich committed
717
    let add_rfr _ reg rfr = Mreg.change (function
718 719
      | Some cvr -> Some (Sreg.add r cvr)
      | None     -> Some (Sreg.singleton r)) reg rfr in
720 721
    Mtv.fold add_rfr sbst rfr) e.eff_writes Mreg.empty in
  { e with eff_resets = Mreg.union merge_covers e.eff_resets rfr }
Andrei Paskevich's avatar
Andrei Paskevich committed
722

723 724 725
exception IllegalAlias of region

let eff_full_inst sbs e =
Andrei Paskevich's avatar
Andrei Paskevich committed
726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
  (* all modified or reset regions in e must be instantiated
     into distinct regions *)
  let inst fn src = Mreg.fold (fun r v acc ->
    let r = ity_full_inst sbs r in
    Mreg.add_new (IllegalAlias r) r (fn v) acc) src Mreg.empty in
  let writes = inst (fun fld -> fld) e.eff_writes in
  let resets = inst (inst (fun () -> ())) e.eff_resets in
  let impact = Mreg.merge (fun r fld cvr -> match fld, cvr with
    | Some _, Some _ -> raise (IllegalAlias r)
    | _ -> Some ()) writes resets in
  (* all type variables must be instantiated into types that are
     not affected by the effect, and all unaffected regions must
     be instantiated into regions outside [impact].

     Now, every region in the instantiated execution is either
     brought in by the type substitution and thus is unaffected,
     or instantiates one of the original regions and is affected
     if and only if the original one is. *)
  let check_inst v dst = match ity_var_unsafe v with
    | {ity_node = Ityvar _} -> Sreg.iter (fun r ->
        if ity_r_occurs r dst then raise (IllegalAlias r)) impact
    | reg when Mreg.mem reg e.eff_writes -> ()
    | reg when Mreg.mem reg e.eff_resets -> ()
    | _   when Sreg.mem dst impact -> raise (IllegalAlias dst)
    | _ -> () in
  Mtv.iter check_inst sbs;
  { e with eff_writes = writes; eff_resets = resets }
753

Andrei Paskevich's avatar
Andrei Paskevich committed
754
(*
755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 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 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016
let eff_filter vars e =
  let check r = reg_occurs r vars in
  let reset r = function
    | _ when not (check r) -> None
    | Some u as v when check u -> Some v
    | _ -> Some None
  in
  { e with
    eff_writes = Sreg.filter check e.eff_writes;
    eff_ghostw = Sreg.filter check e.eff_ghostw;
    eff_resets = Mreg.mapi_filter reset e.eff_resets;
    eff_compar = Stv.inter vars.vars_tv e.eff_compar;
  }

let eff_stale_region eff vars =
  let check_reset r u =
    let rec check_reg reg =
      reg_equal r reg || match u with
        | Some u when reg_equal u reg -> false
        | _ -> Sreg.exists check_reg reg.reg_ity.ity_vars.vars_reg in
    Sreg.exists check_reg vars.vars_reg in
  Mreg.exists check_reset eff.eff_resets

(** specification *)

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

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

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 = {
  c_pre     : pre;
  c_post    : post;
  c_xpost   : xpost;
  c_effect  : effect;
  c_variant : variant list;
  c_letrec  : int;
}

let spec_empty ty = {
  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;
}

let spec_full_inst sbs tvm vsm c =
  let subst = t_ty_subst tvm vsm in {
    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;
  }

let spec_subst sbs c =
  let subst = t_subst sbs in {
    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;
  }

let spec_vsset c =
  let add f s = Mvs.set_union (t_vars f) s in
  let s = add c.c_pre (t_vars c.c_post) in
  let s = Mexn.fold (fun _ f s -> add f s) c.c_xpost s in
  List.fold_left (fun s (t,_) -> add t s) s c.c_variant

let spec_filter ghost svs vars c =
  let s = spec_vsset c in
  if not (Mvs.set_submap s svs) then
    Loc.errorm "Local variable %s escapes from its scope"
      (fst (Mvs.choose (Mvs.set_diff s svs))).vs_name.id_string;
  if not ghost && not (Sexn.is_empty c.c_effect.eff_ghostx) then
    Loc.errorm "Only ghost functions may raise ghost exceptions";
  { c with c_effect = eff_ghostify ghost (eff_filter vars c.c_effect) }

exception UnboundException of xsymbol

let spec_check ~full_xpost 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;
  (* we admit non-empty variant list even for null letrec,
     so that we can store there external variables from
     user-written effects to save them from spec_filter *)
  let check_variant (t,rel) = match rel with
    | Some ps -> ignore (ps_app ps [t;t])
    | None -> ignore (t_type t) in
  List.iter check_variant c.c_variant;
  if full_xpost && not (Mexn.set_submap c.c_effect.eff_raises c.c_xpost) then
    raise (UnboundException
      (Sexn.choose (Mexn.set_diff c.c_effect.eff_raises c.c_xpost)));
  if full_xpost && not (Mexn.set_submap c.c_effect.eff_ghostx c.c_xpost) then
    raise (UnboundException
      (Sexn.choose (Mexn.set_diff c.c_effect.eff_ghostx c.c_xpost)))

(** program variables *)

let pvs_of_vss pvs vss =
  Mvs.fold (fun vs _ s -> Spv.add (restore_pv vs) s) vss pvs

let t_pvset pvs t = pvs_of_vss pvs (t_vars t)

let spec_pvset pvs spec = pvs_of_vss pvs (spec_vsset spec)

(** program types *)

type vty =
  | VTvalue of ity
  | VTarrow of aty

and aty = {
  aty_args   : pvsymbol list;
  aty_result : vty;
  aty_spec   : spec;
}

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

and vty_vars = function
  | VTvalue ity -> ity.ity_vars
  | VTarrow aty -> aty_vars aty

let rec aty_pvset aty =
  let spv = match aty.aty_result with
    | VTarrow a -> aty_pvset a
    | VTvalue _ -> Spv.empty in
  let spv = spec_pvset spv aty.aty_spec in
  List.fold_right Spv.remove aty.aty_args spv

let ity_of_vty = function
  | VTvalue ity -> ity
  | VTarrow _   -> ity_unit

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

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

let vty_arrow_unsafe argl spec vty = {
  aty_args   = argl;
  aty_result = vty;
  aty_spec   = spec;
}

let vty_arrow argl ?spec vty =
  let exn = Invalid_argument "Mlw.vty_arrow" in
  (* the arguments must be all distinct *)
  if argl = [] then raise exn;
  let add_arg pvs pv = Spv.add_new exn pv pvs in
  ignore (List.fold_left add_arg Spv.empty argl);
  let spec = match spec with
    | Some spec -> spec_check spec vty; spec
    | None -> spec_empty (ty_of_vty vty) in
  vty_arrow_unsafe argl spec vty

(* this only compares the types of arguments and results, and ignores
   the spec. In other words, only the type variables and regions in
   [aty_vars aty] are matched. The caller should supply a "freezing"
   substitution that covers all external type variables and regions. *)
let rec aty_vars_match s a argl res =
  let rec match_args s l1 l2 = match l1, l2 with
    | v1::l1, v2::l2 -> match_args (ity_match s v1.pv_ity v2) l1 l2
    | [], l -> s, l
    | _, [] -> invalid_arg "Mlw_ty.aty_vars_match" in
  let s, argl = match_args s a.aty_args argl in
  match a.aty_result, argl with
  | VTvalue v, [] -> ity_match s v res
  | VTvalue _, _
  | VTarrow _, [] -> invalid_arg "Mlw_ty.aty_vars_match"
  | VTarrow a, _  -> aty_vars_match s a argl res

(* the substitution must cover not only [aty_vars aty] but
   also every type variable and every region in [aty_spec] *)
let aty_full_inst sbs aty =
  let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
  let pv_inst { pv_vs = vs; pv_ity = ity; pv_ghost = ghost } =
    create_pvsymbol (id_clone vs.vs_name) ~ghost (ity_full_inst sbs ity) 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 aty_inst vsm aty =
    let vsm, args = Lists.map_fold_left add_arg vsm aty.aty_args in
    let spec = spec_full_inst sbs tvm vsm aty.aty_spec in
    let vty = match aty.aty_result with
      | VTarrow aty -> VTarrow (aty_inst vsm aty)
      | VTvalue ity -> VTvalue (ity_full_inst sbs ity) in
    vty_arrow_unsafe args spec vty
  in
  aty_inst Mvs.empty aty

(* remove from the given arrow every inner effect *)
let rec aty_filter ghost svs vars aty =
  let add svs pv = Svs.add pv.pv_vs svs in
  let svs = List.fold_left add svs aty.aty_args in
  let add vars pv = vars_union vars pv.pv_ity.ity_vars in
  let vars = List.fold_left add vars aty.aty_args in
  (* remove the effects that do not affect the context *)
  let spec = spec_filter ghost svs vars aty.aty_spec in
  (* reset every fresh region in the returned value *)
  let spec = match aty.aty_result with
    | VTvalue v ->
        let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
        { spec with c_effect = reg_fold on_reg v.ity_vars spec.c_effect }
    | VTarrow _ -> spec in
  (* filter the result type *)
  let vty = match aty.aty_result with
    | VTarrow a -> VTarrow (aty_filter ghost svs vars a)
    | VTvalue _ -> aty.aty_result in
  vty_arrow_unsafe aty.aty_args spec vty

let aty_filter ?(ghost=false) pvs aty =
  let add pv svs = Svs.add pv.pv_vs svs in
  let svs = Spv.fold add pvs Svs.empty in
  let add pv vars = vars_union vars pv.pv_ity.ity_vars in
  let vars = Spv.fold add pvs vars_empty in
  aty_filter ghost svs vars aty

let aty_app aty pv =
  let arg, rest = match aty.aty_args with
    | arg::rest -> arg,rest | _ -> assert false in
  ity_equal_check arg.pv_ity pv.pv_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.aty_args) ->
        let result = vty_subst a.aty_result in
        let spec = spec_subst sbs a.aty_spec in
        VTarrow (vty_arrow_unsafe a.aty_args spec result)
    | vty -> vty in
  let result = vty_subst aty.aty_result in
  let spec = spec_subst sbs aty.aty_spec in
  if not pv.pv_ghost && arg.pv_ghost then
    Loc.errorm "non-ghost value passed as a ghost argument";
  let ghost = pv.pv_ghost && not arg.pv_ghost in
  if rest = [] then
    spec, ghost, result
  else
    spec_empty ty_unit, ghost, VTarrow (vty_arrow_unsafe rest spec result)
*)