1 {-
2 From: dw@minster.york.ac.uk
3 To: partain
4 Subject: a compiler test
5 Date: 3 Mar 1992 12:31:00 GMT
7 Will,
8 One of the decisions taken at the FLARE meeting yesterday was that we
9 (FLARE people) should send you (GRASP people) interesting Haskell programs
10 to test your new compiler. So allow me to present the following program,
11 written by Colin Runciman in various functional languages over the years,
12 which puts propositions into clausal form. The original program was
13 interactive, but I've made it batch so that you can run it over night.
14 Here is an example run with the prototype compiler. Note the result is
15 "a <=".
17 hc clausify.hs
19 Glasgow University Haskell Compiler, version 0.41
20 G-Code version
21 -71\$ a.out
22 a <=
23 -71\$
25 Cheers,
27 David
28 -}
30 ------------------------------------------------------------------------------
31 -- reducing propositions to clausal form
32 -- Colin Runciman, University of York, 18/10/90
34 -- an excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
35 -- batch mode version David Wakeling, February 1992
37 module Main(main) where
39 import Data.Ix
40 import System.Environment
42 main = do
43 (n:_) <- getArgs
46 res n = concat (map clauses xs)
47 where xs = take n (repeat "(a = a = a) = (a = a = a) = (a = a = a)")
48 {-# NOINLINE xs #-}
50 data StackFrame = Ast Formula | Lex Char
52 data Formula =
53 Sym Char |
54 Not Formula |
55 Dis Formula Formula |
56 Con Formula Formula |
57 Imp Formula Formula |
58 Eqv Formula Formula
60 -- separate positive and negative literals, eliminating duplicates
61 clause p = clause' p ([] , [])
62 where
63 clause' (Dis p q) x = clause' p (clause' q x)
64 clause' (Sym s) (c,a) = (insert s c , a)
65 clause' (Not (Sym s)) (c,a) = (c , insert s a)
67 -- the main pipeline from propositional formulae to printed clauses
68 clauses = concat . map disp . unicl . split . disin . negin . elim . parse
70 conjunct (Con p q) = True
71 conjunct p = False
73 -- shift disjunction within conjunction
74 disin (Dis p (Con q r)) = Con (disin (Dis p q)) (disin (Dis p r))
75 disin (Dis (Con p q) r) = Con (disin (Dis p r)) (disin (Dis q r))
76 disin (Dis p q) =
77 if conjunct dp || conjunct dq then disin (Dis dp dq)
78 else (Dis dp dq)
79 where
80 dp = disin p
81 dq = disin q
82 disin (Con p q) = Con (disin p) (disin q)
83 disin p = p
85 -- format pair of lists of propositional symbols as clausal axiom
86 disp (l,r) = interleave l spaces ++ "<=" ++ interleave spaces r ++ "\n"
88 -- eliminate connectives other than not, disjunction and conjunction
89 elim (Sym s) = Sym s
90 elim (Not p) = Not (elim p)
91 elim (Dis p q) = Dis (elim p) (elim q)
92 elim (Con p q) = Con (elim p) (elim q)
93 elim (Imp p q) = Dis (Not (elim p)) (elim q)
94 elim (Eqv f f') = Con (elim (Imp f f')) (elim (Imp f' f))
96 -- the priorities of propositional expressions
97 {- UNUSED:
98 fpri (Sym c) = 6
99 fpri (Not p) = 5
100 fpri (Con p q) = 4
101 fpri (Dis p q) = 3
102 fpri (Imp p q) = 2
103 fpri (Eqv p q) = 1
104 -}
106 -- insertion of an item into an ordered list
107 -- Note: this is a corrected version from Colin (94/05/03 WDP)
108 insert x [] = [x]
109 insert x p@(y:ys) =
110 if x < y then x : p
111 else if x > y then y : insert x ys
112 else p
115 interleave (x:xs) ys = x : interleave ys xs
116 interleave [] _ = []
118 -- shift negation to innermost positions
119 negin (Not (Not p)) = negin p
120 negin (Not (Con p q)) = Dis (negin (Not p)) (negin (Not q))
121 negin (Not (Dis p q)) = Con (negin (Not p)) (negin (Not q))
122 negin (Dis p q) = Dis (negin p) (negin q)
123 negin (Con p q) = Con (negin p) (negin q)
124 negin p = p
126 -- the priorities of symbols during parsing
127 opri '(' = 0
128 opri '=' = 1
129 opri '>' = 2
130 opri '|' = 3
131 opri '&' = 4
132 opri '~' = 5
134 -- parsing a propositional formula
135 parse t = f where [Ast f] = parse' t []
137 parse' [] s = redstar s
138 parse' (' ':t) s = parse' t s
139 parse' ('(':t) s = parse' t (Lex '(' : s)
140 parse' (')':t) s = parse' t (x:s')
141 where
142 (x : Lex '(' : s') = redstar s
143 parse' (c:t) s = if inRange ('a','z') c then parse' t (Ast (Sym c) : s)
144 else if spri s > opri c then parse' (c:t) (red s)
145 else parse' t (Lex c : s)
147 -- reduction of the parse stack
148 red (Ast p : Lex '=' : Ast q : s) = Ast (Eqv q p) : s
149 red (Ast p : Lex '>' : Ast q : s) = Ast (Imp q p) : s
150 red (Ast p : Lex '|' : Ast q : s) = Ast (Dis q p) : s
151 red (Ast p : Lex '&' : Ast q : s) = Ast (Con q p) : s
152 red (Ast p : Lex '~' : s) = Ast (Not p) : s
154 -- iterative reduction of the parse stack
155 redstar = while ((/=) 0 . spri) red
157 -- old: partain:
158 --redstar = while ((/=) (0::Int) . spri) red
160 spaces = repeat ' '
162 -- split conjunctive proposition into a list of conjuncts
163 split p = split' p []
164 where
165 split' (Con p q) a = split' p (split' q a)
166 split' p a = p : a
168 -- priority of the parse stack
169 spri (Ast x : Lex c : s) = opri c
170 spri s = 0
172 -- does any symbol appear in both consequent and antecedant of clause
173 tautclause (c,a) = [x | x <- c, x `elem` a] /= []
175 -- form unique clausal axioms excluding tautologies
176 unicl a = foldr unicl' [] a
177 where
178 unicl' p x = if tautclause cp then x else insert cp x
179 where
180 cp = clause p
182 while p f x = if p x then while p f (f x) else x