term.ml 53.7 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
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
(*                                                                  *)
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;
Andrei Paskevich's avatar
Andrei Paskevich committed
221
  t_attrs : Sattr.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)

Andrei Paskevich's avatar
Andrei Paskevich committed
278
let t_compare trigger attr 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);
Andrei Paskevich's avatar
Andrei Paskevich committed
323
      if attr then comp_raise (Sattr.compare t1.t_attrs t2.t_attrs) 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
              comp_raise (Number.compare_const c1 c2)
Andrei Paskevich's avatar
Andrei Paskevich committed
334 335
          | Tapp (s1,l1), Tapp (s2,l2) ->
              comp_raise (ls_compare s1 s2);
336 337 338 339 340 341 342 343 344 345 346 347 348
              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
349
                let bnd,bv1,bv2 = pat_compare (bnd,Mvs.empty,Mvs.empty) p1 p2 in
350 351
                let vml1 = (bv1, b1.bv_subst) :: vml1 in
                let vml2 = (bv2, b2.bv_subst) :: vml2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
352 353
                t_compare bnd vml1 vml2 t1 t2; 0 in
              comp_raise (Lists.compare b_compare bl1 bl2)
354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
          | 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
371
              let tr_cmp t1 t2 = t_compare bnd vml1 vml2 t1 t2; 0 in
372
              if trigger then comp_raise (Lists.compare (Lists.compare tr_cmp) tr1 tr2) else ();
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397
              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

398 399
let t_equal t1 t2 = (t_compare true true t1 t2 = 0)

Andrei Paskevich's avatar
Andrei Paskevich committed
400
let t_equal_nt_na t1 t2 = (t_compare false false t1 t2 = 0)
401 402

let t_compare = t_compare true true
403

404
let t_similar t1 t2 =
405 406
  oty_equal t1.t_ty t2.t_ty &&
  match t1.t_node, t2.t_node with
407
    | Tvar v1, Tvar v2 -> vs_equal v1 v2
408
    | Tconst c1, Tconst c2 -> Number.compare_const c1 c2 = 0
Andrei Paskevich's avatar
Andrei Paskevich committed
409 410 411 412 413 414 415 416 417
    | 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
418 419
    | _, _ -> false

420
let t_hash trigger attr t =
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
  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 =
444 445 446 447 448 449 450
    let h = oty_hash t.t_ty in
    let h =
      if attr then
        let comb l h = Hashcons.combine (attr_hash l) h in
        Sattr.fold comb t.t_attrs h
      else h
    in
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
    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
486 487 488 489 490 491
              let h =
                if trigger then
                  List.fold_left
                    (Hashcons.combine_list (t_hash bnd vml)) h tr
                else h
              in
492 493 494 495 496 497 498 499 500 501 502 503 504
              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
505

506
(* type checking *)
507 508 509 510 511 512 513 514

exception TermExpected of term
exception FmlaExpected of term

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

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

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

524 525
let vs_check v t = ty_equal_check v.vs_ty (t_type t)

526
(* trigger equality and traversal *)
527

528
let tr_equal = Lists.equal (Lists.equal t_equal)
529

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

534
(* bind_info equality, hash, and traversal *)
535

536
let bnd_map fn bv = { bv with bv_subst = Mvs.map fn bv.bv_subst }
537

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

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

544 545
(* hash-consing for terms and formulas *)

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

548
let add_b_vars s (_,b,_) = vars_union s b.bv_vars
549

550 551 552 553 554 555 556 557 558 559 560 561
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
562

563
and add_t_vars s t = vars_union s (t_vars t)
564

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

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

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

579 580 581 582 583 584 585 586 587 588
module TermOHT_nt_na = struct
  type t = term
  let hash = t_hash false false
  let equal = t_equal_nt_na
end

module Hterm_nt_na = Exthtbl.Make(TermOHT_nt_na)

let t_hash = t_hash true true

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

591
let mk_term n ty = {
592
  t_node  = n;
Andrei Paskevich's avatar
Andrei Paskevich committed
593
  t_attrs = Sattr.empty;
594
  t_loc   = None;
595 596
  t_ty    = ty;
}
597

598 599
let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
let t_const c ty    = mk_term (Tconst c) (Some ty)
600 601 602 603 604
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
605 606 607 608 609
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
610

Andrei Paskevich's avatar
Andrei Paskevich committed
611
let t_attr_set ?loc l t = { t with t_attrs = l; t_loc = loc }
612

Andrei Paskevich's avatar
Andrei Paskevich committed
613
let t_attr_add l t = { t with t_attrs = Sattr.add l t.t_attrs }
614

Andrei Paskevich's avatar
Andrei Paskevich committed
615
let t_attr_remove l t = { t with t_attrs = Sattr.remove l t.t_attrs }
616

Andrei Paskevich's avatar
Andrei Paskevich committed
617
let t_attr_copy s t =
618
  if s == t then s else
Andrei Paskevich's avatar
Andrei Paskevich committed
619 620
  if t_similar s t && Sattr.is_empty t.t_attrs && t.t_loc = None then s else
  let attrs = Sattr.union s.t_attrs t.t_attrs in
621
  let loc = if t.t_loc = None then s.t_loc else t.t_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
622
  { t with t_attrs = attrs; t_loc = loc }
623

624
(* unsafe map *)
625

626
let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e)
627

Andrei Paskevich's avatar
Andrei Paskevich committed
628
let t_map_unsafe fn t = t_attr_copy t (match t.t_node with
629
  | Tvar _ | Tconst _ -> t
630 631 632 633 634 635 636 637
  | 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)
638
  | Ttrue | Tfalse -> t)
639

640
(* unsafe fold *)
641

642
let bound_fold fn acc (_,b,e) = fn (bnd_fold fn acc b) e
643

644
let t_fold_unsafe fn acc t = match t.t_node with
645
  | Tvar _ | Tconst _ -> acc
646 647 648 649 650
  | 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
651 652 653 654
  | 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
655

656 657
(* unsafe map_fold *)

658 659 660
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
661 662
  acc, (u,b,e)

663
let t_map_fold_unsafe fn acc t = match t.t_node with
664
  | Tvar _ | Tconst _ ->
665 666
      acc, t
  | Tapp (f,tl) ->
667
      let acc,sl = Lists.map_fold_left fn acc tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
668
      acc, t_attr_copy t (t_app f sl t.t_ty)
669
  | Tif (f,t1,t2) ->
670 671 672
      let acc, g  = fn acc f in
      let acc, s1 = fn acc t1 in
      let acc, s2 = fn acc t2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
673
      acc, t_attr_copy t (t_if g s1 s2)
674
  | Tlet (e,b) ->
675 676
      let acc, e = fn acc e in
      let acc, b = bound_map_fold fn acc b in
Andrei Paskevich's avatar
Andrei Paskevich committed
677
      acc, t_attr_copy t (t_let e b t.t_ty)
678
  | Tcase (e,bl) ->
679
      let acc, e = fn acc e in
680
      let acc, bl = Lists.map_fold_left (bound_map_fold fn) acc bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
681
      acc, t_attr_copy t (t_case e bl t.t_ty)
682
  | Teps b ->
683
      let acc, b = bound_map_fold fn acc b in
Andrei Paskevich's avatar
Andrei Paskevich committed
684
      acc, t_attr_copy t (t_eps b t.t_ty)
685
  | Tquant (q,(vl,b,tl,f1)) ->
686 687 688
      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
Andrei Paskevich's avatar
Andrei Paskevich committed
689
      acc, t_attr_copy t (t_quant q (vl,b,tl,f1))
690
  | Tbinop (op,f1,f2) ->
691 692
      let acc, g1 = fn acc f1 in
      let acc, g2 = fn acc f2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
693
      acc, t_attr_copy t (t_binary op g1 g2)
694
  | Tnot f1 ->
695
      let acc, g1 = fn acc f1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
696
      acc, t_attr_copy t (t_not g1)
697
  | Ttrue | Tfalse ->
698 699
      acc, t

700 701 702 703
(* type-unsafe term substitution *)

let rec t_subst_unsafe m t =
  let t_subst t = t_subst_unsafe m t in
704 705 706
  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
707 708
  match t.t_node with
  | Tvar u ->
Andrei Paskevich's avatar
Andrei Paskevich committed
709
      t_attr_copy t (Mvs.find_def t u m)
710
  | Tlet (e, bt) ->
711
      let d = t_subst e in
Andrei Paskevich's avatar
Andrei Paskevich committed
712
      t_attr_copy t (t_let d (b_subst bt) t.t_ty)
713
  | Tcase (e, bl) ->
714
      let d = t_subst e in
715
      let bl = List.map b_subst bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
716
      t_attr_copy t (t_case d bl t.t_ty)
717
  | Teps bf ->
Andrei Paskevich's avatar
Andrei Paskevich committed
718
      t_attr_copy t (t_eps (b_subst bf) t.t_ty)
719 720 721 722
  | 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
Andrei Paskevich's avatar
Andrei Paskevich committed
723
      t_attr_copy t (t_quant q bq)
724
  | _ ->
725
      t_map_unsafe t_subst t
726 727 728

and bv_subst_unsafe m b =
  (* restrict m to the variables free in b *)
729
  let m = Mvs.set_inter m b.bv_vars in
730 731 732
  (* if m is empty, return early *)
  if Mvs.is_empty m then b else
  (* remove from b.bv_vars the variables replaced by m *)
733
  let s = Mvs.set_diff b.bv_vars m in
734
  (* add to b.bv_vars the free variables added by m *)
735
  let s = Mvs.fold2_inter add_nt_vars b.bv_vars m s in
736 737 738
  (* 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 *)
739
  let h = Mvs.set_union h m in
740 741 742 743 744 745 746
  (* 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 *)
747

748
let bnd_new s = { bv_vars = s ; bv_subst = Mvs.empty }
749

750
let t_close_bound v t = (v, bnd_new (Mvs.remove v (t_vars t)), t)
751

752
let t_close_branch p t = (p, bnd_new (Mvs.set_diff (t_vars t) p.pat_vars), t)
753

754
let t_close_quant vl tl f =
755
  let del_v s v = Mvs.remove v s in
756
  let s = tr_fold add_t_vars (t_vars f) tl in
757
  let s = List.fold_left del_v s vl in
758
  (vl, bnd_new s, tl, t_prop f)
759

760
(* open bindings *)
761

762 763
let fresh_vsymbol v =
  create_vsymbol (id_clone v.vs_name) v.vs_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
764

765 766
let vs_rename h v =
  let u = fresh_vsymbol v in
767
  Mvs.add v (t_var u) h, u
768

769
let vl_rename h vl =
770
  Lists.map_fold_left vs_rename h vl
771

772 773
let pat_rename h p =
  let add_vs v () = fresh_vsymbol v in
774
  let m = Mvs.mapi add_vs p.pat_vars in
775
  let p = pat_rename_all m p in
Andrei Paskevich's avatar
Andrei Paskevich committed
776 777
  Mvs.union (fun _ _ t -> Some t) h (Mvs.map t_var m), p

778
let t_open_bound (v,b,t) =
779 780
  let m,v = vs_rename b.bv_subst v in
  v, t_subst_unsafe m t
781

782 783 784 785 786
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

787
let t_open_branch (p,b,t) =
788 789
  let m,p = pat_rename b.bv_subst p in
  p, t_subst_unsafe m t
790

791
let t_open_quant (vl,b,tl,f) =
792
  let m,vl = vl_rename b.bv_subst vl in
793
  let tl = tr_map (t_subst_unsafe m) tl in
794
  vl, tl, t_subst_unsafe m f
795

796 797
let t_clone_bound_id (v,_,_) = id_clone v.vs_name

798 799 800 801 802
(** open bindings with optimized closing callbacks *)

let t_open_bound_cb tb =
  let v, t = t_open_bound tb in
  let close v' t' =
803
    if t == t' && vs_equal v v' then tb else t_close_bound v' t'
804 805 806 807 808 809
  in
  v, t, close

let t_open_branch_cb tbr =
  let p, t = t_open_branch tbr in
  let close p' t' =
810
    if t == t' && p == p' then tbr else t_close_branch p' t'
811 812 813
  in
  p, t, close

814 815
let t_open_quant_cb fq =
  let vl, tl, f = t_open_quant fq in
816
  let close vl' tl' f' =
817 818 819
    if f == f' &&
      Lists.equal (Lists.equal ((==) : term -> term -> bool)) tl tl' &&
      Lists.equal vs_equal vl vl'
820
    then fq else t_close_quant vl' tl' f'
821 822 823 824
  in
  vl, tl, f, close

(* constructors with type checking *)
825

826
let ls_arg_inst ls tl =
827
  let mtch s ty t = ty_match s ty (t_type t) in
828 829
  try List.fold_left2 mtch Mtv.empty ls.ls_args tl with
    | Invalid_argument _ -> raise (BadArity (ls, List.length tl))
830

831
let ls_app_inst ls tl ty =
832 833
  let s = ls_arg_inst ls tl in
  match ls.ls_value, ty with
834 835
    | Some _, None -> raise (PredicateSymbolExpected ls)
    | None, Some _ -> raise (FunctionSymbolExpected ls)
836 837
    | Some vty, Some ty -> ty_match s vty ty
    | None, None -> s
838

839 840 841
let t_app_infer ls tl =
  let s = ls_arg_inst ls tl in
  t_app ls tl (oty_inst s ls.ls_value)
842

843 844 845 846 847
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

Andrei Paskevich's avatar
Andrei Paskevich committed
848
let t_nat_const n =
849
  assert (n >= 0);
850
  t_const (Number.int_const_of_int n) ty_int
851

852 853 854 855 856
let t_int_const n =
  t_const (Number.int_const n) Ty.ty_int

let t_real_const ?pow2 ?pow5 s =
  t_const (Number.real_const ?pow2 ?pow5 s) Ty.ty_real
Clément Fumex's avatar
Clément Fumex committed
857

MARCHE Claude's avatar
MARCHE Claude committed
858 859
exception InvalidIntegerLiteralType of ty
exception InvalidRealLiteralType of ty
Clément Fumex's avatar
Clément Fumex committed
860

861
let check_literal c ty =
862 863 864 865 866 867 868 869 870 871 872 873
  let open Number in
  let ts = match ty.ty_node, c with
    | Tyapp (ts,[]), _ -> ts
    | _, ConstInt _ -> raise (InvalidIntegerLiteralType ty)
    | _, ConstReal _ -> raise (InvalidRealLiteralType ty) in
  match c, ts.ts_def with
  | ConstInt _, _ when ts_equal ts ts_int -> ()
  | ConstInt n, Range ir -> check_range n ir
  | ConstInt _, _ -> raise (InvalidIntegerLiteralType ty)
  | ConstReal _, _ when ts_equal ts ts_real -> ()
  | ConstReal x, Float fp -> check_float x fp
  | ConstReal _, _ -> raise (InvalidRealLiteralType ty)
874

875 876
let t_const c ty = check_literal c ty; t_const c ty

877 878 879 880 881
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) =
882
  vs_check v t1;
883
  t_let t1 bt t2.t_ty
884

885
exception EmptyCase
886

887
let t_case t bl =
888 889
  let tty = t_type t in
  let bty = match bl with
890
    | (_,_,tbr) :: _ -> tbr.t_ty
891
    | _ -> raise EmptyCase
892
  in
893
  let t_check_branch (p,_,tbr) =
894 895
    ty_equal_check tty p.pat_ty;
    t_ty_check tbr bty
896 897
  in
  List.iter t_check_branch bl;
898
  t_case t bl bty
899

900 901
let t_eps ((v,_,f) as bf) =
  ignore (t_prop f);
902
  t_eps bf (Some v.vs_ty)
903

904 905
let t_quant q ((vl,_,_,f) as qf) =
  if vl = [] then f else t_quant q qf
906

907 908
let t_binary op f1 f2 = t_binary op (t_prop f1) (t_prop f2)
let t_not f = t_not (t_prop f)
909

910 911 912 913 914 915
let t_forall  = t_quant Tforall
let t_exists  = t_quant Texists
let t_and     = t_binary