term.ml 55.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
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.                  *)
(*                                                                        *)
(**************************************************************************)
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
41
let vs_equal = (==)

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
let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_ty
50

51
(** Function and predicate symbols *)
52

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

Andrei Paskevich's avatar
Andrei Paskevich committed
59
module Lsym = WeakStructMake (struct
60
  type t = lsymbol
61
62
63
64
65
66
  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
67
module Wls = Lsym.W
68

69
70
let ls_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
71
72
let ls_hash ls = id_hash ls.ls_name

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

79
80
let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)
81

82
83
84
85
86
87
88
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

89
(** Patterns *)
90
91
92

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

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

105
106
let pat_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
107
108
let pat_hash p = p.pat_tag

109
module Hspat = Hashcons.Make (struct
110
  type t = pattern
111

112
  let equal_node p1 p2 = match p1, p2 with
113
    | Pwild, Pwild -> true
114
115
116
    | 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
117
118
    | Por (p1, q1), Por (p2, q2) ->
        pat_equal p1 p2 && pat_equal q1 q2
119
120
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
121
    | _ -> false
122

123
  let equal p1 p2 =
124
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
125
126

  let hash_node = function
127
    | Pwild -> 0
Andrei Paskevich's avatar
Andrei Paskevich committed
128
129
130
131
    | 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)
132

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

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

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

143
144
145
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
146
147

(* h-consing constructors for patterns *)
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
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 add_no_dup vs s =
  if Svs.mem vs s then raise (DuplicateVar vs) else Svs.add vs s

let pat_wild ty = mk_pattern Pwild Svs.empty ty
let pat_var v   = mk_pattern (Pvar v) (Svs.singleton v) v.vs_ty
let pat_as p v  = mk_pattern (Pas (p,v)) (add_no_dup v p.pat_vars) v.vs_ty

let pat_or p q =
167
168
169
  if Svs.equal p.pat_vars q.pat_vars then
    mk_pattern (Por (p,q)) p.pat_vars p.pat_ty
  else
Andrei Paskevich's avatar
Andrei Paskevich committed
170
    let s1, s2 = p.pat_vars, q.pat_vars in
171
172
    let vs = Svs.choose (Svs.union (Svs.diff s1 s2) (Svs.diff s2 s1)) in
    raise (UncoveredVar vs)
Andrei Paskevich's avatar
Andrei Paskevich committed
173
174
175
176

let pat_app f pl ty =
  let merge s p = Svs.fold add_no_dup s p.pat_vars in
  mk_pattern (Papp (f,pl)) (List.fold_left merge Svs.empty pl) ty
177

178
179
(* generic traversal functions *)

180
let pat_map fn pat = match pat.pat_node with
181
182
183
  | 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
184
  | Por (p, q) -> pat_or (fn p) (fn q)
185

186
187
188
let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

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

let pat_map fn = pat_map (protect fn)

196
197
198
199
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
200
  | Por (p, q) -> fn (fn acc p) q
201

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

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

208
209
(* smart constructors for patterns *)

210
exception BadArity of lsymbol * int * int
211
212
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
213
214

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

let pat_as p v =
226
  check_ty_equal p.pat_ty v.vs_ty;
227
  pat_as p v
228

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

233
234
(* symbol-wise map/fold *)

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

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

255
(** Terms and formulas *)
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
256

257
258
259
260
261
262
263
264
265
266
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

267
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268
269
270
271
272
273
274
  | 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
275
276
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
  t_label : label list;
278
279
280
281
282
283
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284
  f_label : label list;
285
286
287
  f_tag : int;
}

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

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

309
310
and term_bound  = vsymbol * bind_info * term
and fmla_bound  = vsymbol * bind_info * fmla
311

312
313
and term_branch = pattern * bind_info * term
and fmla_branch = pattern * bind_info * fmla
314

315
and fmla_quant  = vsymbol list * bind_info * trigger list * fmla
316

317
318
319
320
321
322
323
and bind_info = {
  bv_bound : int;         (* properly bound and inst-deferred indices *)
  bv_open  : Sint.t;      (* externally visible indices *)
  bv_defer : term Mint.t  (* deferred instantiation *)
}

and trigger = expr list
324

325
326
327
and expr =
  | Term of term
  | Fmla of fmla
328

329
330
331
332
333
(* term and fmla equality *)

let t_equal = (==)
let f_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
334
335
336
let t_hash t = t.t_tag
let f_hash f = f.f_tag

337
338
339
340
341
342
343
(* 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

344
let tr_equal = list_all2 (list_all2 e_equal)
345

346
(* expr and trigger traversal *)
347

348
349
350
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
351

352
353
354
355
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

356
357
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))
358

359
360
let tr_map_fold fnT fnF =
  Util.map_fold_left (Util.map_fold_left (e_map_fold fnT fnF))
361

362
(* bind_info equality, hash, and traversal *)
363

364
365
366
367
let bnd_equal b1 b2 =
  b1.bv_bound = b2.bv_bound && Mint.equal t_equal b1.bv_defer b2.bv_defer

let bnd_hash bv =
Andrei Paskevich's avatar
Andrei Paskevich committed
368
  Mint.fold (fun i t a -> Hashcons.combine2 i (t_hash t) a) bv.bv_defer
369
370
371

let bnd_map fn bv = { bv with bv_defer = Mint.map fn bv.bv_defer }
let bnd_fold fn acc bv = Mint.fold (fun _ t a -> fn a t) bv.bv_defer acc
372

373
374
375
376
377
378
379
let bnd_map_fold fn acc bv =
  let acc,s = Mint.fold
    (fun i t (a,b) -> let a,t = fn a t in a, Mint.add i t b)
    bv.bv_defer (acc, Mint.empty)
  in
  acc, { bv with bv_defer = s }

380
381
(* hash-consing for terms and formulas *)

382
module Hsterm = Hashcons.Make (struct
383

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384
385
  type t = term

386
387
  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
388

389
390
  let t_eq_bound (v1,b1,t1) (v2,b2,t2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2
391

392
393
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
394
395

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

410
  let equal t1 t2 =
411
    t_equal t1.t_ty t2.t_ty &&
412
    t_equal_node t1.t_node t2.t_node &&
413
414
    list_all2 (=) t1.t_label t2.t_label

415
  let t_hash_branch (p,b,t) =
Andrei Paskevich's avatar
Andrei Paskevich committed
416
    Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
417

418
  let t_hash_bound (v,b,t) =
Andrei Paskevich's avatar
Andrei Paskevich committed
419
    Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t))
420

421
  let f_hash_bound (v,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
422
    Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
423

424
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425
    | Tbvar n -> n
Andrei Paskevich's avatar
Andrei Paskevich committed
426
    | Tvar v -> vs_hash v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
    | Tconst c -> Hashtbl.hash c
Andrei Paskevich's avatar
Andrei Paskevich committed
428
429
430
431
    | 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
432
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433

434
  let hash t =
435
    Hashcons.combine (t_hash_node t.t_node)
Andrei Paskevich's avatar
Andrei Paskevich committed
436
      (Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
437

438
  let tag n t = { t with t_tag = n }
439

440
end)
441

442
443
444
445
446
447
448
449
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
450

451
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452
453
454

  type t = fmla

455
456
  let f_eq_branch (p1,b1,f1) (p2,b2,f2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && f_equal f1 f2
457

458
459
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
460

461
  let f_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
462
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
463
    bnd_equal b1 b2 && tr_equal tl1 tl2
464

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

482
  let equal f1 f2 =
483
484
    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
485

486
  let f_hash_branch (p,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
487
    Hashcons.combine (pat_hash p) (bnd_hash b (f_hash f))
488

489
  let f_hash_bound (v,b,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
490
    Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
491

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

494
  let f_hash_quant (vl,b,tl,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
495
496
497
    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
498

499
  let f_hash_node = function
Andrei Paskevich's avatar
Andrei Paskevich committed
500
    | Fapp (p,tl) -> Hashcons.combine_list t_hash (ls_hash p) tl
501
502
    | Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
    | Fbinop (op,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
503
504
        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
505
506
    | Ftrue -> 0
    | Ffalse -> 1
Andrei Paskevich's avatar
Andrei Paskevich committed
507
508
509
    | 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
510
511

  let hash f =
512
    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
513

514
  let tag n f = { f with f_tag = n }
515

516
517
518
519
520
521
end)

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

523
524
525
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
526

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

529
530
let mk_term n ty = Hsterm.hashcons {
  t_node = n; t_label = []; t_ty = ty; t_tag = -1 }
531

532
533
534
535
536
537
538
539
540
541
let t_bvar n ty     = mk_term (Tbvar n) ty
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
542
543
544

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 }
545
546
547

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

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

551
let mk_fmla n = Hsfmla.hashcons { f_node = n; f_label = []; f_tag = -1 }
552

553
554
555
556
557
558
559
560
561
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
562

563
564
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 }
565
566
567

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
568

569
570
571
572
573
let f_and     = f_binary Fand
let f_or      = f_binary For
let f_implies = f_binary Fimplies
let f_iff     = f_binary Fiff

574
(* unsafe map *)
575

576
let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)
577

578
579
580
581
582
let t_map_unsafe fnT fnF t = t_label_copy t (match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> t
  | 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
583
  | Tcase (e,bl) -> t_case (fnT e) (List.map (bound_map fnT fnT) bl) t.t_ty
584
  | Teps b -> t_eps (bound_map fnT fnF b) t.t_ty)
585

586
587
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)
588
589
  | Fquant (q,(vl,b,tl,f1)) ->
      f_quant q (vl, bnd_map fnT b, tr_map fnT fnF tl, fnF f1)
590
591
592
593
594
  | 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)
595
  | Fcase (e,bl) -> f_case (fnT e) (List.map (bound_map fnT fnF) bl))
596

597
(* unsafe fold *)
598

599
let bound_fold fnT fnE acc (_,b,e) = fnE (bnd_fold fnT acc b) e
600

601
602
603
604
605
let t_fold_unsafe fnT fnF acc t = match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> acc
  | 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
606
  | Tcase (e,bl) -> List.fold_left (bound_fold fnT fnT) (fnT acc e) bl
607
608
609
610
  | 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
611
  | Fquant (_,(_,b,tl,f1)) -> fnF (tr_fold fnT fnF (bnd_fold fnT acc b) tl) f1
612
613
614
615
616
  | 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
617
  | Fcase (e,bl) -> List.fold_left (bound_fold fnT fnF) (fnT acc e) bl
618

619
620
621
622
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
623

624
625
let t_all_unsafe prT prF t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) true t
626
627
  with FoldSkip -> false

628
629
let f_all_unsafe prT prF f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) true f
630
631
  with FoldSkip -> false

632
633
let t_any_unsafe prT prF t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) false t
634
635
  with FoldSkip -> true

636
637
let f_any_unsafe prT prF f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) false f
638
639
  with FoldSkip -> true

640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
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
(* 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
  | Tbvar _ | Tvar _ | Tconst _ ->
      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)

702
703
(* replaces variables with de Bruijn indices in term [t] using map [m] *)

704
let rec t_abst m l lvl t = t_label_copy t (match t.t_node with
705
706
  | Tvar u -> begin try
      let i = Mvs.find u m in
Andrei Paskevich's avatar
Andrei Paskevich committed
707
      l := Sint.add i !l;
708
709
      t_bvar (i + lvl) t.t_ty
      with Not_found -> t end
710
711
712
713
714
715
716
717
718
  | Tlet (e, (u,b,t1)) ->
      let b,t1 = bnd_t_abst m l lvl b t1 in
      t_let (t_abst m l lvl e) (u,b,t1) t.t_ty
  | Tcase (e, bl) ->
      let br_abst (p,b,e) = let b,e = bnd_t_abst m l lvl b e in (p,b,e) in
      t_case (t_abst m l lvl e) (List.map br_abst bl) t.t_ty
  | Teps (u,b,f) ->
      let b,f = bnd_f_abst m l lvl b f in
      t_eps (u,b,f) t.t_ty
719
  | _ ->
720
721
722
723
724
725
726
727
728
729
730
      t_map_unsafe (t_abst m l lvl) (f_abst m l lvl) t)

and f_abst m l lvl f = f_label_copy f (match f.f_node with
  | Fquant (q, qf) ->
      f_quant q (bnd_q_abst m l lvl qf)
  | Flet (e, (u,b,f1)) ->
      let b,f1 = bnd_f_abst m l lvl b f1 in
      f_let (t_abst m l lvl e) (u,b,f1)
  | Fcase (e, bl) ->
      let br_abst (p,b,e) = let b,e = bnd_f_abst m l lvl b e in (p,b,e) in
      f_case (t_abst m l lvl e) (List.map br_abst bl)
731
  | _ ->
732
733
734
      f_map_unsafe (t_abst m l lvl) (f_abst m l lvl) f)

and bnd_t_abst m l lvl bv t =
Andrei Paskevich's avatar
Andrei Paskevich committed
735
736
  let l' = ref Sint.empty in
  let t = t_abst m l' (lvl + bv.bv_bound) t in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
737
  update_bv m l lvl l' bv, t
738
739

and bnd_f_abst m l lvl bv f =
Andrei Paskevich's avatar
Andrei Paskevich committed
740
741
  let l' = ref Sint.empty in
  let f = f_abst m l' (lvl + bv.bv_bound) f in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
742
  update_bv m l lvl l' bv, f
743
744

and bnd_q_abst m l lvl (vl,bv,tl,f) =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
745
  let l' = ref Sint.empty and lvl' = lvl + bv.bv_bound in
Andrei Paskevich's avatar
Andrei Paskevich committed
746
747
  let tl = tr_map (t_abst m l' lvl') (f_abst m l' lvl') tl in
  let f = f_abst m l' lvl' f in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
748
  vl, update_bv m l lvl l' bv, tl, f
Andrei Paskevich's avatar
Andrei Paskevich committed
749

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
750
and update_bv m l lvl l' bv =
Andrei Paskevich's avatar
Andrei Paskevich committed
751
  l := Sint.union !l' !l;
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
752
  let bv = bnd_map (t_abst m l lvl) bv in
Andrei Paskevich's avatar
Andrei Paskevich committed
753
754
  let add i acc = Sint.add (i + lvl) acc in
  { bv with bv_open = Sint.fold add !l' bv.bv_open }
755

Andrei Paskevich's avatar
Andrei Paskevich committed
756
757
let t_abst m t = t_abst m (ref Sint.empty) 0 t
let f_abst m f = f_abst m (ref Sint.empty) 0 f
758
759
760

(* replaces de Bruijn indices with variables in term [t] using map [m] *)

761
exception UnboundIndex
762

763
764
let bnd_find i m =
  try Mint.find i m with Not_found -> raise UnboundIndex
765

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
766
767
768
let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } =
  let s = Sint.fold (fun i -> Mint.add (i + d) (bnd_find i m)) b s in
  { bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s }
769

770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
let rec t_inst m nv t = t_label_copy t (match t.t_node with
  | Tbvar i ->
      bnd_find i m
  | Tlet (e,(u,b,t1)) ->
      t_let (t_inst m nv e) (u, bound_inst m nv b, t1) t.t_ty
  | Tcase (e,bl) ->
      let br_inst (u,b,e) = (u, bound_inst m nv b, e) in
      t_case (t_inst m nv e) (List.map br_inst bl) t.t_ty
  | Teps (u,b,f) ->
      t_eps (u, bound_inst m nv b, f) t.t_ty
  | _ ->
      t_map_unsafe (t_inst m nv) (f_inst m nv) t)

and f_inst m nv f = f_label_copy f (match f.f_node with
  | Fquant (q,(vl,b,tl,f)) ->
      f_quant q (vl, bound_inst m nv b, tl, f)
  | Flet (e,(u,b,f1)) ->
      f_let (t_inst m nv e) (u, bound_inst m nv b, f1)
  | Fcase (e,bl) ->
      let br_inst (u,b,e) = (u, bound_inst m nv b, e) in
      f_case (t_inst m nv e) (List.map br_inst bl)
  | _ ->
      f_map_unsafe (t_inst m nv) (f_inst m nv) f)
793

794
and bound_inst m nv b = bnd_inst m nv (bnd_map (t_inst m nv) b)
795
796
797

(* close bindings *)

798
799
800
801
802
let bnd_new nv =
  { bv_bound = nv ; bv_open = Sint.empty ; bv_defer = Mint.empty }

let t_close_bound v t = (v, bnd_new 1, t_abst (Mvs.add v 0 Mvs.empty) t)
let f_close_bound v f = (v, bnd_new 1, f_abst (Mvs.add v 0 Mvs.empty) f)
803
804
805
806
807
808
809
810
811
812
813
814
815

let pat_varmap p =
  let i = ref (-1) in
  let rec mk_map acc p = match p.pat_node with
    | Pvar n -> incr i; Mvs.add n !i acc
    | Pas (p, n) -> incr i; mk_map (Mvs.add n !i acc) p
    | Por (p, _) -> mk_map acc p
    | _ -> pat_fold mk_map acc p
  in
  let m = mk_map Mvs.empty p in
  m, !i + 1

let t_close_branch pat t =
816
  let m,nv = pat_varmap pat in
817
  (pat, bnd_new nv, if nv = 0 then t else t_abst m t)
818
819

let f_close_branch pat f =
820
  let m,nv = pat_varmap pat in
821
  (pat, bnd_new nv, if nv = 0 then f else f_abst m f)
822
823

let f_close_quant vl tl f =
824
  if vl = [] then (vl, bnd_new 0, tl, f) else
825
826
827
828
829
830
  let i = ref (-1) in
  let add m v =
    if Mvs.mem v m then raise (DuplicateVar v);
    incr i; Mvs.add v !i m
  in
  let m = List.fold_left add Mvs.empty vl in
831
  (vl, bnd_new (!i + 1), tr_map (t_abst m) (f_abst m) tl, f_abst m f)
832
833
834

(* open bindings *)

835
836
837
let t_open_bound (v,b,t) =
  let v = fresh_vsymbol v in
  v, t_inst (Mint.add 0 (t_var v) b.bv_defer) b.bv_bound t
838

839
840
841
let f_open_bound (v,b,f) =
  let v = fresh_vsymbol v in
  v, f_inst (Mint.add 0 (t_var v) b.bv_defer) b.bv_bound f
842
843
844
845
846
847
848
849
850
851
852
853

let rec pat_rename ns p = match p.pat_node with
  | Pvar n -> pat_var (Mvs.find n ns)
  | Pas (p, n) -> pat_as (pat_rename ns p) (Mvs.find n ns)
  | _ -> pat_map (pat_rename ns) p

let pat_substs p s =
  let m, _ = pat_varmap p in
  Mvs.fold (fun x i (s, ns) ->
    let x' = fresh_vsymbol x in
    Mint.add i (t_var x') s, Mvs.add x x' ns) m (s, Mvs.empty)

854
let t_open_branch (p,b,t) =
855
  if b.bv_bound = 0 then (p, t) else
856
857
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, t_inst m b.bv_bound t
858

859
let f_open_branch (p,b,f) =
860
  if b.bv_bound = 0 then (p, f) else
861
862
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, f_inst m b.bv_bound f
863

864
865
let quant_vars vl s =
  let i = ref (-1) in
866
867
  let add m v = let v = fresh_vsymbol v in
    incr i; Mint.add !i (t_var v) m, v in
868
869
870
871
872
  map_fold_left add s vl

let f_open_quant (vl,b,tl,f) =
  if b.bv_bound = 0 then (vl, tl, f) else
  let m,vl = quant_vars vl b.bv_defer and nv = b.bv_bound in
873
  (vl, tr_map (t_inst m nv) (f_inst m nv) tl, f_inst m nv f)
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927

let rec f_open_forall f = match f.f_node with
  | Fquant (Fforall, f) ->
      let vl, _, f = f_open_quant f in
      let vl', f = f_open_forall f in
      vl@vl', f
  | _ -> [], f

let rec f_open_exists f = match f.f_node with
  | Fquant (Fexists, f) ->
      let vl, _, f = f_open_quant f in
      let vl', f = f_open_exists f in
      vl@vl', f
  | _ -> [], f

(** open bindings with optimized closing callbacks *)

let t_open_bound_cb tb =
  let v, t = t_open_bound tb in
  let close v' t' =
    if t_equal t t' && vs_equal v v' then tb else t_close_bound v' t'
  in
  v, t, close

let f_open_bound_cb fb =
  let v, f = f_open_bound fb in
  let close v' f' =
    if f_equal f f' && v