term.mli 16.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13
(** Terms and Formulas *)

14
open Ident
15
open Ty
16

17 18
(** {1 Terms and Formulas} *)

Simon Cruanes's avatar
Simon Cruanes committed
19
(** {2 Variable symbols} *)
20 21

type vsymbol = private {
22
  vs_name : ident;
23
  vs_ty   : ty;
24 25
}

26 27 28
module Mvs : Extmap.S with type key = vsymbol
module Svs : Extset.S with module M = Mvs
module Hvs : Exthtbl.S with type key = vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
29
module Wvs : Weakhtbl.S with type key = vsymbol
30

Andrei Paskevich's avatar
Andrei Paskevich committed
31
val vs_compare : vsymbol -> vsymbol -> int
32
val vs_equal : vsymbol -> vsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
33
val vs_hash : vsymbol -> int
34

35
val create_vsymbol : preid -> ty -> vsymbol
36

Simon Cruanes's avatar
Simon Cruanes committed
37
(** {2 Function and predicate symbols} *)
38

39 40 41
type lsymbol = private {
  ls_name   : ident;
  ls_args   : ty list;
42
  ls_value  : ty option;
43
  ls_opaque : Stv.t;
44
  ls_constr : int;
45 46
}

47 48 49
module Mls : Extmap.S with type key = lsymbol
module Sls : Extset.S with module M = Mls
module Hls : Exthtbl.S with type key = lsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
50
module Wls : Weakhtbl.S with type key = lsymbol
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52
val ls_compare : lsymbol -> lsymbol -> int
53
val ls_equal : lsymbol -> lsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
54
val ls_hash : lsymbol -> int
55

56 57 58 59 60 61 62
val create_lsymbol :
  ?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty option -> lsymbol

val create_fsymbol :
  ?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty -> lsymbol

val create_psymbol :
63
  ?opaque:Stv.t -> preid -> ty list -> lsymbol
64

65 66
val ls_ty_freevars : lsymbol -> Stv.t

Simon Cruanes's avatar
Simon Cruanes committed
67
(** {2 Exceptions} *)
68

69
exception EmptyCase
70
exception DuplicateVar of vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
71
exception UncoveredVar of vsymbol
72
exception BadArity of lsymbol * int
73 74
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
75
exception ConstructorExpected of lsymbol
Clément Fumex's avatar
Clément Fumex committed
76
exception InvalidLiteralType of ty
77

Simon Cruanes's avatar
Simon Cruanes committed
78
(** {2 Patterns} *)
79 80 81

type pattern = private {
  pat_node : pattern_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
82
  pat_vars : Svs.t;
83
  pat_ty   : ty;
84 85 86 87 88
}

and pattern_node = private
  | Pwild
  | Pvar of vsymbol
89
  | Papp of lsymbol * pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
90
  | Por  of pattern * pattern
91
  | Pas  of pattern * vsymbol
92

MARCHE Claude's avatar
MARCHE Claude committed
93
(** Smart constructors for patterns *)
94 95 96

val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
97
val pat_app : lsymbol -> pattern list -> ty -> pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
98
val pat_or  : pattern -> pattern -> pattern
99 100
val pat_as  : pattern -> vsymbol -> pattern

MARCHE Claude's avatar
MARCHE Claude committed
101
(** Generic traversal functions *)
102

103 104
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
105 106
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
107

MARCHE Claude's avatar
MARCHE Claude committed
108
(** {2 Terms and Formulas} *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
109

110
type quant =
111 112
  | Tforall
  | Texists
113

114
type binop =
115 116 117 118
  | Tand
  | Tor
  | Timplies
  | Tiff
119

120
type term = private {
121
  t_node  : term_node;
122
  t_ty    : ty option;
123
  t_label : Slab.t;
124
  t_loc   : Loc.position option;
125 126 127 128
}

and term_node = private
  | Tvar of vsymbol
129
  | Tconst of Number.constant
130
  | Tapp of lsymbol * term list
131
  | Tif of term * term * term
132
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
133
  | Tcase of term * term_branch list
134 135 136 137 138 139 140
  | Teps of term_bound
  | Tquant of quant * term_quant
  | Tbinop of binop * term * term
  | Tnot of term
  | Ttrue
  | Tfalse

141
and term_bound
142
and term_branch
143
and term_quant
144

145
and trigger = term list list
146

147 148 149
module Mterm : Extmap.S with type key = term
module Sterm : Extset.S with module M = Mterm
module Hterm : Exthtbl.S with type key = term
Andrei Paskevich's avatar
Andrei Paskevich committed
150

Piotr Trojanek's avatar
Piotr Trojanek committed
151
(** {2 Term equality modulo alpha-equivalence and location} *)
MARCHE Claude's avatar
MARCHE Claude committed
152

Andrei Paskevich's avatar
Andrei Paskevich committed
153
val t_compare : term -> term -> int
154
val t_equal : term -> term -> bool
155
val t_hash : term -> int
156 157
(* Equality modulo labels and triggers *)
val t_equal_nt_nl : term -> term -> bool
158

MARCHE Claude's avatar
MARCHE Claude committed
159
(** {2 Bindings} *)
160

161 162 163 164
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
165
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
166 167 168 169 170

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
171
val t_open_quant : term_quant -> vsymbol list * trigger * term
172 173 174 175 176 177 178 179 180

(** open bindings with optimized closing callbacks *)

val t_open_bound_cb :
  term_bound -> vsymbol * term * (vsymbol -> term -> term_bound)

val t_open_branch_cb :
  term_branch -> pattern * term * (pattern -> term -> term_branch)

181 182 183
val t_open_quant_cb :
  term_quant -> vsymbol list * trigger * term *
              (vsymbol list -> trigger -> term -> term_quant)
184

MARCHE Claude's avatar
MARCHE Claude committed
185
(** {2 Type checking} *)
186 187 188 189 190

exception TermExpected of term
exception FmlaExpected of term

val t_type : term -> ty
191 192
(** [t_type t] checks that [t] is value-typed and returns its type *)

193
val t_prop : term -> term
194 195 196 197 198
(** [t_prop t] checks that [t] is prop-typed and returns [t] *)

val t_ty_check : term -> ty option -> unit
(** [t_ty_check t ty] checks that the type of [t] is [ty] *)

MARCHE Claude's avatar
MARCHE Claude committed
199
(** {2 Smart constructors for terms and formulas} *)
200

201 202
val t_app  : lsymbol -> term list -> ty option -> term
val fs_app : lsymbol -> term list -> ty -> term
203
val ps_app : lsymbol -> term list -> term
204 205

val t_app_infer : lsymbol -> term list -> term
206 207
val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
208

209
val t_var : vsymbol -> term
Clément Fumex's avatar
Clément Fumex committed
210
val t_const : Number.constant -> ty -> term
211
val t_if : term -> term -> term -> term
212 213
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
214 215 216 217 218 219 220 221 222 223 224 225
val t_eps : term_bound -> term
val t_quant : quant -> term_quant -> term
val t_forall : term_quant -> term
val t_exists : term_quant -> term
val t_binary : binop -> term -> term -> term
val t_and : term -> term -> term
val t_or : term -> term -> term
val t_implies : term -> term -> term
val t_iff : term -> term -> term
val t_not : term -> term
val t_true : term
val t_false : term
226

Andrei Paskevich's avatar
Andrei Paskevich committed
227 228 229 230
val t_nat_const : int -> term
(** [t_nat_const n] builds the constant integer term [n],
    n must be non-negative *)

231 232 233 234
val asym_label : label
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term

235
val t_let_close : vsymbol -> term -> term -> term
236
val t_eps_close : vsymbol -> term -> term
237
val t_case_close : term -> (pattern * term) list -> term
238 239 240
val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close : vsymbol list -> trigger -> term -> term
val t_exists_close : vsymbol list -> trigger -> term -> term
241

242
val t_label : ?loc:Loc.position -> Slab.t -> term -> term
243
val t_label_add : label -> term -> term
244
val t_label_remove : label -> term -> term
245
val t_label_copy : term -> term -> term
246

MARCHE Claude's avatar
MARCHE Claude committed
247
(** Constructors with propositional simplification *)
248

249 250
val keep_on_simp_label : label

251
val t_if_simp : term -> term -> term -> term
252
val t_let_simp : term -> term_bound -> term
253
val t_case_simp : term -> term_branch list -> term
254 255 256 257 258 259 260 261 262 263 264
val t_quant_simp : quant -> term_quant -> term
val t_forall_simp : term_quant -> term
val t_exists_simp : term_quant -> term
val t_binary_simp : binop -> term -> term -> term
val t_and_simp : term -> term -> term
val t_and_simp_l : term list -> term
val t_or_simp : term -> term -> term
val t_or_simp_l : term list -> term
val t_implies_simp : term -> term -> term
val t_iff_simp : term -> term -> term
val t_not_simp : term -> term
265

266 267 268 269 270
val t_and_asym_simp : term -> term -> term
val t_and_asym_simp_l : term list -> term
val t_or_asym_simp : term -> term -> term
val t_or_asym_simp_l : term list -> term

271
val t_let_close_simp : vsymbol -> term -> term -> term
272
val t_case_close_simp : term -> (pattern * term) list -> term
273 274 275
val t_quant_close_simp : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close_simp : vsymbol list -> trigger -> term -> term
val t_exists_close_simp : vsymbol list -> trigger -> term -> term
276

277
val t_forall_close_merge : vsymbol list -> term -> term
278 279
val t_exists_close_merge : vsymbol list -> term -> term
(** [t_forall_close_merge vs f] puts a universal quantifier over [f];
280 281
    merges variable lists if [f] is already universally quantified;
    reuses triggers of [f], if any, otherwise puts no triggers. *)
282

MARCHE Claude's avatar
MARCHE Claude committed
283
(** {2 Built-in symbols} *)
284

MARCHE Claude's avatar
MARCHE Claude committed
285 286
val ps_equ : lsymbol
(** equality predicate *)
287

288 289
val t_equ : term -> term -> term
val t_neq : term -> term -> term
290

291 292
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
293

294 295 296 297 298
val fs_bool_true  : lsymbol
val fs_bool_false : lsymbol

val t_bool_true  : term
val t_bool_false : term
299

300 301
val fs_tuple : int -> lsymbol   (* n-tuple *)
val t_tuple : term list -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
302

303
val is_fs_tuple : lsymbol -> bool
304
val is_fs_tuple_id : ident -> int option
Andrei Paskevich's avatar
Andrei Paskevich committed
305

306
val fs_func_app : lsymbol  (* higher-order application symbol *)
307

308 309
val t_func_app : term -> term -> term  (* value-typed application *)
val t_pred_app : term -> term -> term  (* prop-typed application *)
310

311 312
val t_func_app_l : term -> term list -> term  (* value-typed application *)
val t_pred_app_l : term -> term list -> term  (* prop-typed application *)
313

314 315
(** {2 Lambda-term manipulation} *)

316
val t_lambda : vsymbol list -> trigger -> term -> term
MARCHE Claude's avatar
MARCHE Claude committed
317 318
(** [t_lambda vl tr e] produces a term [eps f. (forall vl [tr]. f\@vl = e)]
    or [eps f. (forall vl [tr]. f\@vl = True <-> e] if [e] is prop-typed.
319 320 321 322 323 324 325 326 327 328 329 330 331
    If [vl] is empty, [t_lambda] returns [e] or [if e then True else False],
    if [e] is prop-typed. *)

val t_open_lambda : term -> vsymbol list * trigger * term
(** [t_open_lambda t] returns a triple [(vl,tr,e)], such that [t] is equal
    to [t_lambda vl tr e]. If [t] is not a lambda-term, then [vl] is empty,
    [tr] is empty, and [e] is [t]. The term [e] may be prop-typed. *)

val t_open_lambda_cb : term -> vsymbol list * trigger * term *
                             (vsymbol list -> trigger -> term -> term)
(** the same as [t_open_lambda] but returns additionally an instance of
    [t_lambda] that restores the original term if applied to the physically
    same arguments. Should be used in mapping functions. *)
332 333

val t_is_lambda : term -> bool
334 335 336 337 338
(** [t_is_lambda t] returns [true] if [t] is a lambda-term. Do not use
    this function if you call [t_open_lambda] afterwards. Internally,
    [t_is_lambda] opens binders itself, so you will pay twice the price.
    It is better to optimistically call [t_open_lambda] on any [Teps],
    and handle the generic case if an empty argument list is returned. *)
339 340

val t_closure : lsymbol -> ty list -> ty option -> term
341 342 343 344
(** [t_closure ls tyl oty] returns a type-instantiated lambda-term
    [\xx:tyl.(ls xx : oty)], or [ls : oty] if [ls] is a constant.
    The length of [tyl] must be equal to that of [ls.ls_args], and
    [oty] should be [None] if and only if [ls] is a predicate symbol. *)
345 346

val t_app_partial : lsymbol -> term list -> ty list -> ty option -> term
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
(** [t_app_partial ls tl tyl oty] produces a closure of [ls] and applies
    it to [tl] using [t_func_app]. The type signature of the closure is
    obtained by prepending the list of types of terms in [tl] to [tyl].
    The resulting list must have the same length as [ls.ls_args], and
    [oty] should be [None] if and only if [ls] is a predicate symbol.
    If the symbol is fully applied ([tyl] is empty), the [Tapp] term
    is returned. Otherwise, no beta-reduction is performed, in order
    to preserve the closure. *)

val t_func_app_beta : term -> term -> term
(** [t_func_app_beta f a] applies [f] to [a] performing beta-reduction
    when [f] is a lambda-term. Always returns a value-typed term, even
    if [f] is a lambda-term built on top of a formula. *)

val t_pred_app_beta : term -> term -> term
(** [t_pred_app_beta f a] applies [f] to [a] performing beta-reduction
    when [f] is a lambda-term. Always returns a formula, even if [f] is
    a lambda-term built on top of a bool-typed term. *)

val t_func_app_beta_l : term -> term list -> term
val t_pred_app_beta_l : term -> term list -> term
368

369
(** {2 Term library} *)
370

371
(** One-level (non-recursive) term traversal *)
372

373 374 375
val t_map : (term -> term) -> term -> term
val t_fold : ('a -> term -> 'a) -> 'a -> term -> 'a
val t_map_fold : ('a -> term -> 'a * term) -> 'a -> term -> 'a * term
376

377 378
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
379

380
(** Special maps *)
381

382 383
val t_map_simp : (term -> term) -> term -> term
(** [t_map_simp] reconstructs the term using simplification constructors *)
384

385 386
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
(** [t_map_sign] passes a polarity parameter, unfolds if-then-else and iff *)
387

388 389
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
(** [t_map_cont] is [t_map] in continuation-passing style *)
390

391
val list_map_cont: (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
392

393
(** Trigger traversal *)
394

395 396 397 398
val tr_equal : trigger -> trigger -> bool
val tr_map : (term -> term) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
399

400
(** Traversal with separate functions for value-typed and prop-typed terms *)
401

402
module TermTF : sig
403

404 405 406 407 408 409 410
  val t_select : (term -> 'a) -> (term -> 'a) -> term -> 'a
  (** [t_select fnT fnF t] is [fnT t] if [t] is a value, [fnF t] otherwise *)

  val t_selecti : ('a -> term -> 'b) -> ('a -> term -> 'b) -> 'a -> term -> 'b
  (** [t_selecti fnT fnF acc t] is [t_select (fnT acc) (fnF acc) t] *)

  val t_map : (term -> term) -> (term -> term) -> term -> term
411
  (** [t_map fnT fnF = t_map (t_select fnT fnF)] *)
412 413

  val t_fold : ('a -> term -> 'a) -> ('a -> term -> 'a) -> 'a -> term -> 'a
414
  (** [t_fold fnT fnF = t_fold (t_selecti fnT fnF)] *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415 416

  val t_map_fold : ('a -> term -> 'a * term) ->
417 418 419 420 421 422 423
    ('a -> term -> 'a * term) -> 'a -> term -> 'a * term

  val t_all : (term -> bool) -> (term -> bool) -> term -> bool
  val t_any : (term -> bool) -> (term -> bool) -> term -> bool

  val t_map_simp : (term -> term) -> (term -> term) -> term -> term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
  val t_map_sign : (bool -> term -> term) ->
425 426
    (bool -> term -> term) -> bool -> term -> term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
  val t_map_cont : ((term -> 'a) -> term -> 'a) ->
428 429 430 431 432
    ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a

  val tr_map : (term -> term) -> (term -> term) -> trigger -> trigger

  val tr_fold : ('a -> term -> 'a) -> ('a -> term -> 'a) -> 'a -> trigger -> 'a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433 434

  val tr_map_fold : ('a -> term -> 'a * term) ->
435
    ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
436
end
437

MARCHE Claude's avatar
MARCHE Claude committed
438
(** {2 Map/fold over free variables} *)
439 440 441 442 443 444

val t_v_map : (vsymbol -> term) -> term -> term
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool

445 446 447 448
val t_v_count : ('a -> vsymbol -> int -> 'a) -> 'a -> term -> 'a

val t_v_occurs : vsymbol -> term -> int

MARCHE Claude's avatar
MARCHE Claude committed
449
(** {2 Variable substitution} *)
450 451

val t_subst_single : vsymbol -> term -> term -> term
MARCHE Claude's avatar
MARCHE Claude committed
452
(** [t_subst_single v t1 t2] substitutes variable [v] in [t2] by [t1] *)
453

MARCHE Claude's avatar
MARCHE Claude committed
454 455
val t_subst : term Mvs.t -> term -> term
(** [t_subst m t] substitutes variables in [t] by the variable mapping [m] *)
456

457
val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term
MARCHE Claude's avatar
MARCHE Claude committed
458 459
(** [t_ty_subst mt mv t] substitutes simultaneously type variables by
    mapping [mt] and term variables by mapping [mv] in term [t] *)
460

461 462
val t_subst_types : ty Mtv.t -> term Mvs.t -> term -> term Mvs.t * term
(** [t_subst_types mt mv t] substitutes type variables by
463
    mapping [mt] simultaneously in substitution [mv] and in term [t].
464
    This operation may rename the variables in [t]. *)
465

MARCHE Claude's avatar
MARCHE Claude committed
466
(** {2 Find free variables and type variables} *)
467

468 469 470 471 472 473
val t_closed : term -> bool

val t_vars : term -> int Mvs.t

val t_freevars : int Mvs.t -> term -> int Mvs.t

474
val t_ty_freevars : Stv.t -> term -> Stv.t
475

MARCHE Claude's avatar
MARCHE Claude committed
476
(** {2 Map/fold over types and logical symbols in terms and patterns} *)
477

478 479 480
val t_gen_map :
  (ty -> ty) -> (lsymbol -> lsymbol) -> vsymbol Mvs.t -> term -> term

481 482 483 484 485 486
val t_s_map : (ty -> ty) -> (lsymbol -> lsymbol) -> term -> term
val t_s_fold : ('a -> ty -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a

val t_s_all : (ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_s_any : (ty -> bool) -> (lsymbol -> bool) -> term -> bool

487
val t_ty_map : (ty -> ty) -> term -> term
488 489
val t_ty_fold : ('a -> ty -> 'a) -> 'a -> term -> 'a

MARCHE Claude's avatar
MARCHE Claude committed
490
(** Map/fold over applications in terms (but not in patterns!) *)
491 492 493

val t_app_map :
  (lsymbol -> ty list -> ty option -> lsymbol) -> term -> term
494

495 496 497
val t_app_fold :
  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a

MARCHE Claude's avatar
MARCHE Claude committed
498
(** {2 Subterm occurrence check and replacement} *)
499

500
val t_occurs  : term -> term -> bool
501
val t_replace : term -> term -> term -> term