1(* ========================================================================= *) 2(* FIRST ORDER LOGIC LITERALS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Literal :> Literal = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type for storing first order logic literals. *) 13(* ------------------------------------------------------------------------- *) 14 15type polarity = bool; 16 17type literal = polarity * Atom.atom; 18 19(* ------------------------------------------------------------------------- *) 20(* Constructors and destructors. *) 21(* ------------------------------------------------------------------------- *) 22 23fun polarity ((pol,_) : literal) = pol; 24 25fun atom ((_,atm) : literal) = atm; 26 27fun name lit = Atom.name (atom lit); 28 29fun arguments lit = Atom.arguments (atom lit); 30 31fun arity lit = Atom.arity (atom lit); 32 33fun positive lit = polarity lit; 34 35fun negative lit = not (polarity lit); 36 37fun negate (pol,atm) : literal = (not pol, atm) 38 39fun relation lit = Atom.relation (atom lit); 40 41fun functions lit = Atom.functions (atom lit); 42 43fun functionNames lit = Atom.functionNames (atom lit); 44 45(* Binary relations *) 46 47fun mkBinop rel (pol,a,b) : literal = (pol, Atom.mkBinop rel (a,b)); 48 49fun destBinop rel ((pol,atm) : literal) = 50 case Atom.destBinop rel atm of (a,b) => (pol,a,b); 51 52fun isBinop rel = can (destBinop rel); 53 54(* Formulas *) 55 56fun toFormula (true,atm) = Formula.Atom atm 57 | toFormula (false,atm) = Formula.Not (Formula.Atom atm); 58 59fun fromFormula (Formula.Atom atm) = (true,atm) 60 | fromFormula (Formula.Not (Formula.Atom atm)) = (false,atm) 61 | fromFormula _ = raise Error "Literal.fromFormula"; 62 63(* ------------------------------------------------------------------------- *) 64(* The size of a literal in symbols. *) 65(* ------------------------------------------------------------------------- *) 66 67fun symbols ((_,atm) : literal) = Atom.symbols atm; 68 69(* ------------------------------------------------------------------------- *) 70(* A total comparison function for literals. *) 71(* ------------------------------------------------------------------------- *) 72 73val compare = prodCompare boolCompare Atom.compare; 74 75fun equal (p1,atm1) (p2,atm2) = p1 = p2 andalso Atom.equal atm1 atm2; 76 77(* ------------------------------------------------------------------------- *) 78(* Subterms. *) 79(* ------------------------------------------------------------------------- *) 80 81fun subterm lit path = Atom.subterm (atom lit) path; 82 83fun subterms lit = Atom.subterms (atom lit); 84 85fun replace (lit as (pol,atm)) path_tm = 86 let 87 val atm' = Atom.replace atm path_tm 88 in 89 if Portable.pointerEqual (atm,atm') then lit else (pol,atm') 90 end; 91 92(* ------------------------------------------------------------------------- *) 93(* Free variables. *) 94(* ------------------------------------------------------------------------- *) 95 96fun freeIn v lit = Atom.freeIn v (atom lit); 97 98fun freeVars lit = Atom.freeVars (atom lit); 99 100(* ------------------------------------------------------------------------- *) 101(* Substitutions. *) 102(* ------------------------------------------------------------------------- *) 103 104fun subst sub (lit as (pol,atm)) : literal = 105 let 106 val atm' = Atom.subst sub atm 107 in 108 if Portable.pointerEqual (atm',atm) then lit else (pol,atm') 109 end; 110 111(* ------------------------------------------------------------------------- *) 112(* Matching. *) 113(* ------------------------------------------------------------------------- *) 114 115fun match sub ((pol1,atm1) : literal) (pol2,atm2) = 116 let 117 val _ = pol1 = pol2 orelse raise Error "Literal.match" 118 in 119 Atom.match sub atm1 atm2 120 end; 121 122(* ------------------------------------------------------------------------- *) 123(* Unification. *) 124(* ------------------------------------------------------------------------- *) 125 126fun unify sub ((pol1,atm1) : literal) (pol2,atm2) = 127 let 128 val _ = pol1 = pol2 orelse raise Error "Literal.unify" 129 in 130 Atom.unify sub atm1 atm2 131 end; 132 133(* ------------------------------------------------------------------------- *) 134(* The equality relation. *) 135(* ------------------------------------------------------------------------- *) 136 137fun mkEq l_r : literal = (true, Atom.mkEq l_r); 138 139fun destEq ((true,atm) : literal) = Atom.destEq atm 140 | destEq (false,_) = raise Error "Literal.destEq"; 141 142val isEq = can destEq; 143 144fun mkNeq l_r : literal = (false, Atom.mkEq l_r); 145 146fun destNeq ((false,atm) : literal) = Atom.destEq atm 147 | destNeq (true,_) = raise Error "Literal.destNeq"; 148 149val isNeq = can destNeq; 150 151fun mkRefl tm = (true, Atom.mkRefl tm); 152 153fun destRefl (true,atm) = Atom.destRefl atm 154 | destRefl (false,_) = raise Error "Literal.destRefl"; 155 156val isRefl = can destRefl; 157 158fun mkIrrefl tm = (false, Atom.mkRefl tm); 159 160fun destIrrefl (true,_) = raise Error "Literal.destIrrefl" 161 | destIrrefl (false,atm) = Atom.destRefl atm; 162 163val isIrrefl = can destIrrefl; 164 165fun sym (pol,atm) : literal = (pol, Atom.sym atm); 166 167fun lhs ((_,atm) : literal) = Atom.lhs atm; 168 169fun rhs ((_,atm) : literal) = Atom.rhs atm; 170 171(* ------------------------------------------------------------------------- *) 172(* Special support for terms with type annotations. *) 173(* ------------------------------------------------------------------------- *) 174 175fun typedSymbols ((_,atm) : literal) = Atom.typedSymbols atm; 176 177fun nonVarTypedSubterms ((_,atm) : literal) = Atom.nonVarTypedSubterms atm; 178 179(* ------------------------------------------------------------------------- *) 180(* Parsing and pretty-printing. *) 181(* ------------------------------------------------------------------------- *) 182 183val pp = Print.ppMap toFormula Formula.pp; 184 185val toString = Print.toString pp; 186 187fun fromString s = fromFormula (Formula.fromString s); 188 189val parse = Parse.parseQuotation Term.toString fromString; 190 191end 192 193structure LiteralOrdered = 194struct type t = Literal.literal val compare = Literal.compare end 195 196structure LiteralMap = KeyMap (LiteralOrdered); 197 198structure LiteralSet = 199struct 200 201 local 202 structure S = ElementSet (LiteralMap); 203 in 204 open S; 205 end; 206 207 fun negateMember lit set = member (Literal.negate lit) set; 208 209 val negate = 210 let 211 fun f (lit,set) = add set (Literal.negate lit) 212 in 213 foldl f empty 214 end; 215 216 val relations = 217 let 218 fun f (lit,set) = NameAritySet.add set (Literal.relation lit) 219 in 220 foldl f NameAritySet.empty 221 end; 222 223 val functions = 224 let 225 fun f (lit,set) = NameAritySet.union set (Literal.functions lit) 226 in 227 foldl f NameAritySet.empty 228 end; 229 230 fun freeIn v = exists (Literal.freeIn v); 231 232 val freeVars = 233 let 234 fun f (lit,set) = NameSet.union set (Literal.freeVars lit) 235 in 236 foldl f NameSet.empty 237 end; 238 239 val freeVarsList = 240 let 241 fun f (lits,set) = NameSet.union set (freeVars lits) 242 in 243 List.foldl f NameSet.empty 244 end; 245 246 val symbols = 247 let 248 fun f (lit,z) = Literal.symbols lit + z 249 in 250 foldl f 0 251 end; 252 253 val typedSymbols = 254 let 255 fun f (lit,z) = Literal.typedSymbols lit + z 256 in 257 foldl f 0 258 end; 259 260 fun subst sub lits = 261 let 262 fun substLit (lit,(eq,lits')) = 263 let 264 val lit' = Literal.subst sub lit 265 val eq = eq andalso Portable.pointerEqual (lit,lit') 266 in 267 (eq, add lits' lit') 268 end 269 270 val (eq,lits') = foldl substLit (true,empty) lits 271 in 272 if eq then lits else lits' 273 end; 274 275 fun conjoin set = 276 Formula.listMkConj (List.map Literal.toFormula (toList set)); 277 278 fun disjoin set = 279 Formula.listMkDisj (List.map Literal.toFormula (toList set)); 280 281 val pp = 282 Print.ppMap 283 toList 284 (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)); 285 286end 287 288structure LiteralSetOrdered = 289struct type t = LiteralSet.set val compare = LiteralSet.compare end 290 291structure LiteralSetMap = KeyMap (LiteralSetOrdered); 292 293structure LiteralSetSet = ElementSet (LiteralSetMap); 294