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