39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
|
72004
|
3 |
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
|
39348
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
signature AtomNet =
|
|
7 |
sig
|
|
8 |
|
|
9 |
(* ------------------------------------------------------------------------- *)
|
|
10 |
(* A type of atom sets that can be efficiently matched and unified. *)
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
|
|
13 |
type parameters = {fifo : bool}
|
|
14 |
|
|
15 |
type 'a atomNet
|
|
16 |
|
|
17 |
(* ------------------------------------------------------------------------- *)
|
|
18 |
(* Basic operations. *)
|
|
19 |
(* ------------------------------------------------------------------------- *)
|
|
20 |
|
|
21 |
val new : parameters -> 'a atomNet
|
|
22 |
|
|
23 |
val size : 'a atomNet -> int
|
|
24 |
|
|
25 |
val insert : 'a atomNet -> Atom.atom * 'a -> 'a atomNet
|
|
26 |
|
|
27 |
val fromList : parameters -> (Atom.atom * 'a) list -> 'a atomNet
|
|
28 |
|
|
29 |
val filter : ('a -> bool) -> 'a atomNet -> 'a atomNet
|
|
30 |
|
|
31 |
val toString : 'a atomNet -> string
|
|
32 |
|
|
33 |
val pp : 'a Print.pp -> 'a atomNet Print.pp
|
|
34 |
|
|
35 |
(* ------------------------------------------------------------------------- *)
|
|
36 |
(* Matching and unification queries. *)
|
|
37 |
(* *)
|
|
38 |
(* These function return OVER-APPROXIMATIONS! *)
|
|
39 |
(* Filter afterwards to get the precise set of satisfying values. *)
|
|
40 |
(* ------------------------------------------------------------------------- *)
|
|
41 |
|
|
42 |
val match : 'a atomNet -> Atom.atom -> 'a list
|
|
43 |
|
|
44 |
val matched : 'a atomNet -> Atom.atom -> 'a list
|
|
45 |
|
|
46 |
val unify : 'a atomNet -> Atom.atom -> 'a list
|
|
47 |
|
|
48 |
end
|