term.ml 46.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 42 43
let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}
44

45
let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_ty
46

47
(** Function and predicate symbols *)
48

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

55
module Lsym = StructMake (struct
56
  type t = lsymbol
57 58 59 60 61 62
  let tag ls = ls.ls_name.id_tag
end)

module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H
63

64
let create_lsymbol name args value = {
65 66 67
  ls_name   = id_register name;
  ls_args   = args;
  ls_value  = value;
68 69
}

70 71
let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)
72

73
(** Patterns *)
74 75 76

type pattern = {
  pat_node : pattern_node;
77
  pat_ty : ty;
78 79 80
  pat_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
81 82 83
and pattern_node =
  | Pwild
  | Pvar of vsymbol
84
  | Papp of lsymbol * pattern list
85 86
  | Pas of pattern * vsymbol

87
module Hspat = Hashcons.Make (struct
88
  type t = pattern
89

90
  let equal_node p1 p2 = match p1, p2 with
91 92 93 94 95
    | Pwild, Pwild -> true
    | Pvar v1, Pvar v2 -> v1 == v2
    | Papp (s1, l1), Papp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
    | Pas (p1, n1), Pas (p2, n2) -> p1 == p2 && n1 == n2
    | _ -> false
96

97 98 99
  let equal p1 p2 =
    equal_node p1.pat_node p2.pat_node && p1.pat_ty == p2.pat_ty

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

102
  let hash_node = function
103
    | Pwild -> 0
104
    | Pvar v -> v.vs_name.id_tag
105
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
106
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
107

108
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
109

110
  let tag n p = { p with pat_tag = n }
111 112 113 114 115 116
end)

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

118 119 120
module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H
121 122

(* h-consing constructors for patterns *)
123

124
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
125 126 127 128
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)
129

130 131
(* generic traversal functions *)

132
let pat_map fn pat = match pat.pat_node with
133 134 135 136
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v

137 138 139 140 141 142 143
let protect fn pat =
  let res = fn pat in
  if res.pat_ty != pat.pat_ty then raise TypeMismatch;
  res

let pat_map fn = pat_map (protect fn)

144 145 146 147 148
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

149 150
let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false
151

152 153
let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true
154

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

161 162
(* smart constructors for patterns *)

163
exception BadArity of int * int
164 165
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
166 167

let pat_app fs pl ty =
168
  let s = match fs.ls_value with
169
    | Some vty -> ty_match Mtv.empty vty ty
170 171
    | None -> raise (FunctionSymbolExpected fs)
  in
172
  let mtch s ty p = ty_match s ty p.pat_ty in
173
  ignore (try List.fold_left2 mtch s fs.ls_args pl
174 175
    with Invalid_argument _ -> raise (BadArity
      (List.length fs.ls_args, List.length pl)));
176
  pat_app fs pl ty
177 178

let pat_as p v =
179 180
  if p.pat_ty != v.vs_ty then raise TypeMismatch;
  pat_as p v
181

182 183
(* symbol-wise map/fold *)

184 185
let rec pat_s_map fnT fnV fnL pat =
  let fn p = pat_s_map fnT fnV fnL p in
186
  let ty = fnT pat.pat_ty in
187 188 189
  match pat.pat_node with
    | Pwild -> pat_wild ty
    | Pvar v -> pat_var (fnV v ty)
190
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
Andrei Paskevich's avatar
Andrei Paskevich committed
191
    | Pas (p, v) -> pat_as (fn p) (fnV v ty)
192

193 194
let rec pat_s_fold fnT fnL acc pat =
  let fn acc p = pat_s_fold fnT fnL acc p in
195 196
  let acc = ty_s_fold fnT acc pat.pat_ty in
  match pat.pat_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
197
    | Pwild | Pvar _ -> acc
198
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
199
    | Pas (p, _) -> fn acc p
200

201 202
(** Terms and formulas *)

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
203 204
type label = string

205 206 207 208 209 210 211 212 213 214
type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

215
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216 217 218 219 220 221 222
  | 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
223 224
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
  t_label : label list;
226 227 228 229 230 231
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232
  f_label : label list;
233 234 235
  f_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
236
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237
  | Tbvar of int
238
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
  | Tconst of constant
240
  | Tapp of lsymbol * term list
241
  | Tif of fmla * term * term
242
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
243
  | Tcase of term list * term_branch list
244
  | Teps of fmla_bound
245

Andrei Paskevich's avatar
Andrei Paskevich committed
246
and fmla_node =
247
  | Fapp of lsymbol * term list
248
  | Fquant of quant * fmla_quant
249
  | Fbinop of binop * fmla * fmla
250
  | Fnot of fmla
251 252 253
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
254
  | Flet of term * fmla_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
255
  | Fcase of term list * fmla_branch list
256

257
and term_bound = vsymbol * term
258

259
and fmla_bound = vsymbol * fmla
260

261 262
and fmla_quant = vsymbol list * int * trigger list * fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
263
and term_branch = pattern list * int * term
264

Andrei Paskevich's avatar
Andrei Paskevich committed
265
and fmla_branch = pattern list * int * fmla
266

267 268 269
and expr =
  | Term of term
  | Fmla of fmla
270

271
and trigger = expr list
272

273
(* expr and trigger traversal *)
274

275 276 277
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
278

279 280
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))
281

282
module Hsterm = Hashcons.Make (struct
283

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284 285
  type t = term

Andrei Paskevich's avatar
Andrei Paskevich committed
286
  let t_eq_branch (pl1,_,t1) (pl2,_,t2) = list_all2 (==) pl1 pl2 && t1 == t2
Andrei Paskevich's avatar
Andrei Paskevich committed
287

288
  let t_eq_bound (v1, t1) (v2, t2) = v1 == v2 && t1 == t2
289

290
  let f_eq_bound (v1, f1) (v2, f2) = v1 == v2 && f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
291

292
  let t_equal_node t1 t2 = match t1, t2 with
293 294
    | Tbvar x1, Tbvar x2 -> x1 == x2
    | Tvar v1, Tvar v2 -> v1 == v2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295
    | Tconst c1, Tconst c2 -> c1 = c2
296
    | Tapp (s1, l1), Tapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
297
    | Tif (f1, t1, e1), Tif (f2, t2, e2) -> f1 == f2 && t1 == t2 && e1 == e2
298
    | Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2
Andrei Paskevich's avatar
Andrei Paskevich committed
299 300
    | Tcase (tl1, bl1), Tcase (tl2, bl2) ->
        list_all2 (==) tl1 tl2 && list_all2 t_eq_branch bl1 bl2
301
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
302
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303

304
  let equal t1 t2 =
305
    t_equal_node t1.t_node t2.t_node &&
Andrei Paskevich's avatar
Andrei Paskevich committed
306
    t1.t_ty == t2.t_ty && list_all2 (=) t1.t_label t2.t_label
307

Andrei Paskevich's avatar
Andrei Paskevich committed
308 309 310
  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
311

312
  let t_hash_bound (v, t) = Hashcons.combine v.vs_name.id_tag t.t_tag
313

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

316
  let t_hash t = t.t_tag
317

318
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319
    | Tbvar n -> n
320
    | Tvar v -> v.vs_name.id_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321
    | Tconst c -> Hashtbl.hash c
322
    | Tapp (f, tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
323
    | Tif (f, t, e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
324
    | Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
Andrei Paskevich's avatar
Andrei Paskevich committed
325 326
    | Tcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list t_hash_branch ht bl
327
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328

329
  let hash t =
330
    Hashcons.combine (t_hash_node t.t_node)
331
      (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
332

333
  let tag n t = { t with t_tag = n }
334

335
end)
336

337 338 339 340 341 342 343 344
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
345

346
module Hsfmla = Hashcons.Make (struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347 348 349

  type t = fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
350
  let f_eq_branch (pl1,_,f1) (pl2,_,f2) = list_all2 (==) pl1 pl2 && f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
351

352
  let f_eq_bound (v1, f1) (v2, f2) = v1 == v2 && f1 == f2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353

354
  let tr_eq tr1 tr2 = match tr1,tr2 with
355 356
    | Term t1, Term t2 -> t1 == t2
    | Fmla f1, Fmla f2 -> f1 == f2
357 358
    | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
359 360 361
  let f_eq_quant (vl1, _, tl1, f1) (vl2, _, tl2, f2) =
    f1 == f2 && list_all2 (==) vl1 vl2 &&
    list_all2 (list_all2 tr_eq) tl1 tl2
362

363
  let f_equal_node f1 f2 = match f1, f2 with
364 365
    | Fapp (s1, l1), Fapp (s2, l2) ->
        s1 == s2 && List.for_all2 (==) l1 l2
366
    | Fquant (q1, b1), Fquant (q2, b2) ->
367
        q1 == q2 && f_eq_quant b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
368
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
369
        op1 == op2 && f1 == f2 && g1 == g2
370 371
    | Fnot f1, Fnot f2 ->
        f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
372
    | Ftrue, Ftrue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
373
    | Ffalse, Ffalse ->
Andrei Paskevich's avatar
Andrei Paskevich committed
374
        true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
376
        f1 == f2 && g1 == g2 && h1 == h2
377
    | Flet (t1, b1), Flet (t2, b2) ->
378
        t1 == t2 && f_eq_bound b1 b2
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380
    | Fcase (tl1, bl1), Fcase (tl2, bl2) ->
        list_all2 (==) tl1 tl2 && list_all2 f_eq_branch bl1 bl2
Andrei Paskevich's avatar
Andrei Paskevich committed
381 382
    | _ ->
        false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383

384
  let equal f1 f2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
385
    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
386

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

Andrei Paskevich's avatar
Andrei Paskevich committed
389
  let p_hash p = p.pat_tag
390

Andrei Paskevich's avatar
Andrei Paskevich committed
391
  let t_hash t = t.t_tag
392

Andrei Paskevich's avatar
Andrei Paskevich committed
393
  let f_hash_branch (pl,_,f) = Hashcons.combine_list p_hash f.f_tag pl
394 395 396

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

397
  let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
398

399 400
  let f_hash_quant (vl, _, tl, f) =
    let h = Hashcons.combine_list v_hash f.f_tag vl in
401
    List.fold_left (Hashcons.combine_list tr_hash) h tl
402

403
  let f_hash_node = function
404
    | Fapp (p, tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
405
    | Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
406
    | Fbinop (op, f1, f2) ->
407
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
408
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409 410
    | Ftrue -> 0
    | Ffalse -> 1
411
    | Fif (f1, f2, f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
412
    | Flet (t, bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
413 414
    | Fcase (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list f_hash_branch ht bl
415 416

  let hash f =
417
    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
418

419
  let tag n f = { f with f_tag = n }
420

421 422 423 424 425 426
end)

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

428 429 430
module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H
431

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

434 435 436 437 438 439 440 441 442 443 444 445 446
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
447 448 449

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

452 453
let t_app_unsafe = t_app

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

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

458 459 460 461 462 463 464 465 466
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
467

468 469
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 }
470
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
471

472 473 474 475 476
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
477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492
(* 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_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]

let f_app p tl =
  if p == ps_neq then f_not (f_app ps_equ tl) else f_app p tl

493 494
let f_app_unsafe = f_app

495 496
(* unsafe map with level *)

497 498
exception UnboundIndex

499 500
let brlvl fn lvl (pat, nv, t) = (pat, nv, fn (lvl + nv) t)

501
let t_map_unsafe fnT fnF lvl t = t_label_copy t (match t.t_node with
502
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
503
  | Tbvar _ | Tvar _ | Tconst _ -> t
504
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
505
  | Tif (f, t1, t2) -> t_if (fnF lvl f) (fnT lvl t1) (fnT lvl t2)
506
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
507 508
  | Tcase (tl, bl) ->
      t_case (List.map (fnT lvl) tl) (List.map (brlvl fnT lvl) bl) t.t_ty
509
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f))
510

511
let f_map_unsafe fnT fnF lvl f = f_label_copy f (match f.f_node with
512
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
513
  | Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in
514
      f_quant q vl nv (tr_map (fnT lvl) (fnF lvl) tl) (fnF lvl f1)
515
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
516
  | Fnot f1 -> f_not (fnF lvl f1)
517 518
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
519
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
520 521
  | Fcase (tl, bl) ->
      f_case (List.map (fnT lvl) tl) (List.map (brlvl fnF lvl) bl))
522

523 524 525 526 527 528 529 530
let protect fn lvl t =
  let res = fn lvl t in
  if res.t_ty != t.t_ty then raise TypeMismatch;
  res

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

531 532 533 534
(* unsafe fold with level *)

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

535
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
536
  | Tbvar n when n >= lvl -> raise UnboundIndex
Andrei Paskevich's avatar
Andrei Paskevich committed
537
  | Tbvar _ | Tvar _ | Tconst _ -> acc
538
  | Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl
539
  | Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2
540
  | Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
541 542
  | Tcase (tl, bl) ->
      List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl
543
  | Teps (_, f) -> fnF (lvl + 1) acc f
544

545
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
546 547
  | Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl
  | Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in
548
      tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl
549
  | Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
550 551 552
  | Fnot f1 -> fnF lvl acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
553
  | Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
Andrei Paskevich's avatar
Andrei Paskevich committed
554 555
  | Fcase (tl, bl) ->
      List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl
556

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

562 563
let t_all_unsafe prT prF lvl t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true t
564 565
  with FoldSkip -> false

566 567
let f_all_unsafe prT prF lvl f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) lvl true f
568 569
  with FoldSkip -> false

570 571
let t_any_unsafe prT prF lvl t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false t
572 573
  with FoldSkip -> true

574 575
let f_any_unsafe prT prF lvl f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) lvl false f
576 577
  with FoldSkip -> true

578 579 580 581
(* unsafe constructors with type checking *)

let t_app fs tl ty =
  let s = match fs.ls_value with
582
    | Some vty -> ty_match Mtv.empty vty ty
583 584
    | _ -> raise (FunctionSymbolExpected fs)
  in
585
  let mtch s ty t = ty_match s ty t.t_ty in
586
  ignore (try List.fold_left2 mtch s fs.ls_args tl
587 588
    with Invalid_argument _ -> raise (BadArity
      (List.length fs.ls_args, List.length tl)));
589 590
  t_app fs tl ty

591 592 593 594
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
595 596
    with Invalid_argument _ -> raise (BadArity
      (List.length fs.ls_args, List.length tl))
597 598 599 600 601 602 603
  in
  let ty = match fs.ls_value with
    | Some ty -> ty_inst s ty
    | _ -> raise (FunctionSymbolExpected fs)
  in
  t_app_unsafe fs tl ty

604 605
let f_app ps tl =
  let s = match ps.ls_value with
606
    | None -> Mtv.empty
607 608
    | _ -> raise (PredicateSymbolExpected ps)
  in
609
  let mtch s ty t = ty_match s ty t.t_ty in
610
  ignore (try List.fold_left2 mtch s ps.ls_args tl
611 612
    with Invalid_argument _ -> raise (BadArity
      (List.length ps.ls_args, List.length tl)));
613 614
  f_app ps tl

Andrei Paskevich's avatar
Andrei Paskevich committed
615 616 617 618 619 620 621
let p_check t p =
  if p.pat_ty != t.t_ty then raise TypeMismatch

let t_case tl bl ty =
  let t_check_branch (pl,_,tbr) =
    if tbr.t_ty != ty then raise TypeMismatch;
    List.iter2 p_check tl pl
622 623
  in
  List.iter t_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
624
  t_case tl bl ty
625

Andrei Paskevich's avatar
Andrei Paskevich committed
626 627 628
let f_case tl bl =
  let f_check_branch (pl,_,_) =
    List.iter2 p_check tl pl
629 630
  in
  List.iter f_check_branch bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
631
  f_case tl bl
632

633 634 635 636
let t_if f t1 t2 =
  if t1.t_ty != t2.t_ty then raise TypeMismatch;
  t_if f t1 t2

637
let t_let v t1 t2 =
638 639
  if v.vs_ty != t1.t_ty then raise TypeMismatch;
  t_let v t1 t2
640 641

let f_let v t1 f2 =
642 643
  if v.vs_ty != t1.t_ty then raise TypeMismatch;
  f_let v t1 f2
644 645 646 647 648 649 650

(* map over symbols *)

let rec t_s_map fnT fnV fnL t =
  let fn_t = t_s_map fnT fnV fnL in
  let fn_f = f_s_map fnT fnV fnL in
  let ty = fnT t.t_ty in
651
  t_label_copy t (match t.t_node with
652 653 654 655
    | Tbvar n -> t_bvar n ty
    | Tvar v -> t_var (fnV v ty)
    | Tconst _ -> t
    | Tapp (f, tl) -> t_app (fnL f) (List.map fn_t tl) ty
656
    | Tif (f, t1, t2) -> t_if (fn_f f) (fn_t t1) (fn_t t2)
657 658
    | Tlet (t1, (u, t2)) ->
        let t1 = fn_t t1 in t_let (fnV u t1.t_ty) t1 (fn_t t2)
Andrei Paskevich's avatar
Andrei Paskevich committed
659
    | Tcase (tl, bl) ->
660
        let fn_b = t_branch fnT fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
661
        t_case (List.map fn_t tl) (List.map fn_b bl) ty
662 663 664 665 666
    | Teps (u, f) -> t_eps (fnV u ty) (fn_f f))

and f_s_map fnT fnV fnL f =
  let fn_t = t_s_map fnT fnV fnL in
  let fn_f = f_s_map fnT fnV fnL in
667
  f_label_copy f (match f.f_node with
668 669 670 671 672 673 674 675 676 677 678
    | 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
        let fn_v u = fnV u (fnT u.vs_ty) in
        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)) ->
        let t1 = fn_t t in f_let (fnV u t1.t_ty) t1 (fn_f f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
679
    | Fcase (tl, bl) ->
680
        let fn_b = f_branch fnT fnV fnL in
Andrei Paskevich's avatar
Andrei Paskevich committed
681 682 683 684
        f_case (List.map fn_t tl) (List.map fn_b bl))

and t_branch fnT fnV fnL (pl, nv, t) =
  (List.map (pat_s_map fnT fnV fnL) pl, nv, t_s_map fnT fnV fnL t)
685

Andrei Paskevich's avatar
Andrei Paskevich committed
686 687
and f_branch fnT fnV fnL (pl, nv, f) =
  (List.map (pat_s_map fnT fnV fnL) pl, nv, f_s_map fnT fnV fnL f)
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

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

let get_fnV () =
  let ht = Hid.create 17 in
  let fnV vs ty =
    if vs.vs_ty == ty then vs else
      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

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

(* 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
722
    | Tif (f, t1, t2) -> fn_t (fn_t (fn_f acc f) t1) t2
723
    | Tlet (t1, (_,t2)) -> fn_t (fn_t acc t1) t2
Andrei Paskevich's avatar
Andrei Paskevich committed
724 725
    | Tcase (tl, bl) ->
        List.fold_left (t_branch fnT fnL) (List.fold_left fn_t acc tl) bl
726 727 728 729 730 731 732 733
    | 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
734
    | Fquant (_, (vl,_,tl,f1)) ->
735 736
        let acc = List.fold_left fn_v acc vl in
        fn_f (tr_fold fn_t fn_f acc tl) f1
737
    | Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2
738 739 740 741
    | 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
742 743 744 745 746
    | 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
747

Andrei Paskevich's avatar
Andrei Paskevich committed
748 749
and f_branch fnT fnL acc (pl,_,f) =
  f_s_fold fnT fnL (List.fold_left (pat_s_fold fnT fnL) acc pl) f
750 751 752 753 754 755 756 757 758 759 760 761 762

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