term.mli 13.1 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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
Andrei Paskevich's avatar
Andrei Paskevich committed
56
val ls_hash : lsymbol -> int
57

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

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 * int
70 71
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
72

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

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

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

89
val pat_equal : pattern -> pattern -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
90
val pat_hash : pattern -> int
91

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

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

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

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

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

109
type quant =
110 111
  | Tforall
  | Texists
112

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

119 120 121 122 123 124
type integer_constant =
  | IConstDecimal of string
  | IConstHexa of string
  | IConstOctal of string
  | IConstBinary of string

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

type constant =
130
  | ConstInt of integer_constant
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131 132
  | ConstReal of real_constant

133
type term = private {
134
  t_node  : term_node;
135
  t_ty    : ty option;
136
  t_label : Slab.t;
137
  t_loc   : Loc.position option;
138
  t_vars  : int Mvs.t;
139
  t_tag   : int;
140 141 142 143
}

and term_node = private
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144
  | Tconst of constant
145
  | Tapp of lsymbol * term list
146
  | Tif of term * term * term
147
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
148
  | Tcase of term * term_branch list
149 150 151 152 153 154 155
  | Teps of term_bound
  | Tquant of quant * term_quant
  | Tbinop of binop * term * term
  | Tnot of term
  | Ttrue
  | Tfalse

156
and term_bound
157
and term_branch
158
and term_quant
159

160
and trigger = term list list
161

Andrei Paskevich's avatar
Andrei Paskevich committed
162
module Mterm : Map.S with type key = term
163
module Sterm : Mterm.Set
Andrei Paskevich's avatar
Andrei Paskevich committed
164 165
module Hterm : Hashtbl.S with type key = term

166
val t_equal : term -> term -> bool
167
val t_hash : term -> int
168

169
(** Bindings *)
170

171 172 173 174
(** close bindings *)

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
175
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
176 177 178 179 180

(** open bindings *)

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
181
val t_open_quant : term_quant -> vsymbol list * trigger * term
182 183 184 185 186 187 188 189 190

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

191 192 193
val t_open_quant_cb :
  term_quant -> vsymbol list * trigger * term *
              (vsymbol list -> trigger -> term -> term_quant)
194

195
(** Type checking *)
196 197 198 199 200

exception TermExpected of term
exception FmlaExpected of term

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

203
val t_prop : term -> term
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] *)

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

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

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

219
val t_var : vsymbol -> term
220
val t_const : constant -> term
221 222
val t_int_const : string -> term
val t_real_const : real_constant -> term
223
val t_if : term -> term -> term -> term
224 225
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
226 227 228 229 230 231 232 233 234 235 236 237
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
238

239 240 241 242
val asym_label : label
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term

243
val t_let_close : vsymbol -> term -> term -> term
244 245 246 247
val t_eps_close : vsymbol -> term -> term
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
248

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

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

255
val t_if_simp : term -> term -> term -> term
256
val t_let_simp : term -> term_bound -> 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 276 277
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
278

279
val t_forall_close_merge : vsymbol list -> term -> term
280 281 282
(** [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. *)
283

284
(** Built-in symbols *)
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
val fs_true : lsymbol
val fs_false: lsymbol

297 298
val fs_tuple : int -> lsymbol   (* n-tuple *)
val t_tuple : term list -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
299

300
val is_fs_tuple : lsymbol -> bool
301
val is_fs_tuple_id : ident -> int option
Andrei Paskevich's avatar
Andrei Paskevich committed
302

303 304
val fs_func_app : lsymbol  (* value-typed higher-order application *)
val ps_pred_app : lsymbol  (* prop-typed higher-order application *)
305

306
val t_func_app : term -> term -> term
307
val t_pred_app : term -> term -> term
308

309
val t_func_app_l : term -> term list -> term
310
val t_pred_app_l : term -> term list -> term
311

312
(** {2 Term library} *)
313

314
(** One-level (non-recursive) term traversal *)
315

316 317 318
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
319

320 321
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
322

323
(** Special maps *)
324

325 326
val t_map_simp : (term -> term) -> term -> term
(** [t_map_simp] reconstructs the term using simplification constructors *)
327

328 329
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
(** [t_map_sign] passes a polarity parameter, unfolds if-then-else and iff *)
330

331 332
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
(** [t_map_cont] is [t_map] in continuation-passing style *)
333

334
val list_map_cont: (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
335

336
(** Trigger traversal *)
337

338 339 340 341
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
342

343
(** Traversal with separate functions for value-typed and prop-typed terms *)
344

345
module TermTF : sig
346

347 348 349 350 351 352 353
  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
354
  (** [t_map fnT fnF = t_map (t_select fnT fnF)] *)
355 356

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

  val t_map_fold : ('a -> term -> 'a * term) ->
360 361 362 363 364 365 366
    ('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
367
  val t_map_sign : (bool -> term -> term) ->
368 369
    (bool -> term -> term) -> bool -> term -> term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
370
  val t_map_cont : ((term -> 'a) -> term -> 'a) ->
371 372 373 374 375
    ((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
376 377

  val tr_map_fold : ('a -> term -> 'a * term) ->
378
    ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
379
end
380

381
(** Map/fold over free variables *)
382 383 384 385 386 387

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

388
(** Variable substitution *)
389 390 391 392

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

393 394
val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term

395
(** Find free variables and type variables *)
396

397
val t_freevars    : int Mvs.t -> term -> int Mvs.t
398
val t_ty_freevars : Stv.t -> term -> Stv.t
399

400
(** Map/fold over types and logical symbols in terms and patterns *)
401

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

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

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

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

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

(** Equality modulo alpha *)
420 421

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

423
module Hterm_alpha : Hashtbl.S with type key = term
424

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

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

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