ity.ml 65.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10 11 12 13 14
(********************************************************************)

open Stdlib
open Ident
open Ty
15
open Term
16

17
(** {2 Individual types (first-order types without effects)} *)
18 19

type itysymbol = {
20
  its_ts      : tysymbol;       (** logical type symbol *)
21
  its_nonfree : bool;           (** has no constructors *)
22 23
  its_private : bool;           (** private type *)
  its_mutable : bool;           (** mutable type *)
24
  its_fragile : bool;           (** breakable invariant *)
25
  its_mfields : pvsymbol list;  (** mutable record fields *)
26
  its_regions : region list;    (** shareable components *)
27 28
  its_arg_flg : its_flag list;  (** flags for type args *)
  its_reg_flg : its_flag list;  (** flags for regions *)
29
  its_def     : ity option;     (** type alias *)
30 31
}

32 33 34 35 36 37 38 39
and its_flag = {
  its_frozen  : bool;   (** cannot be updated *)
  its_exposed : bool;   (** directly reachable from a field *)
  its_liable  : bool;   (** exposed in the type invariant *)
  its_fixed   : bool;   (** exposed in a non-mutable field *)
  its_visible : bool;   (** visible from the non-ghost code *)
}

40 41
and ity = {
  ity_node : ity_node;
42
  ity_imm  : bool;
43 44 45 46
  ity_tag  : Weakhtbl.tag;
}

and ity_node =
47
  | Ityreg of region
48
    (** record with mutable fields and shareable components *)
49 50 51 52
  | Ityapp of itysymbol * ity list * ity list
    (** immutable type with shareable components *)
  | Ityvar of tvsymbol * bool
    (** type variable and its purity status *)
53

54
and region = {
55
  reg_name : ident;
56 57
  reg_its  : itysymbol;
  reg_args : ity list;
58
  reg_regs : ity list;
59 60
}

61 62 63 64 65
and pvsymbol = {
  pv_vs    : vsymbol;
  pv_ity   : ity;
  pv_ghost : bool;
}
66 67 68 69 70 71

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

72 73 74 75 76
module Ity = MakeMSHW (struct
  type t = ity
  let tag ity = ity.ity_tag
end)

77 78
module Reg = MakeMSHW (struct
  type t = region
79
  let tag reg = reg.reg_name.id_tag
80 81
end)

82 83 84 85 86
module PVsym = MakeMSHW (struct
  type t = pvsymbol
  let tag pv = pv.pv_vs.vs_name.id_tag
end)

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

92 93 94 95 96
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W

97 98 99 100
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W
101 102 103 104 105 106 107 108

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

(* value type symbols *)

109 110
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
111
let reg_equal : region    -> region    -> bool = (==)
112
let pv_equal  : pvsymbol  -> pvsymbol  -> bool = (==)
113 114 115

let its_hash its = id_hash its.its_ts.ts_name
let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
116
let reg_hash reg = id_hash reg.reg_name
117 118
let pv_hash  pv  = id_hash pv.pv_vs.vs_name

119 120
let its_compare its1 its2 = id_compare its1.its_ts.ts_name its2.its_ts.ts_name
let ity_compare ity1 ity2 = Pervasives.compare (ity_hash ity1) (ity_hash ity2)
121
let reg_compare reg1 reg2 = id_compare reg1.reg_name reg2.reg_name
122 123
let pv_compare  pv1  pv2  = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name

124 125 126 127
module Hsity = Hashcons.Make (struct
  type t = ity

  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
128
    | Ityvar (v1,p1), Ityvar (v2,p2) -> tv_equal v1 v2 && p1 = p2
129
    | Ityreg r1, Ityreg r2 -> reg_equal r1 r2
130 131 132
    | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) ->
        its_equal s1 s2 &&
        List.for_all2 ity_equal l1 l2 &&
133
        List.for_all2 ity_equal r1 r2
134 135 136
    | _ -> false

  let hash ity = match ity.ity_node with
137 138
    | Ityvar (v,p) ->
        Hashcons.combine (tv_hash v) (Hashtbl.hash p)
139
    | Ityreg r -> reg_hash r
140
    | Ityapp (s,tl,rl) ->
141
        Hashcons.combine_list ity_hash
142 143
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl

144
  let immutable ity = match ity.ity_node with
145
    | Ityvar _ -> true
146
    | Ityreg _ -> false
147
    | Ityapp (_,tl,rl) ->
148 149
        let imm ity = ity.ity_imm in
        List.for_all imm tl && List.for_all imm rl
150

151
  let tag n ity = { ity with
152 153
    ity_imm = immutable ity;
    ity_tag = Weakhtbl.create_tag n }
154
end)
155

156 157
let mk_ity node = {
  ity_node = node;
158
  ity_imm  = true;
159 160 161
  ity_tag  = Weakhtbl.dummy_tag;
}

162 163
let mk_reg name s tl rl = {
  reg_name = id_register name;
164
  reg_its  = s;
165
  reg_args = tl;
166 167
  reg_regs = rl;
}
168

169 170 171
let ity_reg r              = Hsity.hashcons (mk_ity (Ityreg r))
let ity_var v              = Hsity.hashcons (mk_ity (Ityvar (v,false)))
let ity_var_pure v         = Hsity.hashcons (mk_ity (Ityvar (v,true)))
172
let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
173

174 175
(* immutability and purity *)

176
let its_immutable s = not s.its_mutable
177

178
let its_pure s = not s.its_mutable && s.its_regions = []
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198

let ity_immutable ity = ity.ity_imm

let rec ity_pure ity = match ity.ity_node with
  | Ityreg _ -> false
  | Ityapp (_,tl,rl) -> List.for_all ity_pure tl && List.for_all ity_pure rl
  | Ityvar (_,p) -> p

let ity_pure ity = ity_immutable ity && ity_pure ity

let rec ity_purify ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} | Ityapp (s,tl,rl) ->
      ity_app_unsafe s (List.map ity_purify tl) (List.map ity_purify rl)
  | Ityvar (v,_) -> ity_var_pure v

let rec ty_of_ity ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
      ty_app s.its_ts (List.map ty_of_ity tl)
  | Ityvar (v,_) -> ty_var v

199
(* generic traversal functions *)
200

201 202 203 204 205 206 207 208
let dfold fn acc tl rl =
  List.fold_left fn (List.fold_left fn acc tl) rl

let dfold2 fn acc tl1 tl2 rl1 rl2 =
  List.fold_left2 fn (List.fold_left2 fn acc tl1 tl2) rl1 rl2

let its_arg_fold fn acc s tl =
  List.fold_left2 fn acc s.its_arg_flg tl
209

210 211 212 213 214
let its_reg_fold fn acc s rl =
  List.fold_left2 fn acc s.its_reg_flg rl

let its_fold fn acc s tl rl =
  its_reg_fold fn (its_arg_fold fn acc s tl) s rl
215

216 217 218
let ity_fold fn acc ity = match ity.ity_node with
  | Ityreg {reg_args = tl; reg_regs = rl}
  | Ityapp (_,tl,rl) -> dfold fn acc tl rl
219 220
  | Ityvar _ -> acc

221
let reg_fold fn acc reg = dfold fn acc reg.reg_args reg.reg_regs
222

223
(* symbol-wise fold *)
224

225
let rec ity_s_fold fn acc ity = match ity.ity_node with
226 227
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) -> dfold (ity_s_fold fn) (fn acc s) tl rl
228 229
  | Ityvar _ -> acc

230
let reg_s_fold fn acc r = reg_fold (ity_s_fold fn) (fn acc r.reg_its) r
231

232
(* traversal functions on type variables *)
233 234

let rec ity_v_fold fn acc ity = match ity.ity_node with
235
  | Ityreg {reg_args = tl} | Ityapp (_,tl,_) ->
236
      List.fold_left (ity_v_fold fn) acc tl
237
  | Ityvar (v,_) -> fn acc v
238 239

let reg_v_fold fn acc r = List.fold_left (ity_v_fold fn) acc r.reg_args
240

241 242
let ity_freevars s ity = ity_v_fold Stv.add_left s ity
let reg_freevars s reg = reg_v_fold Stv.add_left s reg
243

244 245
let ity_v_occurs v ity = Util.any ity_v_fold (tv_equal v) ity
let reg_v_occurs v reg = Util.any reg_v_fold (tv_equal v) reg
246

247
let ity_closed ity = Util.all ity_v_fold Util.ffalse ity
248

249
(* traversal functions on top regions *)
250 251

let rec ity_r_fold fn acc ity =
252
  if ity.ity_imm then acc else
253
  match ity.ity_node with
254
  | Ityapp (_,tl,rl) -> dfold (ity_r_fold fn) acc tl rl
255
  | Ityreg r -> fn acc r
256
  | Ityvar _ -> acc
257

258
let reg_r_fold fn acc reg = reg_fold (ity_r_fold fn) acc reg
259

260
let ity_top_regs regs ity = ity_r_fold Sreg.add_left regs ity
261

262 263
let rec reg_freeregs s reg = reg_r_fold reg_freeregs (Sreg.add reg s) reg
let     ity_freeregs s ity = ity_r_fold reg_freeregs s ity
264

265 266 267
let rec reg_r_occurs r reg = reg_equal r reg ||
                             Util.any reg_r_fold (reg_r_occurs r) reg
let     ity_r_occurs r ity = Util.any ity_r_fold (reg_r_occurs r) ity
268

269 270 271 272 273 274 275 276 277 278
(* traversal functions on exposed regions *)

let rec ity_exp_fold fn acc ity =
  if ity.ity_imm then acc else
  match ity.ity_node with
  | Ityapp (s,tl,rl) -> its_exp_fold fn acc s tl rl
  | Ityreg r -> fn acc r
  | Ityvar _ -> acc

and its_exp_fold fn acc s tl rl =
279 280
  let fn a x t = if x.its_exposed then ity_exp_fold fn a t else a in
  its_fold fn acc s tl rl
281 282 283

let reg_exp_fold fn acc reg =
  its_exp_fold fn acc reg.reg_its reg.reg_args reg.reg_regs
284

285
let ity_exp_regs regs ity = ity_exp_fold Sreg.add_left regs ity
286

287 288
let rec reg_rch_regs s reg = reg_exp_fold reg_rch_regs (Sreg.add reg s) reg
let     ity_rch_regs s ity = ity_exp_fold reg_rch_regs s ity
289

290 291 292
let rec reg_rch_fold fn a reg = reg_exp_fold (reg_rch_fold fn) (fn a reg) reg
let     ity_rch_fold fn a ity = ity_exp_fold (reg_rch_fold fn) a ity

Andrei Paskevich's avatar
Andrei Paskevich committed
293 294
let reg_r_reachable r reg = Util.any reg_rch_fold (reg_equal r) reg
let ity_r_reachable r ity = Util.any ity_rch_fold (reg_equal r) ity
295

Andrei Paskevich's avatar
Andrei Paskevich committed
296 297 298 299 300 301
let rec reg_unc_fold cv fn a r = if Sreg.mem r cv then a else
                                 reg_exp_fold (reg_unc_fold cv fn) (fn a r) r
let     ity_unc_fold cv fn a t = ity_exp_fold (reg_unc_fold cv fn) a t

let reg_r_stale rs cv reg = Util.any (reg_unc_fold cv) (Sreg.contains rs) reg
let ity_r_stale rs cv ity = Util.any (ity_unc_fold cv) (Sreg.contains rs) ity
302

303 304 305 306
(* collect exposed and reachable type variables *)

let rec ity_exp_vars vars ity = match ity.ity_node with
  | Ityapp (s,tl,rl) ->
307 308
      let fn a x t = if x.its_exposed then ity_exp_vars a t else a in
      its_fold fn vars s tl rl
309 310 311 312 313 314
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) | Ityreg _ -> vars

let rec ity_rch_vars vars ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) ->
315 316
      let fn a x t = if x.its_exposed then ity_rch_vars a t else a in
      its_fold fn vars s tl rl
317 318 319 320 321
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) -> vars

(* traversal functions on non-updatable regions *)

322
let fold_on_frz fn_frz fn_rch acc ity = match ity.ity_node with
323 324 325 326
  | Ityapp (s,_,_) when s.its_nonfree && s.its_mutable ->
      fn_rch acc ity
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) ->
327 328 329
      let fn a f t = if not f.its_exposed then a else
        if f.its_frozen then fn_rch a t else fn_frz a t in
      its_fold fn acc s tl rl
330 331
  | Ityvar _ -> acc

332 333
let rec ity_frz_vars vars ity =
  fold_on_frz ity_frz_vars ity_rch_vars vars ity
334

335
let rec ity_frz_regs regs ity =
336
  if ity.ity_imm then regs else
337
  fold_on_frz ity_frz_regs ity_rch_regs regs ity
338

339
let rec ity_frz_fold fn acc ity =
340
  if ity.ity_imm then acc else
341
  fold_on_frz (ity_frz_fold fn) (ity_rch_fold fn) acc ity
342

343 344
let ity_r_frozen s ity =
  Util.any ity_frz_fold (Mreg.contains s) ity
345

346 347
(** detect fragile types *)

Andrei Paskevich's avatar
Andrei Paskevich committed
348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
let rec ity_fragile liable () ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) ->
      (* can we be broken or break an outer invariant? *)
      if s.its_fragile || (liable && s.its_mutable) then raise Exit else
      (* can we have broken reachable components? *)
      if s.its_private || (s.its_nonfree && not s.its_mutable) then () else
      (* reachable frozen components cannot be broken *)
      let fn () x t =
        if x.its_exposed && not x.its_frozen then
          ity_fragile (liable || x.its_liable) () t in
      its_fold fn () s tl rl
  | Ityvar _ -> ()

let ity_liquid ity =
  try ity_fragile true () ity; false with Exit -> true

365
let ity_fragile ity =
Andrei Paskevich's avatar
Andrei Paskevich committed
366
  try ity_fragile false () ity; false with Exit -> true
367

368 369 370 371
(* traversal functions on non-ghost regions *)

let rec ity_vis_fold fn acc ity =
  if ity.ity_imm then acc else
372
  match ity.ity_node with
373 374 375 376 377
  | Ityapp (s,tl,rl) -> its_vis_fold fn acc s tl rl
  | Ityreg r -> reg_vis_fold fn acc r
  | Ityvar _ -> acc

and its_vis_fold fn acc s tl rl =
378 379
  let fn a v t = if v.its_visible then ity_vis_fold fn a t else a in
  its_fold fn acc s tl rl
380 381

and reg_vis_fold fn acc reg =
382
  its_vis_fold fn (fn acc reg) reg.reg_its reg.reg_args reg.reg_regs
383 384 385 386 387 388 389

let ity_vis_regs regs ity = ity_vis_fold Sreg.add_left regs ity

(* collect non-ghost type variables *)

let rec ity_vis_vars vars ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
390 391
      let fn a v t = if v.its_visible then ity_vis_vars a t else a in
      its_arg_fold fn vars s tl
392 393 394 395
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) -> vars

(* type matching *)
396 397 398 399 400 401 402

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

exception DuplicateRegion of region
exception UnboundRegion of region

403 404
exception ImpureType of tvsymbol * ity

405
type ity_subst = {
406 407 408
  isb_var : ity Mtv.t;
  isb_pur : ity Mtv.t;
  isb_reg : ity Mreg.t;
409 410
}

411
let isb_empty = {
412 413
  isb_var = Mtv.empty;
  isb_pur = Mtv.empty;
414
  isb_reg = Mreg.empty;
415 416 417
}

exception TypeMismatch of ity * ity * ity_subst
418

Andrei Paskevich's avatar
Andrei Paskevich committed
419 420
let ity_equal_check t1 t2 = if not (ity_equal t1 t2) then
  raise (TypeMismatch (t1, t2, isb_empty))
421

Andrei Paskevich's avatar
Andrei Paskevich committed
422 423
let reg_equal_check r1 r2 = if not (reg_equal r1 r2) then
  raise (TypeMismatch (ity_reg r1, ity_reg r2, isb_empty))
424 425

let ity_full_inst sbs ity =
426
  let rec inst ity = match ity.ity_node with
427
    | Ityreg r -> Mreg.find r sbs.isb_reg
428
    | Ityapp (s,tl,rl) ->
429 430 431 432 433 434
        ity_app_unsafe s (List.map inst tl) (List.map inst rl)
    | Ityvar (v,false) -> Mtv.find v sbs.isb_var
    | Ityvar (v,true) ->
        try Mtv.find v sbs.isb_pur with Not_found ->
        ity_purify (Mtv.find v sbs.isb_var) in
  if ity.ity_imm && ity_closed ity then ity else inst ity
435

436
let reg_full_inst sbs reg = Mreg.find reg sbs.isb_reg
437 438 439 440 441 442 443 444 445

let add_or_keep eq n = function
  | None -> Some n
  | Some o as r when eq o n -> r
  | _ -> raise Exit

let rec ity_match sbs ity1 ity2 =
  let set = add_or_keep ity_equal ity2 in
  match ity1.ity_node, ity2.ity_node with
446
  | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) when its_equal s1 s2 ->
447 448 449 450 451 452 453 454 455 456 457 458 459 460
      dfold2 ity_match sbs l1 l2 r1 r2
  | Ityreg r1, _ ->
      reg_match sbs r1 ity2
  | Ityvar (v1, false), _ ->
      if Mtv.mem v1 sbs.isb_pur &&
         not (ity_equal (ity_purify ity2) (Mtv.find v1 sbs.isb_pur))
      then raise Exit;
      { sbs with isb_var = Mtv.change set v1 sbs.isb_var }
  | Ityvar (v1, true), _ when ity_pure ity2 ->
      if Mtv.mem v1 sbs.isb_var &&
         not (ity_equal ity2 (ity_purify (Mtv.find v1 sbs.isb_var)))
      then raise Exit;
      { sbs with isb_pur = Mtv.change set v1 sbs.isb_pur }
  | Ityvar (v1, true), _ -> raise (ImpureType (v1, ity2))
461
  | _ -> raise Exit
462

463 464 465 466 467 468 469 470 471 472
and reg_match sbs reg1 ity2 =
  let seen = ref false in
  let set = add_or_keep (fun o n -> seen := true; ity_equal o n) ity2 in
  let sbs = { sbs with isb_reg = Mreg.change set reg1 sbs.isb_reg } in
  if !seen then sbs else
  match ity2.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} | Ityapp (s,tl,rl)
    when its_equal reg1.reg_its s ->
      dfold2 ity_match sbs reg1.reg_args tl reg1.reg_regs rl
  | _ -> raise Exit
473 474

let ity_match sbs ity1 ity2 = try ity_match sbs ity1 ity2
475
  with Exit -> raise (TypeMismatch (ity1, ity2, sbs))
476

477 478
let reg_match sbs reg1 ity2 = try reg_match sbs reg1 ity2
  with Exit -> raise (TypeMismatch (ity_reg reg1, ity2, sbs))
479

480
let ity_freeze sbs ity = ity_match sbs ity ity
481
let reg_freeze sbs reg = reg_match sbs reg (ity_reg reg)
482

483
(* raw type constructors *)
484

485 486 487 488 489
let ity_app_raw sbs id s tl rl = match s.its_def with
  | Some { ity_node = Ityreg r } ->
      let tl = List.map (ity_full_inst sbs) r.reg_args in
      let rl = List.map (ity_full_inst sbs) r.reg_regs in
      ity_reg (mk_reg id r.reg_its tl rl)
490
  | None when s.its_mutable ->
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512
      ity_reg (mk_reg id s tl rl)
  | Some ity -> ity_full_inst sbs ity
  | None -> ity_app_unsafe s tl rl

let create_region_raw sbs id s tl rl =
  match (ity_app_raw sbs id s tl rl).ity_node with
  | Ityreg r -> r
  | _ -> invalid_arg "Ity.create_region"

let ity_app_pure_raw sbs s tl rl = match s.its_def with
  | Some { ity_node = Ityreg r } ->
      let tl = List.map (ity_full_inst sbs) r.reg_args in
      let rl = List.map (ity_full_inst sbs) r.reg_regs in
      ity_app_unsafe r.reg_its tl rl
  | Some ity -> ity_full_inst sbs ity
  | None -> ity_app_unsafe s tl rl

(* smart type constructors *)

let its_check_args s tl =
  if List.length s.its_ts.ts_args <> List.length tl
  then raise (BadItyArity (s, List.length tl))
513

514 515
let its_match_args s tl =
  try {
516 517
    isb_var = List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty;
    isb_pur = Mtv.empty;
518
    isb_reg = Mreg.empty }
519 520 521 522
  with Invalid_argument _ -> raise (BadItyArity (s, List.length tl))

let its_match_regs s tl rl =
  try List.fold_left2 reg_match (its_match_args s tl) s.its_regions rl
523 524
  with Invalid_argument _ -> raise (BadRegArity (s, List.length rl))

525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540
let its_inst_regs fresh_reg s tl =
  let rec ity_inst sbs ity = match ity.ity_node with
    | Ityreg r ->
        reg_inst sbs r
    | Ityapp (s,tl,rl) ->
        let sbs, tl = Lists.map_fold_left ity_inst sbs tl in
        let sbs, rl = Lists.map_fold_left ity_inst sbs rl in
        sbs, ity_app_unsafe s tl rl
    | Ityvar (v, false) ->
        sbs, Mtv.find v sbs.isb_var
    | Ityvar (v,true) ->
        sbs, ity_purify (Mtv.find v sbs.isb_var)
  and reg_inst sbs r =
    try sbs, Mreg.find r sbs.isb_reg with Not_found ->
    let sbs, tl = Lists.map_fold_left ity_inst sbs r.reg_args in
    let sbs, rl = Lists.map_fold_left ity_inst sbs r.reg_regs in
541
    let ity = fresh_reg (id_clone r.reg_name) r.reg_its tl rl in
542 543 544 545 546 547 548 549
    { sbs with isb_reg = Mreg.add r ity sbs.isb_reg }, ity in
  Lists.map_fold_left reg_inst (its_match_args s tl) s.its_regions

let its_match_smart fresh_reg s tl rl =
  if rl <> [] then its_match_regs s tl rl, rl else
  if s.its_regions = [] && s.its_def = None
  then (its_check_args s tl; isb_empty, [])
  else its_inst_regs fresh_reg s tl
550

551
let create_region id s tl rl =
552
  let fresh id s tl rl = ity_reg (mk_reg id s tl rl) in
553 554
  let sbs, rl = its_match_smart fresh s tl rl in
  create_region_raw sbs id s tl rl
555 556

let ity_app s tl rl =
557
  let fresh id s tl rl = ity_reg (mk_reg id s tl rl) in
558 559 560 561 562 563 564
  let sbs, rl = its_match_smart fresh s tl rl in
  ity_app_raw sbs (id_fresh "rho") s tl rl

let ity_app_pure s tl rl =
  let pure _ s tl rl = ity_app_unsafe s tl rl in
  let sbs, rl = its_match_smart pure s tl rl in
  ity_app_pure_raw sbs s tl rl
565 566 567

(* itysymbol creation *)

568
let mk_its, restore_its =
569
  let ts_to_its = Wts.create 17 in
570
  (fun ~ts ~nfr ~priv ~mut ~frg ~mfld ~regs ~aflg ~rflg ~def ->
571
    let its = {
572
      its_ts      = ts;
573
      its_nonfree = nfr;
574 575
      its_private = priv;
      its_mutable = mut;
576
      its_fragile = frg;
577
      its_mfields = mfld;
578
      its_regions = regs;
579 580
      its_arg_flg = aflg;
      its_reg_flg = rflg;
581
      its_def     = def;
582 583 584
    } in
    Wts.set ts_to_its ts its;
    its),
585
  (fun ts -> Wts.find ts_to_its ts)
586

587 588 589 590 591
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
592 593 594 595 596 597 598 599
      ity_app s (List.map ity_of_ty tl) []

let rec ity_of_ty_pure ty = match ty.ty_node with
  | Tyvar v -> ity_var_pure v
  | Tyapp (s,tl) ->
      let s = try restore_its s with Not_found ->
        invalid_arg "Ity.ity_of_ty_pure" in
      ity_app_pure s (List.map ity_of_ty_pure tl) []
600

601 602 603 604
let mk_flg ~frz ~exp ~lbl ~fxd ~vis = {
  its_frozen = frz; its_exposed = exp; its_liable = lbl;
  its_fixed  = fxd; its_visible = vis }

605 606
let its_of_ts ts priv =
  assert (ts.ts_def = None);
607 608 609
  let flg = mk_flg ~frz:priv ~exp:true ~lbl:priv ~fxd:true ~vis:true in
  mk_its ~ts ~nfr:priv ~priv ~mut:false ~frg:false ~mfld:[] ~regs:[]
    ~aflg:(List.map (fun _ -> flg) ts.ts_args) ~rflg:[] ~def:None
610

611
let create_rec_itysymbol id args =
612
  let ts = create_tysymbol id args None in
613 614 615
  let flg = mk_flg ~frz:true ~exp:true ~lbl:false ~fxd:true ~vis:true in
  mk_its ~ts ~nfr:false ~priv:false ~mut:false ~frg:false ~mfld:[] ~regs:[]
    ~aflg:(List.map (fun _ -> flg) ts.ts_args) ~rflg:[] ~def:None
616

617
let create_alias_itysymbol id args def =
618
  let ts = create_tysymbol id args (Some (ty_of_ity def)) in
619 620 621
  let mut, ity = match def.ity_node with (* ignore the top region *)
    | Ityreg r -> true, ity_app_pure r.reg_its r.reg_args r.reg_regs
    | _ -> false, def in
622
  let regs = Sreg.elements (ity_top_regs Sreg.empty ity) in
623 624 625 626
  let flg = mk_flg ~frz:true ~exp:true ~lbl:false ~fxd:true ~vis:true in
  mk_its ~ts ~nfr:false ~priv:false ~mut ~frg:false ~mfld:[] ~regs
    ~aflg:(List.map (fun _ -> flg) args)
    ~rflg:(List.map (fun _ -> flg) regs) ~def:(Some def)
627

628 629
let fields_of_invariant ftv flds invl =
  if invl = [] then Mpv.empty, flds else
630 631 632 633 634 635 636 637 638
  let fvs = Mpv.fold (fun v _ s -> Svs.add v.pv_vs s) flds Svs.empty in
  let check_invariant acc p =
    let ivs = t_freevars Mvs.empty p in
    let itv = t_ty_freevars Stv.empty p in
    if not (Mvs.set_submap ivs fvs) then Loc.error ?loc:p.t_loc
      (Decl.UnboundVar (fst (Mvs.choose (Mvs.set_diff ivs fvs))));
    if not (Stv.subset itv ftv) then Loc.error ?loc:p.t_loc
      (Ty.UnboundTypeVar (Stv.choose (Stv.diff itv ftv)));
    Mvs.set_union acc ivs in
639 640
  let fvs = List.fold_left check_invariant Mvs.empty invl in
  Mpv.partition (fun v _ -> Mvs.mem v.pv_vs fvs) flds
641 642

(*  private immutable:
643 644 645
      all arguments are frozen, exposed, liable, fixed, visible
      all reachable regions are frozen, otherwise we lose unicity [!]
      rexp, rlbl, rfxd, rvis are computed from the known fields
646 647
        => known regions cannot appear in the added fields
           in a refining type (no field aliases)
648 649 650
      cannot have its own invariant broken
      commits fields on construction and freezes them
        => not fragile and cannot have broken components
651 652

    private mutable:
653
      all arguments are frozen, exposed, liable, fixed, visible
654 655
      all regions frozen in the fields or reachable from
        the invariant are frozen, the rest are mutable
656 657
        => mutable regions cannot appear in the strengthened
           invariant in a refining type
658
      rexp, rlbl, rfxd, rvis are computed from the known fields
659 660
        => known regions cannot appear in the added fields
           in a refining type (no field aliases)
661 662 663 664 665
      cannot have its own invariant broken
      commits fields on construction and freezes the non-liables
      cannot have broken type parameters or broken liable fields
      however, a mutable region can break a non-liable field
        => fragile if has a fragile non-liable field
666 667

    nonfree immutable:
668 669 670 671
      all reachable arguments are frozen, otherwise we lose unicity
      all reachable regions are frozen, otherwise we lose unicity [!]
      aexp, albl, afxd, avis are computed from the known fields
      rexp, rlbl, rfxd, rvis are computed from the known fields
672 673 674
      cannot have its own invariant broken
      commits fields on construction and freezes them
        => not fragile and cannot have broken components
675

676
    nonfree mutable:
677 678
      afrz, aexp, albl, afxd, avis are computed from the known fields
      rfrz, rexp, rlbl, rfxd, rvis are computed from the known fields
679 680 681 682
      commits fields on construction but does not freeze them
      can be broken from a liable reachable non-frozen component
      can have broken compontents (reachable and non-frozen)
        => fragile if has a liable mutable field or a fragile field
683

684 685 686 687 688 689 690
    free mutable, free immutable non-recursive:
      afrz, aexp, albl, afxd, avis are computed from the known fields
      rfrz, rexp, rlbl, rfxd, rvis are computed from the known fields
      does not commit fields on construction, and can have a broken
        snapshot field (undetectable from regions)
        => fragile if has a fragile field
      can have broken compontents (reachable and non-frozen)
691

692 693 694 695 696 697 698 699
    recursive (free, immutable, no known fields, no regions):
      all arguments are frozen, exposed, non-liable, fixed, visible
      commits fields on construction and freezes them
        => not fragile and cannot have broken components
        (can treat it as free immutable, since all paths are frozen)

  [!] if this rule makes an exposed region frozen, we declare
      the type mutable to preserve mutability. *)
700

701
let create_plain_record_itysymbol ~priv ~mut id args flds invl =
702
  let sargs = Stv.of_list args in
703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
  let ts = create_tysymbol id args None in
  let fmut, ffix = Mpv.partition (fun _ m -> m) flds in
  let flbl, fout = fields_of_invariant sargs flds invl in
  let fvis = Mpv.filter (fun f _ -> not f.pv_ghost) flds in
  let collect fn = Mpv.fold (fun f _ a -> fn a f.pv_ity) in
  let dargs = collect ity_freevars flds Stv.empty in
  if not (Stv.subset dargs sargs) then raise
    (Ty.UnboundTypeVar (Stv.choose (Stv.diff dargs sargs)));
  let rfrz = if priv (* [!] compute rfrz ignoring mut *)
        then collect ity_rch_regs flbl
            (collect ity_frz_regs fout Sreg.empty)
        else collect ity_frz_regs flds Sreg.empty in
  let rexp = collect ity_exp_regs flds Sreg.empty in
  let rlbl = collect ity_exp_regs flbl Sreg.empty in
  let rfxd = collect ity_exp_regs ffix Sreg.empty in
  let rvis = collect ity_vis_regs fvis Sreg.empty in
  let rtop = collect ity_top_regs flds Sreg.empty in
  let regs = Mreg.keys rtop in
  let nfr = priv || invl <> [] in
722 723 724 725 726 727
  let mut = mut || not (Mpv.is_empty fmut) || (* [!] *)
      (nfr && not (Sreg.subset rexp rfrz)) in
  let frg = if nfr && not mut then false else
    if priv && mut then (* private mutable *)
      Mpv.exists (fun f _ -> ity_fragile f.pv_ity) fout
    else (* non-free mutable or free *)
Andrei Paskevich's avatar
Andrei Paskevich committed
728 729
      Mpv.exists (fun f m -> m || ity_liquid f.pv_ity) flbl ||
      Mpv.exists (fun f _ -> ity_fragile f.pv_ity) fout in
730 731 732 733 734 735 736 737 738 739 740 741 742
  let afrz = if priv then sargs else if nfr && not mut
                                then collect ity_rch_vars flds Stv.empty
                                else collect ity_frz_vars flds Stv.empty in
  let aexp = if priv then sargs else collect ity_exp_vars flds Stv.empty in
  let albl = if priv then sargs else collect ity_exp_vars flbl Stv.empty in
  let afxd = if priv then sargs else collect ity_exp_vars ffix Stv.empty in
  let avis = if priv then sargs else collect ity_vis_vars fvis Stv.empty in
  let arg_flag v = mk_flg ~frz:(Stv.mem v afrz) ~exp:(Stv.mem v aexp)
    ~lbl:(Stv.mem v albl) ~fxd:(Stv.mem v afxd) ~vis:(Stv.mem v avis) in
  let reg_flag r = mk_flg  ~frz:(Sreg.mem r rfrz) ~exp:(Sreg.mem r rexp)
    ~lbl:(Sreg.mem r rlbl) ~fxd:(Sreg.mem r rfxd) ~vis:(Sreg.mem r rvis) in
  mk_its ~ts ~nfr ~priv ~mut ~frg ~mfld:(Mpv.keys fmut) ~regs ~def:None
    ~aflg:(List.map arg_flag args) ~rflg:(List.map reg_flag regs)
743 744 745 746 747

let create_plain_variant_itysymbol id args flds =
  let flds = List.fold_left (fun acc flds ->
    Mpv.set_union acc (Mpv.map Util.ffalse flds)) Mpv.empty flds in
  create_plain_record_itysymbol ~priv:false ~mut:false id args flds []
748

749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764
(** 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)

765 766
let freeze_pv v s = ity_freeze s v.pv_ity

767 768 769 770 771
let pvs_of_vss pvs vss =
  Mvs.fold (fun vs _ s -> Spv.add (restore_pv vs) s) vss pvs

let t_freepvs pvs t = pvs_of_vss pvs (t_vars t)

772 773
(** builtin symbols *)

774 775 776 777
let its_int  = its_of_ts ts_int  true
let its_real = its_of_ts ts_real true
let its_bool = its_of_ts ts_bool true
let its_func = its_of_ts ts_func true
778

779 780 781
let ity_int  = ity_app its_int  [] []
let ity_real = ity_app its_real [] []
let ity_bool = ity_app its_bool [] []
782

783 784
let ity_func a b = ity_app its_func [a;b] []
let ity_pred a   = ity_app its_func [a;ity_bool] []
785

786
let its_tuple = Hint.memo 17 (fun n -> its_of_ts (ts_tuple n) false)
787

788
let ity_tuple tl = ity_app (its_tuple (List.length tl)) tl []
789

790 791
let ts_unit  = ts_tuple  0
let its_unit = its_tuple 0
792

793 794
let ty_unit  = ty_tuple  []
let ity_unit = ity_tuple []
795 796

(* exception symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
797

798 799 800 801 802 803 804
type mask =
  | MaskVisible
  | MaskTuple of mask list
  | MaskGhost

let mask_of_pv v = if v.pv_ghost then MaskGhost else MaskVisible

805
let rec mask_reduce mask = match mask with
806 807
  | MaskVisible | MaskGhost -> mask
  | MaskTuple l ->
808
      let l = List.map mask_reduce l in
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
      if List.for_all ((=) MaskVisible) l then MaskVisible else
      if List.for_all ((=) MaskGhost) l then MaskGhost else
      MaskTuple l

let rec mask_check exn ity mask = match ity.ity_node, mask with
  | _, (MaskVisible | MaskGhost) -> ()
  | Ityapp ({its_ts = s},tl,_), MaskTuple l
    when is_ts_tuple s && List.length tl = List.length l ->
      List.iter2 (mask_check exn) tl l
  | _ -> raise exn

let rec mask_ghost = function
  | MaskVisible -> false
  | MaskTuple l -> List.exists mask_ghost l
  | MaskGhost   -> true

let rec mask_union mask1 mask2 = match mask1, mask2 with
  | MaskVisible, _ | _, MaskGhost -> mask2
  | _, MaskVisible | MaskGhost, _ -> mask1
  | MaskTuple l1, MaskTuple l2 -> MaskTuple (List.map2 mask_union l1 l2)

let mask_equal : mask -> mask -> bool = (=)

let rec mask_sub mask1 mask2 = match mask1, mask2 with
  | MaskVisible, _ | _, MaskGhost -> true
834 835
  | MaskGhost, _ -> mask_reduce mask2 = MaskGhost
  | _, MaskVisible -> mask_reduce mask1 = MaskVisible
836 837 838 839
  | MaskTuple l1, MaskTuple l2 -> Lists.equal mask_sub l1 l2

let mask_spill mask1 mask2 = not (mask_sub mask1 mask2)

840 841 842
type xsymbol = {
  xs_name : ident;
  xs_ity  : ity; (* closed and pure *)
843
  xs_mask : mask;
844 845 846
}

let xs_equal : xsymbol -> xsymbol -> bool = (==)
847 848
let xs_hash xs = id_hash xs.xs_name
let xs_compare xs1 xs2 = id_compare xs1.xs_name xs2.xs_name
849

850
let create_xsymbol id ?(mask=MaskVisible) ity =
851
  if not (ity_closed ity) then Loc.errorm ?loc:id.pre_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
852
    "Exception %s has a polymorphic type" id.pre_name;
853
  if not ity.ity_imm then Loc.errorm ?loc:id.pre_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
854
    "The type of exception %s has mutable components" id.pre_name;
855
  mask_check (Invalid_argument "Ity.create_xsymbol") ity mask;
856
  { xs_name = id_register id; xs_ity = ity; xs_mask = mask_reduce mask }
857 858 859 860 861 862 863 864 865 866

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 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
867

868
exception IllegalSnapshot of ity
869 870
exception IllegalAlias of region
exception AssignPrivate of region
871
exception IllegalUpdate of pvsymbol * region
872
exception StaleVariable of pvsymbol * region
873
exception BadGhostWrite of pvsymbol * region