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

20
open Ident
21
open Ty
22

23 24 25
(** Variable symbols *)

type vsymbol = private {
26
  vs_name : ident;
27 28 29 30
  vs_ty : ty;
}

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

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

36
(** Function and predicate symbols *)
37

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

44
val create_lsymbol : preid -> ty list -> ty option -> lsymbol
45 46
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol
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
(** Exceptions *)

54 55
exception BadArity of int * int
exception DuplicateVar of vsymbol
56 57
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
58

59 60 61 62 63 64 65 66 67 68 69
(** Patterns *)

type pattern = private {
  pat_node : pattern_node;
  pat_ty : ty;
  pat_tag : int;
}

and pattern_node = private
  | Pwild
  | Pvar of vsymbol
70
  | Papp of lsymbol * pattern list
71
  | Pas  of pattern * vsymbol
72 73 74 75 76

(* smart constructors for patterns *)

val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
77
val pat_app : lsymbol -> pattern list -> ty -> pattern
78 79
val pat_as  : pattern -> vsymbol -> pattern

80 81
(* generic traversal functions *)

82 83
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
84 85
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
86

87 88
val pat_freevars : Svs.t -> pattern -> Svs.t

89 90
(** Terms and formulas *)

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

93
type quant =
94 95 96
  | Fforall
  | Fexists

97
type binop =
98 99 100 101 102
  | Fand
  | For
  | Fimplies
  | Fiff

103
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104 105 106 107 108 109 110
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

111 112
type term = private {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113
  t_label : label list;
114 115 116 117 118 119
  t_ty : ty;
  t_tag : int;
}

and fmla = private {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
120
  f_label : label list;
121 122 123 124
  f_tag : int;
}

and term_node = private
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
125
  | Tbvar of int
126
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
  | Tconst of constant
128
  | Tapp of lsymbol * term list
129
  | Tif of fmla * term * term
130
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
131
  | Tcase of term list * term_branch list
132
  | Teps of fmla_bound
133 134

and fmla_node = private
135
  | Fapp of lsymbol * term list
136
  | Fquant of quant * fmla_quant
137
  | Fbinop of binop * fmla * fmla
138
  | Fnot of fmla
139 140 141
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
142
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
143
  | Fcase of term list * fmla_branch list
144

145
and term_bound
146

147
and fmla_bound
148

149 150
and fmla_quant

151
and term_branch
152

153
and fmla_branch
154

155 156 157
and expr =
  | Term of term
  | Fmla of fmla
158

159
and trigger = expr list
160

161 162 163 164 165
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

166 167
(* smart constructors for term *)

168
val t_var : vsymbol -> term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169
val t_const : constant -> ty -> term
170 171
val t_int_const : string -> term
val t_real_const : real_constant -> term
172
val t_app : lsymbol -> term list -> ty -> term
173
val t_if : fmla -> term -> term -> term
174
val t_let : vsymbol -> term -> term -> term
Andrei Paskevich's avatar
Andrei Paskevich committed
175
val t_case : term list -> (pattern list * term) list -> ty -> term
176
val t_eps : vsymbol -> fmla -> term
177

178 179
val t_app_infer : lsymbol -> term list -> term

180
val t_label : label list -> term -> term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
val t_label_add : label -> term -> term
182
val t_label_copy : term -> term -> term
183

184 185
(* smart constructors for fmla *)

186
val f_app : lsymbol -> term list -> fmla
187 188 189
val f_forall : vsymbol list -> trigger list -> fmla -> fmla
val f_exists : vsymbol list -> trigger list -> fmla -> fmla
val f_quant : quant -> vsymbol list -> trigger list -> fmla -> fmla
190
val f_and : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191
val f_or : fmla -> fmla -> fmla
192 193
val f_implies : fmla -> fmla -> fmla
val f_iff : fmla -> fmla -> fmla
194
val f_binary : binop -> fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195
val f_not : fmla -> fmla
196 197
val f_true : fmla
val f_false : fmla
198 199
val f_if : fmla -> fmla -> fmla -> fmla
val f_let : vsymbol -> term -> fmla -> fmla
Andrei Paskevich's avatar
Andrei Paskevich committed
200
val f_case : term list -> (pattern list * fmla) list -> fmla
201

202
val f_label : label list -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
203
val f_label_add : label -> fmla -> fmla
204
val f_label_copy : fmla -> fmla -> fmla
205

206 207 208 209 210 211
(* constructors with propositional simplification *)

val f_forall_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_quant_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_and_simp : fmla -> fmla -> fmla
212
val f_and_simp_l : fmla list -> fmla
213
val f_or_simp : fmla -> fmla -> fmla
214
val f_or_simp_l : fmla list -> fmla
215 216 217 218
val f_implies_simp : fmla -> fmla -> fmla
val f_iff_simp : fmla -> fmla -> fmla
val f_binary_simp : binop -> fmla -> fmla -> fmla
val f_not_simp : fmla -> fmla
219
val t_if_simp : fmla -> term -> term -> term
220 221 222
val f_if_simp : fmla -> fmla -> fmla -> fmla
val f_let_simp : vsymbol -> term -> fmla -> fmla

223
(* open bindings *)
224

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

228 229
val t_open_branch : term_branch -> pattern list * term
val f_open_branch : fmla_branch -> pattern list * fmla
230

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

233 234 235
val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla

236 237 238 239 240
(* expr and trigger traversal *)

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
241

242 243
val tr_map : (term -> term) ->
             (fmla -> fmla) -> trigger list -> trigger list
244

245 246
val tr_fold : ('a -> term -> 'a) ->
              ('a -> fmla -> 'a) -> 'a -> trigger list -> 'a
247 248

(* map/fold over symbols *)
249

250 251
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
252

253 254
val t_s_fold :
  ('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
255

256 257
val f_s_fold :
  ('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> fmla -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
258

259 260 261 262
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
263

264 265
(* built-in symbols *)

266 267
val ps_equ : lsymbol
val ps_neq : lsymbol
268 269 270 271

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

272 273 274 275 276 277 278
(** Term library *)

(* generic term/fmla traversal *)

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

279 280 281 282
val f_map_sign : (term -> term) -> (bool -> fmla -> fmla) ->
                                    bool -> fmla -> fmla
(** give the sign of the subformula:
    - true positive
283 284
    - false negative

285 286
    nb: if-then-else and iff are translated if needed *)

287 288 289 290 291 292 293 294
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

295 296 297 298 299 300 301 302 303 304
(* continuation-passing map *)

val t_map_cont : ((term -> 'a) -> term -> 'a) ->
                 ((fmla -> 'a) -> fmla -> 'a) ->
                  (term -> 'a) -> term -> 'a

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

305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
(* map/fold over free variables *)

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

(* variable occurrence check *)

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

(* substitution for variables *)

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

(* set of free variables *)

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

(* equality modulo alpha *)

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

(* occurrence check *)

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

(* term/fmla replacement *)

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

(* term/fmla matching modulo alpha in the pattern *)

370 371 372 373
exception NoMatch

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