term.ml 58.3 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.                  *)
(*                                                                        *)
(**************************************************************************)
Johannes Kanig's avatar
Johannes Kanig committed
19

20
open Util
21
open Ident
22
open Ty
23

24
(** Variable symbols *)
25

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

Andrei Paskevich's avatar
Andrei Paskevich committed
31
module Vsym = WeakStructMake (struct
32
  type t = vsymbol
33 34
  let tag vs = vs.vs_name.id_tag
end)
35

36 37 38
module Svs = Vsym.S
module Mvs = Vsym.M
module Hvs = Vsym.H
39

40
let vs_equal : vsymbol -> vsymbol -> bool = (==)
41

Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
let vs_hash vs = id_hash vs.vs_name

44 45 46 47
let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}
48

49
(** Function and predicate symbols *)
50

51 52 53 54
type lsymbol = {
  ls_name   : ident;
  ls_args   : ty list;
  ls_value  : ty option;
55 56
}

Andrei Paskevich's avatar
Andrei Paskevich committed
57
module Lsym = WeakStructMake (struct
58
  type t = lsymbol
59 60 61 62 63 64
  let tag ls = ls.ls_name.id_tag
end)

module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H
Andrei Paskevich's avatar
Andrei Paskevich committed
65
module Wls = Lsym.W
66

67
let ls_equal : lsymbol -> lsymbol -> bool = (==)
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69 70
let ls_hash ls = id_hash ls.ls_name

71 72
let create_lsymbol name args value = {
  ls_name   = id_register name;
73 74
  ls_args   = args;
  ls_value  = value;
75 76
}

77 78
let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)
79

80 81 82 83 84 85 86
let ls_ty_freevars ls =
  let acc = match ls.ls_value with
    | None -> Stv.empty
    | Some ty -> ty_freevars Stv.empty ty
  in
  List.fold_left ty_freevars acc ls.ls_args

87
(** Patterns *)
88 89 90

type pattern = {
  pat_node : pattern_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
91
  pat_vars : Svs.t;
92 93
  pat_ty   : ty;
  pat_tag  : int;
94 95
}

Andrei Paskevich's avatar
Andrei Paskevich committed
96 97 98
and pattern_node =
  | Pwild
  | Pvar of vsymbol
99
  | Papp of lsymbol * pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
100 101
  | Por  of pattern * pattern
  | Pas  of pattern * vsymbol
102

103
let pat_equal : pattern -> pattern -> bool = (==)
104

Andrei Paskevich's avatar
Andrei Paskevich committed
105 106
let pat_hash p = p.pat_tag

107
module Hspat = Hashcons.Make (struct
108
  type t = pattern
109

110
  let equal_node p1 p2 = match p1, p2 with
111
    | Pwild, Pwild -> true
112 113 114
    | Pvar v1, Pvar v2 -> vs_equal v1 v2
    | Papp (s1, l1), Papp (s2, l2) ->
        ls_equal s1 s2 && List.for_all2 pat_equal l1 l2
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116
    | Por (p1, q1), Por (p2, q2) ->
        pat_equal p1 p2 && pat_equal q1 q2
117 118
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
119
    | _ -> false
120

121
  let equal p1 p2 =
122
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
123 124

  let hash_node = function
125
    | Pwild -> 0
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127 128 129
    | Pvar v -> vs_hash v
    | Papp (s, pl) -> Hashcons.combine_list pat_hash (ls_hash s) pl
    | Por (p, q) -> Hashcons.combine (pat_hash p) (pat_hash q)
    | Pas (p, v) -> Hashcons.combine (pat_hash p) (vs_hash v)
130

Andrei Paskevich's avatar
Andrei Paskevich committed
131
  let hash p = Hashcons.combine (hash_node p.pat_node) (ty_hash p.pat_ty)
132

133
  let tag n p = { p with pat_tag = n }
134 135 136 137 138 139
end)

module Pat = StructMake (struct
  type t = pattern
  let tag pat = pat.pat_tag
end)
140

141 142 143
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
144 145

(* h-consing constructors for patterns *)
146

Andrei Paskevich's avatar
Andrei Paskevich committed
147 148 149 150 151 152 153 154 155 156 157 158
let mk_pattern n vs ty = Hspat.hashcons {
  pat_node = n;
  pat_vars = vs;
  pat_ty   = ty;
  pat_tag  = -1
}

exception UncoveredVar of vsymbol
exception DuplicateVar of vsymbol

let pat_wild ty = mk_pattern Pwild Svs.empty ty
let pat_var v   = mk_pattern (Pvar v) (Svs.singleton v) v.vs_ty
159 160 161 162

let pat_as p v =
  let s = Svs.add_new v (DuplicateVar v) p.pat_vars in
  mk_pattern (Pas (p,v)) s v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
163 164

let pat_or p q =
165 166 167
  if Svs.equal p.pat_vars q.pat_vars then
    mk_pattern (Por (p,q)) p.pat_vars p.pat_ty
  else
168 169
    let s = Mvs.union (fun _ _ _ -> None) p.pat_vars q.pat_vars in
    raise (UncoveredVar (Svs.choose s))
Andrei Paskevich's avatar
Andrei Paskevich committed
170 171

let pat_app f pl ty =
172 173
  let dup v () () = raise (DuplicateVar v) in
  let merge s p = Mvs.union dup s p.pat_vars in
Andrei Paskevich's avatar
Andrei Paskevich committed
174
  mk_pattern (Papp (f,pl)) (List.fold_left merge Svs.empty pl) ty
175

176 177
(* generic traversal functions *)

178
let pat_map fn pat = match pat.pat_node with
179 180 181
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v
Andrei Paskevich's avatar
Andrei Paskevich committed
182
  | Por (p, q) -> pat_or (fn p) (fn q)
183

184 185 186
let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

187 188
let protect fn pat =
  let res = fn pat in
189
  check_ty_equal pat.pat_ty res.pat_ty;
190 191 192 193
  res

let pat_map fn = pat_map (protect fn)

194 195 196 197
let pat_fold fn acc pat = match pat.pat_node with
  | Pwild | Pvar _ -> acc
  | Papp (_, pl) -> List.fold_left fn acc pl
  | Pas (p, _) -> fn acc p
Andrei Paskevich's avatar
Andrei Paskevich committed
198
  | Por (p, q) -> fn (fn acc p) q
199

200 201
let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false
202

203 204
let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true
205

206 207
(* smart constructors for patterns *)

208
exception BadArity of lsymbol * int * int
209 210
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
211 212

let pat_app fs pl ty =
213
  let s = match fs.ls_value with
214
    | Some vty -> ty_match Mtv.empty vty ty
215 216
    | None -> raise (FunctionSymbolExpected fs)
  in
217
  let mtch s ty p = ty_match s ty p.pat_ty in
218
  ignore (try List.fold_left2 mtch s fs.ls_args pl
219
    with Invalid_argument _ -> raise (BadArity
220
      (fs, List.length fs.ls_args, List.length pl)));
221
  pat_app fs pl ty
222 223

let pat_as p v =
224
  check_ty_equal p.pat_ty v.vs_ty;
225
  pat_as p v
226

Andrei Paskevich's avatar
Andrei Paskevich committed
227 228 229 230
let pat_or p q =
  check_ty_equal p.pat_ty q.pat_ty;
  pat_or p q

231 232
(* symbol-wise map/fold *)

233
let rec pat_gen_map fnT fnL m pat =
Andrei Paskevich's avatar
Andrei Paskevich committed
234
  let fn = pat_gen_map fnT fnL m in
235
  let ty = fnT pat.pat_ty in
236 237
  match pat.pat_node with
    | Pwild -> pat_wild ty
238
    | Pvar v -> pat_var (Mvs.find v m)
239
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
240
    | Pas (p, v) -> pat_as (fn p) (Mvs.find v m)
Andrei Paskevich's avatar
Andrei Paskevich committed
241
    | Por (p, q) -> pat_or (fn p) (fn q)
242

243 244
let rec pat_gen_fold fnT fnL acc pat =
  let fn acc p = pat_gen_fold fnT fnL acc p in
245
  let acc = fnT acc pat.pat_ty in
246
  match pat.pat_node with
247
    | Pwild | Pvar _ -> acc
248
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
249
    | Por (p, q) -> fn (fn acc p) q
250
    | Pas (p, _) -> fn acc p
251

252
(** Terms and formulas *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
253

254 255 256 257 258 259 260 261 262 263
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

264
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265 266 267 268 269 270 271
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

Andrei Paskevich's avatar
Andrei Paskevich committed
272
type term = {
273
  t_node  : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274
  t_label : label list;
275 276 277
  t_vars  : Svs.t;
  t_ty    : ty;
  t_tag   : int;
278 279 280
}

and fmla = {
281
  f_node  : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
  f_label : label list;
283 284
  f_vars  : Svs.t;
  f_tag   : int;
285 286
}

Andrei Paskevich's avatar
Andrei Paskevich committed
287
and term_node =
288
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289
  | Tconst of constant
290
  | Tapp of lsymbol * term list
291
  | Tif of fmla * term * term
292
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
293
  | Tcase of term * term_branch list
294
  | Teps of fmla_bound
295

Andrei Paskevich's avatar
Andrei Paskevich committed
296
and fmla_node =
297
  | Fapp of lsymbol * term list
298
  | Fquant of quant * fmla_quant
299
  | Fbinop of binop * fmla * fmla
300
  | Fnot of fmla
301 302 303
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
304
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
305
  | Fcase of term * fmla_branch list
306

307 308
and term_bound  = vsymbol * bind_info * term
and fmla_bound  = vsymbol * bind_info * fmla
309

310 311
and term_branch = pattern * bind_info * term
and fmla_branch = pattern * bind_info * fmla
312

313
and fmla_quant  = vsymbol list * bind_info * trigger list * fmla
314

315
and bind_info = {
316 317
  bv_vars  : Svs.t;       (* free variables *)
  bv_subst : term Mvs.t   (* deferred substitution *)
318 319 320
}

and trigger = expr list
321

322 323 324
and expr =
  | Term of term
  | Fmla of fmla
325

326 327
(* term and fmla equality *)

328 329
let t_equal : term -> term -> bool = (==)
let f_equal : fmla -> fmla -> bool = (==)
330

Andrei Paskevich's avatar
Andrei Paskevich committed
331 332 333
let t_hash t = t.t_tag
let f_hash f = f.f_tag

334 335 336 337 338 339 340
(* expr and trigger equality *)

let e_equal e1 e2 = match e1, e2 with
  | Term t1, Term t2 -> t_equal t1 t2
  | Fmla f1, Fmla f2 -> f_equal f1 f2
  | _ -> false

341
let tr_equal = list_all2 (list_all2 e_equal)
342

343
(* expr and trigger traversal *)
344

345 346 347
let e_map fnT fnF = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f)
let e_fold fnT fnF acc = function Term t -> fnT acc t | Fmla f -> fnF acc f
let e_apply fnT fnF = function Term t -> fnT t | Fmla f -> fnF f
348

349 350 351 352
let e_map_fold fnT fnF acc = function
  | Term t -> let acc, t = fnT acc t in acc, Term t
  | Fmla f -> let acc, f = fnF acc f in acc, Fmla f

353 354
let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))
355

356 357
let tr_map_fold fnT fnF =
  Util.map_fold_left (Util.map_fold_left (e_map_fold fnT fnF))
358

359
(* bind_info equality, hash, and traversal *)
360

361
let bnd_equal b1 b2 = Mvs.equal t_equal b1.bv_subst b2.bv_subst
362 363

let bnd_hash bv =
364 365
  let comb v t acc = Hashcons.combine2 (vs_hash v) (t_hash t) acc in
  Mvs.fold comb bv.bv_subst
366

367 368
let bnd_map fn bv = { bv with bv_subst = Mvs.map fn bv.bv_subst }
let bnd_fold fn acc bv = Mvs.fold (fun _ t a -> fn a t) bv.bv_subst acc
369

370
let bnd_map_fold fn acc bv =
371 372
  let acc,s = Mvs.mapi_fold (fun _ t a -> fn a t) bv.bv_subst acc in
  acc, { bv with bv_subst = s }
373

374 375
(* hash-consing for terms and formulas *)

376
module Hsterm = Hashcons.Make (struct
377

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
378 379
  type t = term

380 381
  let t_eq_branch (p1,b1,t1) (p2,b2,t2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
382

383 384
  let t_eq_bound (v1,b1,t1) (v2,b2,t2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2
385

386 387
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
388 389

  let t_equal_node t1 t2 = match t1,t2 with
390
    | Tvar v1, Tvar v2 -> vs_equal v1 v2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391
    | Tconst c1, Tconst c2 -> c1 = c2
392
    | Tapp (s1,l1), Tapp (s2,l2) ->
393
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
394
    | Tif (f1,t1,e1), Tif (f2,t2,e2) ->
395
        f_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2
396
    | Tlet (t1,b1), Tlet (t2,b2) ->
397
        t_equal t1 t2 && t_eq_bound b1 b2
398
    | Tcase (t1,bl1), Tcase (t2,bl2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
399
        t_equal t1 t2 && list_all2 t_eq_branch bl1 bl2
400
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
401
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402

403
  let equal t1 t2 =
404
    ty_equal t1.t_ty t2.t_ty &&
405
    t_equal_node t1.t_node t2.t_node &&
406 407
    list_all2 (=) t1.t_label t2.t_label

408
  let t_hash_branch (p,b,t) =
Andrei Paskevich's avatar
Andrei Paskevich committed
409
    Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
410

411
  let t_hash_bound (v,b,t) =
Andrei Paskevich's avatar
Andrei Paskevich committed
412
    Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t))
413

414
  let f_hash_bound (v,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
415
    Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
416

417
  let t_hash_node = function
Andrei Paskevich's avatar
Andrei Paskevich committed
418
    | Tvar v -> vs_hash v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419
    | Tconst c -> Hashtbl.hash c
Andrei Paskevich's avatar
Andrei Paskevich committed
420 421 422 423
    | Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl
    | Tif (f,t,e) -> Hashcons.combine2 (f_hash f) (t_hash t) (t_hash e)
    | Tlet (t,bt) -> Hashcons.combine (t_hash t) (t_hash_bound bt)
    | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch (t_hash t) bl
424
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425

426
  let hash t =
427
    Hashcons.combine (t_hash_node t.t_node)
Andrei Paskevich's avatar
Andrei Paskevich committed
428
      (Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
429

430 431 432 433 434 435 436 437 438 439 440 441 442
  let add_t_vars s t = Svs.union s t.t_vars
  let add_b_vars s (_,b,_) = Svs.union s b.bv_vars

  let t_vars_node = function
    | Tvar v -> Svs.singleton v
    | Tconst _ -> Svs.empty
    | Tapp (_,tl) -> List.fold_left add_t_vars Svs.empty tl
    | Tif (f,t,e) -> add_t_vars (add_t_vars f.f_vars t) e
    | Tlet (t,bt) -> add_b_vars t.t_vars bt
    | Tcase (t,bl) -> List.fold_left add_b_vars t.t_vars bl
    | Teps (_,b,_) -> b.bv_vars

  let tag n t = { t with t_tag = n ; t_vars = t_vars_node t.t_node }
443

444
end)
445

446 447 448 449 450 451 452 453
module Term = StructMake (struct
  type t = term
  let tag term = term.t_tag
end)

module Sterm = Term.S
module Mterm = Term.M
module Hterm = Term.H
454

455
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456 457 458

  type t = fmla

459 460
  let f_eq_branch (p1,b1,f1) (p2,b2,f2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && f_equal f1 f2
461

462 463
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
464

465
  let f_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
466
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
467
    bnd_equal b1 b2 && tr_equal tl1 tl2
468

469 470
  let f_equal_node f1 f2 = match f1,f2 with
    | Fapp (s1,l1), Fapp (s2,l2) ->
471
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
472
    | Fquant (q1,b1), Fquant (q2,b2) ->
473
        q1 = q2 && f_eq_quant b1 b2
474
    | Fbinop (op1,f1,g1), Fbinop (op2,f2,g2) ->
475
        op1 = op2 && f_equal f1 f2 && f_equal g1 g2
476 477 478
    | Fnot f1, Fnot f2 -> f_equal f1 f2
    | Ftrue, Ftrue | Ffalse, Ffalse -> true
    | Fif (f1,g1,h1), Fif (f2,g2,h2) ->
479
        f_equal f1 f2 && f_equal g1 g2 && f_equal h1 h2
480
    | Flet (t1,b1), Flet (t2,b2) ->
481
        t_equal t1 t2 && f_eq_bound b1 b2
482
    | Fcase (t1,bl1), Fcase (t2,bl2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
483
        t_equal t1 t2 && list_all2 f_eq_branch bl1 bl2
484
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485

486
  let equal f1 f2 =
487 488
    f_equal_node f1.f_node f2.f_node &&
    list_all2 (=) f1.f_label f2.f_label
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
489

490
  let f_hash_branch (p,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
491
    Hashcons.combine (pat_hash p) (bnd_hash b (f_hash f))
492

493
  let f_hash_bound (v,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
494
    Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
495

Andrei Paskevich's avatar
Andrei Paskevich committed
496
  let e_hash = function Term t -> t_hash t | Fmla f -> f_hash f
497

498
  let f_hash_quant (vl,b,tl,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
499 500 501
    let h = bnd_hash b (f_hash f) in
    let h = Hashcons.combine_list vs_hash h vl in
    List.fold_left (Hashcons.combine_list e_hash) h tl
502

503
  let f_hash_node = function
Andrei Paskevich's avatar
Andrei Paskevich committed
504
    | Fapp (p,tl) -> Hashcons.combine_list t_hash (ls_hash p) tl
505 506
    | Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
    | Fbinop (op,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
507 508
        Hashcons.combine2 (Hashtbl.hash op) (f_hash f1) (f_hash f2)
    | Fnot f -> Hashcons.combine 1 (f_hash f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
509 510
    | Ftrue -> 0
    | Ffalse -> 1
Andrei Paskevich's avatar
Andrei Paskevich committed
511 512 513
    | Fif (f1,f2,f3) -> Hashcons.combine2 (f_hash f1) (f_hash f2) (f_hash f3)
    | Flet (t,bf) -> Hashcons.combine (t_hash t) (f_hash_bound bf)
    | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch (t_hash t) bl
514 515

  let hash f =
516
    Hashcons.combine_list Hashtbl.hash (f_hash_node f.f_node) f.f_label
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
517

518 519 520 521 522 523 524 525 526 527 528 529 530 531 532
  let add_t_vars s t = Svs.union s t.t_vars
  let add_f_vars s f = Svs.union s f.f_vars
  let add_b_vars s (_,b,_) = Svs.union s b.bv_vars

  let f_vars_node = function
    | Fapp (_,tl) -> List.fold_left add_t_vars Svs.empty tl
    | Fquant (_,(_,b,_,_)) -> b.bv_vars
    | Fbinop (_,f1,f2) -> Svs.union f1.f_vars f2.f_vars
    | Fnot f -> f.f_vars
    | Ftrue | Ffalse -> Svs.empty
    | Fif (f1,f2,f3) -> add_f_vars (add_f_vars f1.f_vars f2) f3
    | Flet (t,bf) -> add_b_vars t.t_vars bf
    | Fcase (t,bl) -> List.fold_left add_b_vars t.t_vars bl

  let tag n f = { f with f_tag = n ; f_vars = f_vars_node f.f_node }
533

534 535 536 537 538 539
end)

module Fmla = StructMake (struct
  type t = fmla
  let tag fmla = fmla.f_tag
end)
540

541 542 543
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
544

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
545 546
(* hash-consing constructors for terms *)

547
let mk_term n ty = Hsterm.hashcons {
548 549 550 551 552 553
  t_node  = n;
  t_label = [];
  t_vars  = Svs.empty;
  t_ty    = ty;
  t_tag   = -1
}
554

555 556 557 558 559 560 561 562 563
let t_var v         = mk_term (Tvar v) v.vs_ty
let t_const c ty    = mk_term (Tconst c) ty
let t_int_const s   = mk_term (Tconst (ConstInt s)) Ty.ty_int
let t_real_const r  = mk_term (Tconst (ConstReal r)) Ty.ty_real
let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
let t_case t1 bl ty = mk_term (Tcase (t1, bl)) ty
let t_eps bf ty     = mk_term (Teps bf) ty
564 565 566

let t_label     l t = Hsterm.hashcons { t with t_label = l }
let t_label_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }
567 568 569

let t_label_copy { t_label = l } t =
  if t.t_label = [] && l <> [] then t_label l t else t
570

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
571
(* hash-consing constructors for formulas *)
572

573 574 575 576 577 578
let mk_fmla n = Hsfmla.hashcons {
  f_node  = n;
  f_label = [];
  f_vars  = Svs.empty;
  f_tag   = -1
}
579

580 581 582 583 584 585 586 587 588
let f_app f tl        = mk_fmla (Fapp (f, tl))
let f_quant q qf      = mk_fmla (Fquant (q, qf))
let f_binary op f1 f2 = mk_fmla (Fbinop (op, f1, f2))
let f_not f           = mk_fmla (Fnot f)
let f_true            = mk_fmla (Ftrue)
let f_false           = mk_fmla (Ffalse)
let f_if f1 f2 f3     = mk_fmla (Fif (f1, f2, f3))
let f_let t bf        = mk_fmla (Flet (t, bf))
let f_case t bl       = mk_fmla (Fcase (t, bl))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
589

590 591
let f_label     l f = Hsfmla.hashcons { f with f_label = l }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }
592 593 594

let f_label_copy { f_label = l } f =
  if f.f_label = [] && l <> [] then f_label l f else f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595

596 597 598 599 600
let f_and     = f_binary Fand
let f_or      = f_binary For
let f_implies = f_binary Fimplies
let f_iff     = f_binary Fiff

601
(* unsafe map *)
602

603
let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)
604

605
let t_map_unsafe fnT fnF t = t_label_copy t (match t.t_node with
606
  | Tvar _ | Tconst _ -> t
607 608 609
  | Tapp (f,tl) -> t_app f (List.map fnT tl) t.t_ty
  | Tif (f,t1,t2) -> t_if (fnF f) (fnT t1) (fnT t2)
  | Tlet (e,b) -> t_let (fnT e) (bound_map fnT fnT b) t.t_ty
610
  | Tcase (e,bl) -> t_case (fnT e) (List.map (bound_map fnT fnT) bl) t.t_ty
611
  | Teps b -> t_eps (bound_map fnT fnF b) t.t_ty)
612

613 614
let f_map_unsafe fnT fnF f = f_label_copy f (match f.f_node with
  | Fapp (p,tl) -> f_app p (List.map fnT tl)
615 616
  | Fquant (q,(vl,b,tl,f1)) ->
      f_quant q (vl, bnd_map fnT b, tr_map fnT fnF tl, fnF f1)
617 618 619 620 621
  | Fbinop (op,f1,f2) -> f_binary op (fnF f1) (fnF f2)
  | Fnot f1 -> f_not (fnF f1)
  | Ftrue | Ffalse -> f
  | Fif (f1,f2,f3) -> f_if (fnF f1) (fnF f2) (fnF f3)
  | Flet (e,b) -> f_let (fnT e) (bound_map fnT fnF b)
622
  | Fcase (e,bl) -> f_case (fnT e) (List.map (bound_map fnT fnF) bl))
623

624
(* unsafe fold *)
625

626
let bound_fold fnT fnE acc (_,b,e) = fnE (bnd_fold fnT acc b) e
627

628
let t_fold_unsafe fnT fnF acc t = match t.t_node with
629
  | Tvar _ | Tconst _ -> acc
630 631 632
  | Tapp (_,tl) -> List.fold_left fnT acc tl
  | Tif (f,t1,t2) -> fnT (fnT (fnF acc f) t1) t2
  | Tlet (e,b) -> fnT (bound_fold fnT fnT acc b) e
633
  | Tcase (e,bl) -> List.fold_left (bound_fold fnT fnT) (fnT acc e) bl
634 635 636 637
  | Teps b -> bound_fold fnT fnF acc b

let f_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (_,tl) -> List.fold_left fnT acc tl
638
  | Fquant (_,(_,b,tl,f1)) -> fnF (tr_fold fnT fnF (bnd_fold fnT acc b) tl) f1
639 640 641 642 643
  | Fbinop (_,f1,f2) -> fnF (fnF acc f1) f2
  | Fnot f1 -> fnF acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1,f2,f3) -> fnF (fnF (fnF acc f1) f2) f3
  | Flet (e,b) -> fnT (bound_fold fnT fnF acc b) e
644
  | Fcase (e,bl) -> List.fold_left (bound_fold fnT fnF) (fnT acc e) bl
645

646 647 648 649
let all_fnT prT _ t = prT t || raise FoldSkip
let all_fnF prF _ f = prF f || raise FoldSkip
let any_fnT prT _ t = prT t && raise FoldSkip
let any_fnF prF _ f = prF f && raise FoldSkip
650

651 652
let t_all_unsafe prT prF t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) true t
653 654
  with FoldSkip -> false

655 656
let f_all_unsafe prT prF f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) true f
657 658
  with FoldSkip -> false

659 660
let t_any_unsafe prT prF t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) false t
661 662
  with FoldSkip -> true

663 664
let f_any_unsafe prT prF f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) false f
665 666
  with FoldSkip -> true

667 668 669 670 671 672 673 674
(* unsafe map_fold *)

let bound_map_fold fnT fnE acc (u,b,e) =
  let acc, b = bnd_map_fold fnT acc b in
  let acc, e = fnE acc e in
  acc, (u,b,e)

let t_map_fold_unsafe fnT fnF acc t = match t.t_node with
675
  | Tvar _ | Tconst _ ->
676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728
      acc, t
  | Tapp (f,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, t_label_copy t (t_app f tl t.t_ty)
  | Tif (f,t1,t2) ->
      let acc, f  = fnF acc f in
      let acc, t1 = fnT acc t1 in
      let acc, t2 = fnT acc t2 in
      acc, t_label_copy t (t_if f t1 t2)
  | Tlet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnT acc b in
      acc, t_label_copy t (t_let e b t.t_ty)
  | Tcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnT) acc bl in
      acc, t_label_copy t (t_case e bl t.t_ty)
  | Teps b ->
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, t_label_copy t (t_eps b t.t_ty)

let f_map_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (p,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, f_label_copy f (f_app p tl)
  | Fquant (q,(vl,b,tl,f1)) ->
      let acc, b = bnd_map_fold fnT acc b in
      let acc, tl = tr_map_fold fnT fnF acc tl in
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_quant q (vl,b,tl,f1))
  | Fbinop (op,f1,f2) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      acc, f_label_copy f (f_binary op f1 f2)
  | Fnot f1 ->
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_not f1)
  | Ftrue | Ffalse ->
      acc, f
  | Fif (f1,f2,f3) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      let acc, f3 = fnF acc f3 in
      acc, f_label_copy f (f_if f1 f2 f3)
  | Flet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, f_label_copy f (f_let e b)
  | Fcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnF) acc bl in
      acc, f_label_copy f (f_case e bl)

729 730 731 732 733 734 735 736 737 738 739
(* type-unsafe term substitution *)

let rec t_subst_unsafe m t =
  let t_subst t = t_subst_unsafe m t in
  let f_subst f = f_subst_unsafe m f in
  let b_subst (u,b,e) = (u, bv_subst_unsafe m b, e) in
  match t.t_node with
  | Tvar u ->
      Mvs.find_default u t m
  | Tlet (e, bt) ->
      t_label_copy t (t_let (t_subst e) (b_subst bt) t.t_ty)
740
  | Tcase (e, bl) ->
741 742 743 744
      let bl = List.map b_subst bl in
      t_label_copy t (t_case (t_subst e) bl t.t_ty)
  | Teps bf ->
      t_label_copy t (t_eps (b_subst bf) t.t_ty)
745
  | _ ->
746
      t_map_unsafe t_subst f_subst t
747

748 749 750 751 752 753 754 755 756 757 758 759 760
and f_subst_unsafe m f =
  let t_subst t = t_subst_unsafe m t in
  let f_subst f = f_subst_unsafe m f in
  let b_subst (u,b,e) = (u, bv_subst_unsafe m b, e) in
  match f.f_node with
  | Fquant (q, (vl,b,tl,f1)) ->
      let b = bv_subst_unsafe m b in
      f_label_copy f (f_quant q (vl,b,tl,f1))
  | Flet (e, bf) ->
      f_label_copy f (f_let (t_subst e) (b_subst bf))
  | Fcase (e, bl) ->
      let bl = List.map b_subst bl in
      f_label_copy f (f_case (t_subst e) bl)
761
  | _ ->
762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
      f_map_unsafe t_subst f_subst f

and bv_subst_unsafe m b =
  (* restrict m to the variables free in b *)
  let m = Mvs.inter (fun _ t () -> Some t) m b.bv_vars in
  (* if m is empty, return early *)
  if Mvs.is_empty m then b else
  (* remove from b.bv_vars the variables replaced by m *)
  let s = Mvs.diff (fun _ () _ -> None) b.bv_vars m in
  (* add to b.bv_vars the free variables added by m *)
  let s = Mvs.fold (fun _ t -> Svs.union t.t_vars) m s in
  (* apply m to the terms in b.bv_subst *)
  let h = Mvs.map (t_subst_unsafe m) b.bv_subst in
  (* join m to b.bv_subst *)
  let h = Mvs.union (fun _ _ t -> Some t) m h in
  (* reconstruct b *)
  { bv_vars = s ; bv_subst = h }

let t_subst_unsafe m t =
  if Mvs.is_empty m then t else t_subst_unsafe m t

let f_subst_unsafe m f =
  if Mvs.is_empty m then f else f_subst_unsafe m f
785

786
(* close bindings *)