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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
17
type label = string
18

19
(** Types *)
20
21
22

module Ty = struct

23
24
25
26
  type tvsymbol = Name.t

  (* type symbols and types *)

27
  type tysymbol = {
28
29
30
31
    ts_name : Name.t;
    ts_args : tvsymbol list;
    ts_def  : ty option;
    ts_tag  : int;
32
33
  }

Andrei Paskevich's avatar
Andrei Paskevich committed
34
35
36
37
  and ty = {
    ty_node : ty_node;
    ty_tag : int;
  }
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
  and ty_node =
40
    | Tyvar of tvsymbol
41
42
    | Tyapp of tysymbol * ty list

43
44
45
46
47
48
49
50
  module Tsym = struct
    type t = tysymbol
    let equal ts1 ts2 = Name.equal ts1.ts_name ts2.ts_name
    let hash ts = Name.hash ts.ts_name
    let tag n ts = { ts with ts_tag = n }
  end
  module Hts = Hashcons.Make(Tsym)

51
  let mk_ts name args def = {
52
53
54
55
    ts_name = name;
    ts_args = args;
    ts_def  = def;
    ts_tag  = -1
56
57
  }

58
  let create_tysymbol name args def = Hts.hashcons (mk_ts name args def)
Andrei Paskevich's avatar
Andrei Paskevich committed
59

60
  module Ty = struct
61

62
63
64
    type t = ty

    let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
65
66
67
      | Tyvar n1, Tyvar n2 -> Name.equal n1 n2
      | Tyapp (s1, l1), Tyapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
      | _ -> false
68

69
    let hash_ty ty = ty.ty_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70

71
    let hash ty = match ty.ty_node with
72
73
      | Tyvar v -> Name.hash v
      | Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl
74

75
    let tag n ty = { ty with ty_tag = n }
Andrei Paskevich's avatar
Andrei Paskevich committed
76

77
  end
78
  module Hty = Hashcons.Make(Ty)
79

80
81
82
  let mk_ty n = { ty_node = n; ty_tag = -1 }
  let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
  let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))
83

84
85
86
87
88
89
  exception BadTypeArity

  let ty_app s tl =
    if List.length tl == List.length s.ts_args
      then ty_app s tl else raise BadTypeArity

90
  exception TypeMismatch
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91

92
93
94
95
96
97
98
99
100
101
102
103
104
  let rec matching s ty1 ty2 =
    if ty1 == ty2 then s
    else match ty1.ty_node, ty2.ty_node with
      | Tyvar n1, _ ->
          (try if Name.M.find n1 s == ty2 then s else raise TypeMismatch
          with Not_found -> Name.M.add n1 ty2 s)
      | Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
          List.fold_left2 matching s l1 l2
      | _ ->
          raise TypeMismatch

  let ty_match ty1 ty2 s =
    try Some (matching s ty1 ty2) with TypeMismatch -> None
105

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
end
107

108
type tvsymbol = Ty.tvsymbol
109
110
111
type tysymbol = Ty.tysymbol
type ty = Ty.ty

112
(** Variable symbols *)
113

114
115
116
117
type vsymbol = {
  vs_name : Name.t;
  vs_ty   : ty;
  vs_tag  : int;
118
119
}

120
121
122
123
124
125
126
module Vsym = struct
  type t = vsymbol
  let equal vs1 vs2 = Name.equal vs1.vs_name vs2.vs_name
  let hash vs = Name.hash vs.vs_name
  let tag n vs = { vs with vs_tag = n }
  let compare vs1 vs2 = Pervasives.compare vs1.vs_tag vs2.vs_tag
end
127

128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
module Hvs = Hashcons.Make(Vsym)
module Mvs = Map.Make(Vsym)
module Svs = Set.Make(Vsym)

let mk_vs name ty = { vs_name = name; vs_ty = ty; vs_tag = -1 }
let create_vsymbol name ty = Hvs.hashcons (mk_vs name ty)

(* TODO: needs refactoring *)
let fresh_vsymbol v = create_vsymbol (Name.fresh v.vs_name) v.vs_ty

(** Function symbols *)

type fsymbol = {
  fs_name   : Name.t;
  fs_scheme : ty list * ty;
  fs_constr : bool;
  fs_tag    : int;
145
146
}

147
148
149
150
151
152
153
154
155
156
157
158
159
module Fsym = struct
  type t = fsymbol
  let equal fs1 fs2 = Name.equal fs1.fs_name fs2.fs_name
  let hash fs = Name.hash fs.fs_name
  let tag n fs = { fs with fs_tag = n }
end
module Hfs = Hashcons.Make(Fsym)

let mk_fs name scheme constr = {
  fs_name = name;
  fs_scheme = scheme;
  fs_constr = constr;
  fs_tag = -1
160
161
}

162
let create_fsymbol name scheme constr = Hfs.hashcons (mk_fs name scheme constr)
163

164
(** Predicate symbols *)
165

166
167
168
169
170
type psymbol = {
  ps_name   : Name.t;
  ps_scheme : ty list;
  ps_tag    : int;
}
171

172
173
174
175
176
177
178
179
180
181
182
183
module Psym = struct
  type t = psymbol
  let equal ps1 ps2 = Name.equal ps1.ps_name ps2.ps_name
  let hash ps = Name.hash ps.ps_name
  let tag n ps = { ps with ps_tag = n }
end
module Hps = Hashcons.Make(Psym)

let mk_ps name scheme = { ps_name = name; ps_scheme = scheme; ps_tag = -1 }
let create_psymbol name scheme = Hps.hashcons (mk_ps name scheme)

(** Hpats *)
184
185
186

type pattern = {
  pat_node : pattern_node;
187
  pat_ty : ty;
188
189
190
  pat_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
191
192
193
and pattern_node =
  | Pwild
  | Pvar of vsymbol
194
195
196
  | Papp of fsymbol * pattern list
  | Pas of pattern * vsymbol

197
module Hpat = struct
198

199
  type t = pattern
200

201
  let equal_node p1 p2 = match p1, p2 with
202
203
204
205
206
    | Pwild, Pwild -> true
    | Pvar v1, Pvar v2 -> v1 == v2
    | Papp (s1, l1), Papp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
    | Pas (p1, n1), Pas (p2, n2) -> p1 == p2 && n1 == n2
    | _ -> false
207

208
209
210
  let equal p1 p2 =
    equal_node p1.pat_node p2.pat_node && p1.pat_ty == p2.pat_ty

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

213
  let hash_node = function
214
    | Pwild -> 0
215
216
217
    | Pvar v -> v.vs_tag
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.fs_tag pl
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_tag
218

219
220
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.Ty.ty_tag

221
  let tag n p = { p with pat_tag = n }
222

223
end
224
225
226
module Hp = Hashcons.Make(Hpat)

(* h-consing constructors for patterns *)
227

228
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
229
230
231
232
233
234
235
let pat_wild ty = Hp.hashcons (mk_pattern Pwild ty)
let pat_var v = Hp.hashcons (mk_pattern (Pvar v) v.vs_ty)
let pat_app f pl ty = Hp.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p v = Hp.hashcons (mk_pattern (Pas (p, v)) p.pat_ty)

(* smart constructors for patterns *)

236
237
exception BadArity

238
239
240
exception ConstructorExpected

let pat_app f pl ty =
241
  if not f.fs_constr then raise ConstructorExpected else
242
243
  let args, res = f.fs_scheme in
  let _ =
244
245
246
247
    try List.fold_left2 Ty.matching
        (Ty.matching Name.M.empty res ty)
        args (List.map (fun p -> p.pat_ty) pl)
    with Invalid_argument _ -> raise BadArity
248
  in
249
  pat_app f pl ty
250
251
252
253
254
255

let pat_as p v =
  if p.pat_ty == v.vs_ty then pat_as p v else raise Ty.TypeMismatch

(* alpha-equality on patterns *)

256
let rec pat_equal_alpha p1 p2 =
257
258
259
260
261
  p1 == p2 ||
  p1.pat_ty == p2.pat_ty &&
  match p1.pat_node, p2.pat_node with
  | Pwild, Pwild | Pvar _, Pvar _ -> true
  | Papp (f1, l1), Papp (f2, l2) ->
262
263
      f1 == f2 && List.for_all2 pat_equal_alpha l1 l2
  | Pas (p1, _), Pas (p2, _) -> pat_equal_alpha p1 p2
264
265
266
267
268
269
270
271
272
273
274
275
276
277
  | _ -> false

(** Terms and formulas *)

type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
291
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292
  | Tbvar of int
293
294
  | Tvar of vsymbol
  | Tapp of fsymbol * term list
295
296
297
  | Tlet of term * term_bound
  | Tcase of term * term_branch list
  | Teps of fmla_bound
298

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

310
and term_bound = vsymbol * term
311

312
and fmla_bound = vsymbol * fmla
313

314
and term_branch = pattern * int * term
315

316
and fmla_branch = pattern * int * fmla
317

318
319
module T = struct

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
320
321
  type t = term

322
  let t_eq_branch (p1, _, t1) (p2, _, t2) = p1 == p2 && t1 == t2
Andrei Paskevich's avatar
Andrei Paskevich committed
323

324
  let t_eq_bound (v1, t1) (v2, t2) = v1 == v2 && t1 == t2
325

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

328
  let t_equal_node t1 t2 = match t1, t2 with
329
330
331
    | Tbvar x1, Tbvar x2 -> x1 == x2
    | Tvar v1, Tvar v2 -> v1 == v2
    | Tapp (s1, l1), Tapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
332
    | Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
    | Tcase (t1, l1), Tcase (t2, l2) ->
334
        t1 == t2 &&
335
        (try List.for_all2 t_eq_branch l1 l2
336
        with Invalid_argument _ -> false)
337
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
338
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339

340
  let equal t1 t2 =
341
    t_equal_node t1.t_node t2.t_node &&
342
343
344
345
    t1.t_ty == t2.t_ty &&
    try List.for_all2 (=) t1.t_label t2.t_label
    with Invalid_argument _ -> false

346
  let t_hash_branch (p, _, t) = Hashcons.combine p.pat_tag t.t_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347

348
  let t_hash_bound (v, t) = Hashcons.combine v.vs_tag t.t_tag
349

350
  let f_hash_bound (v, f) = Hashcons.combine v.vs_tag f.f_tag
351

352
  let t_hash t = t.t_tag
353

354
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355
    | Tbvar n -> n
356
    | Tvar v -> v.vs_tag
357
358
359
360
    | Tapp (f, tl) -> Hashcons.combine_list t_hash (f.fs_tag) tl
    | Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
    | Tcase (t, bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
    | Teps f -> f_hash_bound f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
361

362
  let hash t =
363
    Hashcons.combine (t_hash_node t.t_node)
364
      (Hashcons.combine_list Hashtbl.hash t.t_ty.Ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
365

366
  let tag n t = { t with t_tag = n }
367

368
369
  let compare t1 t2 = Pervasives.compare t1.t_tag t2.t_tag

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
370
end
371
module Hterm = Hashcons.Make(T)
372
373
module Mterm = Map.Make(T)
module Sterm = Set.Make(T)
374
375

module F = struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
376
377
378

  type t = fmla

379
  let f_eq_branch (p1, _, f1) (p2, _, f2) = p1 == p2 && f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
380

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

383
  let f_equal_node f1 f2 = match f1, f2 with
384
385
    | Fapp (s1, l1), Fapp (s2, l2) ->
        s1 == s2 && List.for_all2 (==) l1 l2
386
    | Fquant (q1, b1), Fquant (q2, b2) ->
387
        q1 == q2 && f_eq_bound b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
389
        op1 == op2 && f1 == f2 && g1 == g2
390
391
    | Fnot f1, Fnot f2 ->
        f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
392
    | Ftrue, Ftrue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393
    | Ffalse, Ffalse ->
Andrei Paskevich's avatar
Andrei Paskevich committed
394
        true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
395
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
396
        f1 == f2 && g1 == g2 && h1 == h2
397
    | Flet (t1, b1), Flet (t2, b2) ->
398
        t1 == t2 && f_eq_bound b1 b2
399
    | Fcase (t1, l1), Fcase (t2, l2) ->
400
        t1 == t2 &&
401
        (try List.for_all2 f_eq_branch l1 l2
402
        with Invalid_argument _ -> false)
Andrei Paskevich's avatar
Andrei Paskevich committed
403
404
    | _ ->
        false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405

406
  let equal f1 f2 =
407
    f_equal_node f1.f_node f2.f_node &&
408
409
    try List.for_all2 (=) f1.f_label f2.f_label
    with Invalid_argument _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410

411
  let f_hash_branch (p, _, f) = Hashcons.combine p.pat_tag f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412

413
  let f_hash_bound (v, f) = Hashcons.combine v.vs_tag f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414

415
  let t_hash t = t.t_tag
416

417
  let f_hash f = f.f_tag
418

419
420
421
  let f_hash_node = function
    | Fapp (p, tl) -> Hashcons.combine_list t_hash p.ps_tag tl
    | Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_bound bf)
Andrei Paskevich's avatar
Andrei Paskevich committed
422
    | Fbinop (op, f1, f2) ->
423
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
424
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425
426
    | Ftrue -> 0
    | Ffalse -> 1
427
    | Fif (f1, f2, f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
428
429
    | Flet (t, bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
    | Fcase (t, bl) -> Hashcons.combine_list f_hash_branch t.t_tag bl
430
431

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

434
  let tag n f = { f with f_tag = n }
435

436
437
  let compare f1 f2 = Pervasives.compare f1.f_tag f2.f_tag

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
439
end
module Hfmla = Hashcons.Make(F)
440
441
module Mfmla = Map.Make(F)
module Sfmla = Set.Make(F)
442

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

445
let mk_term n ty = { t_node = n; t_label = []; t_ty = ty; t_tag = -1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
446
let t_bvar n ty = Hterm.hashcons (mk_term (Tbvar n) ty)
447
let t_var v = Hterm.hashcons (mk_term (Tvar v) v.vs_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448
let t_app f tl ty = Hterm.hashcons (mk_term (Tapp (f, tl)) ty)
449
let t_let v t1 t2 = Hterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
450
let t_case t bl ty = Hterm.hashcons (mk_term (Tcase (t, bl)) ty)
451
let t_eps u f = Hterm.hashcons (mk_term (Teps (u, f)) u.vs_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452

453
454
455
let t_label l t = Hterm.hashcons { t with t_label = l }
let t_label_add l t = Hterm.hashcons { t with t_label = l :: t.t_label }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456
(* hash-consing constructors for formulas *)
457
458

let mk_fmla n = { f_node = n; f_label = []; f_tag = -1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459
let f_app f tl = Hfmla.hashcons (mk_fmla (Fapp (f, tl)))
460
let f_quant q u f = Hfmla.hashcons (mk_fmla (Fquant (q, (u, f))))
461

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
462
463
464
465
466
let f_binary op f1 f2 = Hfmla.hashcons (mk_fmla (Fbinop (op, f1, f2)))
let f_and = f_binary Fand
let f_or = f_binary For
let f_implies = f_binary Fimplies
let f_iff = f_binary Fiff
467

468
469
470
let f_not f = Hfmla.hashcons (mk_fmla (Fnot f))
let f_true = Hfmla.hashcons (mk_fmla Ftrue)
let f_false = Hfmla.hashcons (mk_fmla Ffalse)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
471
let f_if f1 f2 f3 = Hfmla.hashcons (mk_fmla (Fif (f1, f2, f3)))
472
let f_let v t f = Hfmla.hashcons (mk_fmla (Flet (t, (v, f))))
473
let f_case t bl = Hfmla.hashcons (mk_fmla (Fcase (t, bl)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474
475
476
477

let f_label l f = Hfmla.hashcons { f with f_label = l }
let f_label_add l f = Hfmla.hashcons { f with f_label = l :: f.f_label }

478
479
480
481
(* unsafe map with level *)

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

482
let t_map_unsafe fnT fnF lvl t = match t.t_node with
483
484
  | Tbvar _ | Tvar _ -> t
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
485
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
486
  | Tcase (t1, bl) -> t_case (fnT lvl t1) (List.map (brlvl fnT lvl) bl) t.t_ty
487
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f)
488

489
let f_map_unsafe fnT fnF lvl f = match f.f_node with
490
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
491
  | Fquant (q, (u, f1)) -> f_quant q u (fnF (lvl + 1) f1)
492
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
493
  | Fnot f1 -> f_not (fnF lvl f1)
494
495
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
496
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
497
498
  | Fcase (t, bl) -> f_case (fnT lvl t) (List.map (brlvl fnF lvl) bl)

499
500
501
502
(* unsafe fold with level *)

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

503
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
504
505
506
507
508
509
  | Tbvar _ | Tvar _ -> acc
  | Tapp (f, tl) -> List.fold_left (fnT lvl) acc tl
  | Tlet (t1, (u, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
  | Tcase (t1, bl) -> List.fold_left (brlvl fnT lvl) (fnT lvl acc t1) bl
  | Teps (u, f) -> fnF (lvl + 1) acc f

510
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
511
512
513
514
515
516
517
518
519
520
521
522
523
  | Fapp (p, tl) -> List.fold_left (fnT lvl) acc tl
  | Fquant (q, (u, f1)) -> fnF (lvl + 1) acc f1
  | Fbinop (op, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
  | Fnot f1 -> fnF lvl acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
  | Flet (t, (u, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
  | Fcase (t, bl) -> List.fold_left (brlvl fnF lvl) (fnT lvl acc t) bl

exception FoldSkip

let forall_fnT prT lvl _ t = prT lvl t || raise FoldSkip
let forall_fnF prF lvl _ f = prF lvl f || raise FoldSkip
524
525
let exists_fnT prT lvl _ t = prT lvl t && raise FoldSkip
let exists_fnF prF lvl _ f = prF lvl f && raise FoldSkip
526

527
528
let t_forall_unsafe prT prF lvl t =
  try t_fold_unsafe (forall_fnT prT) (forall_fnF prF) lvl true t
529
530
  with FoldSkip -> false

531
532
let f_forall_unsafe prT prF lvl f =
  try f_fold_unsafe (forall_fnT prT) (forall_fnF prF) lvl true f
533
534
  with FoldSkip -> false

535
536
let t_exists_unsafe prT prF lvl t =
  try t_fold_unsafe (exists_fnT prT) (exists_fnF prF) lvl false t
537
538
  with FoldSkip -> true

539
540
let f_exists_unsafe prT prF lvl f =
  try f_fold_unsafe (exists_fnT prT) (exists_fnF prF) lvl false f
541
542
543
  with FoldSkip -> true

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

545
let rec t_abst m lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
546
  | Tvar u ->
547
      (try t_bvar (Mvs.find u m + lvl) t.t_ty with Not_found -> t)
548
  | _ -> t_map_unsafe (t_abst m) (f_abst m) lvl t
549

550
and f_abst m lvl f = f_map_unsafe (t_abst m) (f_abst m) lvl f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
551

552
553
let t_abst_single v t = t_abst (Mvs.add v 0 Mvs.empty) 0 t
let f_abst_single v f = f_abst (Mvs.add v 0 Mvs.empty) 0 f
554
555

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

557
module Im = Map.Make(struct type t = int let compare = Pervasives.compare end)
558

559
let rec t_inst m lvl t = match t.t_node with
560
  | Tbvar n when n >= lvl ->
561
      (try t_var (Im.find (n - lvl) m) with Not_found -> assert false)
562
  | _ -> t_map_unsafe (t_inst m) (f_inst m) lvl t
563

564
and f_inst m lvl f = f_map_unsafe (t_inst m) (f_inst m) lvl f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
565

566
567
let t_inst_single v t = t_inst (Im.add 0 v Im.empty) 0 t
let f_inst_single v f = f_inst (Im.add 0 v Im.empty) 0 f
568

Andrei Paskevich's avatar
Andrei Paskevich committed
569
570
(* looks for free de Bruijn indices *)

571
let rec t_closed lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
572
  | Tbvar x -> x < lvl
573
  | _ -> t_forall_unsafe t_closed f_closed lvl t
Andrei Paskevich's avatar
Andrei Paskevich committed
574

575
and f_closed lvl f = f_forall_unsafe t_closed f_closed lvl f
Andrei Paskevich's avatar
Andrei Paskevich committed
576

577
578
(* looks for occurrence of a variable from set [s] in a term [t] *)

579
let rec t_occurs s lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
580
  | Tvar u -> Svs.mem u s
581
  | _ -> t_exists_unsafe (t_occurs s) (f_occurs s) lvl t
582

583
and f_occurs s lvl f = f_exists_unsafe (t_occurs s) (f_occurs s) lvl f
584

585
586
let t_occurs_single v t = t_occurs (Svs.add v Svs.empty) 0 t
let f_occurs_single v f = f_occurs (Svs.add v Svs.empty) 0 f
587

588
589
let t_occurs s t = t_occurs s 0 t
let f_occurs s f = f_occurs s 0 f
590
591
592

(* replaces variables with terms in term [t] using map [m] *)

593
let rec t_subst m lvl t = match t.t_node with
594
  | Tvar u -> (try Mvs.find u m with Not_found -> t)
595
  | _ -> t_map_unsafe (t_subst m) (f_subst m) lvl t
596

597
and f_subst m lvl f = f_map_unsafe (t_subst m) (f_subst m) lvl f
598

599
let t_subst_single v t1 t =
600
  if v.vs_ty == t1.t_ty then t_subst (Mvs.add v t1 Mvs.empty) 0 t
601
602
                        else raise Ty.TypeMismatch

603
let f_subst_single v t1 f =
604
  if v.vs_ty == t1.t_ty then f_subst (Mvs.add v t1 Mvs.empty) 0 f
605
606
607
608
                        else raise Ty.TypeMismatch

let vt_check v t = if v.vs_ty == t.t_ty then () else raise Ty.TypeMismatch

609
610
let t_subst m t = let _ = Mvs.iter vt_check m in t_subst m 0 t
let f_subst m f = let _ = Mvs.iter vt_check m in f_subst m 0 f
611
612
613

(* set of free variables *)

614
let rec t_freevars lvl acc t = match t.t_node with
615
  | Tvar u -> Svs.add u acc
616
  | _ -> t_fold_unsafe t_freevars f_freevars lvl acc t
617

618
and f_freevars lvl acc t = f_fold_unsafe t_freevars f_freevars lvl acc t
619

620
621
let t_freevars t = t_freevars 0 Svs.empty t
let f_freevars f = f_freevars 0 Svs.empty f
622

623
624
(* USE PHYSICAL EQUALITY *)
(*
625
626
627
628
(* equality *)

let t_equal = (==)
let f_equal = (==)
629
*)
630

631
(* equality modulo alpha *)
632

633
let rec t_equal_alpha t1 t2 =
634
635
636
637
638
639
640
641
  t1 == t2 ||
  t1.t_ty == t2.t_ty &&
  match t1.t_node, t2.t_node with
    | Tbvar x1, Tbvar x2 ->
        x1 == x2
    | Tvar v1, Tvar v2 ->
        v1 == v2
    | Tapp (s1, l1), Tapp (s2, l2) ->
642
        (* assert (List.length l1 == List.length l2); *)
643
        s1 == s2 && List.for_all2 t_equal_alpha l1 l2
644
645
    | Tlet (t1, (v1, b1)), Tlet (t2, (v2, b2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
646
        t_equal_alpha t1 t2 && t_equal_alpha b1 b2
647
    | Tcase (t1, l1), Tcase (t2, l2) ->
648
649
        t_equal_alpha t1 t2 &&
        (try List.for_all2 t_branch_equal_alpha l1 l2
650
651
652
        with Invalid_argument _ -> false)
    | Teps (v1, f1), Teps (v2, f2) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
653
        f_equal_alpha f1 f2
654
655
    | _ -> false

656
and f_equal_alpha f1 f2 =
657
658
  f1 == f2 ||
  match f1.f_node, f2.f_node with
659
660
    | Fapp (s1, l1), Fapp (s2, l2) ->
        (* assert (List.length l1 == List.length l2); *)
661
        s1 == s2 && List.for_all2 t_equal_alpha l1 l2
662
    | Fquant (q1, (v1, f1)), Fquant (q2, (v2, f2)) ->
663
        q1 == q2 && v1.vs_ty == v2.vs_ty && f_equal_alpha f1 f2
664
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
665
        op1 == op2 && f_equal_alpha f1 f2 && f_equal_alpha g1 g2
666
    | Fnot f1, Fnot f2 ->
667
        f_equal_alpha f1 f2
668
669
670
671
    | Ftrue, Ftrue
    | Ffalse, Ffalse ->
        true
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
672
        f_equal_alpha f1 f2 && f_equal_alpha g1 g2 && f_equal_alpha h1 h2
673
674
    | Flet (t1, (v1, f1)), Flet (t2, (v2, f2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
675
        t_equal_alpha t1 t2 && f_equal_alpha f1 f2
676
    | Fcase (t1, l1), Fcase (t2, l2) ->
677
678
        t_equal_alpha t1 t2 &&
        (try List.for_all2 f_branch_equal_alpha l1 l2
679
        with Invalid_argument _ -> false)
680
    | _ -> false
681

682
683
and t_branch_equal_alpha (pat1, _, t1) (pat2, _, t2) =
  pat_equal_alpha pat1 pat2 && t_equal_alpha t1 t2
684

685
686
and f_branch_equal_alpha (pat1, _, f1) (pat2, _, f2) =
  pat_equal_alpha pat1 pat2 && f_equal_alpha f1 f2
687

688
689
690
691
(* matching modulo alpha in the pattern *)

exception NoMatch

Andrei Paskevich's avatar
Andrei Paskevich committed
692
let rec t_match s t1 t2 =
693
694
695
696
697
698
  if t1 == t2 then s else
  if t1.t_ty != t2.t_ty then raise NoMatch else
  match t1.t_node, t2.t_node with
    | Tbvar x1, Tbvar x2 when x1 == x2 ->
        s
    | Tvar v1, _ ->
699
        (try if Mvs.find v1 s == t2 then s else raise NoMatch
700
        with Not_found -> if t_closed 0 t2
701
          then Mvs.add v1 t2 s else raise NoMatch)
702
703
    | Tapp (s1, l1), Tapp (s2, l2) when s1 == s2 ->
        (* assert (List.length l1 == List.length l2); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
704
        List.fold_left2 t_match s l1 l2
705
706
    | Tlet (t1, (v1, b1)), Tlet (t2, (v2, b2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
707
        t_match (t_match s t1 t2) b1 b2
708
    | Tcase (t1, l1), Tcase (t2, l2) ->
709
        (try List.fold_left2 t_branch_match (t_match s t1 t2) l1 l2
710
711
712
        with Invalid_argument _ -> raise NoMatch)
    | Teps (v1, f1), Teps (v2, f2) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
713
        f_match s f1 f2
714
715
    | _ -> raise NoMatch

Andrei Paskevich's avatar
Andrei Paskevich committed
716
and f_match s f1 f2 =
717
718
719
720
  if f1 == f2 then s else
  match f1.f_node, f2.f_node with
    | Fapp (s1, l1), Fapp (s2, l2) when s1 == s2 ->
        (* assert (List.length l1 == List.length l2); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
721
        List.fold_left2 t_match s l1 l2
722
723
    | Fquant (q1, (v1, f1)), Fquant (q2, (v2, f2))
            when q1 == q2 && v1.vs_ty == v2.vs_ty ->
Andrei Paskevich's avatar
Andrei Paskevich committed
724
        f_match s f1 f2
725
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) when op1 == op2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
726
        f_match (f_match s f1 f2) g1 g2
727
    | Fnot f1, Fnot f2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
728
        f_match s f1 f2
729
730
731
732
    | Ftrue, Ftrue
    | Ffalse, Ffalse ->
        s
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
733
        f_match (f_match (f_match s f1 f2) g1 g2) h1 h2
734
735
    | Flet (t1, (v1, f1)), Flet (t2, (v2, f2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
736
        f_match (t_match s t1 t2) f1 f2
737
    | Fcase (t1, l1), Fcase (t2, l2) ->
738
        (try List.fold_left2 f_branch_match (t_match s t1 t2) l1 l2
739
740
741
        with Invalid_argument _ -> raise NoMatch)
    | _ -> raise NoMatch

742
743
and t_branch_match s (pat1, _, t1) (pat2, _, t2) =
  if pat_equal_alpha pat1 pat2 then t_match s t1 t2 else raise NoMatch
744

745
746
and f_branch_match s (pat1, _, f1) (pat2, _, f2) =
  if pat_equal_alpha pat1 pat2 then f_match s f1 f2 else raise NoMatch
747

Andrei Paskevich's avatar
Andrei Paskevich committed
748
749
let t_match t1 t2 s = try Some (t_match s t1 t2) with NoMatch -> None
let f_match f1 f2 s = try Some (f_match s f1 f2) with NoMatch -> None
750

751
752
753
(* occurrence check *)

let rec t_occurs_term r lvl t = r == t ||
754
  t_exists_unsafe (t_occurs_term r) (f_occurs_term r) lvl t
755

756
757
and f_occurs_term r lvl f =
  f_exists_unsafe (t_occurs_term r) (f_occurs_term r) lvl f
758
759

let t_occurs_term r t = t_occurs_term r 0 t
760
let f_occurs_term r f = f_occurs_term r 0 f
761

762
763
let rec t_occurs_fmla r lvl t =
  t_exists_unsafe (t_occurs_fmla r) (f_occurs_fmla r) lvl t
764
765

and f_occurs_fmla r lvl f = r == f ||
766
  f_exists_unsafe (t_occurs_fmla r) (f_occurs_fmla r) lvl f
767

768
let t_occurs_fmla r t = t_occurs_fmla r 0 t
769
770
771
772
let f_occurs_fmla r f = f_occurs_fmla r 0 f

(* occurrence check modulo alpha *)

773
774
let rec t_occurs_term_alpha r lvl t = t_equal_alpha r t ||
  t_exists_unsafe (t_occurs_term_alpha r) (f_occurs_term_alpha r) lvl t
775

776
777
and f_occurs_term_alpha r lvl f =
  f_exists_unsafe (t_occurs_term_alpha r) (f_occurs_term_alpha r) lvl f
778

779
780
let t_occurs_term_alpha r t = t_occurs_term_alpha r 0 t
let f_occurs_term_alpha r f = f_occurs_term_alpha r 0 f
781

782
783
let rec t_occurs_fmla_alpha r lvl t =
  t_exists_unsafe (t_occurs_fmla_alpha r) (f_occurs_fmla_alpha r) lvl t
784

785
786
and f_occurs_fmla_alpha r lvl f = f_equal_alpha r f ||
  f_exists_unsafe (t_occurs_fmla_alpha r) (f_occurs_fmla_alpha r) lvl f
787

788
789
let t_occurs_fmla_alpha r t = t_occurs_fmla_alpha r 0 t
let f_occurs_fmla_alpha r f = f_occurs_fmla_alpha r 0 f
790

791
(* substitutes term [t2] for term [t1] in term [t] *)
792
793

let rec t_subst_term t1 t2 lvl t =
794
  if t == t1 then t2 else
795
  t_map_unsafe (t_subst_term t1 t2) (f_subst_term t1 t2) lvl t
796

797
798
and f_subst_term t1 t2 lvl f =
  f_map_unsafe (t_subst_term t1 t2) (f_subst_term t1 t2) lvl f
799
800
801
802
803

let t_subst_term t1 t2 t =
  if t1.t_ty == t2.t_ty then t_subst_term t1 t2 0 t
                        else raise Ty.TypeMismatch

804
805
let f_subst_term t1 t2 f =
  if t1.t_ty == t2.t_ty then f_subst_term t1 t2 0 f
806
807
                        else raise Ty.TypeMismatch

808
(* substitutes fmla [f2] for fmla [f1] in term [t] *)
809

810
811
let rec t_subst_fmla f1 f2 lvl t =
  t_map_unsafe (t_subst_fmla f1 f2) (f_subst_fmla f1 f2) lvl t