blob: 6f55d854189e2448703d489c01ceddecc68f7e13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
val init_size : int
type term = Symb of Term.constr | Appli of term * term
module UF :
sig
type tag = Congr | Ax of Names.identifier
and cl =
Rep of int * int list
| Eqto of int * (int * int * tag)
and vertex = Leaf | Node of (int * int)
and t = int ref * (int, cl * vertex * term) Hashtbl.t
val empty : unit -> t
val add_lst : int -> int -> t -> unit
val find : t -> int -> int
val list : t -> int -> int list
val size : t -> int -> int
val signature : t -> int -> int * int
val nodes : t -> int list
val add :
term ->
int ref * (int, cl * vertex * term) Hashtbl.t ->
(term, int) Hashtbl.t -> int
val union :
t -> int -> int -> int * int * tag -> unit
end
module ST :
sig
type t =
(int * int, int) Hashtbl.t *
(int, int * int) Hashtbl.t
val empty :
unit -> ('a, 'b) Hashtbl.t * ('c, 'd) Hashtbl.t
val enter : int -> int * int -> t -> unit
val query : int * int -> t -> int
val delete : int -> t -> unit
val delete_list : int list -> t -> unit
end
val combine_rec :
UF.t -> ST.t -> int list -> (int * int) list
val process_rec :
UF.t -> ST.t -> (int * int) list -> int list
val cc_rec : UF.t -> ST.t -> int list -> unit
val cc : UF.t -> unit
val make_uf :
(term, int) Hashtbl.t ->
(Names.identifier * (term * term)) list -> UF.t
val decide_prb :
(Names.identifier * (term * term)) list * (term * term) ->
bool
|
