1(* ========================================================================= *)
2(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure AtomNet :> AtomNet =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* Helper functions.                                                         *)
13(* ------------------------------------------------------------------------- *)
14
15fun atomToTerm atom = Term.Fn atom;
16
17fun 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
24type parameters = TermNet.parameters;
25
26type 'a atomNet = 'a TermNet.termNet;
27
28(* ------------------------------------------------------------------------- *)
29(* Basic operations.                                                         *)
30(* ------------------------------------------------------------------------- *)
31
32val new = TermNet.new;
33
34val size = TermNet.size;
35
36fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a);
37
38fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
39
40val filter = TermNet.filter;
41
42fun toString net = "AtomNet[" ^ Int.toString (size net) ^ "]";
43
44val 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
53fun match net atm = TermNet.match net (atomToTerm atm);
54
55fun matched net atm = TermNet.matched net (atomToTerm atm);
56
57fun unify net atm = TermNet.unify net (atomToTerm atm);
58
59end
60