term.ml 46 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
Johannes Kanig's avatar
Johannes Kanig committed
11

12
open Util
13
open Ident
14
open Ty
15
open Stdlib
16

17
(** Variable symbols *)
18

19
type vsymbol = {
20
  vs_name : ident;
21
  vs_ty   : ty;
22 23
}

Andrei Paskevich's avatar
Andrei Paskevich committed
24
module Vsym = WeakStructMake (struct
25
  type t = vsymbol
26 27
  let tag vs = vs.vs_name.id_tag
end)
28

29 30 31
module Svs = Vsym.S
module Mvs = Vsym.M
module Hvs = Vsym.H
32
module Wvs = Vsym.W
33

34
let vs_equal : vsymbol -> vsymbol -> bool = (==)
35

Andrei Paskevich's avatar
Andrei Paskevich committed
36 37
let vs_hash vs = id_hash vs.vs_name

38 39 40 41
let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}
42

43
(** Function and predicate symbols *)
44

45 46 47
type lsymbol = {
  ls_name   : ident;
  ls_args   : ty list;
48
  ls_value  : ty option;
49 50
}

Andrei Paskevich's avatar
Andrei Paskevich committed
51
module Lsym = WeakStructMake (struct
52
  type t = lsymbol
53 54 55 56 57 58
  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
59
module Wls = Lsym.W
60

61
let ls_equal : lsymbol -> lsymbol -> bool = (==)
62

Andrei Paskevich's avatar
Andrei Paskevich committed
63 64
let ls_hash ls = id_hash ls.ls_name

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

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

74
let ls_ty_freevars ls =
75
  let acc = oty_freevars Stv.empty ls.ls_value in
76 77
  List.fold_left ty_freevars acc ls.ls_args

78
(** Patterns *)
79 80 81

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

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

94
let pat_equal : pattern -> pattern -> bool = (==)
95

Andrei Paskevich's avatar
Andrei Paskevich committed
96 97
let pat_hash p = p.pat_tag

98
module Hspat = Hashcons.Make (struct
99
  type t = pattern
100

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

112
  let equal p1 p2 =
113
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
114 115

  let hash_node = function
116
    | Pwild -> 0
Andrei Paskevich's avatar
Andrei Paskevich committed
117 118 119 120
    | 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)
121

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

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

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

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

(* h-consing constructors for patterns *)
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138 139 140 141 142 143 144 145 146 147 148 149
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 pat_wild ty = mk_pattern Pwild Svs.empty ty
let pat_var v   = mk_pattern (Pvar v) (Svs.singleton v) v.vs_ty
150 151

let pat_as p v =
152
  let s = Svs.add_new (DuplicateVar v) v p.pat_vars in
153
  mk_pattern (Pas (p,v)) s v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
154 155

let pat_or p q =
156 157 158
  if Svs.equal p.pat_vars q.pat_vars then
    mk_pattern (Por (p,q)) p.pat_vars p.pat_ty
  else
159 160
    let s = Mvs.union (fun _ _ _ -> None) p.pat_vars q.pat_vars in
    raise (UncoveredVar (Svs.choose s))
Andrei Paskevich's avatar
Andrei Paskevich committed
161 162

let pat_app f pl ty =
163 164
  let dup v () () = raise (DuplicateVar v) in
  let merge s p = Mvs.union dup s p.pat_vars in
Andrei Paskevich's avatar
Andrei Paskevich committed
165
  mk_pattern (Papp (f,pl)) (List.fold_left merge Svs.empty pl) ty
166

167 168
(* generic traversal functions *)

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

175 176
let pat_map fn = pat_map (fun p ->
  let res = fn p in ty_equal_check p.pat_ty res.pat_ty; res)
177

178 179 180 181
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
182
  | Por (p, q) -> fn (fn acc p) q
183

184 185
let pat_all pr pat = try pat_fold (all_fn pr) true pat with FoldSkip -> false
let pat_any pr pat = try pat_fold (any_fn pr) false pat with FoldSkip -> true
186

187 188
(* smart constructors for patterns *)

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
208
let pat_or p q =
209
  ty_equal_check p.pat_ty q.pat_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
210 211
  pat_or p q

212 213 214 215 216 217 218
(* rename all variables in a pattern *)

let rec pat_rename_all m p = match p.pat_node with
  | Pvar v -> pat_var (Mvs.find v m)
  | Pas (p, v) -> pat_as (pat_rename_all m p) (Mvs.find v m)
  | _ -> pat_map (pat_rename_all m) p

219 220
(* symbol-wise map/fold *)

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

231 232
let rec pat_gen_fold fnT fnL acc pat =
  let fn acc p = pat_gen_fold fnT fnL acc p in
233
  let acc = fnT acc pat.pat_ty in
234
  match pat.pat_node with
235
    | Pwild | Pvar _ -> acc
236
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
237
    | Por (p, q) -> fn (fn acc p) q
238
    | Pas (p, _) -> fn acc p
239

240
(** Terms and formulas *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
241

242
type quant =
243 244
  | Tforall
  | Texists
245 246

type binop =
247 248 249 250
  | Tand
  | Tor
  | Timplies
  | Tiff
251

252 253 254 255 256 257
type integer_constant =
  | IConstDecimal of string
  | IConstHexa of string
  | IConstOctal of string
  | IConstBinary of string

258
type real_constant =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259 260 261 262
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
263
  | ConstInt of integer_constant
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264 265
  | ConstReal of real_constant

Andrei Paskevich's avatar
Andrei Paskevich committed
266
type term = {
267
  t_node  : term_node;
268
  t_ty    : ty option;
269
  t_label : Slab.t;
270
  t_loc   : Loc.position option;
271
  t_vars  : int Mvs.t;
272
  t_tag   : int;
273 274
}

Andrei Paskevich's avatar
Andrei Paskevich committed
275
and term_node =
276
  | Tvar of vsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277
  | Tconst of constant
278
  | Tapp of lsymbol * term list
279
  | Tif of term * term * term
280
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
281
  | Tcase of term * term_branch list
282 283 284 285 286 287 288
  | Teps of term_bound
  | Tquant of quant * term_quant
  | Tbinop of binop * term * term
  | Tnot of term
  | Ttrue
  | Tfalse

289 290
and term_bound  = vsymbol * bind_info * term
and term_branch = pattern * bind_info * term
291
and term_quant  = vsymbol list * bind_info * trigger * term
292

293
and trigger = term list list
294

295
and bind_info = {
296
  bv_vars  : int Mvs.t;   (* free variables *)
297
  bv_subst : term Mvs.t   (* deferred substitution *)
298 299
}

300
(* term equality and hash *)
301

302
let t_equal : term -> term -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
303 304
let t_hash t = t.t_tag

305
(* type checking *)
306 307 308 309 310 311 312 313

exception TermExpected of term
exception FmlaExpected of term

let t_type t = match t.t_ty with
  | Some ty -> ty
  | None -> raise (TermExpected t)

314
let t_prop f =
Andrei Paskevich's avatar
Andrei Paskevich committed
315
  if f.t_ty = None then f else raise (FmlaExpected f)
316

317 318
let t_ty_check t ty = match ty, t.t_ty with
  | Some l, Some r -> ty_equal_check l r
319 320 321 322
  | Some _, None -> raise (TermExpected t)
  | None, Some _ -> raise (FmlaExpected t)
  | None, None -> ()

323 324
let vs_check v t = ty_equal_check v.vs_ty (t_type t)

325
(* trigger equality and traversal *)
326

327
let tr_equal = list_all2 (list_all2 t_equal)
328

329 330 331
let tr_map fn = List.map (List.map fn)
let tr_fold fn = List.fold_left (List.fold_left fn)
let tr_map_fold fn = Util.map_fold_left (Util.map_fold_left fn)
332

333
(* bind_info equality, hash, and traversal *)
334

335
let bnd_equal b1 b2 = Mvs.equal t_equal b1.bv_subst b2.bv_subst
336 337

let bnd_hash bv =
338 339
  let comb v t acc = Hashcons.combine2 (vs_hash v) (t_hash t) acc in
  Mvs.fold comb bv.bv_subst
340

341
let bnd_map fn bv = { bv with bv_subst = Mvs.map fn bv.bv_subst }
342

343
let bnd_fold fn acc bv = Mvs.fold (fun _ t a -> fn a t) bv.bv_subst acc
344

345
let bnd_map_fold fn acc bv =
346 347
  let acc,s = Mvs.mapi_fold (fun _ t a -> fn a t) bv.bv_subst acc in
  acc, { bv with bv_subst = s }
348

349 350
(* hash-consing for terms and formulas *)

351 352 353
let some_plus _ m n = Some (m + n)
let add_t_vars s t = Mvs.union some_plus s t.t_vars
let add_b_vars s (_,b,_) = Mvs.union some_plus s b.bv_vars
354 355
let add_nt_vars _ n t s = Mvs.union some_plus s
  (if n = 1 then t.t_vars else Mvs.map (( * ) n) t.t_vars)
356

357
module Hsterm = Hashcons.Make (struct
358

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359 360
  type t = term

361 362
  let t_eq_bound (v1,b1,t1) (v2,b2,t2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2
363

364 365 366
  let t_eq_branch (p1,b1,t1) (p2,b2,t2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2

367
  let t_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
368
    t_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
369
    bnd_equal b1 b2 && tr_equal tl1 tl2
370 371

  let t_equal_node t1 t2 = match t1,t2 with
372
    | Tvar v1, Tvar v2 -> vs_equal v1 v2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
373
    | Tconst c1, Tconst c2 -> c1 = c2
374
    | Tapp (s1,l1), Tapp (s2,l2) ->
375
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
376
    | Tif (f1,t1,e1), Tif (f2,t2,e2) ->
377
        t_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2
378
    | Tlet (t1,b1), Tlet (t2,b2) ->
379
        t_equal t1 t2 && t_eq_bound b1 b2
380
    | Tcase (t1,bl1), Tcase (t2,bl2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
381
        t_equal t1 t2 && list_all2 t_eq_branch bl1 bl2
382
    | Teps f1, Teps f2 -> t_eq_bound f1 f2
383 384 385
    | Tquant (q1,b1), Tquant (q2,b2) ->
        q1 = q2 && t_eq_quant b1 b2
    | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) ->
386
        op1 = op2 && t_equal f1 f2 && t_equal g1 g2
387 388
    | Tnot f1, Tnot f2 -> t_equal f1 f2
    | Ttrue, Ttrue | Tfalse, Tfalse -> true
389
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
390

391
  let equal t1 t2 =
392
    oty_equal t1.t_ty t2.t_ty &&
393
    t_equal_node t1.t_node t2.t_node &&
394
    Slab.equal t1.t_label t2.t_label &&
395
    Opt.equal Loc.equal t1.t_loc t2.t_loc
396

397 398 399
  let t_hash_bound (v,b,t) =
    Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t))

400
  let t_hash_branch (p,b,t) =
Andrei Paskevich's avatar
Andrei Paskevich committed
401
    Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
402

403 404
  let t_hash_quant (vl,b,tl,f) =
    let h = bnd_hash b (t_hash f) in
405
    let h = Hashcons.combine_list vs_hash h vl in
406
    List.fold_left (Hashcons.combine_list t_hash) h tl
407

408
  let t_hash_node = function
Andrei Paskevich's avatar
Andrei Paskevich committed
409
    | Tvar v -> vs_hash v
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410
    | Tconst c -> Hashtbl.hash c
Andrei Paskevich's avatar
Andrei Paskevich committed
411
    | Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl
412
    | Tif (f,t,e) -> Hashcons.combine2 (t_hash f) (t_hash t) (t_hash e)
Andrei Paskevich's avatar
Andrei Paskevich committed
413 414
    | 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
415
    | Teps f -> t_hash_bound f
416 417
    | Tquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (t_hash_quant bf)
    | Tbinop (op,f1,f2) ->
418
        Hashcons.combine2 (Hashtbl.hash op) (t_hash f1) (t_hash f2)
419 420 421
    | Tnot f -> Hashcons.combine 1 (t_hash f)
    | Ttrue -> 0
    | Tfalse -> 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422

423
  let hash t =
424
    let comb l = Hashcons.combine (lab_hash l) in
425 426
    Hashcons.combine2 (t_hash_node t.t_node)
      (Hashcons.combine_option Loc.hash t.t_loc)
427
      (Slab.fold comb t.t_label (oty_hash t.t_ty))
Andrei Paskevich's avatar
Andrei Paskevich committed
428

429
  let t_vars_node = function
430 431 432
    | Tvar v -> Mvs.singleton v 1
    | Tconst _ -> Mvs.empty
    | Tapp (_,tl) -> List.fold_left add_t_vars Mvs.empty tl
433
    | Tif (f,t,e) -> add_t_vars (add_t_vars f.t_vars t) e
434 435 436
    | Tlet (t,bt) -> add_b_vars t.t_vars bt
    | Tcase (t,bl) -> List.fold_left add_b_vars t.t_vars bl
    | Teps (_,b,_) -> b.bv_vars
437
    | Tquant (_,(_,b,_,_)) -> b.bv_vars
438
    | Tbinop (_,f1,f2) -> add_t_vars f1.t_vars f2
439
    | Tnot f -> f.t_vars
440
    | Ttrue | Tfalse -> Mvs.empty
441 442

  let tag n t = { t with t_tag = n ; t_vars = t_vars_node t.t_node }
443

444
end)
445

446 447 448 449 450 451 452 453
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
454

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

457
let mk_term n ty = Hsterm.hashcons {
458
  t_node  = n;
459
  t_label = Slab.empty;
460
  t_loc   = None;
461
  t_vars  = Mvs.empty;
462 463 464
  t_ty    = ty;
  t_tag   = -1
}
465

466 467
let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
let t_const c ty    = mk_term (Tconst c) (Some ty)
468
let t_int_const s   = mk_term (Tconst (ConstInt (IConstDecimal s))) (Some Ty.ty_int)
469
let t_real_const r  = mk_term (Tconst (ConstReal r)) (Some Ty.ty_real)
470 471 472 473 474
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
475 476 477 478 479
let t_quant q qf    = mk_term (Tquant (q, qf)) None
let t_binary op f g = mk_term (Tbinop (op, f, g)) None
let t_not f         = mk_term (Tnot f) None
let t_true          = mk_term (Ttrue) None
let t_false         = mk_term (Tfalse) None
480

481 482
let t_label ?loc l t =
  Hsterm.hashcons { t with t_label = l; t_loc = loc }
483

484 485 486 487 488 489 490
let t_label_add l t =
  Hsterm.hashcons { t with t_label = Slab.add l t.t_label }

let t_label_copy { t_label = lab; t_loc = loc } t =
  let lab = Slab.union lab t.t_label in
  let loc = if t.t_loc = None then loc else t.t_loc in
  Hsterm.hashcons { t with t_label = lab; t_loc = loc }
491

492
(* unsafe map *)
493

494
let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e)
495

496
let t_map_unsafe fn t = t_label_copy t (match t.t_node with
497
  | Tvar _ | Tconst _ -> t
498 499 500 501 502 503 504 505 506 507 508 509 510 511
  | Tapp (f,tl) ->
      let sl = List.map fn tl in
      if List.for_all2 t_equal sl tl then t else
      t_app f sl t.t_ty
  | Tif (f,t1,t2) ->
      let g = fn f and s1 = fn t1 and s2 = fn t2 in
      if t_equal g f && t_equal s1 t1 && t_equal s2 t2 then t else
      t_if g s1 s2
  | Tlet (e,b) ->
      t_let (fn e) (bound_map fn b) t.t_ty
  | Tcase (e,bl) ->
      t_case (fn e) (List.map (bound_map fn) bl) t.t_ty
  | Teps b ->
      t_eps (bound_map fn b) t.t_ty
512 513
  | Tquant (q,(vl,b,tl,f1)) ->
      t_quant q (vl, bnd_map fn b, tr_map fn tl, fn f1)
514 515 516 517 518 519 520 521
  | Tbinop (op,f1,f2) ->
      let g1 = fn f1 and g2 = fn f2 in
      if t_equal g1 f1 && t_equal g2 f2 then t else
      t_binary op g1 g2
  | Tnot f1 ->
      let g1 = fn f1 in
      if t_equal g1 f1 then t else
      t_not g1
522
  | Ttrue | Tfalse -> t)
523

524
(* unsafe fold *)
525

526
let bound_fold fn acc (_,b,e) = fn (bnd_fold fn acc b) e
527

528
let t_fold_unsafe fn acc t = match t.t_node with
529
  | Tvar _ | Tconst _ -> acc
530 531 532 533 534
  | Tapp (_,tl) -> List.fold_left fn acc tl
  | Tif (f,t1,t2) -> fn (fn (fn acc f) t1) t2
  | Tlet (e,b) -> fn (bound_fold fn acc b) e
  | Tcase (e,bl) -> List.fold_left (bound_fold fn) (fn acc e) bl
  | Teps b -> bound_fold fn acc b
535 536 537 538
  | Tquant (_,(_,b,tl,f1)) -> fn (tr_fold fn (bnd_fold fn acc b) tl) f1
  | Tbinop (_,f1,f2) -> fn (fn acc f1) f2
  | Tnot f1 -> fn acc f1
  | Ttrue | Tfalse -> acc
539

540 541
(* unsafe map_fold *)

542 543 544
let bound_map_fold fn acc (u,b,e) =
  let acc, b = bnd_map_fold fn acc b in
  let acc, e = fn acc e in
545 546
  acc, (u,b,e)

547
let t_map_fold_unsafe fn acc t = match t.t_node with
548
  | Tvar _ | Tconst _ ->
549 550
      acc, t
  | Tapp (f,tl) ->
551 552 553
      let acc,sl = map_fold_left fn acc tl in
      if List.for_all2 t_equal sl tl then acc,t else
      acc, t_label_copy t (t_app f sl t.t_ty)
554
  | Tif (f,t1,t2) ->
555 556 557 558 559
      let acc, g  = fn acc f in
      let acc, s1 = fn acc t1 in
      let acc, s2 = fn acc t2 in
      if t_equal g f && t_equal s1 t1 && t_equal s2 t2 then acc,t else
      acc, t_label_copy t (t_if g s1 s2)
560
  | Tlet (e,b) ->
561 562
      let acc, e = fn acc e in
      let acc, b = bound_map_fold fn acc b in
563 564
      acc, t_label_copy t (t_let e b t.t_ty)
  | Tcase (e,bl) ->
565 566
      let acc, e = fn acc e in
      let acc, bl = map_fold_left (bound_map_fold fn) acc bl in
567 568
      acc, t_label_copy t (t_case e bl t.t_ty)
  | Teps b ->
569
      let acc, b = bound_map_fold fn acc b in
570
      acc, t_label_copy t (t_eps b t.t_ty)
571
  | Tquant (q,(vl,b,tl,f1)) ->
572 573 574
      let acc, b = bnd_map_fold fn acc b in
      let acc, tl = tr_map_fold fn acc tl in
      let acc, f1 = fn acc f1 in
575 576
      acc, t_label_copy t (t_quant q (vl,b,tl,f1))
  | Tbinop (op,f1,f2) ->
577 578 579 580
      let acc, g1 = fn acc f1 in
      let acc, g2 = fn acc f2 in
      if t_equal g1 f1 && t_equal g2 f2 then acc,t else
      acc, t_label_copy t (t_binary op g1 g2)
581
  | Tnot f1 ->
582 583 584
      let acc, g1 = fn acc f1 in
      if t_equal g1 f1 then acc,t else
      acc, t_label_copy t (t_not g1)
585
  | Ttrue | Tfalse ->
586 587
      acc, t

588 589 590 591 592
(* type-unsafe term substitution *)

let rec t_subst_unsafe m t =
  let t_subst t = t_subst_unsafe m t in
  let b_subst (u,b,e) = (u, bv_subst_unsafe m b, e) in
593
  let nosubst (_,b,_) = Mvs.set_disjoint m b.bv_vars in
594 595
  match t.t_node with
  | Tvar u ->
596
      Mvs.find_def t u m
597
  | Tlet (e, bt) ->
598 599 600
      let d = t_subst e in
      if t_equal d e && nosubst bt then t else
      t_label_copy t (t_let d (b_subst bt) t.t_ty)
601
  | Tcase (e, bl) ->
602 603
      let d = t_subst e in
      if t_equal d e && List.for_all nosubst bl then t else
604
      let bl = List.map b_subst bl in
605
      t_label_copy t (t_case d bl t.t_ty)
606
  | Teps bf ->
607
      if nosubst bf then t else
608
      t_label_copy t (t_eps (b_subst bf) t.t_ty)
609
  | Tquant (q, (vl,b,tl,f1)) ->
610
      if Mvs.set_disjoint m b.bv_vars then t else
611
      let b = bv_subst_unsafe m b in
612
      t_label_copy t (t_quant q (vl,b,tl,f1))
613
  | _ ->
614
      t_map_unsafe t_subst t
615 616 617

and bv_subst_unsafe m b =
  (* restrict m to the variables free in b *)
618
  let m = Mvs.set_inter m b.bv_vars in
619 620 621
  (* if m is empty, return early *)
  if Mvs.is_empty m then b else
  (* remove from b.bv_vars the variables replaced by m *)
622
  let s = Mvs.set_diff b.bv_vars m in
623
  (* add to b.bv_vars the free variables added by m *)
624
  let s = Mvs.fold2_inter add_nt_vars b.bv_vars m s in
625 626 627 628 629 630 631 632 633 634 635
  (* apply m to the terms in b.bv_subst *)
  let h = Mvs.map (t_subst_unsafe m) b.bv_subst in
  (* join m to b.bv_subst *)
  let h = Mvs.union (fun _ _ t -> Some t) m h in
  (* reconstruct b *)
  { bv_vars = s ; bv_subst = h }

let t_subst_unsafe m t =
  if Mvs.is_empty m then t else t_subst_unsafe m t

(* close bindings *)
636

637
let bnd_new s = { bv_vars = s ; bv_subst = Mvs.empty }
638

639
let t_close_bound v t = (v, bnd_new (Mvs.remove v t.t_vars), t)
640

641
let t_close_branch p t = (p, bnd_new (Mvs.set_diff t.t_vars p.pat_vars), t)
642

643
let t_close_quant vl tl f =
644 645
  let del_v s v = Mvs.remove v s in
  let s = tr_fold add_t_vars f.t_vars tl in
646
  let s = List.fold_left del_v s vl in
647
  (vl, bnd_new s, tl, t_prop f)
648

649
(* open bindings *)
650

651 652
let fresh_vsymbol v =
  create_vsymbol (id_clone v.vs_name) v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
653

654 655
let vs_rename h v =
  let u = fresh_vsymbol v in
656
  Mvs.add v (t_var u) h, u
657

658 659
let vl_rename h vl =
  Util.map_fold_left vs_rename h vl
660

661 662
let pat_rename h p =
  let add_vs v () = fresh_vsymbol v in
663
  let m = Mvs.mapi add_vs p.pat_vars in
664
  let p = pat_rename_all m p in
Andrei Paskevich's avatar
Andrei Paskevich committed
665 666
  Mvs.union (fun _ _ t -> Some t) h (Mvs.map t_var m), p

667
let t_open_bound (v,b,t) =
668 669
  let m,v = vs_rename b.bv_subst v in
  v, t_subst_unsafe m t
670

671
let t_open_branch (p,b,t) =
672 673
  let m,p = pat_rename b.bv_subst p in
  p, t_subst_unsafe m t
674

675
let t_open_quant (vl,b,tl,f) =
676
  let m,vl = vl_rename b.bv_subst vl in
677
  let tl = tr_map (t_subst_unsafe m) tl in
678
  (vl, tl, t_subst_unsafe m f)
679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695

(** open bindings with optimized closing callbacks *)

let t_open_bound_cb tb =
  let v, t = t_open_bound tb in
  let close v' t' =
    if t_equal t t' && vs_equal v v' then tb else t_close_bound v' t'
  in
  v, t, close

let t_open_branch_cb tbr =
  let p, t = t_open_branch tbr in
  let close p' t' =
    if t_equal t t' && pat_equal p p' then tbr else t_close_branch p' t'
  in
  p, t, close

696 697
let t_open_quant_cb fq =
  let vl, tl, f = t_open_quant fq in
698
  let close vl' tl' f' =
699
    if t_equal f f' && tr_equal tl tl' && list_all2 vs_equal vl vl'
700
    then fq else t_close_quant vl' tl' f'
701 702 703 704
  in
  vl, tl, f, close

(* constructors with type checking *)
705

706
let ls_arg_inst ls tl =
707
  let mtch s ty t = ty_match s ty (t_type t) in
708 709 710 711
  try List.fold_left2 mtch Mtv.empty ls.ls_args tl
  with Invalid_argument _ -> raise (BadArity
    (ls, List.length ls.ls_args, List.length tl))

712
let ls_app_inst ls tl ty =
713 714
  let s = ls_arg_inst ls tl in
  match ls.ls_value, ty with
715 716
    | Some _, None -> raise (PredicateSymbolExpected ls)
    | None, Some _ -> raise (FunctionSymbolExpected ls)
717 718
    | Some vty, Some ty -> ty_match s vty ty
    | None, None -> s
719

720 721 722
let t_app_infer ls tl =
  let s = ls_arg_inst ls tl in
  t_app ls tl (oty_inst s ls.ls_value)
723

724 725 726 727 728 729 730 731 732 733 734 735 736 737
let t_app ls tl ty = ignore (ls_app_inst ls tl ty); t_app ls tl ty

let fs_app fs tl ty = t_app fs tl (Some ty)
let ps_app ps tl    = t_app ps tl None

let t_const c = match c with
  | ConstInt _  -> t_const c ty_int
  | ConstReal _ -> t_const c ty_real

let t_if f t1 t2 =
  t_ty_check t2 t1.t_ty;
  t_if (t_prop f) t1 t2

let t_let t1 ((v,_,t2) as bt) =
738
  vs_check v t1;
739
  t_let t1 bt t2.t_ty
740

741
exception EmptyCase
742

743
let t_case t bl =
744 745
  let tty = t_type t in
  let bty = match bl with
746
    | (_,_,tbr) :: _ -> tbr.t_ty
747
    | _ -> raise EmptyCase
748
  in
749
  let t_check_branch (p,_,tbr) =
750 751
    ty_equal_check tty p.pat_ty;
    t_ty_check tbr bty
752 753
  in
  List.iter t_check_branch bl;
754
  t_case t bl bty
755

756 757
let t_eps ((v,_,f) as bf) =
  ignore (t_prop f);
758
  t_eps bf (Some v.vs_ty)
759

760 761
let t_quant q ((vl,_,_,f) as qf) =
  if vl =