summaryrefslogtreecommitdiff
path: root/testsuite/tests/profiling/should_run/heapprof001.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/profiling/should_run/heapprof001.hs')
-rw-r--r--testsuite/tests/profiling/should_run/heapprof001.hs182
1 files changed, 182 insertions, 0 deletions
diff --git a/testsuite/tests/profiling/should_run/heapprof001.hs b/testsuite/tests/profiling/should_run/heapprof001.hs
new file mode 100644
index 0000000000..67c6a17867
--- /dev/null
+++ b/testsuite/tests/profiling/should_run/heapprof001.hs
@@ -0,0 +1,182 @@
+{-
+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