term.ml 53.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
Johannes Kanig's avatar
Johannes Kanig committed
11

12
open Wstdlib
13
open Ident
14
open Ty
15

16
(** Variable symbols *)
17

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

23
module Vsym = MakeMSHW (struct
24
  type t = vsymbol
25 26
  let tag vs = vs.vs_name.id_tag
end)
27

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

33
let vs_equal : vsymbol -> vsymbol -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
34
let vs_hash vs = id_hash vs.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
35
let vs_compare vs1 vs2 = id_compare vs1.vs_name vs2.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
36

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

42
(** Function and predicate symbols *)
43

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

51
module Lsym = MakeMSHW (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 = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
62
let ls_hash ls = id_hash ls.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
63
let ls_compare ls1 ls2 = id_compare ls1.ls_name ls2.ls_name
Andrei Paskevich's avatar
Andrei Paskevich committed
64

Andrei Paskevich's avatar
Andrei Paskevich committed
65 66 67
let check_constr constr _args value =
  if constr = 0 || (constr > 0 && value <> None)
  then constr else invalid_arg "Term.create_lsymbol"
68

69
let create_lsymbol ?(constr=0) name args value = {
70
  ls_name   = id_register name;
71 72
  ls_args   = args;
  ls_value  = value;
73
  ls_constr = check_constr constr args value;
74 75
}

76 77
let create_fsymbol ?constr nm al vl =
  create_lsymbol ?constr nm al (Some vl)
78

79 80
let create_psymbol nm al =
  create_lsymbol ~constr:0 nm al None
81

82
let ls_ty_freevars ls =
83
  let acc = oty_freevars Stv.empty ls.ls_value in
84 85
  List.fold_left ty_freevars acc ls.ls_args

86
(** Patterns *)
87 88 89

type pattern = {
  pat_node : pattern_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
90
  pat_vars : Svs.t;
91
  pat_ty   : ty;
92 93
}

Andrei Paskevich's avatar
Andrei Paskevich committed
94
and pattern_node =
95 96 97 98
  | Pwild (* _ *)
  | Pvar of vsymbol (* newly introduced variables *)
  | Papp of lsymbol * pattern list (* application *)
  | Por  of pattern * pattern (* | *)
Andrei Paskevich's avatar
Andrei Paskevich committed
99
  | Pas  of pattern * vsymbol
100
  (* naming a term recognized by pattern as a variable *)
101

102
(* h-consing constructors for patterns *)
103

104
let mk_pattern n vs ty = {
Andrei Paskevich's avatar
Andrei Paskevich committed
105 106 107 108 109 110 111 112 113 114
  pat_node = n;
  pat_vars = vs;
  pat_ty   = ty;
}

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
115 116

let pat_as p v =
117
  let s = Svs.add_new (DuplicateVar v) v p.pat_vars in
118
  mk_pattern (Pas (p,v)) s v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
119 120

let pat_or p q =
121 122 123
  if Svs.equal p.pat_vars q.pat_vars then
    mk_pattern (Por (p,q)) p.pat_vars p.pat_ty
  else
124 125
    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
126 127

let pat_app f pl ty =
128 129
  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
130
  mk_pattern (Papp (f,pl)) (List.fold_left merge Svs.empty pl) ty
131

132 133
(* generic traversal functions *)

134
let pat_map fn pat = match pat.pat_node with
135 136 137
  | 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
138
  | Por (p, q) -> pat_or (fn p) (fn q)
139

140 141
let pat_map fn = pat_map (fun p ->
  let res = fn p in ty_equal_check p.pat_ty res.pat_ty; res)
142

143 144 145 146
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
147
  | Por (p, q) -> fn (fn acc p) q
148

149 150
let pat_all pr pat = Util.all pat_fold pr pat
let pat_any pr pat = Util.any pat_fold pr pat
151

152 153
(* smart constructors for patterns *)

154
exception BadArity of lsymbol * int
155 156
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
157
exception ConstructorExpected of lsymbol
158 159

let pat_app fs pl ty =
160
  let s = match fs.ls_value with
161
    | Some vty -> ty_match Mtv.empty vty ty
162 163
    | None -> raise (FunctionSymbolExpected fs)
  in
164
  let mtch s ty p = ty_match s ty p.pat_ty in
165 166
  ignore (try List.fold_left2 mtch s fs.ls_args pl with
    | Invalid_argument _ -> raise (BadArity (fs, List.length pl)));
167
  if fs.ls_constr = 0 then raise (ConstructorExpected fs);
168
  pat_app fs pl ty
169 170

let pat_as p v =
171
  ty_equal_check p.pat_ty v.vs_ty;
172
  pat_as p v
173

Andrei Paskevich's avatar
Andrei Paskevich committed
174
let pat_or p q =
175
  ty_equal_check p.pat_ty q.pat_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
176 177
  pat_or p q

178 179 180 181 182 183 184
(* 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

185 186
(* symbol-wise map/fold *)

187
let rec pat_gen_map fnT fnL m pat =
Andrei Paskevich's avatar
Andrei Paskevich committed
188
  let fn = pat_gen_map fnT fnL m in
189
  let ty = fnT pat.pat_ty in
190 191
  match pat.pat_node with
    | Pwild -> pat_wild ty
192
    | Pvar v -> pat_var (Mvs.find v m)
193
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
194
    | Pas (p, v) -> pat_as (fn p) (Mvs.find v m)
Andrei Paskevich's avatar
Andrei Paskevich committed
195
    | Por (p, q) -> pat_or (fn p) (fn q)
196

197 198
let rec pat_gen_fold fnT fnL acc pat =
  let fn acc p = pat_gen_fold fnT fnL acc p in
199
  let acc = fnT acc pat.pat_ty in
200
  match pat.pat_node with
201
    | Pwild | Pvar _ -> acc
202
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
203
    | Por (p, q) -> fn (fn acc p) q
204
    | Pas (p, _) -> fn acc p
205

206
(** Terms and formulas *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
207

208
type quant =
209 210
  | Tforall
  | Texists
211 212

type binop =
213 214 215 216
  | Tand
  | Tor
  | Timplies
  | Tiff
217

Andrei Paskevich's avatar
Andrei Paskevich committed
218
type term = {
219
  t_node  : term_node;
220
  t_ty    : ty option;
221
  t_label : Slab.t;
222
  t_loc   : Loc.position option;
223 224
}

Andrei Paskevich's avatar
Andrei Paskevich committed
225
and term_node =
226
  | Tvar of vsymbol
227
  | Tconst of Number.constant
228
  | Tapp of lsymbol * term list
229
  | Tif of term * term * term
230
  | Tlet of term * term_bound
Andrei Paskevich's avatar
Andrei Paskevich committed
231
  | Tcase of term * term_branch list
232 233 234 235 236 237 238
  | Teps of term_bound
  | Tquant of quant * term_quant
  | Tbinop of binop * term * term
  | Tnot of term
  | Ttrue
  | Tfalse

239 240
and term_bound  = vsymbol * bind_info * term
and term_branch = pattern * bind_info * term
241
and term_quant  = vsymbol list * bind_info * trigger * term
242

243
and trigger = term list list
244

245
and bind_info = {
246
  bv_vars  : int Mvs.t;   (* free variables *)
247
  bv_subst : term Mvs.t   (* deferred substitution *)
248 249
}

250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
(* term equality modulo alpha-equivalence and location *)

exception CompLT
exception CompGT

type frame = int Mvs.t * term Mvs.t

type term_or_bound =
  | Trm of term * frame list
  | Bnd of int

let rec descend vml t = match t.t_node with
  | Tvar vs ->
      let rec find vs = function
        | (bv,vm)::vml ->
            begin match Mvs.find_opt vs bv with
            | Some i -> Bnd i
            | None ->
                begin match Mvs.find_opt vs vm with
                | Some t -> descend vml t
                | None   -> find vs vml
                end
            end
        | [] -> Trm (t, [])
      in
      find vs vml
  | _ -> Trm (t, vml)

278
let t_compare trigger label t1 t2 =
279 280 281
  let comp_raise c =
    if c < 0 then raise CompLT else if c > 0 then raise CompGT in
  let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
282
  let rec pat_compare (bnd,bv1,bv2 as state) p1 p2 =
283 284 285 286 287
    match p1.pat_node, p2.pat_node with
    | Pwild, Pwild ->
        bnd, bv1, bv2
    | Pvar v1, Pvar v2 ->
        bnd + 1, Mvs.add v1 bnd bv1, Mvs.add v2 bnd bv2
Andrei Paskevich's avatar
Andrei Paskevich committed
288 289 290
    | Papp (s1, l1), Papp (s2, l2) ->
        comp_raise (ls_compare s1 s2);
        List.fold_left2 pat_compare state l1 l2
291
    | Por (p1, q1), Por (p2, q2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
292
        let (_,bv1,bv2 as res) = pat_compare state p1 p2 in
293 294 295 296
        let rec or_cmp q1 q2 = match q1.pat_node, q2.pat_node with
          | Pwild, Pwild -> ()
          | Pvar v1, Pvar v2 ->
              perv_compare (Mvs.find v1 bv1) (Mvs.find v2 bv2)
Andrei Paskevich's avatar
Andrei Paskevich committed
297 298
          | Papp (s1, l1), Papp (s2, l2) ->
              comp_raise (ls_compare s1 s2);
299 300 301 302 303 304 305 306 307 308 309 310 311 312
              List.iter2 or_cmp l1 l2
          | Por (p1, q1), Por (p2, q2) ->
              or_cmp p1 p2; or_cmp q1 q2
          | Pas (p1, v1), Pas (p2, v2) ->
              or_cmp p1 p2;
              perv_compare (Mvs.find v1 bv1) (Mvs.find v2 bv2)
          | Pwild,  _ -> raise CompLT | _, Pwild  -> raise CompGT
          | Pvar _, _ -> raise CompLT | _, Pvar _ -> raise CompGT
          | Papp _, _ -> raise CompLT | _, Papp _ -> raise CompGT
          | Por _,  _ -> raise CompLT | _, Por _  -> raise CompGT
        in
        or_cmp q1 q2;
        res
    | Pas (p1, v1), Pas (p2, v2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
313
        let bnd, bv1, bv2 = pat_compare state p1 p2 in
314 315 316 317 318 319 320
        bnd + 1, Mvs.add v1 bnd bv1, Mvs.add v2 bnd bv2
    | Pwild, _  -> raise CompLT | _, Pwild  -> raise CompGT
    | Pvar _, _ -> raise CompLT | _, Pvar _ -> raise CompGT
    | Papp _, _ -> raise CompLT | _, Papp _ -> raise CompGT
    | Por _, _  -> raise CompLT | _, Por _  -> raise CompGT
  in
  let rec t_compare bnd vml1 vml2 t1 t2 =
321
    if t1 != t2 || vml1 <> [] || vml2 <> [] then begin
Andrei Paskevich's avatar
Andrei Paskevich committed
322
      comp_raise (oty_compare t1.t_ty t2.t_ty);
323
      if label then comp_raise (Slab.compare t1.t_label t2.t_label) else ();
324 325 326 327 328 329
      match descend vml1 t1, descend vml2 t2 with
      | Bnd i1, Bnd i2 -> perv_compare i1 i2
      | Bnd _, Trm _ -> raise CompLT
      | Trm _, Bnd _ -> raise CompGT
      | Trm (t1,vml1), Trm (t2,vml2) ->
          begin match t1.t_node, t2.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
330 331 332
          | Tvar v1, Tvar v2 ->
              comp_raise (vs_compare v1 v2)
          | Tconst c1, Tconst c2 ->
333 334 335 336 337 338 339 340
              let open Number in
              begin match c1, c2 with
              | ConstInt { ic_negative = s1; ic_abs = IConstRaw b1 },
                ConstInt { ic_negative = s2; ic_abs = IConstRaw b2 } ->
                  perv_compare s1 s2;
                  comp_raise (BigInt.compare b1 b2)
              | _, _ -> perv_compare c1 c2
              end
Andrei Paskevich's avatar
Andrei Paskevich committed
341 342
          | Tapp (s1,l1), Tapp (s2,l2) ->
              comp_raise (ls_compare s1 s2);
343 344 345 346 347 348 349 350 351 352 353 354 355
              List.iter2 (t_compare bnd vml1 vml2) l1 l2
          | Tif (f1,t1,e1), Tif (f2,t2,e2) ->
              t_compare bnd vml1 vml2 f1 f2;
              t_compare bnd vml1 vml2 t1 t2;
              t_compare bnd vml1 vml2 e1 e2
          | Tlet (t1,(v1,b1,e1)), Tlet (t2,(v2,b2,e2)) ->
              t_compare bnd vml1 vml2 t1 t2;
              let vml1 = (Mvs.singleton v1 bnd, b1.bv_subst) :: vml1 in
              let vml2 = (Mvs.singleton v2 bnd, b2.bv_subst) :: vml2 in
              t_compare (bnd + 1) vml1 vml2 e1 e2
          | Tcase (t1,bl1), Tcase (t2,bl2) ->
              t_compare bnd vml1 vml2 t1 t2;
              let b_compare (p1,b1,t1) (p2,b2,t2) =
Andrei Paskevich's avatar
Andrei Paskevich committed
356
                let bnd,bv1,bv2 = pat_compare (bnd,Mvs.empty,Mvs.empty) p1 p2 in
357 358
                let vml1 = (bv1, b1.bv_subst) :: vml1 in
                let vml2 = (bv2, b2.bv_subst) :: vml2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
359 360
                t_compare bnd vml1 vml2 t1 t2; 0 in
              comp_raise (Lists.compare b_compare bl1 bl2)
361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
          | Teps (v1,b1,e1), Teps (v2,b2,e2) ->
              let vml1 = (Mvs.singleton v1 bnd, b1.bv_subst) :: vml1 in
              let vml2 = (Mvs.singleton v2 bnd, b2.bv_subst) :: vml2 in
              t_compare (bnd + 1) vml1 vml2 e1 e2
          | Tquant (q1,(vl1,b1,tr1,f1)), Tquant (q2,(vl2,b2,tr2,f2)) ->
              perv_compare q1 q2;
              let rec add bnd bv1 bv2 vl1 vl2 = match vl1, vl2 with
                | (v1::vl1), (v2::vl2) ->
                    let bv1 = Mvs.add v1 bnd bv1 in
                    let bv2 = Mvs.add v2 bnd bv2 in
                    add (bnd + 1) bv1 bv2 vl1 vl2
                | [], (_::_) -> raise CompLT
                | (_::_), [] -> raise CompGT
                | [], [] -> bnd, bv1, bv2 in
              let bnd, bv1, bv2 = add bnd Mvs.empty Mvs.empty vl1 vl2 in
              let vml1 = (bv1, b1.bv_subst) :: vml1 in
              let vml2 = (bv2, b2.bv_subst) :: vml2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
378
              let tr_cmp t1 t2 = t_compare bnd vml1 vml2 t1 t2; 0 in
379
              if trigger then comp_raise (Lists.compare (Lists.compare tr_cmp) tr1 tr2) else ();
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
              t_compare bnd vml1 vml2 f1 f2
          | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) ->
              perv_compare op1 op2;
              t_compare bnd vml1 vml2 f1 f2;
              t_compare bnd vml1 vml2 g1 g2
          | Tnot f1, Tnot f2 ->
              t_compare bnd vml1 vml2 f1 f2
          | Ttrue, Ttrue -> ()
          | Tfalse, Tfalse -> ()
          | Tvar _, _   -> raise CompLT | _, Tvar _   -> raise CompGT
          | Tconst _, _ -> raise CompLT | _, Tconst _ -> raise CompGT
          | Tapp _, _   -> raise CompLT | _, Tapp _   -> raise CompGT
          | Tif _, _    -> raise CompLT | _, Tif _    -> raise CompGT
          | Tlet _, _   -> raise CompLT | _, Tlet _   -> raise CompGT
          | Tcase _, _  -> raise CompLT | _, Tcase _  -> raise CompGT
          | Teps _, _   -> raise CompLT | _, Teps _   -> raise CompGT
          | Tquant _, _ -> raise CompLT | _, Tquant _ -> raise CompGT
          | Tbinop _, _ -> raise CompLT | _, Tbinop _ -> raise CompGT
          | Tnot _, _   -> raise CompLT | _, Tnot _   -> raise CompGT
          | Ttrue, _    -> raise CompLT | _, Ttrue    -> raise CompGT
          end
    end in
  try t_compare 0 [] [] t1 t2; 0
  with CompLT -> -1 | CompGT -> 1

405 406 407 408 409
let t_equal t1 t2 = (t_compare true true t1 t2 = 0)

let t_equal_nt_nl t1 t2 = (t_compare false false t1 t2 = 0)

let t_compare = t_compare true true
410

411
let t_similar t1 t2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
412 413
  oty_equal t1.t_ty t2.t_ty &&
  match t1.t_node, t2.t_node with
414 415
    | Tvar v1, Tvar v2 -> vs_equal v1 v2
    | Tconst c1, Tconst c2 -> c1 = c2
Andrei Paskevich's avatar
Andrei Paskevich committed
416 417 418 419 420 421 422 423 424
    | Tapp (s1,l1), Tapp (s2,l2) -> ls_equal s1 s2 && Lists.equal (==) l1 l2
    | Tif (f1,t1,e1), Tif (f2,t2,e2) -> f1 == f2 && t1 == t2 && e1 == e2
    | Tlet (t1,bv1), Tlet (t2,bv2) -> t1 == t2 && bv1 == bv2
    | Tcase (t1,bl1), Tcase (t2,bl2) -> t1 == t2 && Lists.equal (==) bl1 bl2
    | Teps bv1, Teps bv2 -> bv1 == bv2
    | Tquant (q1,bv1), Tquant (q2,bv2) -> q1 = q2 && bv1 == bv2
    | Tbinop (o1,f1,g1), Tbinop (o2,f2,g2) -> o1 = o2 && f1 == f2 && g1 == g2
    | Tnot f1, Tnot f2 -> f1 == f2
    | Ttrue, Ttrue | Tfalse, Tfalse -> true
425 426
    | _, _ -> false

427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
let t_hash t =
  let rec pat_hash bnd bv p = match p.pat_node with
    | Pwild -> bnd, bv, 0
    | Pvar v -> bnd + 1, Mvs.add v bnd bv, bnd + 1
    | Papp (s,l) ->
        let hash (bnd,bv,h) p =
          let bnd,bv,hp = pat_hash bnd bv p in
          bnd, bv, Hashcons.combine h hp in
        List.fold_left hash (bnd,bv,ls_hash s) l
    | Por (p,q) ->
        let bnd,bv,hp = pat_hash bnd bv p in
        let rec or_hash q = match q.pat_node with
          | Pwild -> 0
          | Pvar v -> Mvs.find v bv + 1
          | Papp (s,l) -> Hashcons.combine_list or_hash (ls_hash s) l
          | Por (p,q) -> Hashcons.combine (or_hash p) (or_hash q)
          | Pas (p,v) -> Hashcons.combine (or_hash p) (Mvs.find v bv + 1)
        in
        bnd, bv, Hashcons.combine hp (or_hash q)
    | Pas (p,v) ->
        let bnd,bv,hp = pat_hash bnd bv p in
        bnd + 1, Mvs.add v bnd bv, Hashcons.combine hp (bnd + 1)
  in
  let rec t_hash bnd vml t =
    let comb l h = Hashcons.combine (lab_hash l) h in
    let h = Slab.fold comb t.t_label (oty_hash t.t_ty) in
    Hashcons.combine h
      begin match descend vml t with
      | Bnd i -> i + 1
      | Trm (t,vml) ->
          begin match t.t_node with
          | Tvar v -> vs_hash v
          | Tconst c -> Hashtbl.hash c
          | Tapp (s,l) ->
              Hashcons.combine_list (t_hash bnd vml) (ls_hash s) l
          | Tif (f,t,e) ->
              let hf = t_hash bnd vml f in
              let ht = t_hash bnd vml t in
              let he = t_hash bnd vml e in
              Hashcons.combine2 hf ht he
          | Tlet (t,(v,b,e)) ->
              let h = t_hash bnd vml t in
              let vml = (Mvs.singleton v bnd, b.bv_subst) :: vml in
              Hashcons.combine h (t_hash (bnd + 1) vml e)
          | Tcase (t,bl) ->
              let h = t_hash bnd vml t in
              let b_hash (p,b,t) =
                let bnd,bv,hp = pat_hash bnd Mvs.empty p in
                let vml = (bv, b.bv_subst) :: vml in
                Hashcons.combine hp (t_hash bnd vml t) in
              Hashcons.combine_list b_hash h bl
          | Teps (v,b,e) ->
              let vml = (Mvs.singleton v bnd, b.bv_subst) :: vml in
              t_hash (bnd + 1) vml e
          | Tquant (q,(vl,b,tr,f)) ->
              let h = Hashtbl.hash q in
              let rec add bnd bv vl = match vl with
                | v::vl -> add (bnd + 1) (Mvs.add v bnd bv) vl
                | [] -> bnd, bv in
              let bnd, bv = add bnd Mvs.empty vl in
              let vml = (bv, b.bv_subst) :: vml in
              let h = List.fold_left
                (Hashcons.combine_list (t_hash bnd vml)) h tr in
              Hashcons.combine h (t_hash bnd vml f)
          | Tbinop (op,f,g) ->
              let ho = Hashtbl.hash op in
              let hf = t_hash bnd vml f in
              let hg = t_hash bnd vml g in
              Hashcons.combine2 ho hf hg
          | Tnot f ->
              Hashcons.combine 1 (t_hash bnd vml f)
          | Ttrue -> 2
          | Tfalse -> 3
          end
    end in
  t_hash 0 [] t
Andrei Paskevich's avatar
Andrei Paskevich committed
503

504
(* type checking *)
505 506 507 508 509 510 511 512

exception TermExpected of term
exception FmlaExpected of term

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

513
let t_prop f =
Andrei Paskevich's avatar
Andrei Paskevich committed
514
  if f.t_ty = None then f else raise (FmlaExpected f)
515

516 517
let t_ty_check t ty = match ty, t.t_ty with
  | Some l, Some r -> ty_equal_check l r
518 519 520 521
  | Some _, None -> raise (TermExpected t)
  | None, Some _ -> raise (FmlaExpected t)
  | None, None -> ()

522 523
let vs_check v t = ty_equal_check v.vs_ty (t_type t)

524
(* trigger equality and traversal *)
525

526
let tr_equal = Lists.equal (Lists.equal t_equal)
527

528 529
let tr_map fn = List.map (List.map fn)
let tr_fold fn = List.fold_left (List.fold_left fn)
530
let tr_map_fold fn = Lists.map_fold_left (Lists.map_fold_left fn)
531

532
(* bind_info equality, hash, and traversal *)
533

534
let bnd_map fn bv = { bv with bv_subst = Mvs.map fn bv.bv_subst }
535

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

538
let bnd_map_fold fn acc bv =
539 540
  let acc,s = Mvs.mapi_fold (fun _ t a -> fn a t) bv.bv_subst acc in
  acc, { bv with bv_subst = s }
541

542 543
(* hash-consing for terms and formulas *)

544
let vars_union s1 s2 = Mvs.union (fun _ m n -> Some (m + n)) s1 s2
545

546
let add_b_vars s (_,b,_) = vars_union s b.bv_vars
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547

548 549 550 551 552 553 554 555 556 557 558 559
let rec t_vars t = match t.t_node with
  | Tvar v -> Mvs.singleton v 1
  | Tconst _ -> Mvs.empty
  | Tapp (_,tl) -> List.fold_left add_t_vars Mvs.empty tl
  | Tif (f,t,e) -> add_t_vars (add_t_vars (t_vars f) t) e
  | Tlet (t,bt) -> add_b_vars (t_vars t) bt
  | Tcase (t,bl) -> List.fold_left add_b_vars (t_vars t) bl
  | Teps (_,b,_) -> b.bv_vars
  | Tquant (_,(_,b,_,_)) -> b.bv_vars
  | Tbinop (_,f1,f2) -> add_t_vars (t_vars f1) f2
  | Tnot f -> t_vars f
  | Ttrue | Tfalse -> Mvs.empty
560

561
and add_t_vars s t = vars_union s (t_vars t)
562

563 564
let add_nt_vars _ n t s = vars_union s
  (if n = 1 then t_vars t else Mvs.map (( * ) n) (t_vars t))
565

566
module TermOHT = struct
567
  type t = term
568 569 570 571
  let hash = t_hash
  let equal = t_equal
  let compare = t_compare
end
572

573 574 575
module Mterm = Extmap.Make(TermOHT)
module Sterm = Extset.MakeOfMap(Mterm)
module Hterm = Exthtbl.Make(TermOHT)
576

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

579
let mk_term n ty = {
580
  t_node  = n;
581
  t_label = Slab.empty;
582
  t_loc   = None;
583 584
  t_ty    = ty;
}
585

586 587
let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
let t_const c ty    = mk_term (Tconst c) (Some ty)
588 589 590 591 592
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
593 594 595 596 597
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
598

599
let t_label ?loc l t = { t with t_label = l; t_loc = loc }
600

601
let t_label_add l t = { t with t_label = Slab.add l t.t_label }
602

603
let t_label_remove l t = { t with t_label = Slab.remove l t.t_label }
604

605
let t_label_copy s t =
Andrei Paskevich's avatar
Andrei Paskevich committed
606 607 608 609 610
  if s == t then s else
  if t_similar s t && Slab.is_empty t.t_label && t.t_loc = None then s else
  let lab = Slab.union s.t_label t.t_label in
  let loc = if t.t_loc = None then s.t_loc else t.t_loc in
  { t with t_label = lab; t_loc = loc }
611

612
(* unsafe map *)
613

614
let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e)
615

616
let t_map_unsafe fn t = t_label_copy t (match t.t_node with
617
  | Tvar _ | Tconst _ -> t
618 619 620 621 622 623 624 625
  | Tapp (f,tl) -> t_app f (List.map fn tl) t.t_ty
  | Tif (f,t1,t2) -> t_if (fn f) (fn t1) (fn t2)
  | 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
  | Tquant (q,(vl,b,tl,f)) -> t_quant q (vl, bnd_map fn b, tr_map fn tl, fn f)
  | Tbinop (op,f1,f2) -> t_binary op (fn f1) (fn f2)
  | Tnot f1 -> t_not (fn f1)
626
  | Ttrue | Tfalse -> t)
627

628
(* unsafe fold *)
629

630
let bound_fold fn acc (_,b,e) = fn (bnd_fold fn acc b) e
631

632
let t_fold_unsafe fn acc t = match t.t_node with
633
  | Tvar _ | Tconst _ -> acc
634 635 636 637 638
  | 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
639 640 641 642
  | 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
643

644 645
(* unsafe map_fold *)

646 647 648
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
649 650
  acc, (u,b,e)

651
let t_map_fold_unsafe fn acc t = match t.t_node with
652
  | Tvar _ | Tconst _ ->
653 654
      acc, t
  | Tapp (f,tl) ->
655
      let acc,sl = Lists.map_fold_left fn acc tl in
656
      acc, t_label_copy t (t_app f sl t.t_ty)
657
  | Tif (f,t1,t2) ->
658 659 660 661
      let acc, g  = fn acc f in
      let acc, s1 = fn acc t1 in
      let acc, s2 = fn acc t2 in
      acc, t_label_copy t (t_if g s1 s2)
662
  | Tlet (e,b) ->
663 664
      let acc, e = fn acc e in
      let acc, b = bound_map_fold fn acc b in
665 666
      acc, t_label_copy t (t_let e b t.t_ty)
  | Tcase (e,bl) ->
667
      let acc, e = fn acc e in
668
      let acc, bl = Lists.map_fold_left (bound_map_fold fn) acc bl in
669 670
      acc, t_label_copy t (t_case e bl t.t_ty)
  | Teps b ->
671
      let acc, b = bound_map_fold fn acc b in
672
      acc, t_label_copy t (t_eps b t.t_ty)
673
  | Tquant (q,(vl,b,tl,f1)) ->
674 675 676
      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
677 678
      acc, t_label_copy t (t_quant q (vl,b,tl,f1))
  | Tbinop (op,f1,f2) ->
679 680 681
      let acc, g1 = fn acc f1 in
      let acc, g2 = fn acc f2 in
      acc, t_label_copy t (t_binary op g1 g2)
682
  | Tnot f1 ->
683 684
      let acc, g1 = fn acc f1 in
      acc, t_label_copy t (t_not g1)
685
  | Ttrue | Tfalse ->
686 687
      acc, t

688 689 690 691
(* type-unsafe term substitution *)

let rec t_subst_unsafe m t =
  let t_subst t = t_subst_unsafe m t in
692 693 694
  let b_subst (u,b,e as bv) =
    if Mvs.set_disjoint m b.bv_vars then bv else
    (u, bv_subst_unsafe m b, e) in
695 696
  match t.t_node with
  | Tvar u ->
697
      t_label_copy t (Mvs.find_def t u m)
698
  | Tlet (e, bt) ->
699 700
      let d = t_subst e in
      t_label_copy t (t_let d (b_subst bt) t.t_ty)
701
  | Tcase (e, bl) ->
702
      let d = t_subst e in
703
      let bl = List.map b_subst bl in
704
      t_label_copy t (t_case d bl t.t_ty)
705 706
  | Teps bf ->
      t_label_copy t (t_eps (b_subst bf) t.t_ty)
707 708 709 710 711
  | Tquant (q, (vl,b,tl,f1 as bq)) ->
      let bq =
        if Mvs.set_disjoint m b.bv_vars then bq else
        (vl,bv_subst_unsafe m b,tl,f1) in
      t_label_copy t (t_quant q bq)
712
  | _ ->
713
      t_map_unsafe t_subst t
714 715 716

and bv_subst_unsafe m b =
  (* restrict m to the variables free in b *)
717
  let m = Mvs.set_inter m b.bv_vars in
718 719 720
  (* if m is empty, return early *)
  if Mvs.is_empty m then b else
  (* remove from b.bv_vars the variables replaced by m *)
721
  let s = Mvs.set_diff b.bv_vars m in
722
  (* add to b.bv_vars the free variables added by m *)
723
  let s = Mvs.fold2_inter add_nt_vars b.bv_vars m s in
724 725 726
  (* 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 *)
727
  let h = Mvs.set_union h m in
728 729 730 731 732 733 734
  (* 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 *)
735

736
let bnd_new s = { bv_vars = s ; bv_subst = Mvs.empty }
737

738
let t_close_bound v t = (v, bnd_new (Mvs.remove v (t_vars t)), t)
739

740
let t_close_branch p t = (p, bnd_new (Mvs.set_diff (t_vars t) p.pat_vars), t)
741

742
let t_close_quant vl tl f =
743
  let del_v s v = Mvs.remove v s in
744
  let s = tr_fold add_t_vars (t_vars f) tl in
745
  let s = List.fold_left del_v s vl in
746
  (vl, bnd_new s, tl, t_prop f)
747

748
(* open bindings *)
749

750 751
let fresh_vsymbol v =
  create_vsymbol (id_clone v.vs_name) v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
752

753 754
let vs_rename h v =
  let u = fresh_vsymbol v in
755
  Mvs.add v (t_var u) h, u
756

757
let vl_rename h vl =
758
  Lists.map_fold_left vs_rename h vl
759

760 761
let pat_rename h p =
  let add_vs v () = fresh_vsymbol v in
762
  let m = Mvs.mapi add_vs p.pat_vars in
763
  let p = pat_rename_all m p in
Andrei Paskevich's avatar
Andrei Paskevich committed
764 765
  Mvs.union (fun _ _ t -> Some t) h (Mvs.map t_var m), p

766
let t_open_bound (v,b,t) =
767 768
  let m,v = vs_rename b.bv_subst v in
  v, t_subst_unsafe m t
769

770 771 772 773 774
let t_open_bound_with e (v,b,t) =
  vs_check v e;
  let m = Mvs.add v e b.bv_subst in
  t_subst_unsafe m t

775
let t_open_branch (p,b,t) =
776 777
  let m,p = pat_rename b.bv_subst p in
  p, t_subst_unsafe m t
778

779
let t_open_quant (vl,b,tl,f) =
780
  let m,vl = vl_rename b.bv_subst vl in
781
  let tl = tr_map (t_subst_unsafe m) tl in
782
  vl, tl, t_subst_unsafe m f
783

784 785
let t_clone_bound_id (v,_,_) = id_clone v.vs_name

786 787 788 789 790
(** open bindings with optimized closing callbacks *)

let t_open_bound_cb tb =
  let v, t = t_open_bound tb in
  let close v' t' =
791
    if t == t' && vs_equal v v' then tb else t_close_bound v' t'
792 793 794 795 796 797
  in
  v, t, close

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