diff options
Diffstat (limited to 'testsuite/tests/profiling/should_run/heapprof001.hs')
-rw-r--r-- | testsuite/tests/profiling/should_run/heapprof001.hs | 182 |
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 |