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