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