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

François Bobot's avatar
François Bobot committed
12
open Stdlib
13
open Ident
14
open Ty
15

16 17
(** Terms and Formulas *)

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

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

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

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_opaque : Stv.t;
42
  ls_constr : int;
43 44
}

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

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

53 54 55 56 57 58 59 60
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 :
  ?opaque:Stv.t -> ?constr:int -> preid -> ty list -> lsymbol
61

62 63
val ls_ty_freevars : lsymbol -> Stv.t

Simon Cruanes's avatar
Simon Cruanes committed
64
(** {2 Exceptions} *)
65

66
exception EmptyCase
67
exception DuplicateVar of vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
68
exception UncoveredVar of vsymbol
69
exception BadArity of lsymbol * int
70 71
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
72
exception ConstructorExpected of lsymbol
73

Simon Cruanes's avatar
Simon Cruanes committed
74
(** {2 Patterns} *)
75 76 77

type pattern = private {
  pat_node : pattern_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
78
  pat_vars : Svs.t;
79 80
  pat_ty   : ty;
  pat_tag  : int;
81 82 83 84 85
}

and pattern_node = private
  | Pwild
  | Pvar of vsymbol
86
  | Papp of lsymbol * pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
87
  | Por  of pattern * pattern
88
  | Pas  of pattern * vsymbol
89

90
val pat_equal : pattern -> pattern -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
91
val pat_hash : pattern -> int
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
  t_vars  : int Mvs.t;
126
  t_tag   : int;
127 128 129 130
}

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

143
and term_bound
144
and term_branch
145
and term_quant
146

147
and trigger = term list list
148

149 150 151
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
152

153
val t_equal : term -> term -> bool
154
val t_hash : term -> int
155

156
(** Bindings *)
157

158 159 160 161
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
162
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
163 164 165 166 167

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
168
val t_open_quant : term_quant -> vsymbol list * trigger * term
169 170 171 172 173 174 175 176 177

(** 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)

178 179 180
val t_open_quant_cb :
  term_quant -> vsymbol list * trigger * term *
              (vsymbol list -> trigger -> term -> term_quant)
181

182
(** Type checking *)
183 184 185 186 187

exception TermExpected of term
exception FmlaExpected of term

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

190
val t_prop : term -> term
191 192 193 194 195
(** [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] *)

196 197
(** Smart constructors for terms and formulas *)

198 199
val t_app  : lsymbol -> term list -> ty option -> term
val fs_app : lsymbol -> term list -> ty -> term
200
val ps_app : lsymbol -> term list -> term
201 202

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

206
val t_var : vsymbol -> term
207
val t_const : Number.constant -> 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 231
val asym_label : label
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term

232
val t_let_close : vsymbol -> term -> term -> term
233
val t_eps_close : vsymbol -> term -> term
234
val t_case_close : term -> (pattern * term) list -> term
235 236 237
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
238

239
val t_label : ?loc:Loc.position -> Slab.t -> term -> term
240 241
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
242

MARCHE Claude's avatar
MARCHE Claude committed
243
(** Constructors with propositional simplification *)
244

245 246
val keep_on_simp_label : label

247
val t_if_simp : term -> term -> term -> term
248
val t_let_simp : term -> term_bound -> term
249
val t_case_simp : term -> term_branch list -> term
250 251 252 253 254 255 256 257 258 259 260
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
261

262 263 264 265 266
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

267
val t_let_close_simp : vsymbol -> term -> term -> term
268
val t_case_close_simp : term -> (pattern * term) list -> term
269 270 271
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
272

273
val t_forall_close_merge : vsymbol list -> term -> term
274 275 276
(** [forall_close_merge vs f] puts a universal quantifier over [f];
    merges variable lists if [f] is already universally quantified;
    reuses triggers of [f], if any, otherwise puts no triggers. *)
277

278
(** Built-in symbols *)
279

280
val ps_equ : lsymbol  (* equality predicate *)
281

282 283
val t_equ : term -> term -> term
val t_neq : term -> term -> term
284

285 286
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
287

288 289 290 291 292
val fs_bool_true  : lsymbol
val fs_bool_false : lsymbol

val t_bool_true  : term
val t_bool_false : term
293

294 295
val fs_tuple : int -> lsymbol   (* n-tuple *)
val t_tuple : term list -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
296

297
val is_fs_tuple : lsymbol -> bool
298
val is_fs_tuple_id : ident -> int option
Andrei Paskevich's avatar
Andrei Paskevich committed
299

300
val fs_func_app : lsymbol  (* higher-order application symbol *)
301

302 303
val t_func_app : term -> term -> term  (* value-typed application *)
val t_pred_app : term -> term -> term  (* prop-typed application *)
304

305 306
val t_func_app_l : term -> term list -> term  (* value-typed application *)
val t_pred_app_l : term -> term list -> term  (* prop-typed application *)
307

308
(** {2 Term library} *)
309

310
(** One-level (non-recursive) term traversal *)
311

312 313 314
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
315

316 317
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
318

319
(** Special maps *)
320

321 322
val t_map_simp : (term -> term) -> term -> term
(** [t_map_simp] reconstructs the term using simplification constructors *)
323

324 325
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
(** [t_map_sign] passes a polarity parameter, unfolds if-then-else and iff *)
326

327 328
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
(** [t_map_cont] is [t_map] in continuation-passing style *)
329

330
val list_map_cont: (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
331

332
(** Trigger traversal *)
333

334 335 336 337
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
338

339
(** Traversal with separate functions for value-typed and prop-typed terms *)
340

341
module TermTF : sig
342

343 344 345 346 347 348 349
  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
350
  (** [t_map fnT fnF = t_map (t_select fnT fnF)] *)
351 352

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

  val t_map_fold : ('a -> term -> 'a * term) ->
356 357 358 359 360 361 362
    ('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
363
  val t_map_sign : (bool -> term -> term) ->
364 365
    (bool -> term -> term) -> bool -> term -> term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366
  val t_map_cont : ((term -> 'a) -> term -> 'a) ->
367 368 369 370 371
    ((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
372 373

  val tr_map_fold : ('a -> term -> 'a * term) ->
374
    ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
375
end
376

377
(** Map/fold over free variables *)
378 379 380 381 382 383

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

384
(** Variable substitution *)
385 386 387 388

val t_subst : term Mvs.t -> term -> term
val t_subst_single : vsymbol -> term -> term -> term

389 390
val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term

391
(** Find free variables and type variables *)
392

393
val t_freevars    : int Mvs.t -> term -> int Mvs.t
394
val t_ty_freevars : Stv.t -> term -> Stv.t
395

396
(** Map/fold over types and logical symbols in terms and patterns *)
397

398 399 400
val t_gen_map :
  (ty -> ty) -> (lsymbol -> lsymbol) -> vsymbol Mvs.t -> term -> term

401 402 403 404 405 406
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

407
val t_ty_map : (ty -> ty) -> term -> term
408 409
val t_ty_fold : ('a -> ty -> 'a) -> 'a -> term -> 'a

410 411 412 413
(* Map/fold over applications in terms (but not in patterns!) *)

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

415 416 417 418
val t_app_fold :
  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a

(** Equality modulo alpha *)
419 420

val t_equal_alpha : term -> term -> bool
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
421

422
module Hterm_alpha : Exthtbl.S with type key = term
423

424
(** Subterm occurrence check and replacement *)
425

426 427
val t_occurs : term -> term -> bool
val t_occurs_alpha : term -> term -> bool
428

429 430
val t_replace : term -> term -> term -> term
val t_replace_alpha : term -> term -> term -> term
431