1(* ========================================================================= *)
2(* FIRST ORDER LOGIC FORMULAS                                                *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Formula :> Formula =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* A type of first order logic formulas.                                     *)
13(* ------------------------------------------------------------------------- *)
14
15datatype formula =
16    True
17  | False
18  | Atom of Atom.atom
19  | Not of formula
20  | And of formula * formula
21  | Or of formula * formula
22  | Imp of formula * formula
23  | Iff of formula * formula
24  | Forall of Term.var * formula
25  | Exists of Term.var * formula;
26
27(* ------------------------------------------------------------------------- *)
28(* Constructors and destructors.                                             *)
29(* ------------------------------------------------------------------------- *)
30
31(* Booleans *)
32
33fun mkBoolean true = True
34  | mkBoolean false = False;
35
36fun destBoolean True = true
37  | destBoolean False = false
38  | destBoolean _ = raise Error "destBoolean";
39
40val isBoolean = can destBoolean;
41
42fun isTrue fm =
43    case fm of
44      True => true
45    | _ => false;
46
47fun isFalse fm =
48    case fm of
49      False => true
50    | _ => false;
51
52(* Functions *)
53
54local
55  fun funcs fs [] = fs
56    | funcs fs (True :: fms) = funcs fs fms
57    | funcs fs (False :: fms) = funcs fs fms
58    | funcs fs (Atom atm :: fms) =
59      funcs (NameAritySet.union (Atom.functions atm) fs) fms
60    | funcs fs (Not p :: fms) = funcs fs (p :: fms)
61    | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
62    | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
63    | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
64    | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
65    | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
66    | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
67in
68  fun functions fm = funcs NameAritySet.empty [fm];
69end;
70
71local
72  fun funcs fs [] = fs
73    | funcs fs (True :: fms) = funcs fs fms
74    | funcs fs (False :: fms) = funcs fs fms
75    | funcs fs (Atom atm :: fms) =
76      funcs (NameSet.union (Atom.functionNames atm) fs) fms
77    | funcs fs (Not p :: fms) = funcs fs (p :: fms)
78    | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
79    | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
80    | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
81    | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
82    | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
83    | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
84in
85  fun functionNames fm = funcs NameSet.empty [fm];
86end;
87
88(* Relations *)
89
90local
91  fun rels fs [] = fs
92    | rels fs (True :: fms) = rels fs fms
93    | rels fs (False :: fms) = rels fs fms
94    | rels fs (Atom atm :: fms) =
95      rels (NameAritySet.add fs (Atom.relation atm)) fms
96    | rels fs (Not p :: fms) = rels fs (p :: fms)
97    | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
98    | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
99    | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
100    | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
101    | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
102    | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
103in
104  fun relations fm = rels NameAritySet.empty [fm];
105end;
106
107local
108  fun rels fs [] = fs
109    | rels fs (True :: fms) = rels fs fms
110    | rels fs (False :: fms) = rels fs fms
111    | rels fs (Atom atm :: fms) = rels (NameSet.add fs (Atom.name atm)) fms
112    | rels fs (Not p :: fms) = rels fs (p :: fms)
113    | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
114    | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
115    | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
116    | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
117    | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
118    | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
119in
120  fun relationNames fm = rels NameSet.empty [fm];
121end;
122
123(* Atoms *)
124
125fun destAtom (Atom atm) = atm
126  | destAtom _ = raise Error "Formula.destAtom";
127
128val isAtom = can destAtom;
129
130(* Negations *)
131
132fun destNeg (Not p) = p
133  | destNeg _ = raise Error "Formula.destNeg";
134
135val isNeg = can destNeg;
136
137val stripNeg =
138    let
139      fun strip n (Not fm) = strip (n + 1) fm
140        | strip n fm = (n,fm)
141    in
142      strip 0
143    end;
144
145(* Conjunctions *)
146
147fun listMkConj fms =
148    case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms;
149
150local
151  fun strip cs (And (p,q)) = strip (p :: cs) q
152    | strip cs fm = List.rev (fm :: cs);
153in
154  fun stripConj True = []
155    | stripConj fm = strip [] fm;
156end;
157
158val flattenConj =
159    let
160      fun flat acc [] = acc
161        | flat acc (And (p,q) :: fms) = flat acc (q :: p :: fms)
162        | flat acc (True :: fms) = flat acc fms
163        | flat acc (fm :: fms) = flat (fm :: acc) fms
164    in
165      fn fm => flat [] [fm]
166    end;
167
168(* Disjunctions *)
169
170fun listMkDisj fms =
171    case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
172
173local
174  fun strip cs (Or (p,q)) = strip (p :: cs) q
175    | strip cs fm = List.rev (fm :: cs);
176in
177  fun stripDisj False = []
178    | stripDisj fm = strip [] fm;
179end;
180
181val flattenDisj =
182    let
183      fun flat acc [] = acc
184        | flat acc (Or (p,q) :: fms) = flat acc (q :: p :: fms)
185        | flat acc (False :: fms) = flat acc fms
186        | flat acc (fm :: fms) = flat (fm :: acc) fms
187    in
188      fn fm => flat [] [fm]
189    end;
190
191(* Equivalences *)
192
193fun listMkEquiv fms =
194    case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
195
196local
197  fun strip cs (Iff (p,q)) = strip (p :: cs) q
198    | strip cs fm = List.rev (fm :: cs);
199in
200  fun stripEquiv True = []
201    | stripEquiv fm = strip [] fm;
202end;
203
204val flattenEquiv =
205    let
206      fun flat acc [] = acc
207        | flat acc (Iff (p,q) :: fms) = flat acc (q :: p :: fms)
208        | flat acc (True :: fms) = flat acc fms
209        | flat acc (fm :: fms) = flat (fm :: acc) fms
210    in
211      fn fm => flat [] [fm]
212    end;
213
214(* Universal quantifiers *)
215
216fun destForall (Forall v_f) = v_f
217  | destForall _ = raise Error "destForall";
218
219val isForall = can destForall;
220
221fun listMkForall ([],body) = body
222  | listMkForall (v :: vs, body) = Forall (v, listMkForall (vs,body));
223
224fun setMkForall (vs,body) = NameSet.foldr Forall body vs;
225
226local
227  fun strip vs (Forall (v,b)) = strip (v :: vs) b
228    | strip vs tm = (List.rev vs, tm);
229in
230  val stripForall = strip [];
231end;
232
233(* Existential quantifiers *)
234
235fun destExists (Exists v_f) = v_f
236  | destExists _ = raise Error "destExists";
237
238val isExists = can destExists;
239
240fun listMkExists ([],body) = body
241  | listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body));
242
243fun setMkExists (vs,body) = NameSet.foldr Exists body vs;
244
245local
246  fun strip vs (Exists (v,b)) = strip (v :: vs) b
247    | strip vs tm = (List.rev vs, tm);
248in
249  val stripExists = strip [];
250end;
251
252(* ------------------------------------------------------------------------- *)
253(* The size of a formula in symbols.                                         *)
254(* ------------------------------------------------------------------------- *)
255
256local
257  fun sz n [] = n
258    | sz n (True :: fms) = sz (n + 1) fms
259    | sz n (False :: fms) = sz (n + 1) fms
260    | sz n (Atom atm :: fms) = sz (n + Atom.symbols atm) fms
261    | sz n (Not p :: fms) = sz (n + 1) (p :: fms)
262    | sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
263    | sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
264    | sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
265    | sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
266    | sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms)
267    | sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms);
268in
269  fun symbols fm = sz 0 [fm];
270end;
271
272(* ------------------------------------------------------------------------- *)
273(* A total comparison function for formulas.                                 *)
274(* ------------------------------------------------------------------------- *)
275
276local
277  fun cmp [] = EQUAL
278    | cmp (f1_f2 :: fs) =
279      if Portable.pointerEqual f1_f2 then cmp fs
280      else
281        case f1_f2 of
282          (True,True) => cmp fs
283        | (True,_) => LESS
284        | (_,True) => GREATER
285        | (False,False) => cmp fs
286        | (False,_) => LESS
287        | (_,False) => GREATER
288        | (Atom atm1, Atom atm2) =>
289          (case Atom.compare (atm1,atm2) of
290             LESS => LESS
291           | EQUAL => cmp fs
292           | GREATER => GREATER)
293        | (Atom _, _) => LESS
294        | (_, Atom _) => GREATER
295        | (Not p1, Not p2) => cmp ((p1,p2) :: fs)
296        | (Not _, _) => LESS
297        | (_, Not _) => GREATER
298        | (And (p1,q1), And (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
299        | (And _, _) => LESS
300        | (_, And _) => GREATER
301        | (Or (p1,q1), Or (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
302        | (Or _, _) => LESS
303        | (_, Or _) => GREATER
304        | (Imp (p1,q1), Imp (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
305        | (Imp _, _) => LESS
306        | (_, Imp _) => GREATER
307        | (Iff (p1,q1), Iff (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
308        | (Iff _, _) => LESS
309        | (_, Iff _) => GREATER
310        | (Forall (v1,p1), Forall (v2,p2)) =>
311          (case Name.compare (v1,v2) of
312             LESS => LESS
313           | EQUAL => cmp ((p1,p2) :: fs)
314           | GREATER => GREATER)
315        | (Forall _, Exists _) => LESS
316        | (Exists _, Forall _) => GREATER
317        | (Exists (v1,p1), Exists (v2,p2)) =>
318          (case Name.compare (v1,v2) of
319             LESS => LESS
320           | EQUAL => cmp ((p1,p2) :: fs)
321           | GREATER => GREATER);
322in
323  fun compare fm1_fm2 = cmp [fm1_fm2];
324end;
325
326fun equal fm1 fm2 = compare (fm1,fm2) = EQUAL;
327
328(* ------------------------------------------------------------------------- *)
329(* Free variables.                                                           *)
330(* ------------------------------------------------------------------------- *)
331
332fun freeIn v =
333    let
334      fun f [] = false
335        | f (True :: fms) = f fms
336        | f (False :: fms) = f fms
337        | f (Atom atm :: fms) = Atom.freeIn v atm orelse f fms
338        | f (Not p :: fms) = f (p :: fms)
339        | f (And (p,q) :: fms) = f (p :: q :: fms)
340        | f (Or (p,q) :: fms) = f (p :: q :: fms)
341        | f (Imp (p,q) :: fms) = f (p :: q :: fms)
342        | f (Iff (p,q) :: fms) = f (p :: q :: fms)
343        | f (Forall (w,p) :: fms) =
344          if Name.equal v w then f fms else f (p :: fms)
345        | f (Exists (w,p) :: fms) =
346          if Name.equal v w then f fms else f (p :: fms)
347    in
348      fn fm => f [fm]
349    end;
350
351local
352  fun fv vs [] = vs
353    | fv vs ((_,True) :: fms) = fv vs fms
354    | fv vs ((_,False) :: fms) = fv vs fms
355    | fv vs ((bv, Atom atm) :: fms) =
356      fv (NameSet.union vs (NameSet.difference (Atom.freeVars atm) bv)) fms
357    | fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms)
358    | fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
359    | fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
360    | fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
361    | fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
362    | fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms)
363    | fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms);
364
365  fun add (fm,vs) = fv vs [(NameSet.empty,fm)];
366in
367  fun freeVars fm = add (fm,NameSet.empty);
368
369  fun freeVarsList fms = List.foldl add NameSet.empty fms;
370end;
371
372fun specialize fm = snd (stripForall fm);
373
374fun generalize fm = listMkForall (NameSet.toList (freeVars fm), fm);
375
376(* ------------------------------------------------------------------------- *)
377(* Substitutions.                                                            *)
378(* ------------------------------------------------------------------------- *)
379
380local
381  fun substCheck sub fm = if Subst.null sub then fm else substFm sub fm
382
383  and substFm sub fm =
384      case fm of
385        True => fm
386      | False => fm
387      | Atom (p,tms) =>
388        let
389          val tms' = Sharing.map (Subst.subst sub) tms
390        in
391          if Portable.pointerEqual (tms,tms') then fm else Atom (p,tms')
392        end
393      | Not p =>
394        let
395          val p' = substFm sub p
396        in
397          if Portable.pointerEqual (p,p') then fm else Not p'
398        end
399      | And (p,q) => substConn sub fm And p q
400      | Or (p,q) => substConn sub fm Or p q
401      | Imp (p,q) => substConn sub fm Imp p q
402      | Iff (p,q) => substConn sub fm Iff p q
403      | Forall (v,p) => substQuant sub fm Forall v p
404      | Exists (v,p) => substQuant sub fm Exists v p
405
406  and substConn sub fm conn p q =
407      let
408        val p' = substFm sub p
409        and q' = substFm sub q
410      in
411        if Portable.pointerEqual (p,p') andalso
412           Portable.pointerEqual (q,q')
413        then fm
414        else conn (p',q')
415      end
416
417  and substQuant sub fm quant v p =
418      let
419        val v' =
420            let
421              fun f (w,s) =
422                  if Name.equal w v then s
423                  else
424                    case Subst.peek sub w of
425                      NONE => NameSet.add s w
426                    | SOME tm => NameSet.union s (Term.freeVars tm)
427
428              val vars = freeVars p
429              val vars = NameSet.foldl f NameSet.empty vars
430            in
431              Term.variantPrime vars v
432            end
433
434        val sub =
435            if Name.equal v v' then Subst.remove sub (NameSet.singleton v)
436            else Subst.insert sub (v, Term.Var v')
437
438        val p' = substCheck sub p
439      in
440        if Name.equal v v' andalso Portable.pointerEqual (p,p') then fm
441        else quant (v',p')
442      end;
443in
444  val subst = substCheck;
445end;
446
447(* ------------------------------------------------------------------------- *)
448(* The equality relation.                                                    *)
449(* ------------------------------------------------------------------------- *)
450
451fun mkEq a_b = Atom (Atom.mkEq a_b);
452
453fun destEq fm = Atom.destEq (destAtom fm);
454
455val isEq = can destEq;
456
457fun mkNeq a_b = Not (mkEq a_b);
458
459fun destNeq (Not fm) = destEq fm
460  | destNeq _ = raise Error "Formula.destNeq";
461
462val isNeq = can destNeq;
463
464fun mkRefl tm = Atom (Atom.mkRefl tm);
465
466fun destRefl fm = Atom.destRefl (destAtom fm);
467
468val isRefl = can destRefl;
469
470fun sym fm = Atom (Atom.sym (destAtom fm));
471
472fun lhs fm = fst (destEq fm);
473
474fun rhs fm = snd (destEq fm);
475
476(* ------------------------------------------------------------------------- *)
477(* Parsing and pretty-printing.                                              *)
478(* ------------------------------------------------------------------------- *)
479
480type quotation = formula Parse.quotation;
481
482val truthName = Name.fromString "T"
483and falsityName = Name.fromString "F"
484and conjunctionName = Name.fromString "/\\"
485and disjunctionName = Name.fromString "\\/"
486and implicationName = Name.fromString "==>"
487and equivalenceName = Name.fromString "<=>"
488and universalName = Name.fromString "!"
489and existentialName = Name.fromString "?";
490
491local
492  fun demote True = Term.Fn (truthName,[])
493    | demote False = Term.Fn (falsityName,[])
494    | demote (Atom (p,tms)) = Term.Fn (p,tms)
495    | demote (Not p) =
496      let
497        val ref s = Term.negation
498      in
499        Term.Fn (Name.fromString s, [demote p])
500      end
501    | demote (And (p,q)) = Term.Fn (conjunctionName, [demote p, demote q])
502    | demote (Or (p,q)) = Term.Fn (disjunctionName, [demote p, demote q])
503    | demote (Imp (p,q)) = Term.Fn (implicationName, [demote p, demote q])
504    | demote (Iff (p,q)) = Term.Fn (equivalenceName, [demote p, demote q])
505    | demote (Forall (v,b)) = Term.Fn (universalName, [Term.Var v, demote b])
506    | demote (Exists (v,b)) =
507      Term.Fn (existentialName, [Term.Var v, demote b]);
508in
509  fun pp fm = Term.pp (demote fm);
510end;
511
512val toString = Print.toString pp;
513
514local
515  fun isQuant [Term.Var _, _] = true
516    | isQuant _ = false;
517
518  fun promote (Term.Var v) = Atom (v,[])
519    | promote (Term.Fn (f,tms)) =
520      if Name.equal f truthName andalso List.null tms then
521        True
522      else if Name.equal f falsityName andalso List.null tms then
523        False
524      else if Name.toString f = !Term.negation andalso length tms = 1 then
525        Not (promote (hd tms))
526      else if Name.equal f conjunctionName andalso length tms = 2 then
527        And (promote (hd tms), promote (List.nth (tms,1)))
528      else if Name.equal f disjunctionName andalso length tms = 2 then
529        Or (promote (hd tms), promote (List.nth (tms,1)))
530      else if Name.equal f implicationName andalso length tms = 2 then
531        Imp (promote (hd tms), promote (List.nth (tms,1)))
532      else if Name.equal f equivalenceName andalso length tms = 2 then
533        Iff (promote (hd tms), promote (List.nth (tms,1)))
534      else if Name.equal f universalName andalso isQuant tms then
535        Forall (Term.destVar (hd tms), promote (List.nth (tms,1)))
536      else if Name.equal f existentialName andalso isQuant tms then
537        Exists (Term.destVar (hd tms), promote (List.nth (tms,1)))
538      else
539        Atom (f,tms);
540in
541  fun fromString s = promote (Term.fromString s);
542end;
543
544val parse = Parse.parseQuotation toString fromString;
545
546(* ------------------------------------------------------------------------- *)
547(* Splitting goals.                                                          *)
548(* ------------------------------------------------------------------------- *)
549
550local
551  fun add_asms asms goal =
552      if List.null asms then goal else Imp (listMkConj (List.rev asms), goal);
553
554  fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
555
556  fun split asms pol fm =
557      case (pol,fm) of
558        (* Positive splittables *)
559        (true,True) => []
560      | (true, Not f) => split asms false f
561      | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
562      | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
563      | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
564      | (true, Iff (f1,f2)) =>
565        split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
566      | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
567        (* Negative splittables *)
568      | (false,False) => []
569      | (false, Not f) => split asms true f
570      | (false, And (f1,f2)) => split (f1 :: asms) false f2
571      | (false, Or (f1,f2)) =>
572        split asms false f1 @ split (Not f1 :: asms) false f2
573      | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
574      | (false, Iff (f1,f2)) =>
575        split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
576      | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
577        (* Unsplittables *)
578      | _ => [add_asms asms (if pol then fm else Not fm)];
579in
580  fun splitGoal fm = split [] true fm;
581end;
582
583(*MetisTrace3
584val splitGoal = fn fm =>
585    let
586      val result = splitGoal fm
587      val () = Print.trace pp "Formula.splitGoal: fm" fm
588      val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
589    in
590      result
591    end;
592*)
593
594end
595
596structure FormulaOrdered =
597struct type t = Formula.formula val compare = Formula.compare end
598
599structure FormulaMap = KeyMap (FormulaOrdered);
600
601structure FormulaSet = ElementSet (FormulaMap);
602