term.mli 16.5 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

Simon Cruanes's avatar
Simon Cruanes committed
17
(** {2 Variable symbols} *)
18 19

type vsymbol = private {
20
  vs_name : ident;
21
  vs_ty   : ty;
22 23
}

24 25 26
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
27
module Wvs : Weakhtbl.S with type key = vsymbol
28

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

33
val create_vsymbol : preid -> ty -> vsymbol
34

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

37 38 39
type lsymbol = private {
  ls_name   : ident;
  ls_args   : ty list;
40
  ls_value  : ty option;
41
  ls_constr : int;
42 43
}

44 45 46
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
47
module Wls : Weakhtbl.S with type key = lsymbol
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49
val ls_compare : lsymbol -> lsymbol -> int
50
val ls_equal : lsymbol -> lsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
51
val ls_hash : lsymbol -> int
52

53
val create_lsymbol : ?constr:int -> preid -> ty list -> ty option -> lsymbol
54

55
val create_fsymbol : ?constr:int -> preid -> ty list -> ty -> lsymbol
56

57
val create_psymbol : preid -> ty list -> lsymbol
58

59 60
val ls_ty_freevars : lsymbol -> Stv.t

Simon Cruanes's avatar
Simon Cruanes committed
61
(** {2 Exceptions} *)
62

63
exception EmptyCase
64
exception DuplicateVar of vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
65
exception UncoveredVar of vsymbol
66
exception BadArity of lsymbol * int
67 68
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
69
exception ConstructorExpected of lsymbol
Clément Fumex's avatar
Clément Fumex committed
70
exception InvalidLiteralType of ty
71

Simon Cruanes's avatar
Simon Cruanes committed
72
(** {2 Patterns} *)
73 74 75

type pattern = private {
  pat_node : pattern_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
76
  pat_vars : Svs.t;
77
  pat_ty   : ty;
78 79
}

80
and pattern_node =
81 82
  | Pwild
  | Pvar of vsymbol
83
  | Papp of lsymbol * pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
84
  | Por  of pattern * pattern
85
  | Pas  of pattern * vsymbol
86

MARCHE Claude's avatar
MARCHE Claude committed
87
(** Smart constructors for patterns *)
88 89 90

val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
91
val pat_app : lsymbol -> pattern list -> ty -> pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
92
val pat_or  : pattern -> pattern -> pattern
93 94
val pat_as  : pattern -> vsymbol -> pattern

MARCHE Claude's avatar
MARCHE Claude committed
95
(** Generic traversal functions *)
96

97 98
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
99 100
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
101

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

104
type quant =
105 106
  | Tforall
  | Texists
107

108
type binop =
109 110 111 112
  | Tand
  | Tor
  | Timplies
  | Tiff
113

114
type term = private {
115
  t_node  : term_node;
116
  t_ty    : ty option;
117
  t_label : Slab.t;
118
  t_loc   : Loc.position option;
119 120
}

121
and term_node =
122
  | Tvar of vsymbol
123
  | Tconst of Number.constant
124
  | Tapp of lsymbol * term list
125
  | Tif of term * term * term
126
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
127
  | Tcase of term * term_branch list
128 129 130 131 132 133 134
  | Teps of term_bound
  | Tquant of quant * term_quant
  | Tbinop of binop * term * term
  | Tnot of term
  | Ttrue
  | Tfalse

135
and term_bound
136
and term_branch
137
and term_quant
138

139
and trigger = term list list
140

141 142 143
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
144

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

Andrei Paskevich's avatar
Andrei Paskevich committed
147
val t_compare : term -> term -> int
148
val t_equal : term -> term -> bool
149
val t_hash : term -> int
150

MARCHE Claude's avatar
MARCHE Claude committed
151
(** {2 Bindings} *)
152

153 154 155 156
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
157
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
158 159 160 161 162

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
163
val t_open_quant : term_quant -> vsymbol list * trigger * term
164

165
val t_open_bound_with : term -> term_bound -> term
166
val t_clone_bound_id : term_bound -> preid
167

168 169 170 171 172 173 174 175
(** 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)

176 177 178
val t_open_quant_cb :
  term_quant -> vsymbol list * trigger * term *
              (vsymbol list -> trigger -> term -> term_quant)
179

MARCHE Claude's avatar
MARCHE Claude committed
180
(** {2 Type checking} *)
181 182 183 184 185

exception TermExpected of term
exception FmlaExpected of term

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

188
val t_prop : term -> term
189 190 191 192 193
(** [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
194
(** {2 Smart constructors for terms and formulas} *)
195

196 197
val t_app  : lsymbol -> term list -> ty option -> term
val fs_app : lsymbol -> term list -> ty -> term
198
val ps_app : lsymbol -> term list -> term
199 200

val t_app_infer : lsymbol -> term list -> term
201 202
val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
203

204 205
val check_literal : Number.constant -> ty -> unit

206
val t_var : vsymbol -> term
Clément Fumex's avatar
Clément Fumex committed
207
val t_const : Number.constant -> ty -> term
208
val t_if : term -> term -> term -> term
209 210
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
211 212 213 214 215 216 217 218 219 220 221 222
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
223

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

228 229 230
val stop_split : label
val asym_split : label

231 232 233
val t_and_l : term list -> term
val t_or_l : term list -> term

234 235 236
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term

237 238 239
val t_and_asym_l : term list -> term
val t_or_asym_l : term list -> term

240
val t_let_close : vsymbol -> term -> term -> term
241
val t_eps_close : vsymbol -> term -> term
242
val t_case_close : term -> (pattern * term) list -> term
243 244 245
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
246

247
val t_label : ?loc:Loc.position -> Slab.t -> term -> term
248
val t_label_add : label -> term -> term
249
val t_label_remove : label -> term -> term
250
val t_label_copy : term -> term -> term
251

MARCHE Claude's avatar
MARCHE Claude committed
252
(** Constructors with propositional simplification *)
253

254
val t_if_simp : term -> term -> term -> term
255
val t_let_simp : term -> term_bound -> term
256
val t_case_simp : term -> term_branch list -> term
257 258 259 260 261 262 263 264 265 266 267
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
268

269 270 271 272 273
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

274
val t_let_close_simp : vsymbol -> term -> term -> term
275
val t_case_close_simp : term -> (pattern * term) list -> term
276 277 278
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
279

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

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

MARCHE Claude's avatar
MARCHE Claude committed
288 289
val ps_equ : lsymbol
(** equality predicate *)
290

291 292
val t_equ : term -> term -> term
val t_neq : term -> term -> term
293

294 295
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
296

297 298 299 300 301
val fs_bool_true  : lsymbol
val fs_bool_false : lsymbol

val t_bool_true  : term
val t_bool_false : term
302

303 304
val fs_tuple : int -> lsymbol   (* n-tuple *)
val t_tuple : term list -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
305

306
val is_fs_tuple : lsymbol -> bool
307
val is_fs_tuple_id : ident -> int option
Andrei Paskevich's avatar
Andrei Paskevich committed
308

309
val fs_func_app : lsymbol  (* higher-order application symbol *)
310

311 312
val t_func_app : term -> term -> term  (* value-typed application *)
val t_pred_app : term -> term -> term  (* prop-typed application *)
313

314 315
val t_func_app_l : term -> term list -> term  (* value-typed application *)
val t_pred_app_l : term -> term list -> term  (* prop-typed application *)
316

317 318
(** {2 Lambda-term manipulation} *)

319
val t_lambda : vsymbol list -> trigger -> term -> term
MARCHE Claude's avatar
MARCHE Claude committed
320 321
(** [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.
322 323 324 325 326 327 328 329 330 331 332 333 334
    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. *)
335 336

val t_is_lambda : term -> bool
337 338 339 340 341
(** [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. *)
342 343

val t_closure : lsymbol -> ty list -> ty option -> term
344 345 346 347
(** [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. *)
348 349

val t_app_partial : lsymbol -> term list -> ty list -> ty option -> term
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
(** [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
371

372
(** {2 Term library} *)
373

374
(** One-level (non-recursive) term traversal *)
375

376 377 378
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
379

380 381
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
382

383
(** Special maps *)
384

385 386
val t_map_simp : (term -> term) -> term -> term
(** [t_map_simp] reconstructs the term using simplification constructors *)
387

388 389
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
(** [t_map_sign] passes a polarity parameter, unfolds if-then-else and iff *)
390

391 392
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
(** [t_map_cont] is [t_map] in continuation-passing style *)
393

394
val list_map_cont: (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
395

396
(** Trigger traversal *)
397

398 399 400 401
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
402

403
(** Traversal with separate functions for value-typed and prop-typed terms *)
404

405
module TermTF : sig
406

407 408 409 410 411 412 413
  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
414
  (** [t_map fnT fnF = t_map (t_select fnT fnF)] *)
415 416

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

  val t_map_fold : ('a -> term -> 'a * term) ->
420 421 422 423 424 425 426
    ('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
427
  val t_map_sign : (bool -> term -> term) ->
428 429
    (bool -> term -> term) -> bool -> term -> term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
430
  val t_map_cont : ((term -> 'a) -> term -> 'a) ->
431 432 433 434 435
    ((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
436 437

  val tr_map_fold : ('a -> term -> 'a * term) ->
438
    ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
439
end
440

MARCHE Claude's avatar
MARCHE Claude committed
441
(** {2 Map/fold over free variables} *)
442 443 444 445 446 447

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

448 449 450 451
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
452
(** {2 Variable substitution} *)
453 454

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

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

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

464 465
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
466
    mapping [mt] simultaneously in substitution [mv] and in term [t].
467
    This operation may rename the variables in [t]. *)
468

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

471 472 473 474 475 476
val t_closed : term -> bool

val t_vars : term -> int Mvs.t

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

477
val t_ty_freevars : Stv.t -> term -> Stv.t
478

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

481 482 483
val t_gen_map :
  (ty -> ty) -> (lsymbol -> lsymbol) -> vsymbol Mvs.t -> term -> term

484 485 486 487 488 489
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

490
val t_ty_map : (ty -> ty) -> term -> term
491 492
val t_ty_fold : ('a -> ty -> 'a) -> 'a -> term -> 'a

MARCHE Claude's avatar
MARCHE Claude committed
493
(** Map/fold over applications in terms (but not in patterns!) *)
494 495 496

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

498 499 500
val t_app_fold :
  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a

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

503
val t_occurs  : term -> term -> bool
504
val t_replace : term -> term -> term -> term