67c6a17867ec89e220d6246147177cbb1c050f2a
[ghc.git] / testsuite / tests / profiling / should_run / heapprof001.hs
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
6
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 <=".
16
17 hc clausify.hs
18 Haskell-0.41 (EXPERIMENTAL)
19 Glasgow University Haskell Compiler, version 0.41
20 G-Code version
21 -71$ a.out
22 a <=
23 -71$
24
25 Cheers,
26
27 David
28 -}
29
30 ------------------------------------------------------------------------------
31 -- reducing propositions to clausal form
32 -- Colin Runciman, University of York, 18/10/90
33
34 -- an excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
35 -- batch mode version David Wakeling, February 1992
36
37 module Main(main) where
38
39 import Data.Ix
40 import System.Environment
41
42 main = do
43 (n:_) <- getArgs
44 putStr (res (read n))
45
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 #-}
49
50 data StackFrame = Ast Formula | Lex Char
51
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
59
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)
66
67 -- the main pipeline from propositional formulae to printed clauses
68 clauses = concat . map disp . unicl . split . disin . negin . elim . parse
69
70 conjunct (Con p q) = True
71 conjunct p = False
72
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
84
85 -- format pair of lists of propositional symbols as clausal axiom
86 disp (l,r) = interleave l spaces ++ "<=" ++ interleave spaces r ++ "\n"
87
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))
95
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 -}
105
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
113
114
115 interleave (x:xs) ys = x : interleave ys xs
116 interleave [] _ = []
117
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
125
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
133
134 -- parsing a propositional formula
135 parse t = f where [Ast f] = parse' t []
136
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)
146
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
153
154 -- iterative reduction of the parse stack
155 redstar = while ((/=) 0 . spri) red
156
157 -- old: partain:
158 --redstar = while ((/=) (0::Int) . spri) red
159
160 spaces = repeat ' '
161
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
167
168 -- priority of the parse stack
169 spri (Ast x : Lex c : s) = opri c
170 spri s = 0
171
172 -- does any symbol appear in both consequent and antecedant of clause
173 tautclause (c,a) = [x | x <- c, x `elem` a] /= []
174
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
181
182 while p f x = if p x then while p f (f x) else x