term.ml 49.8 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 mk_ls name args value = {
  ls_name   = name;
70
71
  ls_args   = args;
  ls_value  = value;
72
73
}

74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
let lsymbol_table = Wid.create 63

let create_lsymbol name args value =
  let id = id_register name in
  let ls = mk_ls id args value in
  let wa = Weak.create 1 in
  Weak.set wa 0 (Some ls);
  Wid.set lsymbol_table id wa;
  ls

let find_lsymbol id =
  match Weak.get (Wid.find lsymbol_table id) 0 with
  | Some ls -> ls
  | None -> raise Not_found

89
90
let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)
91

92
(** Patterns *)
93
94
95

type pattern = {
  pat_node : pattern_node;
96
  pat_ty : ty;
97
98
99
  pat_tag : int;
}

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

106
107
let pat_equal = (==)

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

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

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

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

125
  let hash_node = function
126
    | Pwild -> 0
127
    | Pvar v -> v.vs_name.id_tag
128
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
129
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
130

131
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
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

147
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
148
149
150
151
let pat_wild ty = Hspat.hashcons (mk_pattern Pwild ty)
let pat_var v = Hspat.hashcons (mk_pattern (Pvar v) v.vs_ty)
let pat_app f pl ty = Hspat.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p v = Hspat.hashcons (mk_pattern (Pas (p, v)) p.pat_ty)
152

153
154
(* generic traversal functions *)

155
let pat_map fn pat = match pat.pat_node with
156
157
158
159
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v

160
161
162
let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

163
164
let protect fn pat =
  let res = fn pat in
165
  check_ty_equal pat.pat_ty res.pat_ty;
166
167
168
169
  res

let pat_map fn = pat_map (protect fn)

170
171
172
173
174
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

175
176
let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false
177

178
179
let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true
180

181
182
183
184
185
186
let rec pat_freevars s pat = match pat.pat_node with
  | Pwild -> s
  | Pvar v -> Svs.add v s
  | Pas (p, v) -> pat_freevars (Svs.add v s) p
  | Papp (_,pl) -> List.fold_left pat_freevars s pl

187
188
(* smart constructors for patterns *)

189
exception BadArity of lsymbol * int * int
190
191
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
192
193

let pat_app fs pl ty =
194
  let s = match fs.ls_value with
195
    | Some vty -> ty_match Mtv.empty vty ty
196
197
    | None -> raise (FunctionSymbolExpected fs)
  in
198
  let mtch s ty p = ty_match s ty p.pat_ty in
199
  ignore (try List.fold_left2 mtch s fs.ls_args pl
200
    with Invalid_argument _ -> raise (BadArity
201
      (fs, List.length fs.ls_args, List.length pl)));
202
  pat_app fs pl ty
203
204

let pat_as p v =
205
  check_ty_equal p.pat_ty v.vs_ty;
206
  pat_as p v
207

208
209
(* symbol-wise map/fold *)

210
211
let rec pat_s_map fnT fnV fnL pat =
  let fn p = pat_s_map fnT fnV fnL p in
212
  let ty = fnT pat.pat_ty in
213
214
215
  match pat.pat_node with
    | Pwild -> pat_wild ty
    | Pvar v -> pat_var (fnV v ty)
216
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
Andrei Paskevich's avatar
Andrei Paskevich committed
217
    | Pas (p, v) -> pat_as (fn p) (fnV v ty)
218

219
220
let rec pat_s_fold fnT fnL acc pat =
  let fn acc p = pat_s_fold fnT fnL acc p in
221
222
  let acc = ty_s_fold fnT acc pat.pat_ty in
  match pat.pat_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
223
    | Pwild | Pvar _ -> acc
224
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
225
    | Pas (p, _) -> fn acc p
226

227
228
(** Terms and formulas *)

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
229
230
type label = string

231
232
233
234
235
236
237
238
239
240
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

241
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242
243
244
245
246
247
248
  | 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
249
250
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251
  t_label : label list;
252
253
254
255
256
257
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258
  f_label : label list;
259
260
261
  f_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
262
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263
  | Tbvar of int
264
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
  | Tconst of constant
266
  | Tapp of lsymbol * term list
267
  | Tif of fmla * term * term
268
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
269
  | Tcase of term list * term_branch list
270
  | Teps of fmla_bound
271

Andrei Paskevich's avatar
Andrei Paskevich committed
272
and fmla_node =
273
  | Fapp of lsymbol * term list
274
  | Fquant of quant * fmla_quant
275
  | Fbinop of binop * fmla * fmla
276
  | Fnot of fmla
277
278
279
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
280
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
281
  | Fcase of term list * fmla_branch list
282

283
and term_bound = vsymbol * term
284

285
and fmla_bound = vsymbol * fmla
286

287
288
and fmla_quant = vsymbol list * int * trigger list * fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
289
and term_branch = pattern list * int * term
290

Andrei Paskevich's avatar
Andrei Paskevich committed
291
and fmla_branch = pattern list * int * fmla
292

293
294
295
and expr =
  | Term of term
  | Fmla of fmla
296

297
and trigger = expr list
298

299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
(* 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

let tr_equal  = list_all2 e_equal
let trl_equal = list_all2 tr_equal

314
(* expr and trigger traversal *)
315

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

320
321
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))
322

323
module Hsterm = Hashcons.Make (struct
324

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
325
326
  type t = term

327
328
  let t_eq_branch (pl1,_,t1) (pl2,_,t2) =
    list_all2 pat_equal pl1 pl2 && t_equal t1 t2
329

330
331
  let t_eq_bound (v1, t1) (v2, t2) = vs_equal v1 v2 && t_equal t1 t2
  let f_eq_bound (v1, f1) (v2, f2) = vs_equal v1 v2 && f_equal f1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
332

333
  let t_equal_node t1 t2 = match t1, t2 with
334
335
    | 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
336
    | Tconst c1, Tconst c2 -> c1 = c2
337
338
339
340
341
342
    | Tapp (s1, l1), Tapp (s2, l2) ->
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
    | Tif (f1, t1, e1), Tif (f2, t2, e2) ->
        f_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2
    | Tlet (t1, b1), Tlet (t2, b2) ->
        t_equal t1 t2 && t_eq_bound b1 b2
Andrei Paskevich's avatar
Andrei Paskevich committed
343
    | Tcase (tl1, bl1), Tcase (tl2, bl2) ->
344
        list_all2 t_equal tl1 tl2 && list_all2 t_eq_branch bl1 bl2
345
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
346
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347

348
  let equal t1 t2 =
349
    t_equal_node t1.t_node t2.t_node &&
350
    t_equal t1.t_ty t2.t_ty && list_all2 (=) t1.t_label t2.t_label
351

Andrei Paskevich's avatar
Andrei Paskevich committed
352
353
354
  let p_hash p = p.pat_tag

  let t_hash_branch (pl,_,t) = Hashcons.combine_list p_hash t.t_tag pl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355

356
  let t_hash_bound (v, t) = Hashcons.combine v.vs_name.id_tag t.t_tag
357

358
  let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag f.f_tag
359

360
  let t_hash t = t.t_tag
361

362
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
363
    | Tbvar n -> n
364
    | Tvar v -> v.vs_name.id_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
365
    | Tconst c -> Hashtbl.hash c
366
    | Tapp (f, tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
367
    | Tif (f, t, e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
368
    | Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
Andrei Paskevich's avatar
Andrei Paskevich committed
369
370
    | Tcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list t_hash_branch ht bl
371
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
372

373
  let hash t =
374
    Hashcons.combine (t_hash_node t.t_node)
375
      (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
376

377
  let tag n t = { t with t_tag = n }
378

379
end)
380

381
382
383
384
385
386
387
388
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
389

390
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391
392
393

  type t = fmla

394
395
  let f_eq_branch (pl1,_,f1) (pl2,_,f2) =
    list_all2 pat_equal pl1 pl2 && f_equal f1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
396

397
  let f_eq_bound (v1, f1) (v2, f2) = vs_equal v1 v2 && f_equal f1 f2
398

Andrei Paskevich's avatar
Andrei Paskevich committed
399
  let f_eq_quant (vl1, _, tl1, f1) (vl2, _, tl2, f2) =
400
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 && trl_equal tl1 tl2
401

402
  let f_equal_node f1 f2 = match f1, f2 with
403
    | Fapp (s1, l1), Fapp (s2, l2) ->
404
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
405
    | Fquant (q1, b1), Fquant (q2, b2) ->
406
        q1 = q2 && f_eq_quant b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
408
        op1 = op2 && f_equal f1 f2 && f_equal g1 g2
409
    | Fnot f1, Fnot f2 ->
410
        f_equal f1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
411
    | Ftrue, Ftrue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
    | Ffalse, Ffalse ->
Andrei Paskevich's avatar
Andrei Paskevich committed
413
        true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
415
        f_equal f1 f2 && f_equal g1 g2 && f_equal h1 h2
416
    | Flet (t1, b1), Flet (t2, b2) ->
417
        t_equal t1 t2 && f_eq_bound b1 b2
Andrei Paskevich's avatar
Andrei Paskevich committed
418
    | Fcase (tl1, bl1), Fcase (tl2, bl2) ->
419
        list_all2 t_equal tl1 tl2 && list_all2 f_eq_branch bl1 bl2
Andrei Paskevich's avatar
Andrei Paskevich committed
420
421
    | _ ->
        false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422

423
  let equal f1 f2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
424
    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
425

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

Andrei Paskevich's avatar
Andrei Paskevich committed
428
  let p_hash p = p.pat_tag
429

Andrei Paskevich's avatar
Andrei Paskevich committed
430
  let t_hash t = t.t_tag
431

Andrei Paskevich's avatar
Andrei Paskevich committed
432
  let f_hash_branch (pl,_,f) = Hashcons.combine_list p_hash f.f_tag pl
433
434
435

  let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag f.f_tag

436
  let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
437

438
439
  let f_hash_quant (vl, _, tl, f) =
    let h = Hashcons.combine_list v_hash f.f_tag vl in
440
    List.fold_left (Hashcons.combine_list tr_hash) h tl
441

442
  let f_hash_node = function
443
    | Fapp (p, tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
444
    | Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
445
    | Fbinop (op, f1, f2) ->
446
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
447
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448
449
    | Ftrue -> 0
    | Ffalse -> 1
450
    | Fif (f1, f2, f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
451
    | Flet (t, bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
    | Fcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list f_hash_branch ht bl
454
455

  let hash f =
456
    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
457

458
  let tag n f = { f with f_tag = n }
459

460
461
462
463
464
465
end)

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

467
468
469
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
470

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

473
474
475
476
477
478
479
480
481
482
483
484
485
let mk_term n ty = Hsterm.hashcons
  { t_node = n; t_label = []; t_ty = ty; t_tag = -1 }

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 v t1 t2   = mk_term (Tlet (t1, (v, t2))) t2.t_ty
let t_case tl bl ty = mk_term (Tcase (tl, bl)) ty
let t_eps u f       = mk_term (Teps (u, f)) u.vs_ty
486
487
488

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 }
489
let t_label_copy { t_label = l } t = if l = [] then t else t_label l t
490

491
492
let t_app_unsafe = t_app

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

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

497
498
499
500
501
502
503
504
505
let f_app f tl          = mk_fmla (Fapp (f, tl))
let f_quant q ul n tl f = mk_fmla (Fquant (q, (ul,n,tl,f)))
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 v t f         = mk_fmla (Flet (t, (v, f)))
let f_case tl bl        = mk_fmla (Fcase (tl, bl))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
506

507
508
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 }
509
let f_label_copy { f_label = l } f = if l = [] then f else f_label l f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
510

511
512
513
514
515
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
516
517
518
519
520
521
522
523
524
525
526
(* 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 =
527
  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
528

Simon Cruanes's avatar
Simon Cruanes committed
529
530
531
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]

532
533
let f_app_unsafe = f_app

534
535
let fs_tuple n =
  let tyl = ref [] in
536
  for i = 1 to n
537
  do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
538
539
540
541
542
  let ty = ty_tuple !tyl in
  create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty

let fs_tuple = Util.memo fs_tuple

543
544
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)

545
546
547
548
549
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


550
551
(* unsafe map with level *)

552
553
exception UnboundIndex

554
555
let brlvl fn lvl (pat, nv, t) = (pat, nv, fn (lvl + nv) t)

556
let t_map_unsafe fnT fnF lvl t = t_label_copy t (match t.t_node with
557
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
558
  | Tbvar _ | Tvar _ | Tconst _ -> t
559
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
560
  | Tif (f, t1, t2) -> t_if (fnF lvl f) (fnT lvl t1) (fnT lvl t2)
561
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
562
563
  | Tcase (tl, bl) ->
      t_case (List.map (fnT lvl) tl) (List.map (brlvl fnT lvl) bl) t.t_ty
564
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f))
565

566
let f_map_unsafe fnT fnF lvl f = f_label_copy f (match f.f_node with
567
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
568
  | Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in
569
      f_quant q vl nv (tr_map (fnT lvl) (fnF lvl) tl) (fnF lvl f1)
570
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
571
  | Fnot f1 -> f_not (fnF lvl f1)
572
573
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
574
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
575
576
  | Fcase (tl, bl) ->
      f_case (List.map (fnT lvl) tl) (List.map (brlvl fnF lvl) bl))
577

578
579
let protect fn lvl t =
  let res = fn lvl t in
580
  check_ty_equal t.t_ty res.t_ty;
581
582
583
584
585
  res

let t_map_unsafe fnT = t_map_unsafe (protect fnT)
let f_map_unsafe fnT = f_map_unsafe (protect fnT)

586
587
588
589
(* unsafe fold with level *)

let brlvl fn lvl acc (_, nv, t) = fn (lvl + nv) acc t

590
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
591
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
592
  | Tbvar _ | Tvar _ | Tconst _ -> acc
593
  | Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl
594
  | Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2
595
  | Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
596
597
  | Tcase (tl, bl) ->
      List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl
598
  | Teps (_, f) -> fnF (lvl + 1) acc f
599

600
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
601
602
  | Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl
  | Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in
603
      tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl
604
  | Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
605
606
607
  | Fnot f1 -> fnF lvl acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
608
  | Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
Andrei Paskevich's avatar
Andrei Paskevich committed
609
610
  | Fcase (tl, bl) ->
      List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl
611

612
613
614
615
let all_fnT prT lvl _ t = prT lvl t || raise FoldSkip
let all_fnF prF lvl _ f = prF lvl f || raise FoldSkip
let any_fnT prT lvl _ t = prT lvl t && raise FoldSkip
let any_fnF prF lvl _ f = prF lvl f && raise FoldSkip
616

617
618
let t_all_unsafe prT prF lvl t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true t
619
620
  with FoldSkip -> false

621
622
let f_all_unsafe prT prF lvl f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true f
623
624
  with FoldSkip -> false

625
626
let t_any_unsafe prT prF lvl t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false t
627
628
  with FoldSkip -> true

629
630
let f_any_unsafe prT prF lvl f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false f
631
632
  with FoldSkip -> true

633
634
(* unsafe constructors with type checking *)

635
let t_app_inst fs tl ty =
636
  let s = match fs.ls_value with
637
    | Some vty -> ty_match Mtv.empty vty ty
638
639
    | _ -> raise (FunctionSymbolExpected fs)
  in
640
  let mtch s ty t = ty_match s ty t.t_ty in
641
  try List.fold_left2 mtch s fs.ls_args tl
642
643
  with Invalid_argument _ -> raise (BadArity
    (fs, List.length fs.ls_args, List.length tl))
644
645

let t_app fs tl ty = ignore (t_app_inst fs tl ty); t_app fs tl ty
646

647
648
649
650
let t_app_infer fs tl =
  let mtch s ty t = ty_match s ty t.t_ty in
  let s =
    try List.fold_left2 mtch Mtv.empty fs.ls_args tl
651
    with Invalid_argument _ -> raise (BadArity
652
      (fs, List.length fs.ls_args, List.length tl))
653
654
655
656
657
658
659
  in
  let ty = match fs.ls_value with
    | Some ty -> ty_inst s ty
    | _ -> raise (FunctionSymbolExpected fs)
  in
  t_app_unsafe fs tl ty

660
let f_app_inst ps tl =
661
  let s = match ps.ls_value with
662
    | None -> Mtv.empty
663
664
    | _ -> raise (PredicateSymbolExpected ps)
  in
665
  let mtch s ty t = ty_match s ty t.t_ty in
666
  try List.fold_left2 mtch s ps.ls_args tl
667
668
  with Invalid_argument _ -> raise (BadArity
    (ps, List.length ps.ls_args, List.length tl))
669
670

let f_app ps tl = ignore (f_app_inst ps tl); f_app ps tl
671

Andrei Paskevich's avatar
Andrei Paskevich committed
672
let p_check t p =
673
  check_ty_equal p.pat_ty t.t_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
674
675
676

let t_case tl bl ty =
  let t_check_branch (pl,_,tbr) =
677
    check_ty_equal ty tbr.t_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
678
    List.iter2 p_check tl pl
679
680
  in
  List.iter t_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
681
  t_case tl bl ty
682

Andrei Paskevich's avatar
Andrei Paskevich committed
683
684
685
let f_case tl bl =
  let f_check_branch (pl,_,_) =
    List.iter2 p_check tl pl
686
687
  in
  List.iter f_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
688
  f_case tl bl
689

690
let t_if f t1 t2 =
691
  check_ty_equal t1.t_ty t2.t_ty;
692
693
  t_if f t1 t2

694
let t_let v t1 t2 =
695
  check_ty_equal v.vs_ty t1.t_ty;
696
  t_let v t1 t2
697
698

let f_let v t1 f2 =
699
  check_ty_equal v.vs_ty t1.t_ty;
700
  f_let v t1 f2
701

702
(* generic map over types, symbols and variables *)
703

704
705
706
let rec t_gen_map fnT fnB fnV fnL t =
  let fn_t = t_gen_map fnT fnB fnV fnL in
  let fn_f = f_gen_map fnT fnB fnV fnL in
707
  let ty = fnT t.t_ty in
708
  t_label_copy t (match t.t_node with
709
    | Tbvar n -> t_bvar n ty
710
    | Tvar v -> fnV v ty
711
712
    | Tconst _ -> t
    | Tapp (f, tl) -> t_app (fnL f) (List.map fn_t tl) ty
713
    | Tif (f, t1, t2) -> t_if (fn_f f) (fn_t t1) (fn_t t2)
714
    | Tlet (t1, (u, t2)) ->
715
        let t1 = fn_t t1 in t_let (fnB u t1.t_ty) t1 (fn_t t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
716
    | Tcase (tl, bl) ->
717
        let fn_b = t_branch fnT fnB fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
718
        t_case (List.map fn_t tl) (List.map fn_b bl) ty
719
    | Teps (u, f) -> t_eps (fnB u ty) (fn_f f))
720

721
722
723
and f_gen_map fnT fnB fnV fnL f =
  let fn_t = t_gen_map fnT fnB fnV fnL in
  let fn_f = f_gen_map fnT fnB fnV fnL in
724
  f_label_copy f (match f.f_node with
725
726
727
    | Fapp (p, tl) -> f_app (fnL p) (List.map fn_t tl)
    | Fquant (q, (vl, nv, tl, f1)) ->
        let tl = tr_map fn_t fn_f tl in
728
        let fn_v u = fnB u (fnT u.vs_ty) in
729
730
731
732
733
734
        f_quant q (List.map fn_v vl) nv tl (fn_f f1)
    | Fbinop (op, f1, f2) -> f_binary op (fn_f f1) (fn_f f2)
    | Fnot f1 -> f_not (fn_f f1)
    | Ftrue | Ffalse -> f
    | Fif (f1, f2, f3) -> f_if (fn_f f1) (fn_f f2) (fn_f f3)
    | Flet (t, (u, f1)) ->
735
        let t1 = fn_t t in f_let (fnB u t1.t_ty) t1 (fn_f f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
736
    | Fcase (tl, bl) ->
737
        let fn_b = f_branch fnT fnB fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
738
739
        f_case (List.map fn_t tl) (List.map fn_b bl))

740
741
and t_branch fnT fnB fnV fnL (pl, nv, t) =
  (List.map (pat_s_map fnT fnB fnL) pl, nv, t_gen_map fnT fnB fnV fnL t)
742

743
744
and f_branch fnT fnB fnV fnL (pl, nv, f) =
  (List.map (pat_s_map fnT fnB fnL) pl, nv, f_gen_map fnT fnB fnV fnL f)
745
746
747
748
749
750
751
752
753
754
755

let get_fnT fn =
  let ht = Hashtbl.create 17 in
  let fnT ty =
    try Hashtbl.find ht ty.ty_tag with Not_found ->
      let nt = ty_s_map fn ty in
      Hashtbl.add ht ty.ty_tag nt;
      nt
  in
  fnT

756
let get_fnB () =
757
758
  let ht = Hid.create 17 in
  let fnV vs ty =
759
    if ty_equal vs.vs_ty ty then vs else
760
761
762
763
764
765
766
      try Hid.find ht vs.vs_name with Not_found ->
        let nv = create_vsymbol (id_dup vs.vs_name) ty in
        Hid.add ht vs.vs_name nv;
        nv
  in
  fnV

767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
let get_fnV () =
  let fnB = get_fnB () in
  fun vs ty -> t_var (fnB vs ty)

let t_s_map fnT fnL t = t_gen_map (get_fnT fnT) (get_fnB ()) (get_fnV ()) fnL t
let f_s_map fnT fnL f = f_gen_map (get_fnT fnT) (get_fnB ()) (get_fnV ()) fnL f

(* simultaneous substitution into types and terms *)

let t_ty_subst mapT mapV t =
  let fnV vs _ty = try Mvs.find vs mapV with Not_found -> t_var vs in
  t_gen_map (ty_inst mapT) (get_fnB ()) fnV (fun ls -> ls) t

let f_ty_subst mapT mapV f =
  let fnV vs _ty = try Mvs.find vs mapV with Not_found -> t_var vs in
  f_gen_map (ty_inst mapT) (get_fnB ()) fnV (fun ls -> ls) f
783
784
785
786
787
788
789
790
791
792

(* fold over symbols *)

let rec t_s_fold fnT fnL acc t =
  let fn_t = t_s_fold fnT fnL in
  let fn_f = f_s_fold fnT fnL in
  let acc = ty_s_fold fnT acc t.t_ty in
  match t.t_node with
    | Tbvar _ | Tvar _ | Tconst _ -> acc
    | Tapp (f, tl) -> List.fold_left fn_t (fnL acc f) tl
793
    | Tif (f, t1, t2) -> fn_t (fn_t (fn_f acc f) t1) t2
794
    | Tlet (t1, (_,t2)) -> fn_t (fn_t acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
795
796
    | Tcase (tl, bl) ->
        List.fold_left (t_branch fnT fnL) (List.fold_left fn_t acc tl) bl
797
798
799
800
801
802
803
804
    | Teps (_,f) -> fn_f acc f

and f_s_fold fnT fnL acc f =
  let fn_t = t_s_fold fnT fnL in
  let fn_f = f_s_fold fnT fnL in
  let fn_v acc u = ty_s_fold fnT acc u.vs_ty in
  match f.f_node with
    | Fapp (p, tl) -> List.fold_left fn_t (fnL acc p) tl
805
    | Fquant (_, (vl,_,tl,f1)) ->
806
807
        let acc = List.fold_left fn_v acc vl in
        fn_f (tr_fold fn_t fn_f acc tl) f1
808
    | Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2
809
810
811
812
    | Fnot f1 -> fn_f acc f1
    | Ftrue | Ffalse -> acc
    | Fif (f1, f2, f3) -> fn_f (fn_f (fn_f acc f1) f2) f3
    | Flet (t, (_,f1)) -> fn_f (fn_t acc t) f1
Andrei Paskevich's avatar
Andrei Paskevich committed
813
814
815
816
817
    | Fcase (tl, bl) ->
        List.fold_left (f_branch fnT fnL) (List.fold_left fn_t acc tl) bl

and t_branch