content: {-
  From: dw@minster.york.ac.uk
  To: partain
  Subject:    a compiler test
  Date:        3 Mar 1992 12:31:00 GMT
  
  Will,
     One of the decisions taken at the FLARE meeting yesterday was that we 
  (FLARE people) should send you (GRASP people) interesting Haskell programs 
  to test your new compiler. So allow me to present the following program, 
  written by Colin Runciman in various functional languages over the years,
  which puts propositions into clausal form. The original program was 
  interactive, but I've made it batch so that you can run it over night.
  Here is an example run with the prototype compiler. Note the result is 
  "a <=".
  
  	hc clausify.hs
  	Haskell-0.41 (EXPERIMENTAL)
  	Glasgow University Haskell Compiler, version 0.41
  	G-Code version
  	-71$ a.out
  	a <= 
  	-71$
  
  Cheers,
  
  David
  -}
  
  ------------------------------------------------------------------------------
  -- reducing propositions to clausal form
  -- Colin Runciman, University of York, 18/10/90
  
  -- an excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
  -- batch mode version David Wakeling, February 1992
  
  module Main(main) where
  
  import Data.Ix
  import System.Environment
  
  main = do
    (n:_) <- getArgs
    putStr (res (read n))
  
  res n = concat (map clauses xs)
   where xs = take n (repeat "(a = a = a) = (a = a = a) = (a = a = a)")
         {-# NOINLINE xs #-}
  
  data StackFrame = Ast Formula | Lex Char 
  
  data Formula =
    Sym Char |
    Not Formula |
    Dis Formula Formula |
    Con Formula Formula |
    Imp Formula Formula |
    Eqv Formula Formula 
  
  -- separate positive and negative literals, eliminating duplicates
  clause p = clause' p ([] , [])
             where
             clause' (Dis p q)       x   = clause' p (clause' q x)
             clause' (Sym s)       (c,a) = (insert s c , a)
             clause' (Not (Sym s)) (c,a) = (c , insert s a)
  
  -- the main pipeline from propositional formulae to printed clauses
  clauses = concat . map disp . unicl . split . disin . negin . elim . parse
  
  conjunct (Con p q) = True
  conjunct p = False
  
  -- shift disjunction within conjunction
  disin (Dis p (Con q r)) = Con (disin (Dis p q)) (disin (Dis p r))
  disin (Dis (Con p q) r) = Con (disin (Dis p r)) (disin (Dis q r))
  disin (Dis p q) =
    if conjunct dp || conjunct dq then disin (Dis dp dq)
    else (Dis dp dq)
    where
    dp = disin p
    dq = disin q
  disin (Con p q) = Con (disin p) (disin q)
  disin p = p
  
  -- format pair of lists of propositional symbols as clausal axiom
  disp (l,r) = interleave l spaces ++ "<=" ++ interleave spaces r ++ "\n"
  
  -- eliminate connectives other than not, disjunction and conjunction
  elim (Sym s) = Sym s
  elim (Not p) = Not (elim p)
  elim (Dis p q) = Dis (elim p) (elim q)
  elim (Con p q) = Con (elim p) (elim q)
  elim (Imp p q) = Dis (Not (elim p)) (elim q)
  elim (Eqv f f') = Con (elim (Imp f f')) (elim (Imp f' f))
  
  -- the priorities of propositional expressions
  {- UNUSED:
  fpri   (Sym c) = 6
  fpri   (Not p) = 5
  fpri (Con p q) = 4
  fpri (Dis p q) = 3
  fpri (Imp p q) = 2
  fpri (Eqv p q) = 1
  -}
  
  -- insertion of an item into an ordered list
  -- Note: this is a corrected version from Colin (94/05/03 WDP)
  insert x [] = [x]
  insert x p@(y:ys) =
    if x < y then x : p
    else if x > y then y : insert x ys
    else p
  
  
  interleave (x:xs) ys = x : interleave ys xs
  interleave []     _  = []
  
  -- shift negation to innermost positions
  negin (Not (Not p)) = negin p
  negin (Not (Con p q)) = Dis (negin (Not p)) (negin (Not q))
  negin (Not (Dis p q)) = Con (negin (Not p)) (negin (Not q))
  negin (Dis p q) = Dis (negin p) (negin q)
  negin (Con p q) = Con (negin p) (negin q)
  negin p = p
  
  -- the priorities of symbols during parsing
  opri '(' = 0
  opri '=' = 1
  opri '>' = 2
  opri '|' = 3
  opri '&' = 4
  opri '~' = 5
  
  -- parsing a propositional formula
  parse t = f where [Ast f] = parse' t []
  
  parse' [] s = redstar s
  parse' (' ':t) s = parse' t s
  parse' ('(':t) s = parse' t (Lex '(' : s)
  parse' (')':t) s = parse' t (x:s')
                     where
                     (x : Lex '(' : s') = redstar s
  parse' (c:t) s = if inRange ('a','z') c then parse' t (Ast (Sym c) : s)
                   else if spri s > opri c then parse' (c:t) (red s)
                   else parse' t (Lex c : s)
  
  -- reduction of the parse stack
  red (Ast p : Lex '=' : Ast q : s) = Ast (Eqv q p) : s
  red (Ast p : Lex '>' : Ast q : s) = Ast (Imp q p) : s
  red (Ast p : Lex '|' : Ast q : s) = Ast (Dis q p) : s
  red (Ast p : Lex '&' : Ast q : s) = Ast (Con q p) : s
  red (Ast p : Lex '~' : s) = Ast (Not p) : s
  
  -- iterative reduction of the parse stack
  redstar = while ((/=) 0 . spri) red
  
  -- old: partain:
  --redstar = while ((/=) (0::Int) . spri) red
  
  spaces = repeat ' '
  
  -- split conjunctive proposition into a list of conjuncts
  split p = split' p []
            where
            split' (Con p q) a = split' p (split' q a)
            split' p a = p : a
  
  -- priority of the parse stack
  spri (Ast x : Lex c : s) = opri c
  spri s = 0
  
  -- does any symbol appear in both consequent and antecedant of clause
  tautclause (c,a) = [x | x <- c, x `elem` a] /= []
  
  -- form unique clausal axioms excluding tautologies
  unicl a = foldr unicl' [] a
            where
            unicl' p x = if tautclause cp then x else insert cp x
                         where
                         cp = clause p
  
  while p f x = if p x then while p f (f x) else x
  
  
  