1 -- CLAUSIFY: Reducing Propositions to Clausal Form
2 -- Colin Runciman, University of York, 10/90
4 -- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
6 -- Optimised version: based on Runciman & Wakeling [1993]
7 -- Patrick Sansom, University of Glasgow, 2/94
9 -- Char# specialisation test
10 -- Patrick Sansom, University of Glasgow, 12/94
12 module Main ( main ) where
14 -- the main program: reads stdin and writes stdout
15 main = _scc_ "CAF:main"
18 putStr (clausify input)
20 -- convert lines of propostions input to clausal forms
21 clausify input = _scc_ "clausify"
23 (interleave (repeat "prop> ")
24 (map clausifyline (lines input)))
26 clausifyline = _scc_ "CAF:clausifyline"
27 concat . map disp . clauses . parse
29 -- the main pipeline from propositional formulae to printed clauses
30 clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim
32 -- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) .
33 -- (_scc_ "disin" disin) . (_scc_ "negin" negin) .
34 -- (_scc_ "elim" elim)
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)
42 data StackFrame = Ast Formula | Lex Char
52 -- separate positive and negative literals, eliminating duplicates
53 clause p = _scc_ "clause"
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)
61 conjunct p = _scc_ "conjunct"
66 -- shift disjunction within conjunction
67 disin p = _scc_ "disin"
69 (Con p q) -> Con (disin p) (disin q)
70 (Dis p q) -> disin' (disin p) (disin q)
73 -- auxilary definition encoding (disin . Dis)
74 disin' p r = _scc_ "disin'"
76 (Con p q) -> Con (disin' p r) (disin' q r)
78 (Con q r) -> Con (disin' p q) (disin' p r)
81 -- format pair of lists of propositional symbols as clausal axiom
84 (l,r) -> interleave (foldr ((:) . C#) [] l) spaces ++ "<=" -- ***
85 ++ interleave spaces (foldr ((:) . C#) [] r) ++ "\n" -- ***
87 -- eliminate connectives other than not, disjunction and conjunction
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))
97 -- remove duplicates and any elements satisfying p
98 filterset p s = _scc_ "filterset"
101 filterset' res p l = _scc_ "filterset'"
104 (x:xs) -> if (notElem x res) && (p x) then
105 x : filterset' (x:res) p xs
109 -- insertion of an item into an ordered list
110 insert x l = _scc_ "insert"
113 (y:ys) -> if x < y then x:(y:ys)
114 else if x > y then y : insert x ys
117 interleave xs ys = _scc_ "interleave"
119 (x:xs) -> x : interleave ys xs
122 -- shift negation to innermost positions
123 negin f = _scc_ "negin"
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)
132 -- the priorities of symbols during parsing
133 opri c = _scc_ "opri"
142 -- parsing a propositional formula
143 parse t = _scc_ "parse"
144 let [Ast f] = parse' t []
147 parse' cs s = _scc_ "parse'"
150 (' ':t) -> parse' t s
151 ('(':t) -> parse' t (Lex '(' : s)
152 (')':t) -> let (x : Lex '(' : s') = redstar 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)
159 -- reduction of the parse stack
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
168 -- iterative reduction of the parse stack
169 redstar = _scc_ "CAF:redstar"
170 while ((/=) 0 . spri) red
172 spaces = _scc_ "CAF:spaces"
175 -- split conjunctive proposition into a list of conjuncts
176 split p = _scc_ "split"
178 split' (Con p q) a = split' p (split' q a)
183 -- priority of the parse stack
184 spri s = _scc_ "spri"
186 (Ast x : Lex c : s) -> opri c
189 -- does any symbol appear in both consequent and antecedant of clause
190 tautclause p = _scc_ "tautclause"
192 (c,a) -> -- [x | x <- c, x `elem` a] /= []
193 any (\x -> x `elem` a) c
195 -- form unique clausal axioms excluding tautologies
196 unicl = _scc_ "CAF:unicl"
197 filterset (not . tautclause) . map clause
199 -- functional while loop
200 while p f x = _scc_ "while"
201 if p x then while p f (f x) else x