Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

term.mli 13.8 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

Simon Cruanes's avatar
Simon Cruanes committed
20 21
(** terms module *)

22
open Ident
23
open Ty
24

Simon Cruanes's avatar
Simon Cruanes committed
25
(** {2 Variable symbols} *)
26 27

type vsymbol = private {
28
  vs_name : ident;
29 30 31 32
  vs_ty : ty;
}

module Svs : Set.S with type elt = vsymbol
33
module Mvs : Map.S with type key = vsymbol
34
module Hvs : Hashtbl.S with type key = vsymbol
35

36 37
val vs_equal : vsymbol -> vsymbol -> bool

38
val create_vsymbol : preid -> ty -> vsymbol
39

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

42 43 44 45
type lsymbol = private {
  ls_name   : ident;
  ls_args   : ty list;
  ls_value  : ty option;
46 47
}

48 49 50
module Sls : Set.S with type elt = lsymbol
module Mls : Map.S with type key = lsymbol
module Hls : Hashtbl.S with type key = lsymbol
51

52 53 54 55 56 57
val ls_equal : lsymbol -> lsymbol -> bool

val create_lsymbol : preid -> ty list -> ty option -> lsymbol
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol

58 59
val ls_ty_freevars : lsymbol -> Stv.t

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

62
exception EmptyCase
63
exception DuplicateVar of vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
64
exception UncoveredVar of vsymbol
65
exception BadArity of lsymbol * int * int
66 67
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
68

Simon Cruanes's avatar
Simon Cruanes committed
69
(** {2 Patterns} *)
70 71 72

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

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

85 86
val pat_equal : pattern -> pattern -> bool

Simon Cruanes's avatar
Simon Cruanes 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

Simon Cruanes's avatar
Simon Cruanes 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

Simon Cruanes's avatar
Simon Cruanes committed
102
(** {2 Terms and formulas} *)
103

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104
type label = string
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
105

106
type quant =
107 108 109
  | Fforall
  | Fexists

110
type binop =
111 112 113 114 115
  | Fand
  | For
  | Fimplies
  | Fiff

116
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117 118 119 120 121 122 123
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

124 125
type term = private {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126
  t_label : label list;
127 128 129 130 131 132
  t_ty : ty;
  t_tag : int;
}

and fmla = private {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133
  f_label : label list;
134 135 136 137
  f_tag : int;
}

and term_node = private
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
138
  | Tbvar of int
139
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
140
  | Tconst of constant
141
  | Tapp of lsymbol * term list
142
  | Tif of fmla * term * term
143
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
144
  | Tcase of term * term_branch list
145
  | Teps of fmla_bound
146 147

and fmla_node = private
148
  | Fapp of lsymbol * term list
149
  | Fquant of quant * fmla_quant
150
  | Fbinop of binop * fmla * fmla
151
  | Fnot of fmla
152 153 154
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
155
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
156
  | Fcase of term * fmla_branch list
157

158
and term_bound
159

160
and fmla_bound
161

162 163
and fmla_quant

164
and term_branch
165

166
and fmla_branch
167

168 169 170
and expr =
  | Term of term
  | Fmla of fmla
171

172
and trigger = expr list
173

174 175 176 177 178
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
module Mfmla : Map.S with type key = fmla
module Sfmla : Set.S with type elt = fmla

179 180 181 182
val t_equal : term -> term -> bool
val f_equal : fmla -> fmla -> bool
val e_equal : expr -> expr -> bool

183
val tr_equal : trigger list -> trigger list -> bool
184

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val f_close_bound : vsymbol -> fmla -> fmla_bound

val t_close_branch : pattern -> term -> term_branch
val f_close_branch : pattern -> fmla -> fmla_branch

val f_close_quant : vsymbol list -> trigger list -> fmla -> fmla_quant

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val f_open_bound : fmla_bound -> vsymbol * fmla

val t_open_branch : term_branch -> pattern * term
val f_open_branch : fmla_branch -> pattern * fmla

val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla

val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla

(** open bindings with optimized closing callbacks *)

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

val f_open_bound_cb :
  fmla_bound -> vsymbol * fmla * (vsymbol -> fmla -> fmla_bound)

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

val f_open_branch_cb :
  fmla_branch -> pattern * fmla * (pattern -> fmla -> fmla_branch)

val f_open_quant_cb :
  fmla_quant -> vsymbol list * trigger list * fmla *
              (vsymbol list -> trigger list -> fmla -> fmla_quant)

226 227 228 229 230 231
(** compute type instance *)

val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
val fs_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
val ps_app_inst : lsymbol -> term list -> ty Mtv.t

Simon Cruanes's avatar
Simon Cruanes committed
232
(** smart constructors for term *)
233

234
val t_var : vsymbol -> term
235
val t_const : constant -> term
236 237
val t_int_const : string -> term
val t_real_const : real_constant -> term
238
val t_app : lsymbol -> term list -> ty -> term
239
val t_if : fmla -> term -> term -> term
240 241 242 243 244 245
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : fmla_bound -> term

val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> fmla -> term
246

247 248
val t_app_infer : lsymbol -> term list -> term

249
val t_label : label list -> term -> term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
val t_label_add : label -> term -> term
251
val t_label_copy : term -> term -> term
252

Simon Cruanes's avatar
Simon Cruanes committed
253
(** smart constructors for fmla *)
254

255
val f_app : lsymbol -> term list -> fmla
256 257 258 259
val f_quant : quant -> fmla_quant -> fmla
val f_forall : fmla_quant -> fmla
val f_exists : fmla_quant -> fmla
val f_binary : binop -> fmla -> fmla -> fmla
260
val f_and : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
val f_or : fmla -> fmla -> fmla
262 263
val f_implies : fmla -> fmla -> fmla
val f_iff : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264
val f_not : fmla -> fmla
265 266
val f_true : fmla
val f_false : fmla
267
val f_if : fmla -> fmla -> fmla -> fmla
268 269 270 271 272 273 274
val f_let : term -> fmla_bound -> fmla
val f_case : term -> fmla_branch list -> fmla

val f_let_close : vsymbol -> term -> fmla -> fmla
val f_quant_close : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close : vsymbol list -> trigger list -> fmla -> fmla
275

276
val f_label : label list -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
val f_label_add : label -> fmla -> fmla
278
val f_label_copy : fmla -> fmla -> fmla
279

Simon Cruanes's avatar
Simon Cruanes committed
280
(** constructors with propositional simplification *)
281

282 283 284 285
val f_quant_simp : quant -> fmla_quant -> fmla
val f_forall_simp : fmla_quant -> fmla
val f_exists_simp : fmla_quant -> fmla
val f_binary_simp : binop -> fmla -> fmla -> fmla
286
val f_and_simp : fmla -> fmla -> fmla
287
val f_and_simp_l : fmla list -> fmla
288
val f_or_simp : fmla -> fmla -> fmla
289
val f_or_simp_l : fmla list -> fmla
290 291 292
val f_implies_simp : fmla -> fmla -> fmla
val f_iff_simp : fmla -> fmla -> fmla
val f_not_simp : fmla -> fmla
293
val t_if_simp : fmla -> term -> term -> term
294
val f_if_simp : fmla -> fmla -> fmla -> fmla
295
val f_let_simp : term -> fmla_bound -> fmla
296

297 298 299 300
val f_let_close_simp : vsymbol -> term -> fmla -> fmla
val f_quant_close_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close_simp : vsymbol list -> trigger list -> fmla -> fmla
301

Simon Cruanes's avatar
Simon Cruanes committed
302
(** expr and trigger traversal *)
303 304 305 306

val e_map : (term -> term) -> (fmla -> fmla) -> expr -> expr
val e_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> expr -> 'a
val e_apply : (term -> 'a) -> (fmla -> 'a) -> expr -> 'a
307

308 309 310
val e_map_fold : ('a -> term -> 'a * term) ->
                 ('a -> fmla -> 'a * fmla) -> 'a -> expr -> 'a * expr

311 312
val tr_map : (term -> term) ->
             (fmla -> fmla) -> trigger list -> trigger list
313

314 315
val tr_fold : ('a -> term -> 'a) ->
              ('a -> fmla -> 'a) -> 'a -> trigger list -> 'a
316

317 318 319
val tr_map_fold : ('a -> term -> 'a * term) -> ('a -> fmla -> 'a * fmla) ->
                   'a -> trigger list -> 'a * trigger list

Simon Cruanes's avatar
Simon Cruanes committed
320
(** map/fold over symbols *)
321

322 323
val t_s_map : (tysymbol -> tysymbol) -> (lsymbol -> lsymbol) -> term -> term
val f_s_map : (tysymbol -> tysymbol) -> (lsymbol -> lsymbol) -> fmla -> fmla
Andrei Paskevich's avatar
Andrei Paskevich committed
324

325 326
val t_s_fold :
  ('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
327

328 329
val f_s_fold :
  ('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> fmla -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
330

331 332 333 334
val t_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
val t_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
335

Simon Cruanes's avatar
Simon Cruanes committed
336
(** built-in symbols *)
337

MARCHE Claude's avatar
MARCHE Claude committed
338
(* equality predicate *)
339
val ps_equ : lsymbol
340 341 342 343

val f_equ : term -> term -> fmla
val f_neq : term -> term -> fmla

344 345 346
val f_equ_simp : term -> term -> fmla
val f_neq_simp : term -> term -> fmla

347 348 349
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term

350 351
val is_fs_tuple : lsymbol -> bool

Simon Cruanes's avatar
Simon Cruanes committed
352
(** {2 Term library} *)
353

Simon Cruanes's avatar
Simon Cruanes committed
354
(** generic term/fmla traversal *)
355 356 357 358

val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla

359 360 361 362
val f_map_sign : (term -> term) -> (bool -> fmla -> fmla) ->
                                    bool -> fmla -> fmla
(** give the sign of the subformula:
    - true positive
363 364
    - false negative

365 366
    nb: if-then-else and iff are translated if needed *)

367 368 369 370 371 372 373 374
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a

val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_all : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_any : (term -> bool) -> (fmla -> bool) -> fmla -> bool

375 376 377 378 379 380
val t_map_fold : ('a -> term -> 'a * term) ->
                 ('a -> fmla -> 'a * fmla) -> 'a -> term -> 'a * term

val f_map_fold : ('a -> term -> 'a * term) ->
                 ('a -> fmla -> 'a * fmla) -> 'a -> fmla -> 'a * fmla

Simon Cruanes's avatar
Simon Cruanes committed
381
(** continuation-passing map *)
382 383

val t_map_cont : ((term -> 'a) -> term -> 'a) ->
384
                 ((fmla -> 'a) -> fmla -> 'a) -> (term -> 'a) -> term -> 'a
385 386

val f_map_cont : ((term -> 'a) -> term -> 'a) ->
387
                 ((fmla -> 'a) -> fmla -> 'a) -> (fmla -> 'a) -> fmla -> 'a
388

Simon Cruanes's avatar
Simon Cruanes committed
389
(** simplification map *)
390 391
val f_map_simp : (term -> term) -> (fmla -> fmla) -> fmla -> fmla

Simon Cruanes's avatar
Simon Cruanes committed
392
(** map/fold over free variables *)
393 394 395 396 397 398 399 400 401 402 403 404

val t_v_map : (vsymbol -> term) -> term -> term
val f_v_map : (vsymbol -> term) -> fmla -> fmla

val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val f_v_fold : ('a -> vsymbol -> 'a) -> 'a -> fmla -> 'a

val t_v_all : (vsymbol -> bool) -> term -> bool
val f_v_all : (vsymbol -> bool) -> fmla -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val f_v_any : (vsymbol -> bool) -> fmla -> bool

Simon Cruanes's avatar
Simon Cruanes committed
405
(** variable occurrence check *)
406 407 408 409 410 411 412

val t_occurs : Svs.t -> term -> bool
val f_occurs : Svs.t -> fmla -> bool

val t_occurs_single : vsymbol -> term -> bool
val f_occurs_single : vsymbol -> fmla -> bool

Simon Cruanes's avatar
Simon Cruanes committed
413
(** substitution for variables *)
414 415 416 417 418 419 420

val t_subst : term Mvs.t -> term -> term
val f_subst : term Mvs.t -> fmla -> fmla

val t_subst_single : vsymbol -> term -> term -> term
val f_subst_single : vsymbol -> term -> fmla -> fmla

421 422 423
val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term
val f_ty_subst : ty Mtv.t -> term Mvs.t -> fmla -> fmla

Simon Cruanes's avatar
Simon Cruanes committed
424
(** set of free variables *)
425 426 427 428

val t_freevars : Svs.t -> term -> Svs.t
val f_freevars : Svs.t -> fmla -> Svs.t

429 430 431 432 433
(** set of free type variables *)

val t_ty_freevars : Stv.t -> term -> Stv.t
val f_ty_freevars : Stv.t -> fmla -> Stv.t

Simon Cruanes's avatar
Simon Cruanes committed
434
(** equality modulo alpha *)
435 436 437 438

val t_equal_alpha : term -> term -> bool
val f_equal_alpha : fmla -> fmla -> bool

Simon Cruanes's avatar
Simon Cruanes committed
439
(** occurrence check *)
440 441 442 443 444 445 446 447 448 449 450

val t_occurs_term : term -> term -> bool
val f_occurs_term : term -> fmla -> bool
val t_occurs_fmla : fmla -> term -> bool
val f_occurs_fmla : fmla -> fmla -> bool

val t_occurs_term_alpha : term -> term -> bool
val f_occurs_term_alpha : term -> fmla -> bool
val t_occurs_fmla_alpha : fmla -> term -> bool
val f_occurs_fmla_alpha : fmla -> fmla -> bool

Simon Cruanes's avatar
Simon Cruanes committed
451
(** term/fmla replacement *)
452 453 454 455 456 457 458 459 460 461 462

val t_subst_term : term -> term -> term -> term
val f_subst_term : term -> term -> fmla -> fmla
val t_subst_fmla : fmla -> fmla -> term -> term
val f_subst_fmla : fmla -> fmla -> fmla -> fmla

val t_subst_term_alpha : term -> term -> term -> term
val f_subst_term_alpha : term -> term -> fmla -> fmla
val t_subst_fmla_alpha : fmla -> fmla -> term -> term
val f_subst_fmla_alpha : fmla -> fmla -> fmla -> fmla

463
(** binder-free term/fmla matching *)
464

465 466 467 468
exception NoMatch

val t_match : term Mvs.t -> term -> term -> term Mvs.t
val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
469