MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

term.ml 35.2 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
20
21
22
23
24
25
26
exception FoldSkip

let forall_fn pr _ t = pr t || raise FoldSkip
let exists_fn pr _ t = pr t && raise FoldSkip

exception NonLinearPattern
exception UnboundVariable

27
(** Types *)
28
29
30

module Ty = struct

31
32
33
34
  type tvsymbol = Name.t

  (* type symbols and types *)

35
  type tysymbol = {
36
37
38
39
    ts_name : Name.t;
    ts_args : tvsymbol list;
    ts_def  : ty option;
    ts_tag  : int;
40
41
  }

Andrei Paskevich's avatar
Andrei Paskevich committed
42
43
44
45
  and ty = {
    ty_node : ty_node;
    ty_tag : int;
  }
46

Andrei Paskevich's avatar
Andrei Paskevich committed
47
  and ty_node =
48
    | Tyvar of tvsymbol
49
50
    | Tyapp of tysymbol * ty list

51
52
53
54
55
56
57
58
  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)

59
  let mk_ts name args def = {
60
61
62
63
    ts_name = name;
    ts_args = args;
    ts_def  = def;
    ts_tag  = -1
64
65
  }

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

68
  module Ty = struct
69

70
71
72
    type t = ty

    let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
73
74
75
      | Tyvar n1, Tyvar n2 -> Name.equal n1 n2
      | Tyapp (s1, l1), Tyapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
      | _ -> false
76

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

79
    let hash ty = match ty.ty_node with
80
81
      | Tyvar v -> Name.hash v
      | Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl
82

83
    let tag n ty = { ty with ty_tag = n }
Andrei Paskevich's avatar
Andrei Paskevich committed
84

85
  end
86
  module Hty = Hashcons.Make(Ty)
87

88
89
90
  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)))
91

92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
  (* generic traversal functions *)

  let ty_map fn ty = match ty.ty_node with
    | Tyvar _ -> ty
    | Tyapp (f, tl) -> ty_app f (List.map fn tl)

  let ty_fold fn acc ty = match ty.ty_node with
    | Tyvar _ -> acc
    | Tyapp (f, tl) -> List.fold_left fn acc tl

  let ty_forall pr ty =
    try ty_fold (forall_fn pr) true ty with FoldSkip -> false

  let ty_exists pr ty =
    try ty_fold (exists_fn pr) false ty with FoldSkip -> true

108
  (* smart constructors *)
Andrei Paskevich's avatar
Andrei Paskevich committed
109

110
111
  let tv_add_unique vs tv = if Name.S.mem tv vs
    then raise NonLinearPattern else Name.S.add tv vs
Andrei Paskevich's avatar
Andrei Paskevich committed
112

113
114
115
116
117
118
119
120
121
122
123
  let rec tv_known vs ty = match ty.ty_node with
    | Tyvar n -> Name.S.mem n vs
    | _ -> ty_forall (tv_known vs) ty

  let create_tysymbol name args def =
    let tvs = List.fold_left tv_add_unique Name.S.empty args in
    let _ = match def with
      | Some ty -> tv_known tvs ty || raise UnboundVariable
      | _ -> true
    in
    create_tysymbol name args def
124

125
126
127
128
129
130
  exception BadTypeArity

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

131
132
  (* type matching *)

133
  exception TypeMismatch
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134

135
136
137
138
139
140
141
142
143
144
145
146
147
  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
148

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
149
end
150

151
type tvsymbol = Ty.tvsymbol
152
153
154
type tysymbol = Ty.tysymbol
type ty = Ty.ty

155
(** Variable symbols *)
156

157
158
159
160
type vsymbol = {
  vs_name : Name.t;
  vs_ty   : ty;
  vs_tag  : int;
161
162
}

163
164
165
166
167
168
169
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
170

171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
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;
188
189
}

190
191
192
193
194
195
196
197
198
199
200
201
202
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
203
204
}

205
let create_fsymbol name scheme constr = Hfs.hashcons (mk_fs name scheme constr)
206

207
(** Predicate symbols *)
208

209
210
211
212
213
type psymbol = {
  ps_name   : Name.t;
  ps_scheme : ty list;
  ps_tag    : int;
}
214

215
216
217
218
219
220
221
222
223
224
225
226
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 *)
227
228
229

type pattern = {
  pat_node : pattern_node;
230
  pat_ty : ty;
231
232
233
  pat_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
234
235
236
and pattern_node =
  | Pwild
  | Pvar of vsymbol
237
238
239
  | Papp of fsymbol * pattern list
  | Pas of pattern * vsymbol

240
module Hpat = struct
241

242
  type t = pattern
243

244
  let equal_node p1 p2 = match p1, p2 with
245
246
247
248
249
    | 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
250

251
252
253
  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
254
255
  let hash_pattern p = p.pat_tag

256
  let hash_node = function
257
    | Pwild -> 0
258
259
260
    | 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
261

262
263
  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.Ty.ty_tag

264
  let tag n p = { p with pat_tag = n }
265

266
end
267
268
269
module Hp = Hashcons.Make(Hpat)

(* h-consing constructors for patterns *)
270

271
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
272
273
274
275
276
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)

277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
(* generic traversal functions *)

let pat_map_unsafe fn pat = match pat.pat_node with
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v

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

let pat_forall pr pat =
  try pat_fold (forall_fn pr) true pat with FoldSkip -> false

let pat_exists pr pat =
  try pat_fold (exists_fn pr) false pat with FoldSkip -> true

295
296
(* smart constructors for patterns *)

297
298
exception BadArity

299
300
301
exception ConstructorExpected

let pat_app f pl ty =
302
  if not f.fs_constr then raise ConstructorExpected else
303
304
  let args, res = f.fs_scheme in
  let _ =
305
306
307
308
    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
309
  in
310
  pat_app f pl ty
311
312
313
314

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

315
316
317
318
319
320
321
(* safe map over patterns *)

let pat_map fn pat = match pat.pat_node with
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v

322
323
(* alpha-equality on patterns *)

324
let rec pat_equal_alpha p1 p2 =
325
326
327
328
329
  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) ->
330
331
      f1 == f2 && List.for_all2 pat_equal_alpha l1 l2
  | Pas (p1, _), Pas (p2, _) -> pat_equal_alpha p1 p2
332
333
334
335
336
337
338
339
340
341
342
343
344
345
  | _ -> false

(** Terms and formulas *)

type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

Andrei Paskevich's avatar
Andrei Paskevich committed
346
347
type term = {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
  t_label : label list;
349
350
351
352
353
354
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355
  f_label : label list;
356
357
358
  f_tag : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
359
and term_node =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360
  | Tbvar of int
361
362
  | Tvar of vsymbol
  | Tapp of fsymbol * term list
363
364
365
  | Tlet of term * term_bound
  | Tcase of term * term_branch list
  | Teps of fmla_bound
366

Andrei Paskevich's avatar
Andrei Paskevich committed
367
and fmla_node =
368
  | Fapp of psymbol * term list
369
  | Fquant of quant * fmla_bound
370
  | Fbinop of binop * fmla * fmla
371
  | Fnot of fmla
372
373
374
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
375
376
  | Flet of term * fmla_bound
  | Fcase of term * fmla_branch list
377

378
and term_bound = vsymbol * term
379

380
and fmla_bound = vsymbol * fmla
381

382
and term_branch = pattern * int * term
383

384
and fmla_branch = pattern * int * fmla
385

386
387
module T = struct

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388
389
  type t = term

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

392
  let t_eq_bound (v1, t1) (v2, t2) = v1 == v2 && t1 == t2
393

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

396
  let t_equal_node t1 t2 = match t1, t2 with
397
398
399
    | 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
400
    | Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
401
    | Tcase (t1, l1), Tcase (t2, l2) ->
402
        t1 == t2 &&
403
        (try List.for_all2 t_eq_branch l1 l2
404
        with Invalid_argument _ -> false)
405
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
406
    | _ -> false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407

408
  let equal t1 t2 =
409
    t_equal_node t1.t_node t2.t_node &&
410
411
412
413
    t1.t_ty == t2.t_ty &&
    try List.for_all2 (=) t1.t_label t2.t_label
    with Invalid_argument _ -> false

414
  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
415

416
  let t_hash_bound (v, t) = Hashcons.combine v.vs_tag t.t_tag
417

418
  let f_hash_bound (v, f) = Hashcons.combine v.vs_tag f.f_tag
419

420
  let t_hash t = t.t_tag
421

422
  let t_hash_node = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
423
    | Tbvar n -> n
424
    | Tvar v -> v.vs_tag
425
426
427
428
    | 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
429

430
  let hash t =
431
    Hashcons.combine (t_hash_node t.t_node)
432
      (Hashcons.combine_list Hashtbl.hash t.t_ty.Ty.ty_tag t.t_label)
Andrei Paskevich's avatar
Andrei Paskevich committed
433

434
  let tag n t = { t with t_tag = n }
435

436
437
  let compare t1 t2 = Pervasives.compare t1.t_tag t2.t_tag

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
end
439
module Hterm = Hashcons.Make(T)
440
441
module Mterm = Map.Make(T)
module Sterm = Set.Make(T)
442
443

module F = struct
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
444
445
446

  type t = fmla

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

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

451
  let f_equal_node f1 f2 = match f1, f2 with
452
453
    | Fapp (s1, l1), Fapp (s2, l2) ->
        s1 == s2 && List.for_all2 (==) l1 l2
454
    | Fquant (q1, b1), Fquant (q2, b2) ->
455
        q1 == q2 && f_eq_bound b1 b2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
457
        op1 == op2 && f1 == f2 && g1 == g2
458
459
    | Fnot f1, Fnot f2 ->
        f1 == f2
Andrei Paskevich's avatar
Andrei Paskevich committed
460
    | Ftrue, Ftrue
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461
    | Ffalse, Ffalse ->
Andrei Paskevich's avatar
Andrei Paskevich committed
462
        true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
464
        f1 == f2 && g1 == g2 && h1 == h2
465
    | Flet (t1, b1), Flet (t2, b2) ->
466
        t1 == t2 && f_eq_bound b1 b2
467
    | Fcase (t1, l1), Fcase (t2, l2) ->
468
        t1 == t2 &&
469
        (try List.for_all2 f_eq_branch l1 l2
470
        with Invalid_argument _ -> false)
Andrei Paskevich's avatar
Andrei Paskevich committed
471
472
    | _ ->
        false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
473

474
  let equal f1 f2 =
475
    f_equal_node f1.f_node f2.f_node &&
476
477
    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
478

479
  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
480

481
  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
482

483
  let t_hash t = t.t_tag
484

485
  let f_hash f = f.f_tag
486

487
488
489
  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
490
    | Fbinop (op, f1, f2) ->
491
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
492
    | Fnot f -> Hashcons.combine 1 f.f_tag
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
493
494
    | Ftrue -> 0
    | Ffalse -> 1
495
    | Fif (f1, f2, f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
496
497
    | 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
498
499

  let hash f =
500
    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
501

502
  let tag n f = { f with f_tag = n }
503

504
505
  let compare f1 f2 = Pervasives.compare f1.f_tag f2.f_tag

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
506
507
end
module Hfmla = Hashcons.Make(F)
508
509
module Mfmla = Map.Make(F)
module Sfmla = Set.Make(F)
510

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

513
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
514
let t_bvar n ty = Hterm.hashcons (mk_term (Tbvar n) ty)
515
let t_var v = Hterm.hashcons (mk_term (Tvar v) v.vs_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516
let t_app f tl ty = Hterm.hashcons (mk_term (Tapp (f, tl)) ty)
517
let t_let v t1 t2 = Hterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
518
let t_case t bl ty = Hterm.hashcons (mk_term (Tcase (t, bl)) ty)
519
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
520

521
522
523
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
524
(* hash-consing constructors for formulas *)
525
526

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530
531
532
533
534
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
535

536
537
538
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
539
let f_if f1 f2 f3 = Hfmla.hashcons (mk_fmla (Fif (f1, f2, f3)))
540
let f_let v t f = Hfmla.hashcons (mk_fmla (Flet (t, (v, f))))
541
let f_case t bl = Hfmla.hashcons (mk_fmla (Fcase (t, bl)))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
542
543
544
545

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 }

546
547
548
549
(* unsafe map with level *)

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

550
let t_map_unsafe fnT fnF lvl t = match t.t_node with
551
552
  | Tbvar _ | Tvar _ -> t
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
553
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
554
  | Tcase (t1, bl) -> t_case (fnT lvl t1) (List.map (brlvl fnT lvl) bl) t.t_ty
555
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f)
556

557
let f_map_unsafe fnT fnF lvl f = match f.f_node with
558
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
559
  | Fquant (q, (u, f1)) -> f_quant q u (fnF (lvl + 1) f1)
560
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
561
  | Fnot f1 -> f_not (fnF lvl f1)
562
563
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
564
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
565
566
  | Fcase (t, bl) -> f_case (fnT lvl t) (List.map (brlvl fnF lvl) bl)

567
568
569
570
(* unsafe fold with level *)

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

571
let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
572
573
574
575
576
577
  | 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

578
let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
579
580
581
582
583
584
585
586
587
588
589
  | 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

let forall_fnT prT lvl _ t = prT lvl t || raise FoldSkip
let forall_fnF prF lvl _ f = prF lvl f || raise FoldSkip
590
591
let exists_fnT prT lvl _ t = prT lvl t && raise FoldSkip
let exists_fnF prF lvl _ f = prF lvl f && raise FoldSkip
592

593
594
let t_forall_unsafe prT prF lvl t =
  try t_fold_unsafe (forall_fnT prT) (forall_fnF prF) lvl true t
595
596
  with FoldSkip -> false

597
598
let f_forall_unsafe prT prF lvl f =
  try f_fold_unsafe (forall_fnT prT) (forall_fnF prF) lvl true f
599
600
  with FoldSkip -> false

601
602
let t_exists_unsafe prT prF lvl t =
  try t_fold_unsafe (exists_fnT prT) (exists_fnF prF) lvl false t
603
604
  with FoldSkip -> true

605
606
let f_exists_unsafe prT prF lvl f =
  try f_fold_unsafe (exists_fnT prT) (exists_fnF prF) lvl false f
607
608
609
  with FoldSkip -> true

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

611
let rec t_abst m lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
612
  | Tvar u ->
613
      (try t_bvar (Mvs.find u m + lvl) t.t_ty with Not_found -> t)
614
  | _ -> t_map_unsafe (t_abst m) (f_abst m) lvl t
615

616
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
617

618
619
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
620
621

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

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

625
let rec t_inst m lvl t = match t.t_node with
626
  | Tbvar n when n >= lvl ->
627
      (try t_var (Im.find (n - lvl) m) with Not_found -> assert false)
628
  | _ -> t_map_unsafe (t_inst m) (f_inst m) lvl t
629

630
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
631

632
633
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
634

Andrei Paskevich's avatar
Andrei Paskevich committed
635
636
(* looks for free de Bruijn indices *)

637
let rec t_closed lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
638
  | Tbvar x -> x < lvl
639
  | _ -> t_forall_unsafe t_closed f_closed lvl t
Andrei Paskevich's avatar
Andrei Paskevich committed
640

641
and f_closed lvl f = f_forall_unsafe t_closed f_closed lvl f
Andrei Paskevich's avatar
Andrei Paskevich committed
642

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

645
let rec t_occurs s lvl t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
646
  | Tvar u -> Svs.mem u s
647
  | _ -> t_exists_unsafe (t_occurs s) (f_occurs s) lvl t
648

649
and f_occurs s lvl f = f_exists_unsafe (t_occurs s) (f_occurs s) lvl f
650

651
652
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
653

654
655
let t_occurs s t = t_occurs s 0 t
let f_occurs s f = f_occurs s 0 f
656
657
658

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

659
let rec t_subst m lvl t = match t.t_node with
660
  | Tvar u -> (try Mvs.find u m with Not_found -> t)
661
  | _ -> t_map_unsafe (t_subst m) (f_subst m) lvl t
662

663
and f_subst m lvl f = f_map_unsafe (t_subst m) (f_subst m) lvl f
664

665
let t_subst_single v t1 t =
666
  if v.vs_ty == t1.t_ty then t_subst (Mvs.add v t1 Mvs.empty) 0 t
667
668
                        else raise Ty.TypeMismatch

669
let f_subst_single v t1 f =
670
  if v.vs_ty == t1.t_ty then f_subst (Mvs.add v t1 Mvs.empty) 0 f
671
672
673
674
                        else raise Ty.TypeMismatch

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

675
676
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
677
678
679

(* set of free variables *)

Andrei Paskevich's avatar
Andrei Paskevich committed
680
let rec t_vars lvl acc t = match t.t_node with
681
  | Tvar u -> Svs.add u acc
Andrei Paskevich's avatar
Andrei Paskevich committed
682
  | _ -> t_fold_unsafe t_vars f_vars lvl acc t
683

Andrei Paskevich's avatar
Andrei Paskevich committed
684
and f_vars lvl acc t = f_fold_unsafe t_vars f_vars lvl acc t
685

686
687
let t_freevars s t = t_vars 0 s t
let f_freevars s f = f_vars 0 s f
688

689
690
(* USE PHYSICAL EQUALITY *)
(*
691
692
693
694
(* equality *)

let t_equal = (==)
let f_equal = (==)
695
*)
696

697
(* equality modulo alpha *)
698

699
let rec t_equal_alpha t1 t2 =
700
701
702
703
704
705
706
707
  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) ->
708
        (* assert (List.length l1 == List.length l2); *)
709
        s1 == s2 && List.for_all2 t_equal_alpha l1 l2
710
711
    | Tlet (t1, (v1, b1)), Tlet (t2, (v2, b2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
712
        t_equal_alpha t1 t2 && t_equal_alpha b1 b2
713
    | Tcase (t1, l1), Tcase (t2, l2) ->
714
        t_equal_alpha t1 t2 &&
715
        (try List.for_all2 t_equal_branch_alpha l1 l2
716
717
718
        with Invalid_argument _ -> false)
    | Teps (v1, f1), Teps (v2, f2) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
719
        f_equal_alpha f1 f2
720
721
    | _ -> false

722
and f_equal_alpha f1 f2 =
723
724
  f1 == f2 ||
  match f1.f_node, f2.f_node with
725
726
    | Fapp (s1, l1), Fapp (s2, l2) ->
        (* assert (List.length l1 == List.length l2); *)
727
        s1 == s2 && List.for_all2 t_equal_alpha l1 l2
728
    | Fquant (q1, (v1, f1)), Fquant (q2, (v2, f2)) ->
729
        q1 == q2 && v1.vs_ty == v2.vs_ty && f_equal_alpha f1 f2
730
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) ->
731
        op1 == op2 && f_equal_alpha f1 f2 && f_equal_alpha g1 g2
732
    | Fnot f1, Fnot f2 ->
733
        f_equal_alpha f1 f2
734
735
736
737
    | Ftrue, Ftrue
    | Ffalse, Ffalse ->
        true
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
738
        f_equal_alpha f1 f2 && f_equal_alpha g1 g2 && f_equal_alpha h1 h2
739
740
    | Flet (t1, (v1, f1)), Flet (t2, (v2, f2)) ->
        (* assert (v1.vs_ty == t1.t_ty && v2.vs_ty == t2.t_ty); *)
741
        t_equal_alpha t1 t2 && f_equal_alpha f1 f2
742
    | Fcase (t1, l1), Fcase (t2, l2) ->
743
        t_equal_alpha t1 t2 &&
744
        (try List.for_all2 f_equal_branch_alpha l1 l2
745
        with Invalid_argument _ -> false)
746
    | _ -> false
747

748
and t_equal_branch_alpha (pat1, _, t1) (pat2, _, t2) =
749
  pat_equal_alpha pat1 pat2 && t_equal_alpha t1 t2
750

751
and f_equal_branch_alpha (pat1, _, f1) (pat2, _, f2) =
752
  pat_equal_alpha pat1 pat2 && f_equal_alpha f1 f2
753

754
755
756
757
(* matching modulo alpha in the pattern *)

exception NoMatch

Andrei Paskevich's avatar
Andrei Paskevich committed
758
let rec t_match s t1 t2 =
759
760
761
762
763
764
  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, _ ->
765
        (try if Mvs.find v1 s == t2 then s else raise NoMatch
766
        with Not_found -> if t_closed 0 t2
767
          then Mvs.add v1 t2 s else raise NoMatch)
768
769
    | Tapp (s1, l1), Tapp (s2, l2) when s1 == s2 ->
        (* assert (List.length l1 == List.length l2); *)
Andrei Paskevich's avatar
Andrei Paskevich committed
770
        List.fold_left2 t_match s l1 l2
771
772
    | 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
773
        t_match (t_match s t1 t2) b1 b2
774
    | Tcase (t1, l1), Tcase (t2, l2) ->
775
        (try List.fold_left2 t_match_branch (t_match s t1 t2) l1 l2
776
777
778
        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
779
        f_match s f1 f2
780
781
    | _ -> raise NoMatch

Andrei Paskevich's avatar
Andrei Paskevich committed
782
and f_match s f1 f2 =
783
784
785
786
  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
787
        List.fold_left2 t_match s l1 l2
788
789
    | Fquant (q1, (v1, f1)), Fquant (q2, (v2, f2))
            when q1 == q2 && v1.vs_ty == v2.vs_ty ->
Andrei Paskevich's avatar
Andrei Paskevich committed
790
        f_match s f1 f2
791
    | Fbinop (op1, f1, g1), Fbinop (op2, f2, g2) when op1 == op2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
792
        f_match (f_match s f1 f2) g1 g2
793
    | Fnot f1, Fnot f2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
794
        f_match s f1 f2
795
796
797
798
    | Ftrue, Ftrue
    | Ffalse, Ffalse ->
        s
    | Fif (f1, g1, h1), Fif (f2, g2, h2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
799
        f_match (f_match (f_match s f1 f2) g1 g2) h1 h2
800
801
    | 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
802
        f_match (t_match s t1 t2) f1 f2
803
    | Fcase (t1, l1), Fcase (t2, l2) ->
804
        (try List.fold_left2 f_match_branch (t_match s t1 t2) l1 l2
805
806
807
        with Invalid_argument _ -> raise NoMatch)
    | _ -> raise NoMatch

808
and t_match_branch s (pat1, _, t1) (pat2, _, t2) =
809
  if pat_equal_alpha pat1 pat2 then t_match s t1 t2 else raise NoMatch
810

811
and f_match_branch s (pat1, _, f1) (pat2, _, f2) =
812
  if pat_equal_alpha pat1 pat2 then f_match s f1 f2 else raise NoMatch
813

Andrei Paskevich's avatar
Andrei Paskevich committed
814
815
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
816

817
818
819
(* occurrence check *)

let rec t_occurs_term r lvl t = r == t ||
820
  t_exists_unsafe (t_occurs_term r) (f_occurs_term r) lvl t
821

822
823
and f_occurs_term r lvl f =
  f_exists_unsafe (t_occurs_term r) (f_occurs_term r) lvl f
824
825

let t_occurs_term r t = t_occurs_term r 0 t
826
let f_occurs_term r f = f_occurs_term r 0 f
827

828
829
let rec t_occurs_fmla r lvl t =
  t_exists_unsafe (t_occurs_fmla r) (f_occurs_fmla r) lvl t
830
831

and f_occurs_fmla r lvl f = r == f ||
832
  f_exists_unsafe (t_occurs_fmla r) (f_occurs_fmla r) lvl f
833