term.ml 49.4 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
let create_lsymbol name args value = {
69
70
71
  ls_name   = id_register name;
  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;
81
  pat_ty : ty;
82
83
84
  pat_tag : int;
}

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

91
92
let pat_equal = (==)

93
module Hspat = Hashcons.Make (struct
94
  type t = pattern
95

96
  let equal_node p1 p2 = match p1, p2 with
97
    | Pwild, Pwild -> true
98
99
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
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
103
    | _ -> false
104

105
  let equal p1 p2 =
106
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
107

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

110
  let hash_node = function
111
    | Pwild -> 0
112
    | Pvar v -> v.vs_name.id_tag
113
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
114
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
115

116
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
117

118
  let tag n p = { p with pat_tag = n }
119
120
121
122
123
124
end)

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

126
127
128
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
129
130

(* h-consing constructors for patterns *)
131

132
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
133
134
135
136
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)
137

138
139
(* generic traversal functions *)

140
let pat_map fn pat = match pat.pat_node with
141
142
143
144
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v

145
146
147
let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

148
149
let protect fn pat =
  let res = fn pat in
150
  check_ty_equal pat.pat_ty res.pat_ty;
151
152
153
154
  res

let pat_map fn = pat_map (protect fn)

155
156
157
158
159
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

160
161
let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false
162

163
164
let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true
165

166
167
168
169
170
171
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

172
173
(* smart constructors for patterns *)

174
exception BadArity of int * int
175
176
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
177
178

let pat_app fs pl ty =
179
  let s = match fs.ls_value with
180
    | Some vty -> ty_match Mtv.empty vty ty
181
182
    | None -> raise (FunctionSymbolExpected fs)
  in
183
  let mtch s ty p = ty_match s ty p.pat_ty in
184
  ignore (try List.fold_left2 mtch s fs.ls_args pl
185
186
    with Invalid_argument _ -> raise (BadArity
      (List.length fs.ls_args, List.length pl)));
187
  pat_app fs pl ty
188
189

let pat_as p v =
190
  check_ty_equal p.pat_ty v.vs_ty;
191
  pat_as p v
192

193
194
(* symbol-wise map/fold *)

195
196
let rec pat_s_map fnT fnV fnL pat =
  let fn p = pat_s_map fnT fnV fnL p in
197
  let ty = fnT pat.pat_ty in
198
199
200
  match pat.pat_node with
    | Pwild -> pat_wild ty
    | Pvar v -> pat_var (fnV v ty)
201
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
Andrei Paskevich's avatar
Andrei Paskevich committed
202
    | Pas (p, v) -> pat_as (fn p) (fnV v ty)
203

204
205
let rec pat_s_fold fnT fnL acc pat =
  let fn acc p = pat_s_fold fnT fnL acc p in
206
207
  let acc = ty_s_fold fnT acc pat.pat_ty in
  match pat.pat_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
208
    | Pwild | Pvar _ -> acc
209
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
210
    | Pas (p, _) -> fn acc p
211

212
213
(** Terms and formulas *)

Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
214
215
type label = string

216
217
218
219
220
221
222
223
224
225
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

226
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227
228
229
230
231
232
233
  | 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
234
235
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236
  t_label : label list;
237
238
239
240
241
242
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243
  f_label : label list;
244
245
246
  f_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
247
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248
  | Tbvar of int
249
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
  | Tconst of constant
251
  | Tapp of lsymbol * term list
252
  | Tif of fmla * term * term
253
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
254
  | Tcase of term list * term_branch list
255
  | Teps of fmla_bound
256

Andrei Paskevich's avatar
Andrei Paskevich committed
257
and fmla_node =
258
  | Fapp of lsymbol * term list
259
  | Fquant of quant * fmla_quant
260
  | Fbinop of binop * fmla * fmla
261
  | Fnot of fmla
262
263
264
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
265
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  | Fcase of term list * fmla_branch list
267

268
and term_bound = vsymbol * term
269

270
and fmla_bound = vsymbol * fmla
271

272
273
and fmla_quant = vsymbol list * int * trigger list * fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
274
and term_branch = pattern list * int * term
275

Andrei Paskevich's avatar
Andrei Paskevich committed
276
and fmla_branch = pattern list * int * fmla
277

278
279
280
and expr =
  | Term of term
  | Fmla of fmla
281

282
and trigger = expr list
283

284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
(* 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

299
(* expr and trigger traversal *)
300

301
302
303
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
304

305
306
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))
307

308
module Hsterm = Hashcons.Make (struct
309

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
310
311
  type t = term

312
313
  let t_eq_branch (pl1,_,t1) (pl2,_,t2) =
    list_all2 pat_equal pl1 pl2 && t_equal t1 t2
314

315
316
  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
317

318
  let t_equal_node t1 t2 = match t1, t2 with
319
320
    | 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
321
    | Tconst c1, Tconst c2 -> c1 = c2
322
323
324
325
326
327
    | 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
328
    | Tcase (tl1, bl1), Tcase (tl2, bl2) ->
329
        list_all2 t_equal tl1 tl2 && list_all2 t_eq_branch bl1 bl2
330
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
331
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332

333
  let equal t1 t2 =
334
    t_equal_node t1.t_node t2.t_node &&
335
    t_equal t1.t_ty t2.t_ty && list_all2 (=) t1.t_label t2.t_label
336

Andrei Paskevich's avatar
Andrei Paskevich committed
337
338
339
  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
340

341
  let t_hash_bound (v, t) = Hashcons.combine v.vs_name.id_tag t.t_tag
342

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

345
  let t_hash t = t.t_tag
346

347
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
    | Tbvar n -> n
349
    | Tvar v -> v.vs_name.id_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350
    | Tconst c -> Hashtbl.hash c
351
    | Tapp (f, tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
352
    | Tif (f, t, e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
353
    | Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
Andrei Paskevich's avatar
Andrei Paskevich committed
354
355
    | Tcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list t_hash_branch ht bl
356
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
357

358
  let hash t =
359
    Hashcons.combine (t_hash_node t.t_node)
360
      (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
361

362
  let tag n t = { t with t_tag = n }
363

364
end)
365

366
367
368
369
370
371
372
373
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
374

375
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
376
377
378

  type t = fmla

379
380
  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
381

382
  let f_eq_bound (v1, f1) (v2, f2) = vs_equal v1 v2 && f_equal f1 f2
383

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

387
  let f_equal_node f1 f2 = match f1, f2 with
388
    | Fapp (s1, l1), Fapp (s2, l2) ->
389
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
390
    | Fquant (q1, b1), Fquant (q2, b2) ->
391
        q1 = q2 && f_eq_quant b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
392
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
393
        op1 = op2 && f_equal f1 f2 && f_equal g1 g2
394
    | Fnot f1, Fnot f2 ->
395
        f_equal f1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
396
    | Ftrue, Ftrue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
397
    | Ffalse, Ffalse ->
Andrei Paskevich's avatar
Andrei Paskevich committed
398
        true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
400
        f_equal f1 f2 && f_equal g1 g2 && f_equal h1 h2
401
    | Flet (t1, b1), Flet (t2, b2) ->
402
        t_equal t1 t2 && f_eq_bound b1 b2
Andrei Paskevich's avatar
Andrei Paskevich committed
403
    | Fcase (tl1, bl1), Fcase (tl2, bl2) ->
404
        list_all2 t_equal tl1 tl2 && list_all2 f_eq_branch bl1 bl2
Andrei Paskevich's avatar
Andrei Paskevich committed
405
406
    | _ ->
        false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407

408
  let equal f1 f2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
409
    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
410

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

Andrei Paskevich's avatar
Andrei Paskevich committed
413
  let p_hash p = p.pat_tag
414

Andrei Paskevich's avatar
Andrei Paskevich committed
415
  let t_hash t = t.t_tag
416

Andrei Paskevich's avatar
Andrei Paskevich committed
417
  let f_hash_branch (pl,_,f) = Hashcons.combine_list p_hash f.f_tag pl
418
419
420

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

421
  let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
422

423
424
  let f_hash_quant (vl, _, tl, f) =
    let h = Hashcons.combine_list v_hash f.f_tag vl in
425
    List.fold_left (Hashcons.combine_list tr_hash) h tl
426

427
  let f_hash_node = function
428
    | Fapp (p, tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
429
    | Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
430
    | Fbinop (op, f1, f2) ->
431
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
432
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433
434
    | Ftrue -> 0
    | Ffalse -> 1
435
    | Fif (f1, f2, f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
436
    | Flet (t, bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
437
438
    | Fcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list f_hash_branch ht bl
439
440

  let hash f =
441
    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
442

443
  let tag n f = { f with f_tag = n }
444

445
446
447
448
449
450
end)

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

452
453
454
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
455

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

458
459
460
461
462
463
464
465
466
467
468
469
470
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
471
472
473

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

476
477
let t_app_unsafe = t_app

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

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

482
483
484
485
486
487
488
489
490
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
491

492
493
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 }
494
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
495

496
497
498
499
500
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
501
502
503
504
505
506
507
508
509
510
511
(* 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 =
512
  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
513

Simon Cruanes's avatar
Simon Cruanes committed
514
515
516
let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]

517
518
let f_app_unsafe = f_app

519
520
let fs_tuple n =
  let tyl = ref [] in
521
522
  for i = 1 to n 
  do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
523
524
525
526
527
  let ty = ty_tuple !tyl in
  create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty

let fs_tuple = Util.memo fs_tuple

528
529
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)

530
531
532
533
534
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


535
536
(* unsafe map with level *)

537
538
exception UnboundIndex

539
540
let brlvl fn lvl (pat, nv, t) = (pat, nv, fn (lvl + nv) t)

541
let t_map_unsafe fnT fnF lvl t = t_label_copy t (match t.t_node with
542
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
543
  | Tbvar _ | Tvar _ | Tconst _ -> t
544
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
545
  | Tif (f, t1, t2) -> t_if (fnF lvl f) (fnT lvl t1) (fnT lvl t2)
546
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
547
548
  | Tcase (tl, bl) ->
      t_case (List.map (fnT lvl) tl) (List.map (brlvl fnT lvl) bl) t.t_ty
549
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f))
550

551
let f_map_unsafe fnT fnF lvl f = f_label_copy f (match f.f_node with
552
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
553
  | Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in
554
      f_quant q vl nv (tr_map (fnT lvl) (fnF lvl) tl) (fnF lvl f1)
555
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
556
  | Fnot f1 -> f_not (fnF lvl f1)
557
558
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
559
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
560
561
  | Fcase (tl, bl) ->
      f_case (List.map (fnT lvl) tl) (List.map (brlvl fnF lvl) bl))
562

563
564
let protect fn lvl t =
  let res = fn lvl t in
565
  check_ty_equal t.t_ty res.t_ty;
566
567
568
569
570
  res

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

571
572
573
574
(* unsafe fold with level *)

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

575
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
576
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
577
  | Tbvar _ | Tvar _ | Tconst _ -> acc
578
  | Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl
579
  | Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2
580
  | Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
581
582
  | Tcase (tl, bl) ->
      List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl
583
  | Teps (_, f) -> fnF (lvl + 1) acc f
584

585
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
586
587
  | Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl
  | Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in
588
      tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl
589
  | Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
590
591
592
  | Fnot f1 -> fnF lvl acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
593
  | Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
Andrei Paskevich's avatar
Andrei Paskevich committed
594
595
  | Fcase (tl, bl) ->
      List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl
596

597
598
599
600
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
601

602
603
let t_all_unsafe prT prF lvl t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true t
604
605
  with FoldSkip -> false

606
607
let f_all_unsafe prT prF lvl f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true f
608
609
  with FoldSkip -> false

610
611
let t_any_unsafe prT prF lvl t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false t
612
613
  with FoldSkip -> true

614
615
let f_any_unsafe prT prF lvl f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false f
616
617
  with FoldSkip -> true

618
619
(* unsafe constructors with type checking *)

620
let t_app_inst fs tl ty =
621
  let s = match fs.ls_value with
622
    | Some vty -> ty_match Mtv.empty vty ty
623
624
    | _ -> raise (FunctionSymbolExpected fs)
  in
625
  let mtch s ty t = ty_match s ty t.t_ty in
626
627
628
629
630
  try List.fold_left2 mtch s fs.ls_args tl
  with Invalid_argument _ -> 
    raise (BadArity (List.length fs.ls_args, List.length tl))

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

632
633
634
635
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
636
637
    with Invalid_argument _ -> raise (BadArity
      (List.length fs.ls_args, List.length tl))
638
639
640
641
642
643
644
  in
  let ty = match fs.ls_value with
    | Some ty -> ty_inst s ty
    | _ -> raise (FunctionSymbolExpected fs)
  in
  t_app_unsafe fs tl ty

645
let f_app_inst ps tl =
646
  let s = match ps.ls_value with
647
    | None -> Mtv.empty
648
649
    | _ -> raise (PredicateSymbolExpected ps)
  in
650
  let mtch s ty t = ty_match s ty t.t_ty in
651
652
653
654
655
  try List.fold_left2 mtch s ps.ls_args tl
  with Invalid_argument _ -> 
    raise (BadArity (List.length ps.ls_args, List.length tl))

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

Andrei Paskevich's avatar
Andrei Paskevich committed
657
let p_check t p =
658
  check_ty_equal p.pat_ty t.t_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
659
660
661

let t_case tl bl ty =
  let t_check_branch (pl,_,tbr) =
662
    check_ty_equal ty tbr.t_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
663
    List.iter2 p_check tl pl
664
665
  in
  List.iter t_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
666
  t_case tl bl ty
667

Andrei Paskevich's avatar
Andrei Paskevich committed
668
669
670
let f_case tl bl =
  let f_check_branch (pl,_,_) =
    List.iter2 p_check tl pl
671
672
  in
  List.iter f_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
673
  f_case tl bl
674

675
let t_if f t1 t2 =
676
  check_ty_equal t1.t_ty t2.t_ty;
677
678
  t_if f t1 t2

679
let t_let v t1 t2 =
680
  check_ty_equal v.vs_ty t1.t_ty;
681
  t_let v t1 t2
682
683

let f_let v t1 f2 =
684
  check_ty_equal v.vs_ty t1.t_ty;
685
  f_let v t1 f2
686

687
(* generic map over types, symbols and variables *)
688

689
690
691
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
692
  let ty = fnT t.t_ty in
693
  t_label_copy t (match t.t_node with
694
    | Tbvar n -> t_bvar n ty
695
    | Tvar v -> fnV v ty
696
697
    | Tconst _ -> t
    | Tapp (f, tl) -> t_app (fnL f) (List.map fn_t tl) ty
698
    | Tif (f, t1, t2) -> t_if (fn_f f) (fn_t t1) (fn_t t2)
699
    | Tlet (t1, (u, t2)) ->
700
        let t1 = fn_t t1 in t_let (fnB u t1.t_ty) t1 (fn_t t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
701
    | Tcase (tl, bl) ->
702
        let fn_b = t_branch fnT fnB fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
703
        t_case (List.map fn_t tl) (List.map fn_b bl) ty
704
    | Teps (u, f) -> t_eps (fnB u ty) (fn_f f))
705

706
707
708
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
709
  f_label_copy f (match f.f_node with
710
711
712
    | 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
713
        let fn_v u = fnB u (fnT u.vs_ty) in
714
715
716
717
718
719
        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)) ->
720
        let t1 = fn_t t in f_let (fnB u t1.t_ty) t1 (fn_f f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
721
    | Fcase (tl, bl) ->
722
        let fn_b = f_branch fnT fnB fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
723
724
        f_case (List.map fn_t tl) (List.map fn_b bl))

725
726
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)
727

728
729
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)
730
731
732
733
734
735
736
737
738
739
740

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

741
let get_fnB () =
742
743
  let ht = Hid.create 17 in
  let fnV vs ty =
744
    if ty_equal vs.vs_ty ty then vs else
745
746
747
748
749
750
751
      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

752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
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
768
769
770
771
772
773
774
775
776
777

(* 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
778
    | Tif (f, t1, t2) -> fn_t (fn_t (fn_f acc f) t1) t2
779
    | Tlet (t1, (_,t2)) -> fn_t (fn_t acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
780
781
    | Tcase (tl, bl) ->
        List.fold_left (t_branch fnT fnL) (List.fold_left fn_t acc tl) bl
782
783
784
785
786
787
788
789
    | 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
790
    | Fquant (_, (vl,_,tl,f1)) ->
791
792
        let acc = List.fold_left fn_v acc vl in
        fn_f (tr_fold fn_t fn_f acc tl) f1
793
    | Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2
794
795
796
797
    | 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
798
799
800
801
802
    | Fcase (tl, bl) ->
        List.fold_left (f_branch fnT fnL) (List.fold_left fn_t acc tl) bl

and t_branch fnT fnL acc (pl,_,t) =
  t_s_fold fnT fnL (List.fold_left (pat_s_fold fnT fnL) acc pl) t
803

Andrei Paskevich's avatar
Andrei Paskevich committed
804
805
and f_branch fnT fnL acc (pl,_,f) =
  f_s_fold fnT fnL (List.fold_left (pat_s_fold fnT fnL) acc pl) f
806
807
808
809
810
811
812
813
814
815
816
817
818

let t_s_all prT prL t =
  try t_s_fold (all_fn prT) (all_fn prL) true t with FoldSkip -> false

let f_s_all prT prL f =
  try f_s_fold (all_fn prT) (all_fn prL) true f with FoldSkip -> false

let t_s_any prT prL t =
  try t_s_fold (any_fn prT) (any_fn prL) false t with FoldSkip -> true

let f_s_any prT prL f =
  try f_s_fold (any_fn prT) (any_fn prL) false f with FoldSkip -> true

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

821
let rec t_abst m lvl t = match t.t_node with