|
1 (* ========================================================================= *) |
|
2 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *) |
|
3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure AtomNet :> AtomNet = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Helper functions. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 fun atomToTerm atom = Term.Fn atom; |
|
16 |
|
17 fun termToAtom (Term.Var _) = raise Bug "AtomNet.termToAtom" |
|
18 | termToAtom (Term.Fn atom) = atom; |
|
19 |
|
20 (* ------------------------------------------------------------------------- *) |
|
21 (* A type of atom sets that can be efficiently matched and unified. *) |
|
22 (* ------------------------------------------------------------------------- *) |
|
23 |
|
24 type parameters = TermNet.parameters; |
|
25 |
|
26 type 'a atomNet = 'a TermNet.termNet; |
|
27 |
|
28 (* ------------------------------------------------------------------------- *) |
|
29 (* Basic operations. *) |
|
30 (* ------------------------------------------------------------------------- *) |
|
31 |
|
32 val new = TermNet.new; |
|
33 |
|
34 val size = TermNet.size; |
|
35 |
|
36 fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a); |
|
37 |
|
38 fun fromList parm l = foldl (fn (atm_a,n) => insert n atm_a) (new parm) l; |
|
39 |
|
40 val filter = TermNet.filter; |
|
41 |
|
42 fun toString net = "AtomNet[" ^ Int.toString (size net) ^ "]"; |
|
43 |
|
44 val pp = TermNet.pp; |
|
45 |
|
46 (* ------------------------------------------------------------------------- *) |
|
47 (* Matching and unification queries. *) |
|
48 (* *) |
|
49 (* These function return OVER-APPROXIMATIONS! *) |
|
50 (* Filter afterwards to get the precise set of satisfying values. *) |
|
51 (* ------------------------------------------------------------------------- *) |
|
52 |
|
53 fun match net atm = TermNet.match net (atomToTerm atm); |
|
54 |
|
55 fun matched net atm = TermNet.matched net (atomToTerm atm); |
|
56 |
|
57 fun unify net atm = TermNet.unify net (atomToTerm atm); |
|
58 |
|
59 end |