term.ml 54.6 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
3
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
}

31
module Vsym = StructMake (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 = (==)

42
43
44
45
let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}
46

47
let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_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
}

57
module Lsym = StructMake (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
65

66
67
let ls_equal = (==)

68
69
let create_lsymbol name args value = {
  ls_name   = id_register name;
70
71
  ls_args   = args;
  ls_value  = value;
72
73
}

74
75
let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)
76

77
(** Patterns *)
78
79
80

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

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

93
94
let pat_equal = (==)

95
module Hspat = Hashcons.Make (struct
96
  type t = pattern
97

98
  let equal_node p1 p2 = match p1, p2 with
99
    | Pwild, Pwild -> true
100
101
102
    | 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
103
104
    | Por (p1, q1), Por (p2, q2) ->
        pat_equal p1 p2 && pat_equal q1 q2
105
106
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
107
    | _ -> false
108

109
  let equal p1 p2 =
110
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
111

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112
113
  let hash_pattern p = p.pat_tag

114
  let hash_node = function
115
    | Pwild -> 0
116
    | Pvar v -> v.vs_name.id_tag
117
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
Andrei Paskevich's avatar
Andrei Paskevich committed
118
    | Por (p, q) -> Hashcons.combine (hash_pattern p) (hash_pattern q)
119
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
120

121
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
122

123
  let tag n p = { p with pat_tag = n }
124
125
126
127
128
129
end)

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

131
132
133
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
134
135

(* h-consing constructors for patterns *)
136

Andrei Paskevich's avatar
Andrei Paskevich committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
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 =
155
156
157
  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
158
    let s1, s2 = p.pat_vars, q.pat_vars in
159
160
    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
161
162
163
164

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
165

166
167
(* generic traversal functions *)

168
let pat_map fn pat = match pat.pat_node with
169
170
171
  | 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
172
  | Por (p, q) -> pat_or (fn p) (fn q)
173

174
175
176
let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

177
178
let protect fn pat =
  let res = fn pat in
179
  check_ty_equal pat.pat_ty res.pat_ty;
180
181
182
183
  res

let pat_map fn = pat_map (protect fn)

184
185
186
187
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
188
  | Por (p, q) -> fn (fn acc p) q
189

190
191
let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false
192

193
194
let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true
195

196
197
(* smart constructors for patterns *)

198
exception BadArity of lsymbol * int * int
199
200
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
201
202

let pat_app fs pl ty =
203
  let s = match fs.ls_value with
204
    | Some vty -> ty_match Mtv.empty vty ty
205
206
    | None -> raise (FunctionSymbolExpected fs)
  in
207
  let mtch s ty p = ty_match s ty p.pat_ty in
208
  ignore (try List.fold_left2 mtch s fs.ls_args pl
209
    with Invalid_argument _ -> raise (BadArity
210
      (fs, List.length fs.ls_args, List.length pl)));
211
  pat_app fs pl ty
212
213

let pat_as p v =
214
  check_ty_equal p.pat_ty v.vs_ty;
215
  pat_as p v
216

Andrei Paskevich's avatar
Andrei Paskevich committed
217
218
219
220
let pat_or p q =
  check_ty_equal p.pat_ty q.pat_ty;
  pat_or p q

221
222
(* symbol-wise map/fold *)

223
224
let rec pat_gen_map fnT fnV fnL pat =
  let fn p = pat_gen_map fnT fnV fnL p in
225
  let ty = fnT pat.pat_ty in
226
227
228
  match pat.pat_node with
    | Pwild -> pat_wild ty
    | Pvar v -> pat_var (fnV v ty)
229
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
Andrei Paskevich's avatar
Andrei Paskevich committed
230
    | Pas (p, v) -> pat_as (fn p) (fnV v ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
231
    | Por (p, q) -> pat_or (fn p) (fn q)
232

233
234
235
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
236
  match pat.pat_node with
237
238
    | Pwild -> acc
    | Pvar v -> fnV acc v
239
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
240
    | Por (p, q) -> fn (fn acc p) q
241
    | Pas (p, v) -> fn (fnV acc v) p
242

243
244
(** Terms and formulas *)

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
245
246
type label = string

247
248
249
250
251
252
253
254
255
256
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

257
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258
259
260
261
262
263
264
  | 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
265
266
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267
  t_label : label list;
268
269
270
271
272
273
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274
  f_label : label list;
275
276
277
  f_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
278
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
  | Tbvar of int
280
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281
  | Tconst of constant
282
  | Tapp of lsymbol * term list
283
  | Tif of fmla * term * term
284
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
285
  | Tcase of term * term_branch list
286
  | Teps of fmla_bound
287

Andrei Paskevich's avatar
Andrei Paskevich committed
288
and fmla_node =
289
  | Fapp of lsymbol * term list
290
  | Fquant of quant * fmla_quant
291
  | Fbinop of binop * fmla * fmla
292
  | Fnot of fmla
293
294
295
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
296
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
297
  | Fcase of term * fmla_branch list
298

299
300
and term_bound  = vsymbol * bind_info * term
and fmla_bound  = vsymbol * bind_info * fmla
301

302
303
and term_branch = pattern * bind_info * term
and fmla_branch = pattern * bind_info * fmla
304

305
and fmla_quant  = vsymbol list * bind_info * trigger list * fmla
306

307
308
309
310
311
312
313
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
314

315
316
317
and expr =
  | Term of term
  | Fmla of fmla
318

319
320
321
322
323
324
325
326
327
328
329
330
(* term and fmla equality *)

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

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

331
let tr_equal = list_all2 (list_all2 e_equal)
332

333
(* expr and trigger traversal *)
334

335
336
337
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
338

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

343
344
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))
345

346
347
let tr_map_fold fnT fnF =
  Util.map_fold_left (Util.map_fold_left (e_map_fold fnT fnF))
348

349
(* bind_info equality, hash, and traversal *)
350

351
352
353
354
355
356
357
358
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 =
  Mint.fold (fun i t a -> Hashcons.combine2 i t.t_tag a) bv.bv_defer

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
359

360
361
362
363
364
365
366
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 }

367
368
(* hash-consing for terms and formulas *)

369
module Hsterm = Hashcons.Make (struct
370

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
371
372
  type t = term

373
374
  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
375

376
377
  let t_eq_bound (v1,b1,t1) (v2,b2,t2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2
378

379
380
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
381
382

  let t_equal_node t1 t2 = match t1,t2 with
383
384
    | 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
385
    | Tconst c1, Tconst c2 -> c1 = c2
386
    | Tapp (s1,l1), Tapp (s2,l2) ->
387
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
388
    | Tif (f1,t1,e1), Tif (f2,t2,e2) ->
389
        f_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2
390
    | Tlet (t1,b1), Tlet (t2,b2) ->
391
        t_equal t1 t2 && t_eq_bound b1 b2
392
    | Tcase (t1,bl1), Tcase (t2,bl2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
393
        t_equal t1 t2 && list_all2 t_eq_branch bl1 bl2
394
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
395
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
396

397
  let equal t1 t2 =
398
    t_equal t1.t_ty t2.t_ty &&
399
    t_equal_node t1.t_node t2.t_node &&
400
401
    list_all2 (=) t1.t_label t2.t_label

402
403
  let t_hash_branch (p,b,t) =
    Hashcons.combine p.pat_tag (bnd_hash b t.t_tag)
404

405
406
  let t_hash_bound (v,b,t) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b t.t_tag)
407

408
409
  let f_hash_bound (v,b,f) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
410

411
  let t_hash t = t.t_tag
412

413
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414
    | Tbvar n -> n
415
    | Tvar v -> v.vs_name.id_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
    | Tconst c -> Hashtbl.hash c
417
418
419
420
    | Tapp (f,tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
    | Tif (f,t,e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
    | Tlet (t,bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
    | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
421
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422

423
  let hash t =
424
    Hashcons.combine (t_hash_node t.t_node)
425
      (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
426

427
  let tag n t = { t with t_tag = n }
428

429
end)
430

431
432
433
434
435
436
437
438
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
439

440
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
442
443

  type t = fmla

444
445
  let f_eq_branch (p1,b1,f1) (p2,b2,f2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && f_equal f1 f2
446

447
448
  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2
449

450
  let f_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
451
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
452
    bnd_equal b1 b2 && tr_equal tl1 tl2
453

454
455
  let f_equal_node f1 f2 = match f1,f2 with
    | Fapp (s1,l1), Fapp (s2,l2) ->
456
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
457
    | Fquant (q1,b1), Fquant (q2,b2) ->
458
        q1 = q2 && f_eq_quant b1 b2
459
    | Fbinop (op1,f1,g1), Fbinop (op2,f2,g2) ->
460
        op1 = op2 && f_equal f1 f2 && f_equal g1 g2
461
462
463
    | Fnot f1, Fnot f2 -> f_equal f1 f2
    | Ftrue, Ftrue | Ffalse, Ffalse -> true
    | Fif (f1,g1,h1), Fif (f2,g2,h2) ->
464
        f_equal f1 f2 && f_equal g1 g2 && f_equal h1 h2
465
    | Flet (t1,b1), Flet (t2,b2) ->
466
        t_equal t1 t2 && f_eq_bound b1 b2
467
    | Fcase (t1,bl1), Fcase (t2,bl2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
468
        t_equal t1 t2 && list_all2 f_eq_branch bl1 bl2
469
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
470

471
  let equal f1 f2 =
472
473
    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
474

475
  let v_hash v = v.vs_name.id_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476

Andrei Paskevich's avatar
Andrei Paskevich committed
477
  let t_hash t = t.t_tag
478

479
480
  let f_hash_branch (p,b,f) =
    Hashcons.combine p.pat_tag (bnd_hash b f.f_tag)
481

482
483
  let f_hash_bound (v,b,f) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
484

485
  let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
486

487
488
  let f_hash_quant (vl,b,tl,f) =
    let h = bnd_hash b f.f_tag in
489
    let h = Hashcons.combine_list v_hash h vl in
490
    List.fold_left (Hashcons.combine_list tr_hash) h tl
491

492
  let f_hash_node = function
493
494
495
    | Fapp (p,tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
    | Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
    | Fbinop (op,f1,f2) ->
496
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
497
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498
499
    | Ftrue -> 0
    | Ffalse -> 1
500
501
502
    | Fif (f1,f2,f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
    | Flet (t,bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
    | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch t.t_tag bl
503
504

  let hash f =
505
    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
506

507
  let tag n f = { f with f_tag = n }
508

509
510
511
512
513
514
end)

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

516
517
518
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
519

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

522
523
let mk_term n ty = Hsterm.hashcons {
  t_node = n; t_label = []; t_ty = ty; t_tag = -1 }
524

525
526
527
528
529
530
531
532
533
534
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
535
536
537

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 }
538
539
540

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

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

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

546
547
548
549
550
551
552
553
554
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
555

556
557
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 }
558
559
560

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
561

562
563
564
565
566
let f_and     = f_binary Fand
let f_or      = f_binary For
let f_implies = f_binary Fimplies
let f_iff     = f_binary Fiff

Andrei Paskevich's avatar
Andrei Paskevich committed
567
568
569
570
571
572
573
574
575
576
577
(* built-in symbols *)

let ps_equ =
  let v = ty_var (create_tvsymbol (id_fresh "a")) in
  create_psymbol (id_fresh "infix =") [v; v]

let ps_neq =
  let v = ty_var (create_tvsymbol (id_fresh "a")) in
  create_psymbol (id_fresh "infix <>") [v; v]

let f_app p tl =
578
  if ls_equal p ps_neq then f_not (f_app ps_equ tl) else f_app p tl
Andrei Paskevich's avatar
Andrei Paskevich committed
579

Simon Cruanes's avatar
Simon Cruanes committed
580
581
582
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]

583
584
let fs_tuple n =
  let tyl = ref [] in
585
  for i = 1 to n
586
  do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
587
588
589
590
591
  let ty = ty_tuple !tyl in
  create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty

let fs_tuple = Util.memo fs_tuple

592
593
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)

594
595
596
597
let t_tuple tl =
  let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
  t_app (fs_tuple (List.length tl)) tl ty

598
(* unsafe map *)
599

600
let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)
601

602
603
604
605
606
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
607
  | Tcase (e,bl) -> t_case (fnT e) (List.map (bound_map fnT fnT) bl) t.t_ty
608
  | Teps b -> t_eps (bound_map fnT fnF b) t.t_ty)
609

610
611
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)
612
613
  | Fquant (q,(vl,b,tl,f1)) ->
      f_quant q (vl, bnd_map fnT b, tr_map fnT fnF tl, fnF f1)
614
615
616
617
618
  | 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)
619
  | Fcase (e,bl) -> f_case (fnT e) (List.map (bound_map fnT fnF) bl))
620

621
(* unsafe fold *)
622

623
let bound_fold fnT fnE acc (_,b,e) = fnE (bnd_fold fnT acc b) e
624

625
626
627
628
629
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
630
  | Tcase (e,bl) -> List.fold_left (bound_fold fnT fnT) (fnT acc e) bl
631
632
633
634
  | 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
635
  | Fquant (_,(_,b,tl,f1)) -> fnF (tr_fold fnT fnF (bnd_fold fnT acc b) tl) f1
636
637
638
639
640
  | 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
641
  | Fcase (e,bl) -> List.fold_left (bound_fold fnT fnF) (fnT acc e) bl
642

643
644
645
646
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
647

648
649
let t_all_unsafe prT prF t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) true t
650
651
  with FoldSkip -> false

652
653
let f_all_unsafe prT prF f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) true f
654
655
  with FoldSkip -> false

656
657
let t_any_unsafe prT prF t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) false t
658
659
  with FoldSkip -> true

660
661
let f_any_unsafe prT prF f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) false f
662
663
  with FoldSkip -> true

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
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
(* 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)

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

728
let rec t_abst m l lvl t = t_label_copy t (match t.t_node with
729
730
  | Tvar u -> begin try
      let i = Mvs.find u m in
Andrei Paskevich's avatar
Andrei Paskevich committed
731
      l := Sint.add i !l;
732
733
      t_bvar (i + lvl) t.t_ty
      with Not_found -> t end
734
735
736
737
738
739
740
741
742
  | 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
743
  | _ ->
744
745
746
747
748
749
750
751
752
753
754
      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)
755
  | _ ->
756
757
758
      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
759
760
  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
761
  update_bv m l lvl l' bv, t
762
763

and bnd_f_abst m l lvl bv f =
Andrei Paskevich's avatar
Andrei Paskevich committed
764
765
  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
766
  update_bv m l lvl l' bv, f
767
768

and bnd_q_abst m l lvl (vl,bv,tl,f) =
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
769
  let l' = ref Sint.empty and lvl' = lvl + bv.bv_bound in
Andrei Paskevich's avatar
Andrei Paskevich committed
770
771
  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
772
  vl, update_bv m l lvl l' bv, tl, f
Andrei Paskevich's avatar
Andrei Paskevich committed
773

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
774
and update_bv m l lvl l' bv =
Andrei Paskevich's avatar
Andrei Paskevich committed
775
  l := Sint.union !l' !l;
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
776
  let bv = bnd_map (t_abst m l lvl) bv in
Andrei Paskevich's avatar
Andrei Paskevich committed
777
778
  let add i acc = Sint.add (i + lvl) acc in
  { bv with bv_open = Sint.fold add !l' bv.bv_open }
779

Andrei Paskevich's avatar
Andrei Paskevich committed
780
781
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
782
783
784

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

785
exception UnboundIndex
786

787
788
let bnd_find i m =
  try Mint.find i m with Not_found -> raise UnboundIndex
789

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
790
791
792
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 }
793

794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
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)
817

818
and bound_inst m nv b = bnd_inst m nv (bnd_map (t_inst m nv) b)
819
820
821

(* close bindings *)

822
823
824
825
826
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)
827
828
829
830
831
832
833
834
835
836
837
838
839

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 =
840
  let m,nv = pat_varmap pat in
841
  (pat, bnd_new nv, if nv = 0 then t else t_abst m t)
842
843

let f_close_branch pat f =
844
  let m,nv = pat_varmap pat in
845
  (pat, bnd_new nv, if nv = 0 then f else f_abst m f)
846
847

let f_close_quant vl tl f =
848
  if vl = [] then (vl, bnd_new 0, tl, f) else
849
850
851
852
853
854
  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
855
  (vl, bnd_new (!i + 1), tr_map (t_abst m) (f_abst m) tl, f_abst m f)
856
857
858

(* open bindings *)

859
860
861
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
862

863
864
865
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
866
867
868
869
870
871
872
873
874
875
876
877

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)

878
let t_open_branch (p,b,t) =
879
  if b.bv_bound = 0 then (p, t) else
880
881
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, t_inst m b.bv_bound t
882

883
let f_open_branch (p,b,f) =
884
  if b.bv_bound = 0 then (p, f) else
885
886
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, f_inst m b.bv_bound f
887

888
889
let quant_vars vl s =
  let i = ref (-1) in
890
891
  let add m v = let v = fresh_vsymbol v in
    incr i; Mint.add !i (t_var v) m, v in