1(* ========================================================================= *) 2(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure LiteralNet :> LiteralNet = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type of literal sets that can be efficiently matched and unified. *) 13(* ------------------------------------------------------------------------- *) 14 15type parameters = AtomNet.parameters; 16 17type 'a literalNet = 18 {positive : 'a AtomNet.atomNet, 19 negative : 'a AtomNet.atomNet}; 20 21(* ------------------------------------------------------------------------- *) 22(* Basic operations. *) 23(* ------------------------------------------------------------------------- *) 24 25fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm}; 26 27local 28 fun pos ({positive,...} : 'a literalNet) = AtomNet.size positive; 29 30 fun neg ({negative,...} : 'a literalNet) = AtomNet.size negative; 31in 32 fun size net = pos net + neg net; 33 34 fun profile net = {positive = pos net, negative = neg net}; 35end; 36 37fun insert {positive,negative} ((true,atm),a) = 38 {positive = AtomNet.insert positive (atm,a), negative = negative} 39 | insert {positive,negative} ((false,atm),a) = 40 {positive = positive, negative = AtomNet.insert negative (atm,a)}; 41 42fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l; 43 44fun filter pred {positive,negative} = 45 {positive = AtomNet.filter pred positive, 46 negative = AtomNet.filter pred negative}; 47 48fun toString net = "LiteralNet[" ^ Int.toString (size net) ^ "]"; 49 50fun pp ppA = 51 Print.ppMap 52 (fn {positive,negative} => (positive,negative)) 53 (Print.ppOp2 " + NEGATIVE" (AtomNet.pp ppA) (AtomNet.pp ppA)); 54 55(* ------------------------------------------------------------------------- *) 56(* Matching and unification queries. *) 57(* *) 58(* These function return OVER-APPROXIMATIONS! *) 59(* Filter afterwards to get the precise set of satisfying values. *) 60(* ------------------------------------------------------------------------- *) 61 62fun match ({positive,...} : 'a literalNet) (true,atm) = 63 AtomNet.match positive atm 64 | match {negative,...} (false,atm) = AtomNet.match negative atm; 65 66fun matched ({positive,...} : 'a literalNet) (true,atm) = 67 AtomNet.matched positive atm 68 | matched {negative,...} (false,atm) = AtomNet.matched negative atm; 69 70fun unify ({positive,...} : 'a literalNet) (true,atm) = 71 AtomNet.unify positive atm 72 | unify {negative,...} (false,atm) = AtomNet.unify negative atm; 73 74end 75