ity.mli 18.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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
open Ident
13
open Ty
14
open Term
15

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

type itysymbol = private {
19
  its_ts      : tysymbol;       (** logical type symbol *)
20
  its_nonfree : bool;           (** has no constructors *)
21 22
  its_private : bool;           (** private type *)
  its_mutable : bool;           (** mutable type *)
23
  its_fragile : bool;           (** breakable invariant *)
24
  its_mfields : pvsymbol list;  (** mutable record fields *)
25
  its_regions : region list;    (** shareable components *)
26 27
  its_arg_flg : its_flag list;  (** flags for type args *)
  its_reg_flg : its_flag list;  (** flags for regions *)
Clément Fumex's avatar
Clément Fumex committed
28
  its_def     : ity type_def;   (** type definition *)
29 30
}

31 32 33 34 35 36 37 38
and its_flag = private {
  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 *)
}

39 40
and ity = private {
  ity_node : ity_node;
41
  ity_pure : bool;
42 43 44 45
  ity_tag  : Weakhtbl.tag;
}

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

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

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

module Mits : Extmap.S with type key = itysymbol
module Sits : Extset.S with module M = Mits
module Hits : Exthtbl.S with type key = itysymbol
module Wits : Weakhtbl.S with type key = itysymbol

module Mity : Extmap.S with type key = ity
module Sity : Extset.S with module M = Mity
module Hity : Exthtbl.S with type key = ity
module Wity : Weakhtbl.S with type key = ity

76
module Mreg : Extmap.S with type key = region
77
module Sreg : Extset.S with module M = Mreg
78 79
module Hreg : Exthtbl.S with type key = region
module Wreg : Weakhtbl.S with type key = region
80

81 82 83 84 85
module Mpv  : Extmap.S with type key = pvsymbol
module Spv  : Extset.S with module M = Mpv
module Hpv  : Exthtbl.S with type key = pvsymbol
module Wpv  : Weakhtbl.S with type key = pvsymbol

86 87 88 89 90
val its_compare : itysymbol -> itysymbol -> int
val ity_compare : ity -> ity -> int
val reg_compare : region -> region -> int
val pv_compare  : pvsymbol -> pvsymbol -> int

91 92
val its_equal : itysymbol -> itysymbol -> bool
val ity_equal : ity -> ity -> bool
93
val reg_equal : region -> region -> bool
94
val pv_equal  : pvsymbol -> pvsymbol -> bool
95 96 97

val its_hash : itysymbol -> int
val ity_hash : ity -> int
98
val reg_hash : region -> int
99
val pv_hash  : pvsymbol -> int
100 101 102 103

exception DuplicateRegion of region
exception UnboundRegion of region

104
(** creation of a type symbol in programs *)
105

106 107
val create_plain_record_itysymbol : priv:bool -> mut:bool ->
  preid -> tvsymbol list -> bool Mpv.t -> term list -> itysymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
108
(** [create_plain_record_itysymbol ~priv ~mut id args fields invl] creates
109 110 111 112
    a new type symbol for a non-recursive record type, possibly private
    or mutable. Every known field is represented by a [pvsymbol] mapped
    to its mutability status in [fields]. Variables corresponding to
    mutable fields are stored in the created type symbol and used in
113 114
    effects. The [priv] flag should be set to [true] for private records.
    The [mut] flag should be set to [true] to mark the new type as mutable
Andrei Paskevich's avatar
Andrei Paskevich committed
115
    even if it does not have known mutable fields. The [invl] parameter
116 117 118 119 120 121 122 123 124 125 126
    contains the list of invariant formulas that may only depend on
    variables from [fields]. Abstract types are considered to be private
    immutable records with no fields. *)

val create_plain_variant_itysymbol :
  preid -> tvsymbol list -> Spv.t list -> itysymbol
(** [create_plain_variant_itysymbol id args fields] creates a new type
    symbol for a non-recursive algebraic type. *)

val create_rec_itysymbol : preid -> tvsymbol list -> itysymbol
(** [create_rec_itysymbol id args] creates a new type symbol for
127
    a recursively defined type. *)
128

129 130 131
val create_alias_itysymbol : preid -> tvsymbol list -> ity -> itysymbol
(** [create_alias_itysymbol id args def] creates a new type alias. *)

132 133 134
val create_range_itysymbol : preid -> Number.int_range -> itysymbol
(** [create_range_itysymbol id r] creates a new range type. *)

MARCHE Claude's avatar
MARCHE Claude committed
135 136 137
val create_float_itysymbol : preid -> Number.float_format -> itysymbol
(** [create_float_itysymbol id f] creates a new float type. *)

138
val restore_its : tysymbol -> itysymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
139
(** raises [Not_found] if the argument is not a [its_ts] *)
140

141
(* {2 Basic properties} *)
142

143 144 145 146 147
val its_pure : itysymbol -> bool
(** a pure type symbol is immutable and has no mutable components *)

val ity_closed : ity -> bool
(** a closed type contains no type variables *)
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149 150 151
val ity_fragile : ity -> bool
(** a fragile type may contain a component with a broken invariant *)

Andrei Paskevich's avatar
Andrei Paskevich committed
152
(** {2 Type constructors} *)
153

Andrei Paskevich's avatar
Andrei Paskevich committed
154 155
exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
156

157 158 159 160
val create_region : preid -> itysymbol -> ity list -> ity list -> region
(** [create_region id s tl rl] creates a fresh region.
    Type symbol [s] must be a mutable record or an alias for one.
    If [rl] is empty, fresh subregions are created when needed. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
161

162 163 164 165 166
val ity_app : itysymbol -> ity list -> ity list -> ity
(** [ity_app s tl rl] creates
    - an [Ityapp] type, if [s] is immutable, or
    - an [Ityreg] type on top of a fresh region, otherwise.
    If [rl] is empty, fresh subregions are created when needed. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
167

168 169 170
val ity_app_pure : itysymbol -> ity list -> ity list -> ity
(** [ity_app s tl rl] creates an [Ityapp] type.
    If [rl] is empty, pure snapshots are substituted when needed. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
171

172
val ity_reg : region -> ity
173

174
val ity_var : tvsymbol -> ity
175

176
val ity_purify : ity -> ity
177
(** replaces regions with pure snapshots *)
178 179

val ity_of_ty : ty -> ity
180
(** fresh regions are created when needed.
181
    Raises [Invalid_argument] for any non-its tysymbol. *)
182

183
val ity_of_ty_pure : ty -> ity
184
(** pure snapshots are substituted when needed.
185 186 187
    Raises [Invalid_argument] for any non-its tysymbol. *)

val ty_of_ity : ity -> ty
188

189 190
(** {2 Generic traversal functions} *)

191 192
val ity_fold : ('a -> ity -> 'a) -> 'a -> ity -> 'a
val reg_fold : ('a -> ity -> 'a) -> 'a -> region -> 'a
193 194 195

(** {2 Traversal functions on type symbols} *)

196
val ity_s_fold : ('a -> itysymbol -> 'a) -> 'a -> ity -> 'a
197
val reg_s_fold : ('a -> itysymbol -> 'a) -> 'a -> region -> 'a
198

199
(** {2 Traversal functions on type variables} *)
200 201

val ity_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ity -> 'a
202
val reg_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> region -> 'a
203

204
val ity_freevars : Stv.t -> ity -> Stv.t
205
val reg_freevars : Stv.t -> region -> Stv.t
206

207
val ity_v_occurs : tvsymbol -> ity -> bool
208
val reg_v_occurs : tvsymbol -> region -> bool
209

210 211 212 213 214 215 216 217
(** {2 Traversal functions on top regions} *)

val ity_r_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_r_fold : ('a -> region -> 'a) -> 'a -> region -> 'a

val ity_freeregs : Sreg.t -> ity -> Sreg.t
val reg_freeregs : Sreg.t -> region -> Sreg.t

218
val ity_r_occurs : region -> ity -> bool
219 220
val reg_r_occurs : region -> region -> bool

Andrei Paskevich's avatar
Andrei Paskevich committed
221
(** {2 Traversal functions on exposed and reachable regions} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
222 223 224

val ity_exp_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_exp_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
225 226 227

val ity_rch_fold : ('a -> region -> 'a) -> 'a -> ity -> 'a
val reg_rch_fold : ('a -> region -> 'a) -> 'a -> region -> 'a
228

229 230
val ity_r_reachable : region -> ity -> bool
val reg_r_reachable : region -> region -> bool
231

232 233
val ity_r_stale : Sreg.t -> Sreg.t -> ity -> bool
val reg_r_stale : Sreg.t -> Sreg.t -> region -> bool
234 235 236 237 238 239

(** {2 Built-in types} *)

val ts_unit : tysymbol (** the same as [Ty.ts_tuple 0] *)
val ty_unit : ty

240
val its_int  : itysymbol
241
val its_real : itysymbol
242 243
val its_bool : itysymbol
val its_unit : itysymbol
244
val its_func : itysymbol
245 246

val ity_int  : ity
247
val ity_real : ity
248 249
val ity_bool : ity
val ity_unit : ity
250 251
val ity_func : ity -> ity -> ity
val ity_pred : ity -> ity (* ity_pred 'a == ity_func 'a ity_bool *)
252

253 254 255
val its_tuple : int -> itysymbol
val ity_tuple : ity list -> ity

256
(** {2 Type matching and instantiation} *)
257

258
type ity_subst = private {
259 260
  isb_var : ity Mtv.t;
  isb_reg : ity Mreg.t;
261 262 263 264
}

exception TypeMismatch of ity * ity * ity_subst

265
val isb_empty : ity_subst
266

267
val ity_match : ity_subst -> ity -> ity -> ity_subst
268
val reg_match : ity_subst -> region -> ity -> ity_subst
269

270
val its_match_args : itysymbol -> ity list -> ity_subst
271
val its_match_regs : itysymbol -> ity list -> ity list -> ity_subst
272

273 274
val ity_freeze : ity_subst -> ity -> ity_subst (* self-match *)
val reg_freeze : ity_subst -> region -> ity_subst (* self-match *)
275 276

val ity_equal_check : ity -> ity -> unit
277
val reg_equal_check : region -> region -> unit
278

279
val ity_full_inst : ity_subst -> ity -> ity
280
val reg_full_inst : ity_subst -> region -> ity
281

Andrei Paskevich's avatar
Andrei Paskevich committed
282 283 284 285 286 287 288
(** {2 Program variables} *)

val create_pvsymbol : preid -> ?ghost:bool -> ity -> pvsymbol

val restore_pv : vsymbol -> pvsymbol
(** raises [Not_found] if the argument is not a [pv_vs] *)

289 290 291 292
val t_freepvs : Spv.t -> term -> Spv.t
(** raises [Not_found] if the term contains a free variable
    which is not a [pv_vs] *)

293
val pvs_of_vss : Spv.t -> 'a Mvs.t -> Spv.t
294

295 296
(** {2 Exception symbols} *)

297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
type mask =
  | MaskVisible
  | MaskTuple of mask list
  | MaskGhost

val mask_ghost : mask -> bool

val mask_of_pv : pvsymbol -> mask

val mask_union : mask -> mask -> mask

val mask_equal : mask -> mask -> bool

val mask_spill : mask -> mask -> bool

312 313 314
type xsymbol = private {
  xs_name : ident;
  xs_ity  : ity; (** closed and immutable *)
315
  xs_mask : mask;
316 317
}

318 319
module Mxs : Extmap.S with type key = xsymbol
module Sxs : Extset.S with module M = Mxs
320

321
val xs_compare : xsymbol -> xsymbol -> int
322
val xs_equal : xsymbol -> xsymbol -> bool
323
val xs_hash : xsymbol -> int
324

325
val create_xsymbol : preid -> ?mask:mask -> ity -> xsymbol
326 327 328

(** {2 Effects} *)

329
exception IllegalSnapshot of ity
330 331
exception IllegalAlias of region
exception AssignPrivate of region
332 333
exception AssignSnapshot of ity
exception WriteImmutable of region * pvsymbol
334
exception IllegalUpdate of pvsymbol * region
335 336 337
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
338
exception IllegalAssign of region * region * region
339
exception ImpureVariable of tvsymbol * ity
340 341
exception GhostDivergence

342 343 344
(* termination status *)
type oneway =
  | Total
345 346 347
  | Partial
  | Diverges

348 349 350
val total : oneway -> bool
val partial : oneway -> bool
val diverges : oneway -> bool
351

352
type effect = private {
353 354 355 356 357 358 359 360 361
  eff_reads  : Spv.t;         (* known variables *)
  eff_writes : Spv.t Mreg.t;  (* writes to fields *)
  eff_taints : Sreg.t;        (* ghost code writes *)
  eff_covers : Sreg.t;        (* surviving writes *)
  eff_resets : Sreg.t;        (* locked by covers *)
  eff_raises : Sxs.t;         (* raised exceptions *)
  eff_spoils : Stv.t;         (* immutable tyvars *)
  eff_oneway : oneway;        (* non-termination *)
  eff_ghost  : bool;          (* ghost status *)
362 363 364 365
}

val eff_empty : effect

366 367
val eff_equal : effect -> effect -> bool
val eff_pure : effect -> bool
368

369 370 371
val eff_read : Spv.t -> effect
val eff_write : Spv.t -> Spv.t Mreg.t -> effect (* drops writes outside reads *)
val eff_assign : (pvsymbol * pvsymbol * pvsymbol) list -> effect (* r,field,v *)
372

373 374 375
val eff_read_pre  : Spv.t -> effect -> effect (* no stale-variable check *)
val eff_read_post : effect -> Spv.t -> effect (* checks for stale variables *)
val eff_bind      : Spv.t -> effect -> effect (* removes variables from reads *)
376

377 378 379 380
val eff_read_single      : pvsymbol -> effect
val eff_read_single_pre  : pvsymbol -> effect -> effect
val eff_read_single_post : effect -> pvsymbol -> effect
val eff_bind_single      : pvsymbol -> effect -> effect
381

382 383
val eff_reset : effect -> Sreg.t -> effect    (* confine to an empty cover *)
val eff_reset_overwritten : effect -> effect  (* confine regions under writes *)
Andrei Paskevich's avatar
Andrei Paskevich committed
384

385 386
val eff_raise : effect -> xsymbol -> effect
val eff_catch : effect -> xsymbol -> effect
Andrei Paskevich's avatar
Andrei Paskevich committed
387

388 389
val eff_spoil : effect -> ity -> effect

390 391 392 393
val eff_partial : effect -> effect                      (* forbidden if ghost *)
val eff_diverge : effect -> effect                      (* forbidden if ghost *)
val eff_ghostify : bool -> effect -> effect (* forbidden if fails or diverges *)
val eff_ghostify_weak : bool -> effect -> effect     (* only if has no effect *)
394

395 396
val eff_union_seq : effect -> effect -> effect  (* checks for stale variables *)
val eff_union_par : effect -> effect -> effect  (* no stale-variable check *)
397

398 399
val mask_adjust : effect -> ity -> mask -> mask

400 401
val eff_escape : effect -> ity -> Sity.t

402
(** {2 Computation types (higher-order types with effects)} *)
403

404 405
type pre = term   (** precondition: pre_fmla *)
type post = term  (** postcondition: eps result . post_fmla *)
406 407

val open_post : post -> vsymbol * term
408
val open_post_with : term -> post -> term
409
val clone_post_result : post -> preid
410 411

val create_post : vsymbol -> term -> post
412

Andrei Paskevich's avatar
Andrei Paskevich committed
413
val annot_attr : attribute
414
val break_attr : attribute
415

416 417 418 419
type cty = private {
  cty_args   : pvsymbol list;
  cty_pre    : pre list;
  cty_post   : post list;
420
  cty_xpost  : post list Mxs.t;
421
  cty_oldies : pvsymbol Mpv.t;
422 423
  cty_effect : effect;
  cty_result : ity;
424
  cty_mask   : mask;
425
  cty_freeze : ity_subst;
426 427
}

Andrei Paskevich's avatar
Andrei Paskevich committed
428 429
val create_cty : ?mask:mask -> pvsymbol list ->
  pre list -> post list -> post list Mxs.t ->
430
  pvsymbol Mpv.t -> effect -> ity -> cty
431 432
(** [create_cty ?mask ?defensive args pre post xpost oldies effect result]
    creates a new cty. [post] and [mask] must be consistent with [result].
433
    The [cty_xpost] field does not have to cover all raised exceptions.
434 435 436
    [cty_effect.eff_reads] is completed wrt the specification and [args].
    [cty_freeze] freezes every unbound pvsymbol in [cty_effect.eff_reads].
    All effects on regions outside [cty_effect.eff_reads] are removed.
437
    Fresh regions in [result] are reset. Every type variable in [pre],
438 439
    [post], and [xpost] must come from [cty_reads], [args] or [result].
    [oldies] maps ghost pure snapshots of the parameters and external
440
    reads to the original pvsymbols: these snapshots are removed from
Andrei Paskevich's avatar
Andrei Paskevich committed
441
    [cty_effect.eff_reads] and replaced with the originals. *)
442

Andrei Paskevich's avatar
Andrei Paskevich committed
443 444 445 446 447 448 449
val create_cty_defensive : ?mask:mask -> pvsymbol list ->
  pre list -> post list -> post list Mxs.t ->
  pvsymbol Mpv.t -> effect -> ity -> cty
(** same as [create_cty], except that type variables in the result
    and exceptional results are spoiled and fresh regions in the
    result and exceptional results are reset. *)

450 451
val cty_apply : cty -> pvsymbol list -> ity list -> ity -> cty
(** [cty_apply cty pvl rest res] instantiates [cty] up to the types in
452
    [pvl], [rest], and [res], then applies it to the arguments in [pvl],
453 454 455
    and returns the computation type of the result, [rest -> res],
    with every type variable and region in [pvl] being frozen. *)

456 457 458 459
val cty_tuple : pvsymbol list -> cty
(** [cty_tuple pvl] returns a nullary tuple-valued cty with
    an appropriate [cty_mask]. *)

460 461 462 463 464
val cty_exec : cty -> cty
(** [cty_exec cty] converts a cty of a partial application into
    a cty of a fully applied application, returning a mapping.
    The original cty must be effectless. *)

465 466 467 468
val cty_exec_post : cty -> post list
(** [cty_exec_post cty] returns a post-condition appropriate
    for use with local let-functions in VC generation. *)

469 470
val cty_ghost : cty -> bool
(** [cty_ghost cty] returns [cty.cty_effect.eff_ghost] *)
471

472 473 474 475
val cty_pure : cty -> bool
(** [cty_pure cty] verifies that [cty] has no side effects
    except allocations. *)

476 477
val cty_ghostify : bool -> cty -> cty
(** [cty_ghostify ghost cty] ghostifies the effect of [cty]. *)
478

479 480
val cty_reads : cty -> Spv.t
(** [cty_reads cty] returns the set of external dependencies of [cty]. *)
481

482 483 484 485 486 487 488
val cty_read_pre : Spv.t -> cty -> cty
(** [cty_read_pre pvs cty] adds [pvs] to [cty.cty_effect.eff_reads].
    This function performs capture: if some variables in [pvs] occur
    in [cty.cty_args], they are not frozen. *)

val cty_read_post : cty -> Spv.t -> cty
(** [cty_read_post cty pvs] adds [pvs] to [cty.cty_effect.eff_reads].
489 490
    This function performs capture: if some variables in [pvs] occur
    in [cty.cty_args], they are not frozen. *)
491

492 493
val cty_add_pre : pre list -> cty -> cty
(** [cty_add_pre fl cty] appends pre-conditions in [fl] to [cty.cty_pre].
494 495
    This function performs capture: the formulas in [fl] may refer to
    the variables in [cty.cty_args]. Only the new external dependencies
496
    in [fl] are added to [cty.cty_effect.eff_reads] and frozen. *)
497 498 499 500 501

val cty_add_post : cty -> post list -> cty
(** [cty_add_post cty fl] appends post-conditions in [fl] to [cty.cty_post].
    This function performs capture: the formulas in [fl] may refer to the
    variables in [cty.cty_args]. Only the new external dependencies in [fl]
502
    are added to [cty.cty_effect.eff_reads] and frozen. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
503 504 505 506 507

(** {2 Pretty-printing} *)

val forget_reg : region -> unit   (* flush id_unique for a region *)
val forget_pv  : pvsymbol -> unit (* flush for a program variable *)
508
val forget_xs  : xsymbol -> unit  (* flush for a local exception *)
509
val forget_cty : cty -> unit      (* forget arguments and oldies *)
Andrei Paskevich's avatar
Andrei Paskevich committed
510

Andrei Paskevich's avatar
Andrei Paskevich committed
511 512 513 514 515 516 517 518 519
val print_its : Format.formatter -> itysymbol -> unit (* type symbol *)
val print_reg : Format.formatter -> region -> unit    (* region *)
val print_ity : Format.formatter -> ity -> unit       (* individual type *)
val print_ity_full : Format.formatter -> ity -> unit  (* type with regions *)

val print_xs   : Format.formatter -> xsymbol -> unit  (* exception symbol *)
val print_pv   : Format.formatter -> pvsymbol -> unit (* program variable *)
val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
val print_cty  : Format.formatter -> cty -> unit      (* computation type *)
Andrei Paskevich's avatar
Andrei Paskevich committed
520

521
val print_spec :
522
  pvsymbol list -> pre list -> post list -> post list Mxs.t -> pvsymbol Mpv.t
523
    -> effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)