term.mli 12.6 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
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    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

François Bobot's avatar
François Bobot committed
20
open Stdlib
21
open Ident
22
open Ty
23

24 25
(** Terms and Formulas *)

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

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

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

37
val vs_equal : vsymbol -> vsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
38
val vs_hash : vsymbol -> int
39

40
val create_vsymbol : preid -> ty -> vsymbol
41

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

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

50
module Mls : Map.S with type key = lsymbol
51
module Sls : Mls.Set
52
module Hls : Hashtbl.S with type key = lsymbol
53
module Wls : Hashweak.S with type key = lsymbol
54

55
val ls_equal : lsymbol -> lsymbol -> bool
56
  (** equality of function and predicate symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
57
val ls_hash : lsymbol -> int
58

59
val create_lsymbol : preid -> ty list -> ty option -> lsymbol
60 61 62
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol

63 64
val ls_ty_freevars : lsymbol -> Stv.t

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

67
exception EmptyCase
68
exception DuplicateVar of vsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
69
exception UncoveredVar of vsymbol
70
exception BadArity of lsymbol * int * int
71 72
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected 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 113
  | Fforall
  | Fexists

114
type binop =
115 116 117 118 119
  | Fand
  | For
  | Fimplies
  | Fiff

120
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121 122 123 124 125 126 127
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

128
type term = private {
129
  t_node  : term_node;
130
  t_ty    : ty option;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131
  t_label : label list;
132
  t_loc   : Loc.position option;
133 134
  t_vars  : Svs.t;
  t_tag   : int;
135 136 137 138
}

and term_node = private
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
  | Tconst of constant
140
  | Tapp of lsymbol * term list
141
  | Tif of fmla * term * term
142
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
143
  | Tcase of term * term_branch list
144
  | Teps of fmla_bound
145
  | Fquant of quant * fmla_quant
146
  | Fbinop of binop * fmla * fmla
147
  | Fnot of fmla
148 149 150
  | Ftrue
  | Ffalse

151 152 153
and fmla = term
and term_bound
and fmla_bound = term_bound
154
and term_branch
155
and fmla_quant
156

157
and trigger = term list list
158

Andrei Paskevich's avatar
Andrei Paskevich committed
159
module Mterm : Map.S with type key = term
160
module Sterm : Mterm.Set
Andrei Paskevich's avatar
Andrei Paskevich committed
161 162
module Hterm : Hashtbl.S with type key = term

163
val t_equal : term -> term -> bool
164
val t_hash : term -> int
165

166
(** Bindings *)
167

168 169 170 171
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
172
val f_close_quant : vsymbol list -> trigger -> fmla -> fmla_quant
173 174 175 176 177

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
178
val f_open_quant : fmla_quant -> vsymbol list * trigger * fmla
179 180 181 182 183 184 185 186 187 188

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

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

192
(** Type checking *)
193 194 195 196 197

exception TermExpected of term
exception FmlaExpected of term

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

200
val t_prop : term -> term
201 202 203 204 205 206 207 208
(** [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] *)

(** [e_map fnT fnF t] is [fnT t] if [t] is value-typed, [fnF t] otherwise *)
val e_map : (term -> 'a) -> (fmla -> 'a) -> term -> 'a
val e_fold : ('a -> term -> 'b) -> ('a -> fmla -> 'b) -> 'a -> term -> 'b
209

210 211
(** Smart constructors for terms and formulas *)

212 213 214
val t_app  : lsymbol -> term list -> ty option -> term
val fs_app : lsymbol -> term list -> ty -> term
val ps_app : lsymbol -> term list -> fmla
215 216

val t_app_infer : lsymbol -> term list -> term
217 218
val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
219

220
val t_var : vsymbol -> term
221
val t_const : constant -> term
222 223
val t_int_const : string -> term
val t_real_const : real_constant -> term
224
val t_if : fmla -> term -> term -> term
225 226 227 228 229 230 231
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : fmla_bound -> term
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
232
val f_and : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233
val f_or : fmla -> fmla -> fmla
234 235
val f_implies : fmla -> fmla -> fmla
val f_iff : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236
val f_not : fmla -> fmla
237 238
val f_true : fmla
val f_false : fmla
239

240 241
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> fmla -> term
242 243 244
val f_quant_close : quant -> vsymbol list -> trigger -> fmla -> fmla
val f_forall_close : vsymbol list -> trigger -> fmla -> fmla
val f_exists_close : vsymbol list -> trigger -> fmla -> fmla
245

246 247 248
val t_label : ?loc:Loc.position -> label list -> term -> term
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
249

MARCHE Claude's avatar
MARCHE Claude committed
250
(** Constructors with propositional simplification *)
251

252 253
val t_if_simp : fmla -> term -> term -> term
val t_let_simp : term -> term_bound -> term
254 255 256 257
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
258
val f_and_simp : fmla -> fmla -> fmla
259
val f_and_simp_l : fmla list -> fmla
260
val f_or_simp : fmla -> fmla -> fmla
261
val f_or_simp_l : fmla list -> fmla
262 263 264
val f_implies_simp : fmla -> fmla -> fmla
val f_iff_simp : fmla -> fmla -> fmla
val f_not_simp : fmla -> fmla
265

266
val t_let_close_simp : vsymbol -> term -> term -> term
267 268 269
val f_quant_close_simp : quant -> vsymbol list -> trigger -> fmla -> fmla
val f_forall_close_simp : vsymbol list -> trigger -> fmla -> fmla
val f_exists_close_simp : vsymbol list -> trigger -> fmla -> fmla
270

271
val f_forall_close_merge : vsymbol list -> fmla -> fmla
272 273 274
(** [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. *)
275

276
(** Built-in symbols *)
277

278
val ps_equ : lsymbol  (* equality predicate *)
279

280 281
val f_equ : term -> term -> fmla
val f_neq : term -> term -> fmla
282

283 284
val f_equ_simp : term -> term -> fmla
val f_neq_simp : term -> term -> fmla
285

286 287
val fs_tuple : int -> lsymbol   (* n-tuple *)
val t_tuple : term list -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
288

289
val is_fs_tuple : lsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
290

291 292
val fs_func_app : lsymbol  (* value-typed higher-order application *)
val ps_pred_app : lsymbol  (* prop-typed higher-order application *)
293

294 295
val t_func_app : term -> term -> term
val f_pred_app : term -> term -> fmla
296

297 298
val t_func_app_l : term -> term list -> term
val f_pred_app_l : term -> term list -> fmla
299

300
(** {2 Term library} *)
301

302
(** One-level (non-recursive) term traversal *)
303

304 305 306
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
307

308 309
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
310

311
(** Special maps *)
312

313 314
val t_map_simp : (term -> term) -> term -> term
(** [t_map_simp] reconstructs the term using simplification constructors *)
315

316 317
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
(** [t_map_sign] passes a polarity parameter, unfolds if-then-else and iff *)
318

319 320
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
(** [t_map_cont] is [t_map] in continuation-passing style *)
321

322
val list_map_cont: (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
323

324
(** Trigger traversal *)
325

326 327 328 329
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
330

331
(** Traversal with separate functions for value-typed and prop-typed terms *)
332

333
module TermTF : sig
334

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
  val t_map : (term -> term) -> (fmla -> fmla) -> term -> term

  val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
    
  val t_map_fold : ('a -> term -> 'a * term) ->
    ('a -> fmla -> 'a * fmla) -> 'a -> term -> 'a * term
    
  val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
  val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
    
  val t_map_simp : (term -> term) -> (fmla -> fmla) -> term -> term
    
  val t_map_sign : (bool -> term -> term) ->
    (bool -> fmla -> fmla) -> bool -> term -> term
    
  val t_map_cont : ((term -> 'a) -> term -> 'a) ->
    ((fmla -> 'a) -> fmla -> 'a) -> (term -> 'a) -> term -> 'a
    
  val tr_map : (term -> term) -> (fmla -> fmla) -> trigger -> trigger
    
  val tr_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> trigger -> 'a

  val tr_map_fold : ('a -> term -> 'a * term) ->
    ('a -> fmla -> 'a * fmla) -> 'a -> trigger -> 'a * trigger
359
end
360

361
(** Map/fold over free variables *)
362 363 364 365 366 367

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

368
(** Variable occurrence check and substitution *)
369 370 371 372 373 374 375

val t_occurs : Svs.t -> term -> bool
val t_occurs_single : vsymbol -> term -> bool

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

376 377
val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term

378
(** Find free variables and type variables *)
379

380 381
val t_freevars    : Svs.t -> term -> Svs.t
val t_ty_freevars : Stv.t -> term -> Stv.t
382

383
(** Map/fold over types and logical symbols *)
384

385 386 387 388 389 390 391 392 393
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

val t_ty_fold : ('a -> ty -> 'a) -> 'a -> term -> 'a

(* Fold over applications in terms (but not in patterns!) *)
394

395 396 397 398
val t_app_fold :
  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a

(** Equality modulo alpha *)
399 400

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

402
module Hterm_alpha : Hashtbl.S with type key = term
403

404
(** Subterm occurrence check and replacement *)
405 406 407 408 409 410 411

val t_occurs_term : term -> term -> bool
val t_occurs_term_alpha : term -> term -> bool

val t_subst_term : term -> term -> term -> term
val t_subst_term_alpha : term -> term -> term -> term

412
(** Binder-free term matching *)
413

414 415 416
exception NoMatch

val t_match : term Mvs.t -> term -> term -> term Mvs.t
417