ghc/tests/specialise/clausify002/PreludeClausify.hs

   1 -- CLAUSIFY: Reducing Propositions to Clausal Form
   2 -- Colin Runciman, University of York, 10/90
   3 --
   4 -- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
   5 --
   6 -- Optimised version: based on Runciman & Wakeling [1993]
   7 -- Patrick Sansom, University of Glasgow, 2/94
   8 --
   9 -- Char# specialisation test with prelude stuff explicit
  10 -- Patrick Sansom, University of Glasgow, 12/94
  11
  12 module PreludeClausify( clausify, AList(..) ) where
  13
  14 -- convert lines of propostions input to clausal forms
  15 clausify input = scc "clausify"
  16                  concat
  17                  (interleave (repeat "prop> ")
  18                              (map clausifyline (lines input)))
  19
  20 clausifyline = scc "CAF:clausifyline"
  21                concat . map disp . clauses . parse
  22
  23 -- the main pipeline from propositional formulae to printed clauses
  24 clauses = scc "CAF:clauses" unicl . split . disin . negin . elim
  25
  26 -- clauses = (scc "unicl" unicl) . (scc "split" split) .
  27 --           (scc "disin" disin) . (scc "negin" negin) .
  28 --           (scc "elim"  elim)
  29
  30 -- clauses = (\x -> scc "unicl" unicl x) .
  31 --           (\x -> scc "split" split x) .
  32 --           (\x -> scc "disin" disin x) .
  33 --           (\x -> scc "negin" negin x) .
  34 --           (\x -> scc "elim"  elim x)
  35
  36 data StackFrame = Ast Formula | Lex Char
  37
  38 data Formula =
  39   Sym (Pr Char# Char) |
  40   Not Formula         |
  41   Dis Formula Formula |
  42   Con Formula Formula |
  43   Imp Formula Formula |
  44   Eqv Formula Formula
  45
  46 -- separate positive and negative literals, eliminating duplicates
  47 clause p = scc "clause"
  48            let
  49            clause' (Dis p q)       x   = clause' p (clause' q x)
  50            clause' (Sym s)       (c,a) = (insert s c , a)
  51            clause' (Not (Sym s)) (c,a) = (c , insert s a)
  52            in
  53            clause' p (ANil , ANil)
  54
  55 conjunct p = scc "conjunct"
  56              case p of
  57              (Con p q) -> True
  58              p         -> False
  59
  60 -- shift disjunction within conjunction
  61 disin p = scc "disin"
  62           case p of
  63           (Con p q) -> Con (disin p) (disin q)
  64           (Dis p q) -> disin' (disin p) (disin q)
  65           p         -> p
  66
  67 -- auxilary definition encoding (disin . Dis)
  68 disin' p r = scc "disin'"
  69              case p of
  70              (Con p q) -> Con (disin' p r) (disin' q r)
  71              p         -> case r of
  72                           (Con q r) -> Con (disin' p q) (disin' p r)
  73                           q         -> Dis p q
  74
  75 -- format pair of lists of propositional symbols as clausal axiom
  76 disp p = scc "disp"
  77          case p of
  78          (l,r) -> interleave (foldrA ((:) `o` unChPr) [] l) spaces ++ "<="
  79                   ++ interleave spaces (foldrA ((:) `o` unChPr) [] r) ++ "\n"
  80
  81 -- eliminate connectives other than not, disjunction and conjunction
  82 elim f = scc "elim"
  83          case f of
  84          (Sym s)    -> Sym s
  85          (Not p)    -> Not (elim p)
  86          (Dis p q)  -> Dis (elim p) (elim q)
  87          (Con p q)  -> Con (elim p) (elim q)
  88          (Imp p q)  -> Dis (Not (elim p)) (elim q)
  89          (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
  90
  91 -- remove duplicates and any elements satisfying p
  92 filterset p s = scc "filterset"
  93                 filterset' [] p s
  94
  95 filterset' res p l = scc "filterset'"
  96                      case l of
  97                      []     -> []
  98                      (x:xs) -> if (notElem x res) && (p x) then
  99                                    x : filterset' (x:res) p xs
 100                                else
 101                                    filterset' res p xs
 102
 103 -- insertion of an item into an ordered list
 104 insert x l = scc "insert"
 105              case l of
 106              ANil    -> x :! ANil
 107              (y:!ys) -> if x < y then x:!(y:!ys)
 108                        else if x > y then y :! insert x ys
 109                        else y:!ys
 110
 111 interleave xs ys = scc "interleave"
 112                    case xs of
 113                    (x:xs) -> x : interleave ys xs
 114                    []     -> []
 115
 116 -- shift negation to innermost positions
 117 negin f = scc "negin"
 118           case f of
 119           (Not (Not p))   -> negin p
 120           (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q))
 121           (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q))
 122           (Dis p q)       -> Dis (negin p) (negin q)
 123           (Con p q)       -> Con (negin p) (negin q)
 124           p               -> p
 125
 126 -- the priorities of symbols during parsing
 127 opri c = scc "opri"
 128          case c of
 129          '(' -> 0
 130          '=' -> 1
 131          '>' -> 2
 132          '|' -> 3
 133          '&' -> 4
 134          '~' -> 5
 135
 136 -- parsing a propositional formula
 137 parse t = scc "parse"
 138           let [Ast f] = parse' t []
 139           in f
 140
 141 parse' cs s = scc "parse'"
 142               case cs of
 143               []      -> redstar s
 144               (' ':t) -> parse' t s
 145               ('(':t) -> parse' t (Lex '(' : s)
 146               (')':t) -> let (x : Lex '(' : s') = redstar s
 147                          in  parse' t (x:s')
 148               (c:t)   -> if inRange ('a','z') c then
 149                             parse' t (Ast (Sym (mkChPr c)) : s) -- ***
 150                          else if spri s > opri c then parse' (c:t) (red s)
 151                          else parse' t (Lex c : s)
 152
 153 -- reduction of the parse stack
 154 red l = scc "red"
 155         case l of
 156         (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s
 157         (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s
 158         (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s
 159         (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s
 160         (Ast p : Lex '~' : s)         -> Ast (Not p) : s
 161
 162 -- iterative reduction of the parse stack
 163 redstar = scc "CAF:redstar"
 164           while ((/=) 0 . spri) red
 165
 166 spaces = scc "CAF:spaces"
 167          repeat ' '
 168
 169 -- split conjunctive proposition into a list of conjuncts
 170 split p = scc "split"
 171           let
 172           split' (Con p q) a = split' p (split' q a)
 173           split' p a = p : a
 174           in
 175           split' p []
 176
 177 -- priority of the parse stack
 178 spri s = scc "spri"
 179          case s of
 180          (Ast x : Lex c : s) -> opri c
 181          s -> 0
 182
 183 -- does any symbol appear in both consequent and antecedant of clause
 184 tautclause p = scc "tautclause"
 185                case p of
 186                (c,a) -> -- [x | x <- c, x `elem` a] /= []
 187                         anyA (\x -> x `elemA` a) c
 188
 189 -- form unique clausal axioms excluding tautologies
 190 unicl = scc "CAF:unicl"
 191         filterset (not . tautclause) . map clause
 192
 193 -- functional while loop
 194 while p f x = scc "while"
 195               if p x then while p f (f x) else x
 196
 197 {- PAIR STUFF -}
 198
 199 data Pr a b = Pr a b
 200
 201 mkChPr c@(C# c#) = Pr c# c
 202 unChPr (Pr c# c) = C# c#
 203
 204 instance (Eq a, Eq b) => Eq (Pr a b) where
 205     (Pr a b) == (Pr c d) = a == c && b == d
 206
 207 instance (Ord a, Ord b) => Ord (Pr a b) where
 208     a <  b  = case _tagCmp a b of { _LT -> True;  _EQ -> False; _GT -> False }
 209     a <= b  = case _tagCmp a b of { _LT -> True;  _EQ -> True;  _GT -> False }
 210     a >= b  = case _tagCmp a b of { _LT -> False; _EQ -> True;  _GT -> True  }
 211     a >  b  = case _tagCmp a b of { _LT -> False; _EQ -> False; _GT -> True  }
 212
 213     max a b = case _tagCmp a b of { _LT -> b; _EQ -> a;  _GT -> a }
 214     min a b = case _tagCmp a b of { _LT -> a; _EQ -> a;  _GT -> b }
 215
 216     _tagCmp (Pr a1 b1) (Pr a2 b2)
 217       = case (_tagCmp a1 a2) of {
 218           _LT -> _LT;
 219           _GT -> _GT;
 220           _EQ -> _tagCmp b1 b2
 221         }
 222
 223 {- STUFF FROM PRELUDE -}
 224
 225 data AList a = ANil | a :! (AList a)
 226      deriving (Eq)
 227
 228 elemA x ANil    = False
 229 elemA x (y:!ys) = x==y || elemA x ys
 230
 231 anyA p ANil     = False
 232 anyA p (x:!xs)  = p x || anyA p xs
 233
 234 foldrA f z ANil   =  z
 235 foldrA f z (x:!xs)=  f x (foldrA f z xs)
 236
 237 o f g x = f (g x)
 238
 239
 240 instance Eq Char# where
 241     x == y = eqChar# x y
 242     x /= y = neChar# x y
 243
 244 instance Ord Char# where
 245     (<=) x y = leChar# x y
 246     (<)  x y = ltChar# x y
 247     (>=) x y = geChar# x y
 248     (>)  x y = gtChar# x y
 249
 250     max a b = case _tagCmp a b of { _LT -> b; _EQ -> a;  _GT -> a }
 251     min a b = case _tagCmp a b of { _LT -> a; _EQ -> a;  _GT -> b }
 252
 253     _tagCmp a b
 254       = if      (eqChar# a b) then _EQ
 255         else if (ltChar# a b) then _LT else _GT
 256