ghc/tests/specialise/clausify000/Main.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 module Main ( main ) where
  10
  11 -- the main program: reads stdin and writes stdout
  12 main = _scc_ "CAF:main"
  13     do
  14         input <- getContents
  15         putStr (clausify input)
  16
  17 -- convert lines of propostions input to clausal forms
  18 clausify input = _scc_ "clausify"
  19                  concat
  20                  (interleave (repeat "prop> ")
  21                              (map clausifyline (lines input)))
  22
  23 clausifyline = _scc_ "CAF:clausifyline"
  24                concat . map disp . clauses . parse
  25
  26 -- the main pipeline from propositional formulae to printed clauses
  27 clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim
  28
  29 -- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) .
  30 --           (_scc_ "disin" disin) . (_scc_ "negin" negin) .
  31 --           (_scc_ "elim"  elim)
  32
  33 -- clauses = (\x -> _scc_ "unicl" unicl x) .
  34 --           (\x -> _scc_ "split" split x) .
  35 --           (\x -> _scc_ "disin" disin x) .
  36 --           (\x -> _scc_ "negin" negin x) .
  37 --           (\x -> _scc_ "elim"  elim x)
  38
  39 data StackFrame = Ast Formula | Lex Char
  40
  41 data Formula =
  42   Sym Char |
  43   Not Formula |
  44   Dis Formula Formula |
  45   Con Formula Formula |
  46   Imp Formula Formula |
  47   Eqv Formula Formula
  48
  49 -- separate positive and negative literals, eliminating duplicates
  50 clause p = _scc_ "clause"
  51            let
  52            clause' (Dis p q)       x   = clause' p (clause' q x)
  53            clause' (Sym s)       (c,a) = (insert s c , a)
  54            clause' (Not (Sym s)) (c,a) = (c , insert s a)
  55            in
  56            clause' p ([] , [])
  57
  58 conjunct p = _scc_ "conjunct"
  59              case p of
  60              (Con p q) -> True
  61              p         -> False
  62
  63 -- shift disjunction within conjunction
  64 disin p = _scc_ "disin"
  65           case p of
  66           (Con p q) -> Con (disin p) (disin q)
  67           (Dis p q) -> disin' (disin p) (disin q)
  68           p         -> p
  69
  70 -- auxilary definition encoding (disin . Dis)
  71 disin' p r = _scc_ "disin'"
  72              case p of
  73              (Con p q) -> Con (disin' p r) (disin' q r)
  74              p         -> case r of
  75                           (Con q r) -> Con (disin' p q) (disin' p r)
  76                           q         -> Dis p q
  77
  78 -- format pair of lists of propositional symbols as clausal axiom
  79 disp p = _scc_ "disp"
  80          case p of
  81          (l,r) -> interleave l spaces ++ "<="
  82                   ++ interleave spaces r ++ "\n"
  83
  84 -- eliminate connectives other than not, disjunction and conjunction
  85 elim f = _scc_ "elim"
  86          case f of
  87          (Sym s)    -> Sym s
  88          (Not p)    -> Not (elim p)
  89          (Dis p q)  -> Dis (elim p) (elim q)
  90          (Con p q)  -> Con (elim p) (elim q)
  91          (Imp p q)  -> Dis (Not (elim p)) (elim q)
  92          (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
  93
  94 -- remove duplicates and any elements satisfying p
  95 filterset p s = _scc_ "filterset"
  96                 filterset' [] p s
  97
  98 filterset' res p l = _scc_ "filterset'"
  99                      case l of
 100                      []     -> []
 101                      (x:xs) -> if (notElem x res) && (p x) then
 102                                    x : filterset' (x:res) p xs
 103                                else
 104                                    filterset' res p xs
 105
 106 -- insertion of an item into an ordered list
 107 insert x l = _scc_ "insert"
 108              case l of
 109              []     -> [x]
 110              (y:ys) -> if x < y then x:(y:ys)
 111                        else if x > y then y : insert x ys
 112                        else y:ys
 113
 114 interleave xs ys = _scc_ "interleave"
 115                    case xs of
 116                    (x:xs) -> x : interleave ys xs
 117                    []     -> []
 118
 119 -- shift negation to innermost positions
 120 negin f = _scc_ "negin"
 121           case f of
 122           (Not (Not p))   -> negin p
 123           (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q))
 124           (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q))
 125           (Dis p q)       -> Dis (negin p) (negin q)
 126           (Con p q)       -> Con (negin p) (negin q)
 127           p               -> p
 128
 129 -- the priorities of symbols during parsing
 130 opri c = _scc_ "opri"
 131          case c of
 132          '(' -> 0
 133          '=' -> 1
 134          '>' -> 2
 135          '|' -> 3
 136          '&' -> 4
 137          '~' -> 5
 138
 139 -- parsing a propositional formula
 140 parse t = _scc_ "parse"
 141           let [Ast f] = parse' t []
 142           in f
 143
 144 parse' cs s = _scc_ "parse'"
 145               case cs of
 146               []      -> redstar s
 147               (' ':t) -> parse' t s
 148               ('(':t) -> parse' t (Lex '(' : s)
 149               (')':t) -> let (x : Lex '(' : s') = redstar s
 150                          in  parse' t (x:s')
 151               (c:t)   -> if inRange ('a','z') c then
 152                             parse' t (Ast (Sym c) : s)
 153                          else if spri s > opri c then parse' (c:t) (red s)
 154                          else parse' t (Lex c : s)
 155
 156 -- reduction of the parse stack
 157 red l = _scc_ "red"
 158         case l of
 159         (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s
 160         (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s
 161         (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s
 162         (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s
 163         (Ast p : Lex '~' : s)         -> Ast (Not p) : s
 164
 165 -- iterative reduction of the parse stack
 166 redstar = _scc_ "CAF:redstar"
 167           while ((/=) 0 . spri) red
 168
 169 spaces = _scc_ "CAF:spaces"
 170          repeat ' '
 171
 172 -- split conjunctive proposition into a list of conjuncts
 173 split p = _scc_ "split"
 174           let
 175           split' (Con p q) a = split' p (split' q a)
 176           split' p a = p : a
 177           in
 178           split' p []
 179
 180 -- priority of the parse stack
 181 spri s = _scc_ "spri"
 182          case s of
 183          (Ast x : Lex c : s) -> opri c
 184          s -> 0
 185
 186 -- does any symbol appear in both consequent and antecedant of clause
 187 tautclause p = _scc_ "tautclause"
 188                case p of
 189                (c,a) -> -- [x | x <- c, x `elem` a] /= []
 190                         any (\x -> x `elem` a) c
 191
 192 -- form unique clausal axioms excluding tautologies
 193 unicl = _scc_ "CAF:unicl"
 194         filterset (not . tautclause) . map clause
 195
 196 -- functional while loop
 197 while p f x = _scc_ "while"
 198               if p x then while p f (f x) else x