term.ml 59.5 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
Johannes Kanig's avatar
Johannes Kanig committed
19

20
open Util
21
open Ident
22
open Ty
23

24
(** Variable symbols *)
25

26
type vsymbol = {
27
  vs_name : ident;
28
  vs_ty   : ty;
29 30
}

Andrei Paskevich's avatar
Andrei Paskevich committed
31
module Vsym = WeakStructMake (struct
32
  type t = vsymbol
33 34
  let tag vs = vs.vs_name.id_tag
end)
35

36 37 38
module Svs = Vsym.S
module Mvs = Vsym.M
module Hvs = Vsym.H
39

40 41
let vs_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
let vs_hash vs = id_hash vs.vs_name

44 45 46 47
let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}
48

49
let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_ty
50

51
(** Function and predicate symbols *)
52

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

Andrei Paskevich's avatar
Andrei Paskevich committed
59
module Lsym = WeakStructMake (struct
60
  type t = lsymbol
61 62 63 64 65 66
  let tag ls = ls.ls_name.id_tag
end)

module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H
Andrei Paskevich's avatar
Andrei Paskevich committed
67
module Wls = Lsym.W
68

69 70
let ls_equal = (==)

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

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

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

82 83 84 85 86 87 88
let ls_ty_freevars ls =
  let acc = match ls.ls_value with
    | None -> Stv.empty
    | Some ty -> ty_freevars Stv.empty ty
  in
  List.fold_left ty_freevars acc ls.ls_args

89
(** Patterns *)
90 91 92

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

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

105 106
let pat_equal = (==)

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

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

112
  let equal_node p1 p2 = match p1, p2 with
113
    | Pwild, Pwild -> true
114 115 116
    | Pvar v1, Pvar v2 -> vs_equal v1 v2
    | Papp (s1, l1), Papp (s2, l2) ->
        ls_equal s1 s2 && List.for_all2 pat_equal l1 l2
Andrei Paskevich's avatar
Andrei Paskevich committed
117 118
    | Por (p1, q1), Por (p2, q2) ->
        pat_equal p1 p2 && pat_equal q1 q2
119 120
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
121
    | _ -> false
122

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

  let hash_node = function
127
    | Pwild -> 0
Andrei Paskevich's avatar
Andrei Paskevich committed
128 129 130 131
    | Pvar v -> vs_hash v
    | Papp (s, pl) -> Hashcons.combine_list pat_hash (ls_hash s) pl
    | Por (p, q) -> Hashcons.combine (pat_hash p) (pat_hash q)
    | Pas (p, v) -> Hashcons.combine (pat_hash p) (vs_hash v)
132

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

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

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

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

(* h-consing constructors for patterns *)
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
let mk_pattern n vs ty = Hspat.hashcons {
  pat_node = n;
  pat_vars = vs;
  pat_ty   = ty;
  pat_tag  = -1
}

exception UncoveredVar of vsymbol
exception DuplicateVar of vsymbol

let add_no_dup vs s =
  if Svs.mem vs s then raise (DuplicateVar vs) else Svs.add vs s

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

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

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

178 179
(* generic traversal functions *)

180
let pat_map fn pat = match pat.pat_node with
181 182 183
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | Por (p, q) -> pat_or (fn p) (fn q)
185

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

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

let pat_map fn = pat_map (protect fn)

196 197 198 199
let pat_fold fn acc pat = match pat.pat_node with
  | Pwild | Pvar _ -> acc
  | Papp (_, pl) -> List.fold_left fn acc pl
  | Pas (p, _) -> fn acc p
Andrei Paskevich's avatar
Andrei Paskevich committed
200
  | Por (p, q) -> fn (fn acc p) q
201

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

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

208 209
(* smart constructors for patterns *)

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

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

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

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

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

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

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

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

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

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

267
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268 269 270 271 272 273 274
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

Andrei Paskevich's avatar
Andrei Paskevich committed
275 276
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
  t_label : label list;
278 279 280 281 282 283
  t_ty : ty;
  t_tag : int;
}

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

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

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

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

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

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

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

and trigger = expr list
324

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

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

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

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

337 338 339 340 341 342 343
(* expr and trigger equality *)

let e_equal e1 e2 = match e1, e2 with
  | Term t1, Term t2 -> t_equal t1 t2
  | Fmla f1, Fmla f2 -> f_equal f1 f2
  | _ -> false

344
let tr_equal = list_all2 (list_all2 e_equal)
345

346
(* expr and trigger traversal *)
347

348 349 350
let e_map fnT fnF = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f)
let e_fold fnT fnF acc = function Term t -> fnT acc t | Fmla f -> fnF acc f
let e_apply fnT fnF = function Term t -> fnT t | Fmla f -> fnF f
351

352 353 354 355
let e_map_fold fnT fnF acc = function
  | Term t -> let acc, t = fnT acc t in acc, Term t
  | Fmla f -> let acc, f = fnF acc f in acc, Fmla f

356 357
let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))
358

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

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

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

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

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

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

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

382
module Hsterm = Hashcons.Make (struct
383

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

386 387
  let t_eq_branch (p1,b1,t1) (p2,b2,t2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
388

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

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

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

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

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

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

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

424
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425
    | Tbvar n -> n
Andrei Paskevich's avatar
Andrei Paskevich committed
426
    | Tvar v -> vs_hash v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
    | Tconst c -> Hashtbl.hash c
Andrei Paskevich's avatar
Andrei Paskevich committed
428 429 430 431
    | Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl
    | Tif (f,t,e) -> Hashcons.combine2 (f_hash f) (t_hash t) (t_hash e)
    | Tlet (t,bt) -> Hashcons.combine (t_hash t) (t_hash_bound bt)
    | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch (t_hash t) bl
432
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433

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

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

440
end)
441

442 443 444 445 446 447 448 449
module Term = StructMake (struct
  type t = term
  let tag term = term.t_tag
end)

module Sterm = Term.S
module Mterm = Term.M
module Hterm = Term.H
450

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

  type t = fmla

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

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

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

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

482
  let equal f1 f2 =
483 484
    f_equal_node f1.f_node f2.f_node &&
    list_all2 (=) f1.f_label f2.f_label
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485

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

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

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

494
  let f_hash_quant (vl,b,tl,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
495 496 497
    let h = bnd_hash b (f_hash f) in
    let h = Hashcons.combine_list vs_hash h vl in
    List.fold_left (Hashcons.combine_list e_hash) h tl
498

499
  let f_hash_node = function
Andrei Paskevich's avatar
Andrei Paskevich committed
500
    | Fapp (p,tl) -> Hashcons.combine_list t_hash (ls_hash p) tl
501 502
    | Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
    | Fbinop (op,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
503 504
        Hashcons.combine2 (Hashtbl.hash op) (f_hash f1) (f_hash f2)
    | Fnot f -> Hashcons.combine 1 (f_hash f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505 506
    | Ftrue -> 0
    | Ffalse -> 1
Andrei Paskevich's avatar
Andrei Paskevich committed
507 508 509
    | Fif (f1,f2,f3) -> Hashcons.combine2 (f_hash f1) (f_hash f2) (f_hash f3)
    | Flet (t,bf) -> Hashcons.combine (t_hash t) (f_hash_bound bf)
    | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch (t_hash t) bl
510 511

  let hash f =
512
    Hashcons.combine_list Hashtbl.hash (f_hash_node f.f_node) f.f_label
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
513

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

516 517 518 519 520 521
end)

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

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

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

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

532 533 534 535 536 537 538 539 540 541
let t_bvar n ty     = mk_term (Tbvar n) ty
let t_var v         = mk_term (Tvar v) v.vs_ty
let t_const c ty    = mk_term (Tconst c) ty
let t_int_const s   = mk_term (Tconst (ConstInt s)) Ty.ty_int
let t_real_const r  = mk_term (Tconst (ConstReal r)) Ty.ty_real
let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
let t_case t1 bl ty = mk_term (Tcase (t1, bl)) ty
let t_eps bf ty     = mk_term (Teps bf) ty
542 543 544

let t_label     l t = Hsterm.hashcons { t with t_label = l }
let t_label_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }
545 546 547

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

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

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

553 554 555 556 557 558 559 560 561
let f_app f tl        = mk_fmla (Fapp (f, tl))
let f_quant q qf      = mk_fmla (Fquant (q, qf))
let f_binary op f1 f2 = mk_fmla (Fbinop (op, f1, f2))
let f_not f           = mk_fmla (Fnot f)
let f_true            = mk_fmla (Ftrue)
let f_false           = mk_fmla (Ffalse)
let f_if f1 f2 f3     = mk_fmla (Fif (f1, f2, f3))
let f_let t bf        = mk_fmla (Flet (t, bf))
let f_case t bl       = mk_fmla (Fcase (t, bl))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562

563 564
let f_label     l f = Hsfmla.hashcons { f with f_label = l }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }
565 566 567

let f_label_copy { f_label = l } f =
  if f.f_label = [] && l <> [] then f_label l f else f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568

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

574
(* unsafe map *)
575

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

578 579 580 581 582
let t_map_unsafe fnT fnF t = t_label_copy t (match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> t
  | Tapp (f,tl) -> t_app f (List.map fnT tl) t.t_ty
  | Tif (f,t1,t2) -> t_if (fnF f) (fnT t1) (fnT t2)
  | Tlet (e,b) -> t_let (fnT e) (bound_map fnT fnT b) t.t_ty
583
  | Tcase (e,bl) -> t_case (fnT e) (List.map (bound_map fnT fnT) bl) t.t_ty
584
  | Teps b -> t_eps (bound_map fnT fnF b) t.t_ty)
585

586 587
let f_map_unsafe fnT fnF f = f_label_copy f (match f.f_node with
  | Fapp (p,tl) -> f_app p (List.map fnT tl)
588 589
  | Fquant (q,(vl,b,tl,f1)) ->
      f_quant q (vl, bnd_map fnT b, tr_map fnT fnF tl, fnF f1)
590 591 592 593 594
  | Fbinop (op,f1,f2) -> f_binary op (fnF f1) (fnF f2)
  | Fnot f1 -> f_not (fnF f1)
  | Ftrue | Ffalse -> f
  | Fif (f1,f2,f3) -> f_if (fnF f1) (fnF f2) (fnF f3)
  | Flet (e,b) -> f_let (fnT e) (bound_map fnT fnF b)
595
  | Fcase (e,bl) -> f_case (fnT e) (List.map (bound_map fnT fnF) bl))
596

597
(* unsafe fold *)
598

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

601 602 603 604 605
let t_fold_unsafe fnT fnF acc t = match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> acc
  | Tapp (_,tl) -> List.fold_left fnT acc tl
  | Tif (f,t1,t2) -> fnT (fnT (fnF acc f) t1) t2
  | Tlet (e,b) -> fnT (bound_fold fnT fnT acc b) e
606
  | Tcase (e,bl) -> List.fold_left (bound_fold fnT fnT) (fnT acc e) bl
607 608 609 610
  | Teps b -> bound_fold fnT fnF acc b

let f_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (_,tl) -> List.fold_left fnT acc tl
611
  | Fquant (_,(_,b,tl,f1)) -> fnF (tr_fold fnT fnF (bnd_fold fnT acc b) tl) f1
612 613 614 615 616
  | Fbinop (_,f1,f2) -> fnF (fnF acc f1) f2
  | Fnot f1 -> fnF acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1,f2,f3) -> fnF (fnF (fnF acc f1) f2) f3
  | Flet (e,b) -> fnT (bound_fold fnT fnF acc b) e
617
  | Fcase (e,bl) -> List.fold_left (bound_fold fnT fnF) (fnT acc e) bl
618

619 620 621 622
let all_fnT prT _ t = prT t || raise FoldSkip
let all_fnF prF _ f = prF f || raise FoldSkip
let any_fnT prT _ t = prT t && raise FoldSkip
let any_fnF prF _ f = prF f && raise FoldSkip
623

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

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

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

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

640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701
(* unsafe map_fold *)

let bound_map_fold fnT fnE acc (u,b,e) =
  let acc, b = bnd_map_fold fnT acc b in
  let acc, e = fnE acc e in
  acc, (u,b,e)

let t_map_fold_unsafe fnT fnF acc t = match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ ->
      acc, t
  | Tapp (f,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, t_label_copy t (t_app f tl t.t_ty)
  | Tif (f,t1,t2) ->
      let acc, f  = fnF acc f in
      let acc, t1 = fnT acc t1 in
      let acc, t2 = fnT acc t2 in
      acc, t_label_copy t (t_if f t1 t2)
  | Tlet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnT acc b in
      acc, t_label_copy t (t_let e b t.t_ty)
  | Tcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnT) acc bl in
      acc, t_label_copy t (t_case e bl t.t_ty)
  | Teps b ->
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, t_label_copy t (t_eps b t.t_ty)

let f_map_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (p,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, f_label_copy f (f_app p tl)
  | Fquant (q,(vl,b,tl,f1)) ->
      let acc, b = bnd_map_fold fnT acc b in
      let acc, tl = tr_map_fold fnT fnF acc tl in
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_quant q (vl,b,tl,f1))
  | Fbinop (op,f1,f2) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      acc, f_label_copy f (f_binary op f1 f2)
  | Fnot f1 ->
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_not f1)
  | Ftrue | Ffalse ->
      acc, f
  | Fif (f1,f2,f3) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      let acc, f3 = fnF acc f3 in
      acc, f_label_copy f (f_if f1 f2 f3)
  | Flet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, f_label_copy f (f_let e b)
  | Fcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnF) acc bl in
      acc, f_label_copy f (f_case e bl)

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

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

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

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

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

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

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

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

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

761
exception UnboundIndex
762

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

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
766
let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } =
767 768
  let s = Sint.fold (fun i -> Mint.add (i + d) (bnd_find i m)) b s in
(* assert (Mint.submap (const3 true) b m);
769 770
  let m = Mint.inter (fun _ () x -> Some x) b m in
  let m = Mint.translate ((+) d) m in
771
  let s = Mint.union (fun _ _ _ -> assert false) m s in *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
772
  { bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s }
773

774 775 776 777 778 779 780 781 782