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