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 with prelude stuff explicit
10 -- Patrick Sansom, University of Glasgow, 12/94
12 module PreludeClausify( clausify, AList(..) ) where
14 -- convert lines of propostions input to clausal forms
15 clausify input = scc "clausify"
17 (interleave (repeat "prop> ")
18 (map clausifyline (lines input)))
20 clausifyline = scc "CAF:clausifyline"
21 concat . map disp . clauses . parse
23 -- the main pipeline from propositional formulae to printed clauses
24 clauses = scc "CAF:clauses" unicl . split . disin . negin . elim
26 -- clauses = (scc "unicl" unicl) . (scc "split" split) .
27 -- (scc "disin" disin) . (scc "negin" negin) .
30 -- clauses = (\x -> scc "unicl" unicl x) .
31 -- (\x -> scc "split" split x) .
32 -- (\x -> scc "disin" disin x) .
33 -- (\x -> scc "negin" negin x) .
34 -- (\x -> scc "elim" elim x)
36 data StackFrame = Ast Formula | Lex Char
46 -- separate positive and negative literals, eliminating duplicates
47 clause p = scc "clause"
49 clause' (Dis p q) x = clause' p (clause' q x)
50 clause' (Sym s) (c,a) = (insert s c , a)
51 clause' (Not (Sym s)) (c,a) = (c , insert s a)
53 clause' p (ANil , ANil)
55 conjunct p = scc "conjunct"
60 -- shift disjunction within conjunction
63 (Con p q) -> Con (disin p) (disin q)
64 (Dis p q) -> disin' (disin p) (disin q)
67 -- auxilary definition encoding (disin . Dis)
68 disin' p r = scc "disin'"
70 (Con p q) -> Con (disin' p r) (disin' q r)
72 (Con q r) -> Con (disin' p q) (disin' p r)
75 -- format pair of lists of propositional symbols as clausal axiom
78 (l,r) -> interleave (foldrA ((:) `o` C#) [] l) spaces ++ "<="
79 ++ interleave spaces (foldrA ((:) `o` C#) [] r) ++ "\n"
81 -- eliminate connectives other than not, disjunction and conjunction
85 (Not p) -> Not (elim p)
86 (Dis p q) -> Dis (elim p) (elim q)
87 (Con p q) -> Con (elim p) (elim q)
88 (Imp p q) -> Dis (Not (elim p)) (elim q)
89 (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
91 -- remove duplicates and any elements satisfying p
92 filterset p s = scc "filterset"
95 filterset' res p l = scc "filterset'"
98 (x:xs) -> if (notElem x res) && (p x) then
99 x : filterset' (x:res) p xs
103 -- insertion of an item into an ordered list
104 insert x l = scc "insert"
107 (y:!ys) -> if x < y then x:!(y:!ys)
108 else if x > y then y :! insert x ys
111 interleave xs ys = scc "interleave"
113 (x:xs) -> x : interleave ys xs
116 -- shift negation to innermost positions
117 negin f = scc "negin"
119 (Not (Not p)) -> negin p
120 (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q))
121 (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q))
122 (Dis p q) -> Dis (negin p) (negin q)
123 (Con p q) -> Con (negin p) (negin q)
126 -- the priorities of symbols during parsing
136 -- parsing a propositional formula
137 parse t = scc "parse"
138 let [Ast f] = parse' t []
141 parse' cs s = scc "parse'"
144 (' ':t) -> parse' t s
145 ('(':t) -> parse' t (Lex '(' : s)
146 (')':t) -> let (x : Lex '(' : s') = redstar s
148 (c:t) -> if inRange ('a','z') c then
149 parse' t (Ast (Sym (case c of C# c# -> c#)) : s) -- ***
150 else if spri s > opri c then parse' (c:t) (red s)
151 else parse' t (Lex c : s)
153 -- reduction of the parse stack
156 (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s
157 (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s
158 (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s
159 (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s
160 (Ast p : Lex '~' : s) -> Ast (Not p) : s
162 -- iterative reduction of the parse stack
163 redstar = scc "CAF:redstar"
164 while ((/=) 0 . spri) red
166 spaces = scc "CAF:spaces"
169 -- split conjunctive proposition into a list of conjuncts
170 split p = scc "split"
172 split' (Con p q) a = split' p (split' q a)
177 -- priority of the parse stack
180 (Ast x : Lex c : s) -> opri c
183 -- does any symbol appear in both consequent and antecedant of clause
184 tautclause p = scc "tautclause"
186 (c,a) -> -- [x | x <- c, x `elem` a] /= []
187 anyA (\x -> x `elemA` a) c
189 -- form unique clausal axioms excluding tautologies
190 unicl = scc "CAF:unicl"
191 filterset (not . tautclause) . map clause
193 -- functional while loop
194 while p f x = scc "while"
195 if p x then while p f (f x) else x
197 {- STUFF FROM PRELUDE -}
199 data AList a = ANil | a :! (AList a)
203 elemA x (y:!ys) = x==y || elemA x ys
206 anyA p (x:!xs) = p x || anyA p xs
209 foldrA f z (x:!xs)= f x (foldrA f z xs)
214 instance Eq Char# where
218 instance Ord Char# where
219 (<=) x y = leChar# x y
220 (<) x y = ltChar# x y
221 (>=) x y = geChar# x y
222 (>) x y = gtChar# x y
224 max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a }
225 min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b }
228 = if (eqChar# a b) then _EQ
229 else if (ltChar# a b) then _LT else _GT