From 05a237528a439d98bea71437ff519d2b8959cf56 Mon Sep 17 00:00:00 2001 From: sof <unknown> Date: Sat, 26 Jul 1997 10:38:49 +0000 Subject: [PATCH] [project @ 1997-07-26 10:38:02 by sof] --- ghc/tests/specialise/COMMENTS | 43 +++ ghc/tests/specialise/Makefile | 5 + ghc/tests/specialise/clausify000/Jmakefile | 11 + ghc/tests/specialise/clausify000/Main.hs | 198 +++++++++++++ .../specialise/clausify000/clausify000.stdin | 1 + .../specialise/clausify000/clausify000.stdout | 2 + ghc/tests/specialise/clausify001/Jmakefile | 1 + ghc/tests/specialise/clausify001/Main.hs | 201 +++++++++++++ .../clausify001/Main.hs-WithPrelude | 8 + .../specialise/clausify001/PreludeClausify.hs | 230 +++++++++++++++ .../specialise/clausify001/clausify001.stdin | 1 + .../specialise/clausify001/clausify001.stdout | 2 + ghc/tests/specialise/clausify002/Jmakefile | 9 + ghc/tests/specialise/clausify002/Main.hs | 8 + .../specialise/clausify002/PreludeClausify.hs | 256 ++++++++++++++++ .../specialise/clausify002/clausify002.stdin | 1 + .../specialise/clausify002/clausify002.stdout | 2 + ghc/tests/specialise/clausify003/Jmakefile | 9 + ghc/tests/specialise/clausify003/Main.hs | 9 + .../specialise/clausify003/PreludeClausify.hs | 278 ++++++++++++++++++ .../specialise/clausify003/clausify003.stdin | 1 + .../specialise/clausify003/clausify003.stdout | 2 + ghc/tests/specialise/code001/Jmakefile | 8 + ghc/tests/specialise/code001/Spec.hs | 51 ++++ ghc/tests/specialise/code001/Use.hs | 33 +++ ghc/tests/specialise/code002/Jmakefile | 8 + ghc/tests/specialise/code002/Spec.hs | 55 ++++ ghc/tests/specialise/code002/Use.hs | 28 ++ ghc/tests/specialise/code003/Jmakefile | 8 + ghc/tests/specialise/code003/PreludeNum.hs | 50 ++++ ghc/tests/specialise/jmake.multi | 12 + ghc/tests/specialise/spec001/Jmakefile | 2 + ghc/tests/specialise/spec001/Main.hs | 40 +++ ghc/tests/specialise/spec001/spec001.stdin | 1 + ghc/tests/specialise/spec001/spec001.stdout | 1 + ghc/tests/specialise/spec002/Jmakefile | 1 + ghc/tests/specialise/spec002/Main.hs | 23 ++ ghc/tests/specialise/spec002/Other.hs | 12 + ghc/tests/specialise/spec002/spec002.stdin | 2 + ghc/tests/specialise/spec002/spec002.stdout | 4 + ghc/tests/specialise/spec003/Jmakefile | 10 + ghc/tests/specialise/spec003/Main.hs | 10 + ghc/tests/specialise/spec003/PreludeNum.hs | 58 ++++ ghc/tests/specialise/spec003/spec003.stdin | 0 ghc/tests/specialise/spec003/spec003.stdout | 0 45 files changed, 1695 insertions(+) create mode 100644 ghc/tests/specialise/COMMENTS create mode 100644 ghc/tests/specialise/Makefile create mode 100644 ghc/tests/specialise/clausify000/Jmakefile create mode 100644 ghc/tests/specialise/clausify000/Main.hs create mode 100644 ghc/tests/specialise/clausify000/clausify000.stdin create mode 100644 ghc/tests/specialise/clausify000/clausify000.stdout create mode 100644 ghc/tests/specialise/clausify001/Jmakefile create mode 100644 ghc/tests/specialise/clausify001/Main.hs create mode 100644 ghc/tests/specialise/clausify001/Main.hs-WithPrelude create mode 100644 ghc/tests/specialise/clausify001/PreludeClausify.hs create mode 100644 ghc/tests/specialise/clausify001/clausify001.stdin create mode 100644 ghc/tests/specialise/clausify001/clausify001.stdout create mode 100644 ghc/tests/specialise/clausify002/Jmakefile create mode 100644 ghc/tests/specialise/clausify002/Main.hs create mode 100644 ghc/tests/specialise/clausify002/PreludeClausify.hs create mode 100644 ghc/tests/specialise/clausify002/clausify002.stdin create mode 100644 ghc/tests/specialise/clausify002/clausify002.stdout create mode 100644 ghc/tests/specialise/clausify003/Jmakefile create mode 100644 ghc/tests/specialise/clausify003/Main.hs create mode 100644 ghc/tests/specialise/clausify003/PreludeClausify.hs create mode 100644 ghc/tests/specialise/clausify003/clausify003.stdin create mode 100644 ghc/tests/specialise/clausify003/clausify003.stdout create mode 100644 ghc/tests/specialise/code001/Jmakefile create mode 100644 ghc/tests/specialise/code001/Spec.hs create mode 100644 ghc/tests/specialise/code001/Use.hs create mode 100644 ghc/tests/specialise/code002/Jmakefile create mode 100644 ghc/tests/specialise/code002/Spec.hs create mode 100644 ghc/tests/specialise/code002/Use.hs create mode 100644 ghc/tests/specialise/code003/Jmakefile create mode 100644 ghc/tests/specialise/code003/PreludeNum.hs create mode 100644 ghc/tests/specialise/jmake.multi create mode 100644 ghc/tests/specialise/spec001/Jmakefile create mode 100644 ghc/tests/specialise/spec001/Main.hs create mode 100644 ghc/tests/specialise/spec001/spec001.stdin create mode 100644 ghc/tests/specialise/spec001/spec001.stdout create mode 100644 ghc/tests/specialise/spec002/Jmakefile create mode 100644 ghc/tests/specialise/spec002/Main.hs create mode 100644 ghc/tests/specialise/spec002/Other.hs create mode 100644 ghc/tests/specialise/spec002/spec002.stdin create mode 100644 ghc/tests/specialise/spec002/spec002.stdout create mode 100644 ghc/tests/specialise/spec003/Jmakefile create mode 100644 ghc/tests/specialise/spec003/Main.hs create mode 100644 ghc/tests/specialise/spec003/PreludeNum.hs create mode 100644 ghc/tests/specialise/spec003/spec003.stdin create mode 100644 ghc/tests/specialise/spec003/spec003.stdout diff --git a/ghc/tests/specialise/COMMENTS b/ghc/tests/specialise/COMMENTS new file mode 100644 index 000000000000..3ff133942c13 --- /dev/null +++ b/ghc/tests/specialise/COMMENTS @@ -0,0 +1,43 @@ +CHAR I/O: +********* + +In clausify ... + +The unifier would like to propogate use of Char#s all the way to the +readChan and appendChan. However these have explicit [Char] arguments +so we must explicitly coerce the Chars as we extract them. + clause produces [Char#]s + parse reads [Char] and builds Sym Char# + disp takes [Char#]s and produces [Char] + +COMMENTS: +* The extent of this unboxification is quite surprising and possibly + unexpected. +* Coersion when constructing or extracting from unboxed structures can + be a pain. Where this occurs defines the extent of the unboxedness. + +OVERLOADING CHARS: + +Might want to introduce versions of I/O operations which read/write +[Char#]. Use a type class to capture either boxed or unboxed Chars. + +class Char a + toChar :: a -> Char + fromChar :: Char -> a + +instance Char Char + toChar = id + fromChar = id + +instance Char Char# + toChar c# = MkChar c# + fromChar c = case c of MkChar c# -> c# + +Now rather than specifying type as + ... Char ... +We use + Char c => ... c ... + +Now just need a specialised versions I/O operations which deal with [Char#] + +The Char class is very similar to the overloading of numeric constants. diff --git a/ghc/tests/specialise/Makefile b/ghc/tests/specialise/Makefile new file mode 100644 index 000000000000..95f62e1ede82 --- /dev/null +++ b/ghc/tests/specialise/Makefile @@ -0,0 +1,5 @@ +TOP = ../../.. +include $(TOP)/mk/boilerplate.mk +SUBDIRS = $(wildcard spec* code* clausify*) +include $(TARGET_MK) + diff --git a/ghc/tests/specialise/clausify000/Jmakefile b/ghc/tests/specialise/clausify000/Jmakefile new file mode 100644 index 000000000000..3f70d4d9c686 --- /dev/null +++ b/ghc/tests/specialise/clausify000/Jmakefile @@ -0,0 +1,11 @@ +HC_OPTS=-v -O -fglasgow-exts \ + -keep-hc-files-too -dcore-lint -ftrace-specialisations -ddump-simpl -ddump-stg -odump clausify000.dump + +SRCS_HS=Main.hs +OBJS_O= Main.o + +NoFibMultiModuleCompileAndRun(clausify000,-i clausify000.stdin -o1 clausify000.stdout) + +NoFibHaskellCompile(clausify000,Main,hs) + +HaskellDependTarget( $(SRCS_HS) ) diff --git a/ghc/tests/specialise/clausify000/Main.hs b/ghc/tests/specialise/clausify000/Main.hs new file mode 100644 index 000000000000..18ca3b521a67 --- /dev/null +++ b/ghc/tests/specialise/clausify000/Main.hs @@ -0,0 +1,198 @@ +-- CLAUSIFY: Reducing Propositions to Clausal Form +-- Colin Runciman, University of York, 10/90 +-- +-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a) +-- +-- Optimised version: based on Runciman & Wakeling [1993] +-- Patrick Sansom, University of Glasgow, 2/94 + +module Main ( main ) where + +-- the main program: reads stdin and writes stdout +main = _scc_ "CAF:main" + do + input <- getContents + putStr (clausify input) + +-- convert lines of propostions input to clausal forms +clausify input = _scc_ "clausify" + concat + (interleave (repeat "prop> ") + (map clausifyline (lines input))) + +clausifyline = _scc_ "CAF:clausifyline" + concat . map disp . clauses . parse + +-- the main pipeline from propositional formulae to printed clauses +clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim + +-- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) . +-- (_scc_ "disin" disin) . (_scc_ "negin" negin) . +-- (_scc_ "elim" elim) + +-- clauses = (\x -> _scc_ "unicl" unicl x) . +-- (\x -> _scc_ "split" split x) . +-- (\x -> _scc_ "disin" disin x) . +-- (\x -> _scc_ "negin" negin x) . +-- (\x -> _scc_ "elim" elim x) + +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 = _scc_ "clause" + let + 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) + in + clause' p ([] , []) + +conjunct p = _scc_ "conjunct" + case p of + (Con p q) -> True + p -> False + +-- shift disjunction within conjunction +disin p = _scc_ "disin" + case p of + (Con p q) -> Con (disin p) (disin q) + (Dis p q) -> disin' (disin p) (disin q) + p -> p + +-- auxilary definition encoding (disin . Dis) +disin' p r = _scc_ "disin'" + case p of + (Con p q) -> Con (disin' p r) (disin' q r) + p -> case r of + (Con q r) -> Con (disin' p q) (disin' p r) + q -> Dis p q + +-- format pair of lists of propositional symbols as clausal axiom +disp p = _scc_ "disp" + case p of + (l,r) -> interleave l spaces ++ "<=" + ++ interleave spaces r ++ "\n" + +-- eliminate connectives other than not, disjunction and conjunction +elim f = _scc_ "elim" + case f of + (Sym s) -> Sym s + (Not p) -> Not (elim p) + (Dis p q) -> Dis (elim p) (elim q) + (Con p q) -> Con (elim p) (elim q) + (Imp p q) -> Dis (Not (elim p)) (elim q) + (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f)) + +-- remove duplicates and any elements satisfying p +filterset p s = _scc_ "filterset" + filterset' [] p s + +filterset' res p l = _scc_ "filterset'" + case l of + [] -> [] + (x:xs) -> if (notElem x res) && (p x) then + x : filterset' (x:res) p xs + else + filterset' res p xs + +-- insertion of an item into an ordered list +insert x l = _scc_ "insert" + case l of + [] -> [x] + (y:ys) -> if x < y then x:(y:ys) + else if x > y then y : insert x ys + else y:ys + +interleave xs ys = _scc_ "interleave" + case xs of + (x:xs) -> x : interleave ys xs + [] -> [] + +-- shift negation to innermost positions +negin f = _scc_ "negin" + case f of + (Not (Not p)) -> negin p + (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q)) + (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q)) + (Dis p q) -> Dis (negin p) (negin q) + (Con p q) -> Con (negin p) (negin q) + p -> p + +-- the priorities of symbols during parsing +opri c = _scc_ "opri" + case c of + '(' -> 0 + '=' -> 1 + '>' -> 2 + '|' -> 3 + '&' -> 4 + '~' -> 5 + +-- parsing a propositional formula +parse t = _scc_ "parse" + let [Ast f] = parse' t [] + in f + +parse' cs s = _scc_ "parse'" + case cs of + [] -> redstar s + (' ':t) -> parse' t s + ('(':t) -> parse' t (Lex '(' : s) + (')':t) -> let (x : Lex '(' : s') = redstar s + in parse' t (x:s') + (c:t) -> 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 l = _scc_ "red" + case l of + (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s + (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s + (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s + (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s + (Ast p : Lex '~' : s) -> Ast (Not p) : s + +-- iterative reduction of the parse stack +redstar = _scc_ "CAF:redstar" + while ((/=) 0 . spri) red + +spaces = _scc_ "CAF:spaces" + repeat ' ' + +-- split conjunctive proposition into a list of conjuncts +split p = _scc_ "split" + let + split' (Con p q) a = split' p (split' q a) + split' p a = p : a + in + split' p [] + +-- priority of the parse stack +spri s = _scc_ "spri" + case s of + (Ast x : Lex c : s) -> opri c + s -> 0 + +-- does any symbol appear in both consequent and antecedant of clause +tautclause p = _scc_ "tautclause" + case p of + (c,a) -> -- [x | x <- c, x `elem` a] /= [] + any (\x -> x `elem` a) c + +-- form unique clausal axioms excluding tautologies +unicl = _scc_ "CAF:unicl" + filterset (not . tautclause) . map clause + +-- functional while loop +while p f x = _scc_ "while" + if p x then while p f (f x) else x diff --git a/ghc/tests/specialise/clausify000/clausify000.stdin b/ghc/tests/specialise/clausify000/clausify000.stdin new file mode 100644 index 000000000000..c6cdc470075f --- /dev/null +++ b/ghc/tests/specialise/clausify000/clausify000.stdin @@ -0,0 +1 @@ +(a = a = a) = (a = a = a) = (a = a = a) diff --git a/ghc/tests/specialise/clausify000/clausify000.stdout b/ghc/tests/specialise/clausify000/clausify000.stdout new file mode 100644 index 000000000000..49fdbda12fda --- /dev/null +++ b/ghc/tests/specialise/clausify000/clausify000.stdout @@ -0,0 +1,2 @@ +prop> a <= +prop> \ No newline at end of file diff --git a/ghc/tests/specialise/clausify001/Jmakefile b/ghc/tests/specialise/clausify001/Jmakefile new file mode 100644 index 000000000000..56e6ab3e9e53 --- /dev/null +++ b/ghc/tests/specialise/clausify001/Jmakefile @@ -0,0 +1 @@ +NoFibOneModuleCompileAndRun(clausify001,-i clausify001.stdin -o1 clausify001.stdout) diff --git a/ghc/tests/specialise/clausify001/Main.hs b/ghc/tests/specialise/clausify001/Main.hs new file mode 100644 index 000000000000..4424df840df7 --- /dev/null +++ b/ghc/tests/specialise/clausify001/Main.hs @@ -0,0 +1,201 @@ +-- CLAUSIFY: Reducing Propositions to Clausal Form +-- Colin Runciman, University of York, 10/90 +-- +-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a) +-- +-- Optimised version: based on Runciman & Wakeling [1993] +-- Patrick Sansom, University of Glasgow, 2/94 +-- +-- Char# specialisation test +-- Patrick Sansom, University of Glasgow, 12/94 + +module Main ( main ) where + +-- the main program: reads stdin and writes stdout +main = _scc_ "CAF:main" + do + input <- getContents + putStr (clausify input) + +-- convert lines of propostions input to clausal forms +clausify input = _scc_ "clausify" + concat + (interleave (repeat "prop> ") + (map clausifyline (lines input))) + +clausifyline = _scc_ "CAF:clausifyline" + concat . map disp . clauses . parse + +-- the main pipeline from propositional formulae to printed clauses +clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim + +-- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) . +-- (_scc_ "disin" disin) . (_scc_ "negin" negin) . +-- (_scc_ "elim" elim) + +-- clauses = (\x -> _scc_ "unicl" unicl x) . +-- (\x -> _scc_ "split" split x) . +-- (\x -> _scc_ "disin" disin x) . +-- (\x -> _scc_ "negin" negin x) . +-- (\x -> _scc_ "elim" elim x) + +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 = _scc_ "clause" + let + 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) + in + clause' p ([] , []) + +conjunct p = _scc_ "conjunct" + case p of + (Con p q) -> True + p -> False + +-- shift disjunction within conjunction +disin p = _scc_ "disin" + case p of + (Con p q) -> Con (disin p) (disin q) + (Dis p q) -> disin' (disin p) (disin q) + p -> p + +-- auxilary definition encoding (disin . Dis) +disin' p r = _scc_ "disin'" + case p of + (Con p q) -> Con (disin' p r) (disin' q r) + p -> case r of + (Con q r) -> Con (disin' p q) (disin' p r) + q -> Dis p q + +-- format pair of lists of propositional symbols as clausal axiom +disp p = _scc_ "disp" + case p of + (l,r) -> interleave (foldr ((:) . C#) [] l) spaces ++ "<=" -- *** + ++ interleave spaces (foldr ((:) . C#) [] r) ++ "\n" -- *** + +-- eliminate connectives other than not, disjunction and conjunction +elim f = _scc_ "elim" + case f of + (Sym s) -> Sym s + (Not p) -> Not (elim p) + (Dis p q) -> Dis (elim p) (elim q) + (Con p q) -> Con (elim p) (elim q) + (Imp p q) -> Dis (Not (elim p)) (elim q) + (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f)) + +-- remove duplicates and any elements satisfying p +filterset p s = _scc_ "filterset" + filterset' [] p s + +filterset' res p l = _scc_ "filterset'" + case l of + [] -> [] + (x:xs) -> if (notElem x res) && (p x) then + x : filterset' (x:res) p xs + else + filterset' res p xs + +-- insertion of an item into an ordered list +insert x l = _scc_ "insert" + case l of + [] -> [x] + (y:ys) -> if x < y then x:(y:ys) + else if x > y then y : insert x ys + else y:ys + +interleave xs ys = _scc_ "interleave" + case xs of + (x:xs) -> x : interleave ys xs + [] -> [] + +-- shift negation to innermost positions +negin f = _scc_ "negin" + case f of + (Not (Not p)) -> negin p + (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q)) + (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q)) + (Dis p q) -> Dis (negin p) (negin q) + (Con p q) -> Con (negin p) (negin q) + p -> p + +-- the priorities of symbols during parsing +opri c = _scc_ "opri" + case c of + '(' -> 0 + '=' -> 1 + '>' -> 2 + '|' -> 3 + '&' -> 4 + '~' -> 5 + +-- parsing a propositional formula +parse t = _scc_ "parse" + let [Ast f] = parse' t [] + in f + +parse' cs s = _scc_ "parse'" + case cs of + [] -> redstar s + (' ':t) -> parse' t s + ('(':t) -> parse' t (Lex '(' : s) + (')':t) -> let (x : Lex '(' : s') = redstar s + in parse' t (x:s') + (c:t) -> if inRange ('a','z') c then + parse' t (Ast (Sym (case c of C# c# -> 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 l = _scc_ "red" + case l of + (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s + (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s + (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s + (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s + (Ast p : Lex '~' : s) -> Ast (Not p) : s + +-- iterative reduction of the parse stack +redstar = _scc_ "CAF:redstar" + while ((/=) 0 . spri) red + +spaces = _scc_ "CAF:spaces" + repeat ' ' + +-- split conjunctive proposition into a list of conjuncts +split p = _scc_ "split" + let + split' (Con p q) a = split' p (split' q a) + split' p a = p : a + in + split' p [] + +-- priority of the parse stack +spri s = _scc_ "spri" + case s of + (Ast x : Lex c : s) -> opri c + s -> 0 + +-- does any symbol appear in both consequent and antecedant of clause +tautclause p = _scc_ "tautclause" + case p of + (c,a) -> -- [x | x <- c, x `elem` a] /= [] + any (\x -> x `elem` a) c + +-- form unique clausal axioms excluding tautologies +unicl = _scc_ "CAF:unicl" + filterset (not . tautclause) . map clause + +-- functional while loop +while p f x = _scc_ "while" + if p x then while p f (f x) else x diff --git a/ghc/tests/specialise/clausify001/Main.hs-WithPrelude b/ghc/tests/specialise/clausify001/Main.hs-WithPrelude new file mode 100644 index 000000000000..86b4b24a5b45 --- /dev/null +++ b/ghc/tests/specialise/clausify001/Main.hs-WithPrelude @@ -0,0 +1,8 @@ +module Main ( main ) where + +import PreludeClausify (clausify) + +-- the main program: reads stdin and writes stdout +main = scc "CAF:main" + readChan stdin exit ( \input -> + appendChan stdout (clausify input) exit done) diff --git a/ghc/tests/specialise/clausify001/PreludeClausify.hs b/ghc/tests/specialise/clausify001/PreludeClausify.hs new file mode 100644 index 000000000000..bb9285ece319 --- /dev/null +++ b/ghc/tests/specialise/clausify001/PreludeClausify.hs @@ -0,0 +1,230 @@ +-- CLAUSIFY: Reducing Propositions to Clausal Form +-- Colin Runciman, University of York, 10/90 +-- +-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a) +-- +-- Optimised version: based on Runciman & Wakeling [1993] +-- Patrick Sansom, University of Glasgow, 2/94 +-- +-- Char# specialisation test with prelude stuff explicit +-- Patrick Sansom, University of Glasgow, 12/94 + +module PreludeClausify( clausify, AList(..) ) where + +-- convert lines of propostions input to clausal forms +clausify input = scc "clausify" + concat + (interleave (repeat "prop> ") + (map clausifyline (lines input))) + +clausifyline = scc "CAF:clausifyline" + concat . map disp . clauses . parse + +-- the main pipeline from propositional formulae to printed clauses +clauses = scc "CAF:clauses" unicl . split . disin . negin . elim + +-- clauses = (scc "unicl" unicl) . (scc "split" split) . +-- (scc "disin" disin) . (scc "negin" negin) . +-- (scc "elim" elim) + +-- clauses = (\x -> scc "unicl" unicl x) . +-- (\x -> scc "split" split x) . +-- (\x -> scc "disin" disin x) . +-- (\x -> scc "negin" negin x) . +-- (\x -> scc "elim" elim x) + +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 = scc "clause" + let + 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) + in + clause' p (ANil , ANil) + +conjunct p = scc "conjunct" + case p of + (Con p q) -> True + p -> False + +-- shift disjunction within conjunction +disin p = scc "disin" + case p of + (Con p q) -> Con (disin p) (disin q) + (Dis p q) -> disin' (disin p) (disin q) + p -> p + +-- auxilary definition encoding (disin . Dis) +disin' p r = scc "disin'" + case p of + (Con p q) -> Con (disin' p r) (disin' q r) + p -> case r of + (Con q r) -> Con (disin' p q) (disin' p r) + q -> Dis p q + +-- format pair of lists of propositional symbols as clausal axiom +disp p = scc "disp" + case p of + (l,r) -> interleave (foldrA ((:) `o` C#) [] l) spaces ++ "<=" + ++ interleave spaces (foldrA ((:) `o` C#) [] r) ++ "\n" + +-- eliminate connectives other than not, disjunction and conjunction +elim f = scc "elim" + case f of + (Sym s) -> Sym s + (Not p) -> Not (elim p) + (Dis p q) -> Dis (elim p) (elim q) + (Con p q) -> Con (elim p) (elim q) + (Imp p q) -> Dis (Not (elim p)) (elim q) + (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f)) + +-- remove duplicates and any elements satisfying p +filterset p s = scc "filterset" + filterset' [] p s + +filterset' res p l = scc "filterset'" + case l of + [] -> [] + (x:xs) -> if (notElem x res) && (p x) then + x : filterset' (x:res) p xs + else + filterset' res p xs + +-- insertion of an item into an ordered list +insert x l = scc "insert" + case l of + ANil -> x :! ANil + (y:!ys) -> if x < y then x:!(y:!ys) + else if x > y then y :! insert x ys + else y:!ys + +interleave xs ys = scc "interleave" + case xs of + (x:xs) -> x : interleave ys xs + [] -> [] + +-- shift negation to innermost positions +negin f = scc "negin" + case f of + (Not (Not p)) -> negin p + (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q)) + (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q)) + (Dis p q) -> Dis (negin p) (negin q) + (Con p q) -> Con (negin p) (negin q) + p -> p + +-- the priorities of symbols during parsing +opri c = scc "opri" + case c of + '(' -> 0 + '=' -> 1 + '>' -> 2 + '|' -> 3 + '&' -> 4 + '~' -> 5 + +-- parsing a propositional formula +parse t = scc "parse" + let [Ast f] = parse' t [] + in f + +parse' cs s = scc "parse'" + case cs of + [] -> redstar s + (' ':t) -> parse' t s + ('(':t) -> parse' t (Lex '(' : s) + (')':t) -> let (x : Lex '(' : s') = redstar s + in parse' t (x:s') + (c:t) -> if inRange ('a','z') c then + parse' t (Ast (Sym (case c of C# c# -> 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 l = scc "red" + case l of + (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s + (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s + (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s + (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s + (Ast p : Lex '~' : s) -> Ast (Not p) : s + +-- iterative reduction of the parse stack +redstar = scc "CAF:redstar" + while ((/=) 0 . spri) red + +spaces = scc "CAF:spaces" + repeat ' ' + +-- split conjunctive proposition into a list of conjuncts +split p = scc "split" + let + split' (Con p q) a = split' p (split' q a) + split' p a = p : a + in + split' p [] + +-- priority of the parse stack +spri s = scc "spri" + case s of + (Ast x : Lex c : s) -> opri c + s -> 0 + +-- does any symbol appear in both consequent and antecedant of clause +tautclause p = scc "tautclause" + case p of + (c,a) -> -- [x | x <- c, x `elem` a] /= [] + anyA (\x -> x `elemA` a) c + +-- form unique clausal axioms excluding tautologies +unicl = scc "CAF:unicl" + filterset (not . tautclause) . map clause + +-- functional while loop +while p f x = scc "while" + if p x then while p f (f x) else x + +{- STUFF FROM PRELUDE -} + +data AList a = ANil | a :! (AList a) + deriving (Eq) + +elemA x ANil = False +elemA x (y:!ys) = x==y || elemA x ys + +anyA p ANil = False +anyA p (x:!xs) = p x || anyA p xs + +foldrA f z ANil = z +foldrA f z (x:!xs)= f x (foldrA f z xs) + +o f g x = f (g x) + + +instance Eq Char# where + x == y = eqChar# x y + x /= y = neChar# x y + +instance Ord Char# where + (<=) x y = leChar# x y + (<) x y = ltChar# x y + (>=) x y = geChar# x y + (>) x y = gtChar# x y + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp a b + = if (eqChar# a b) then _EQ + else if (ltChar# a b) then _LT else _GT + diff --git a/ghc/tests/specialise/clausify001/clausify001.stdin b/ghc/tests/specialise/clausify001/clausify001.stdin new file mode 100644 index 000000000000..c6cdc470075f --- /dev/null +++ b/ghc/tests/specialise/clausify001/clausify001.stdin @@ -0,0 +1 @@ +(a = a = a) = (a = a = a) = (a = a = a) diff --git a/ghc/tests/specialise/clausify001/clausify001.stdout b/ghc/tests/specialise/clausify001/clausify001.stdout new file mode 100644 index 000000000000..49fdbda12fda --- /dev/null +++ b/ghc/tests/specialise/clausify001/clausify001.stdout @@ -0,0 +1,2 @@ +prop> a <= +prop> \ No newline at end of file diff --git a/ghc/tests/specialise/clausify002/Jmakefile b/ghc/tests/specialise/clausify002/Jmakefile new file mode 100644 index 000000000000..9684939db5f8 --- /dev/null +++ b/ghc/tests/specialise/clausify002/Jmakefile @@ -0,0 +1,9 @@ +SRCS_HS=Main.hs PreludeClausify.hs +OBJS_O= Main.o PreludeClausify.o + +NoFibMultiModuleCompileAndRun(clausify002,-i clausify002.stdin -o1 clausify002.stdout) + +NoFibHaskellCompile(clausify002,Main,hs) +NoFibHaskellCompile(clausify002,PreludeClausify,hs) + +NoFibDependTarget(clausify002, $(SRCS_HS)) diff --git a/ghc/tests/specialise/clausify002/Main.hs b/ghc/tests/specialise/clausify002/Main.hs new file mode 100644 index 000000000000..8894c5362cb0 --- /dev/null +++ b/ghc/tests/specialise/clausify002/Main.hs @@ -0,0 +1,8 @@ +module Main ( main ) where + +import PreludeClausify (clausify) + +-- the main program: reads stdin and writes stdout +main = scc "CAF:main" do + input <- getContents + putStr (clausify input) diff --git a/ghc/tests/specialise/clausify002/PreludeClausify.hs b/ghc/tests/specialise/clausify002/PreludeClausify.hs new file mode 100644 index 000000000000..57823440835d --- /dev/null +++ b/ghc/tests/specialise/clausify002/PreludeClausify.hs @@ -0,0 +1,256 @@ +-- CLAUSIFY: Reducing Propositions to Clausal Form +-- Colin Runciman, University of York, 10/90 +-- +-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a) +-- +-- Optimised version: based on Runciman & Wakeling [1993] +-- Patrick Sansom, University of Glasgow, 2/94 +-- +-- Char# specialisation test with prelude stuff explicit +-- Patrick Sansom, University of Glasgow, 12/94 + +module PreludeClausify( clausify, AList(..) ) where + +-- convert lines of propostions input to clausal forms +clausify input = scc "clausify" + concat + (interleave (repeat "prop> ") + (map clausifyline (lines input))) + +clausifyline = scc "CAF:clausifyline" + concat . map disp . clauses . parse + +-- the main pipeline from propositional formulae to printed clauses +clauses = scc "CAF:clauses" unicl . split . disin . negin . elim + +-- clauses = (scc "unicl" unicl) . (scc "split" split) . +-- (scc "disin" disin) . (scc "negin" negin) . +-- (scc "elim" elim) + +-- clauses = (\x -> scc "unicl" unicl x) . +-- (\x -> scc "split" split x) . +-- (\x -> scc "disin" disin x) . +-- (\x -> scc "negin" negin x) . +-- (\x -> scc "elim" elim x) + +data StackFrame = Ast Formula | Lex Char + +data Formula = + Sym (Pr Char# Char) | + Not Formula | + Dis Formula Formula | + Con Formula Formula | + Imp Formula Formula | + Eqv Formula Formula + +-- separate positive and negative literals, eliminating duplicates +clause p = scc "clause" + let + 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) + in + clause' p (ANil , ANil) + +conjunct p = scc "conjunct" + case p of + (Con p q) -> True + p -> False + +-- shift disjunction within conjunction +disin p = scc "disin" + case p of + (Con p q) -> Con (disin p) (disin q) + (Dis p q) -> disin' (disin p) (disin q) + p -> p + +-- auxilary definition encoding (disin . Dis) +disin' p r = scc "disin'" + case p of + (Con p q) -> Con (disin' p r) (disin' q r) + p -> case r of + (Con q r) -> Con (disin' p q) (disin' p r) + q -> Dis p q + +-- format pair of lists of propositional symbols as clausal axiom +disp p = scc "disp" + case p of + (l,r) -> interleave (foldrA ((:) `o` unChPr) [] l) spaces ++ "<=" + ++ interleave spaces (foldrA ((:) `o` unChPr) [] r) ++ "\n" + +-- eliminate connectives other than not, disjunction and conjunction +elim f = scc "elim" + case f of + (Sym s) -> Sym s + (Not p) -> Not (elim p) + (Dis p q) -> Dis (elim p) (elim q) + (Con p q) -> Con (elim p) (elim q) + (Imp p q) -> Dis (Not (elim p)) (elim q) + (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f)) + +-- remove duplicates and any elements satisfying p +filterset p s = scc "filterset" + filterset' [] p s + +filterset' res p l = scc "filterset'" + case l of + [] -> [] + (x:xs) -> if (notElem x res) && (p x) then + x : filterset' (x:res) p xs + else + filterset' res p xs + +-- insertion of an item into an ordered list +insert x l = scc "insert" + case l of + ANil -> x :! ANil + (y:!ys) -> if x < y then x:!(y:!ys) + else if x > y then y :! insert x ys + else y:!ys + +interleave xs ys = scc "interleave" + case xs of + (x:xs) -> x : interleave ys xs + [] -> [] + +-- shift negation to innermost positions +negin f = scc "negin" + case f of + (Not (Not p)) -> negin p + (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q)) + (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q)) + (Dis p q) -> Dis (negin p) (negin q) + (Con p q) -> Con (negin p) (negin q) + p -> p + +-- the priorities of symbols during parsing +opri c = scc "opri" + case c of + '(' -> 0 + '=' -> 1 + '>' -> 2 + '|' -> 3 + '&' -> 4 + '~' -> 5 + +-- parsing a propositional formula +parse t = scc "parse" + let [Ast f] = parse' t [] + in f + +parse' cs s = scc "parse'" + case cs of + [] -> redstar s + (' ':t) -> parse' t s + ('(':t) -> parse' t (Lex '(' : s) + (')':t) -> let (x : Lex '(' : s') = redstar s + in parse' t (x:s') + (c:t) -> if inRange ('a','z') c then + parse' t (Ast (Sym (mkChPr 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 l = scc "red" + case l of + (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s + (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s + (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s + (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s + (Ast p : Lex '~' : s) -> Ast (Not p) : s + +-- iterative reduction of the parse stack +redstar = scc "CAF:redstar" + while ((/=) 0 . spri) red + +spaces = scc "CAF:spaces" + repeat ' ' + +-- split conjunctive proposition into a list of conjuncts +split p = scc "split" + let + split' (Con p q) a = split' p (split' q a) + split' p a = p : a + in + split' p [] + +-- priority of the parse stack +spri s = scc "spri" + case s of + (Ast x : Lex c : s) -> opri c + s -> 0 + +-- does any symbol appear in both consequent and antecedant of clause +tautclause p = scc "tautclause" + case p of + (c,a) -> -- [x | x <- c, x `elem` a] /= [] + anyA (\x -> x `elemA` a) c + +-- form unique clausal axioms excluding tautologies +unicl = scc "CAF:unicl" + filterset (not . tautclause) . map clause + +-- functional while loop +while p f x = scc "while" + if p x then while p f (f x) else x + +{- PAIR STUFF -} + +data Pr a b = Pr a b + +mkChPr c@(C# c#) = Pr c# c +unChPr (Pr c# c) = C# c# + +instance (Eq a, Eq b) => Eq (Pr a b) where + (Pr a b) == (Pr c d) = a == c && b == d + +instance (Ord a, Ord b) => Ord (Pr a b) where + a < b = case _tagCmp a b of { _LT -> True; _EQ -> False; _GT -> False } + a <= b = case _tagCmp a b of { _LT -> True; _EQ -> True; _GT -> False } + a >= b = case _tagCmp a b of { _LT -> False; _EQ -> True; _GT -> True } + a > b = case _tagCmp a b of { _LT -> False; _EQ -> False; _GT -> True } + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp (Pr a1 b1) (Pr a2 b2) + = case (_tagCmp a1 a2) of { + _LT -> _LT; + _GT -> _GT; + _EQ -> _tagCmp b1 b2 + } + +{- STUFF FROM PRELUDE -} + +data AList a = ANil | a :! (AList a) + deriving (Eq) + +elemA x ANil = False +elemA x (y:!ys) = x==y || elemA x ys + +anyA p ANil = False +anyA p (x:!xs) = p x || anyA p xs + +foldrA f z ANil = z +foldrA f z (x:!xs)= f x (foldrA f z xs) + +o f g x = f (g x) + + +instance Eq Char# where + x == y = eqChar# x y + x /= y = neChar# x y + +instance Ord Char# where + (<=) x y = leChar# x y + (<) x y = ltChar# x y + (>=) x y = geChar# x y + (>) x y = gtChar# x y + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp a b + = if (eqChar# a b) then _EQ + else if (ltChar# a b) then _LT else _GT + diff --git a/ghc/tests/specialise/clausify002/clausify002.stdin b/ghc/tests/specialise/clausify002/clausify002.stdin new file mode 100644 index 000000000000..c6cdc470075f --- /dev/null +++ b/ghc/tests/specialise/clausify002/clausify002.stdin @@ -0,0 +1 @@ +(a = a = a) = (a = a = a) = (a = a = a) diff --git a/ghc/tests/specialise/clausify002/clausify002.stdout b/ghc/tests/specialise/clausify002/clausify002.stdout new file mode 100644 index 000000000000..49fdbda12fda --- /dev/null +++ b/ghc/tests/specialise/clausify002/clausify002.stdout @@ -0,0 +1,2 @@ +prop> a <= +prop> \ No newline at end of file diff --git a/ghc/tests/specialise/clausify003/Jmakefile b/ghc/tests/specialise/clausify003/Jmakefile new file mode 100644 index 000000000000..a6cacfce7415 --- /dev/null +++ b/ghc/tests/specialise/clausify003/Jmakefile @@ -0,0 +1,9 @@ +SRCS_HS=Main.hs PreludeClausify.hs +OBJS_O= Main.o PreludeClausify.o + +NoFibMultiModuleCompileAndRun(clausify003,-i clausify003.stdin -o1 clausify003.stdout) + +NoFibHaskellCompile(clausify003,Main,hs) +NoFibHaskellCompile(clausify003,PreludeClausify,hs) + +NoFibDependTarget(clausify003, $(SRCS_HS)) diff --git a/ghc/tests/specialise/clausify003/Main.hs b/ghc/tests/specialise/clausify003/Main.hs new file mode 100644 index 000000000000..b22d92c5afa0 --- /dev/null +++ b/ghc/tests/specialise/clausify003/Main.hs @@ -0,0 +1,9 @@ +module Main ( main ) where + +import PreludeClausify (clausify) + +-- the main program: reads stdin and writes stdout +main = scc "CAF:main" + do + input <- getContents + putStr (clausify input) diff --git a/ghc/tests/specialise/clausify003/PreludeClausify.hs b/ghc/tests/specialise/clausify003/PreludeClausify.hs new file mode 100644 index 000000000000..b04dcaabac5b --- /dev/null +++ b/ghc/tests/specialise/clausify003/PreludeClausify.hs @@ -0,0 +1,278 @@ +-- CLAUSIFY: Reducing Propositions to Clausal Form +-- Colin Runciman, University of York, 10/90 +-- +-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a) +-- +-- Optimised version: based on Runciman & Wakeling [1993] +-- Patrick Sansom, University of Glasgow, 2/94 +-- +-- Char# specialisation test with prelude stuff explicit +-- Patrick Sansom, University of Glasgow, 12/94 + +module PreludeClausify( clausify, AList(..) ) where + +-- convert lines of propostions input to clausal forms +clausify input = scc "clausify" + concat + (interleave (repeat "prop> ") + (map clausifyline (lines input))) + +clausifyline = scc "CAF:clausifyline" + concat . map disp . clauses . parse + +-- the main pipeline from propositional formulae to printed clauses +clauses = scc "CAF:clauses" unicl . split . disin . negin . elim + +-- clauses = (scc "unicl" unicl) . (scc "split" split) . +-- (scc "disin" disin) . (scc "negin" negin) . +-- (scc "elim" elim) + +-- clauses = (\x -> scc "unicl" unicl x) . +-- (\x -> scc "split" split x) . +-- (\x -> scc "disin" disin x) . +-- (\x -> scc "negin" negin x) . +-- (\x -> scc "elim" elim x) + +data StackFrame = Ast Formula | Lex Char + +data Formula = + Sym (Char#, Char) | + Not Formula | + Dis Formula Formula | + Con Formula Formula | + Imp Formula Formula | + Eqv Formula Formula + +-- separate positive and negative literals, eliminating duplicates +clause p = scc "clause" + let + 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) + in + clause' p (ANil , ANil) + +conjunct p = scc "conjunct" + case p of + (Con p q) -> True + p -> False + +-- shift disjunction within conjunction +disin p = scc "disin" + case p of + (Con p q) -> Con (disin p) (disin q) + (Dis p q) -> disin' (disin p) (disin q) + p -> p + +-- auxilary definition encoding (disin . Dis) +disin' p r = scc "disin'" + case p of + (Con p q) -> Con (disin' p r) (disin' q r) + p -> case r of + (Con q r) -> Con (disin' p q) (disin' p r) + q -> Dis p q + +-- format pair of lists of propositional symbols as clausal axiom +disp p = scc "disp" + case p of + (l,r) -> interleave (foldrA ((:) `o` unChPr) [] l) spaces ++ "<=" + ++ interleave spaces (foldrA ((:) `o` unChPr) [] r) ++ "\n" + +-- eliminate connectives other than not, disjunction and conjunction +elim f = scc "elim" + case f of + (Sym s) -> Sym s + (Not p) -> Not (elim p) + (Dis p q) -> Dis (elim p) (elim q) + (Con p q) -> Con (elim p) (elim q) + (Imp p q) -> Dis (Not (elim p)) (elim q) + (Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f)) + +-- remove duplicates and any elements satisfying p +filterset p s = scc "filterset" + filterset' [] p s + +filterset' res p l = scc "filterset'" + case l of + [] -> [] + (x:xs) -> if (notElem x res) && (p x) then + x : filterset' (x:res) p xs + else + filterset' res p xs + +-- insertion of an item into an ordered list +insert x l = scc "insert" + case l of + ANil -> x :! ANil + (y:!ys) -> if x < y then x:!(y:!ys) + else if x > y then y :! insert x ys + else y:!ys + +interleave xs ys = scc "interleave" + case xs of + (x:xs) -> x : interleave ys xs + [] -> [] + +-- shift negation to innermost positions +negin f = scc "negin" + case f of + (Not (Not p)) -> negin p + (Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q)) + (Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q)) + (Dis p q) -> Dis (negin p) (negin q) + (Con p q) -> Con (negin p) (negin q) + p -> p + +-- the priorities of symbols during parsing +opri c = scc "opri" + case c of + '(' -> 0 + '=' -> 1 + '>' -> 2 + '|' -> 3 + '&' -> 4 + '~' -> 5 + +-- parsing a propositional formula +parse t = scc "parse" + let [Ast f] = parse' t [] + in f + +parse' cs s = scc "parse'" + case cs of + [] -> redstar s + (' ':t) -> parse' t s + ('(':t) -> parse' t (Lex '(' : s) + (')':t) -> let (x : Lex '(' : s') = redstar s + in parse' t (x:s') + (c:t) -> if inRange ('a','z') c then + parse' t (Ast (Sym (mkChPr 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 l = scc "red" + case l of + (Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s + (Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s + (Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s + (Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s + (Ast p : Lex '~' : s) -> Ast (Not p) : s + +-- iterative reduction of the parse stack +redstar = scc "CAF:redstar" + while ((/=) 0 . spri) red + +spaces = scc "CAF:spaces" + repeat ' ' + +-- split conjunctive proposition into a list of conjuncts +split p = scc "split" + let + split' (Con p q) a = split' p (split' q a) + split' p a = p : a + in + split' p [] + +-- priority of the parse stack +spri s = scc "spri" + case s of + (Ast x : Lex c : s) -> opri c + s -> 0 + +-- does any symbol appear in both consequent and antecedant of clause +tautclause p = scc "tautclause" + case p of + (c,a) -> -- [x | x <- c, x `elem` a] /= [] + anyA (\x -> x `elemA` a) c + +-- form unique clausal axioms excluding tautologies +unicl = scc "CAF:unicl" + filterset (not . tautclause) . map clause + +-- functional while loop +while p f x = scc "while" + if p x then while p f (f x) else x + +{- PAIR STUFF -} + +-- data Pr a b = (a, b) + +mkChPr c@(C# c#) = (c#,c) +unChPr (c#,c) = C# c# + +instance (Eq a, Eq b) => Eq (a,b) where + (a,b) == (c,d) = a == c && b == d + +instance (Ord a, Ord b) => Ord (a,b) where + a < b = case _tagCmp a b of { _LT -> True; _EQ -> False; _GT -> False } + a <= b = case _tagCmp a b of { _LT -> True; _EQ -> True; _GT -> False } + a >= b = case _tagCmp a b of { _LT -> False; _EQ -> True; _GT -> True } + a > b = case _tagCmp a b of { _LT -> False; _EQ -> False; _GT -> True } + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp (a1,b1) (a2,b2) + = case (_tagCmp a1 a2) of { + _LT -> _LT; + _GT -> _GT; + _EQ -> _tagCmp b1 b2 + } + +{- +instance Eq (Char#, Char) where + (a,b) == (c,d) = a == c && b == d + (a,b) /= (c,d) = a /= c || b /= d + +instance Ord (Char#, Char) where + a < b = case _tagCmp a b of { _LT -> True; _EQ -> False; _GT -> False } + a <= b = case _tagCmp a b of { _LT -> True; _EQ -> True; _GT -> False } + a >= b = case _tagCmp a b of { _LT -> False; _EQ -> True; _GT -> True } + a > b = case _tagCmp a b of { _LT -> False; _EQ -> False; _GT -> True } + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp (a1,b1) (a2,b2) + = case (_tagCmp a1 a2) of { + _LT -> _LT; + _GT -> _GT; + _EQ -> _tagCmp b1 b2 + } +-} + +{- STUFF FROM PRELUDE -} + +data AList a = ANil | a :! (AList a) + deriving (Eq) + +elemA x ANil = False +elemA x (y:!ys) = x==y || elemA x ys + +anyA p ANil = False +anyA p (x:!xs) = p x || anyA p xs + +foldrA f z ANil = z +foldrA f z (x:!xs)= f x (foldrA f z xs) + +o f g x = f (g x) + + +instance Eq Char# where + x == y = eqChar# x y + x /= y = neChar# x y + +instance Ord Char# where + (<=) x y = leChar# x y + (<) x y = ltChar# x y + (>=) x y = geChar# x y + (>) x y = gtChar# x y + + max a b = case _tagCmp a b of { _LT -> b; _EQ -> a; _GT -> a } + min a b = case _tagCmp a b of { _LT -> a; _EQ -> a; _GT -> b } + + _tagCmp a b + = if (eqChar# a b) then _EQ + else if (ltChar# a b) then _LT else _GT + diff --git a/ghc/tests/specialise/clausify003/clausify003.stdin b/ghc/tests/specialise/clausify003/clausify003.stdin new file mode 100644 index 000000000000..c6cdc470075f --- /dev/null +++ b/ghc/tests/specialise/clausify003/clausify003.stdin @@ -0,0 +1 @@ +(a = a = a) = (a = a = a) = (a = a = a) diff --git a/ghc/tests/specialise/clausify003/clausify003.stdout b/ghc/tests/specialise/clausify003/clausify003.stdout new file mode 100644 index 000000000000..49fdbda12fda --- /dev/null +++ b/ghc/tests/specialise/clausify003/clausify003.stdout @@ -0,0 +1,2 @@ +prop> a <= +prop> \ No newline at end of file diff --git a/ghc/tests/specialise/code001/Jmakefile b/ghc/tests/specialise/code001/Jmakefile new file mode 100644 index 000000000000..eea8aeddb846 --- /dev/null +++ b/ghc/tests/specialise/code001/Jmakefile @@ -0,0 +1,8 @@ +SRCS_HS=Spec.hs Use.hs +OBJS_O= Spec.o Use.o + +all : $(OBJS_O) + +NoFibHaskellCompile(code001,Spec,hs) +NoFibHaskellCompile(code001,Use,hs) + diff --git a/ghc/tests/specialise/code001/Spec.hs b/ghc/tests/specialise/code001/Spec.hs new file mode 100644 index 000000000000..7b1b4ba1a6ac --- /dev/null +++ b/ghc/tests/specialise/code001/Spec.hs @@ -0,0 +1,51 @@ +module Spec ( + + Tree(..), + + tree1, tree2, tree3, + + lookup + + ) where + +data Tree k a = Leaf k a + | Branch k (Tree k a) (Tree k a) + +lookup eq lt k def (Leaf k1 v1) + = if eq k k1 then v1 else def +lookup eq lt k def (Branch k1 t1 t2) + = if lt k k1 then lookup eq lt k def t1 + else lookup eq lt k def t2 + +-- Versions of Tree: +-- SPEC Tree Int# Float# +-- SPEC Tree Char# a +-- use Tree Int# Int#, +-- use Tree a Int#, +-- use Tree Char# a (already requested) +-- use Tree Char# Char# (via lookup SPEC) + +-- Versions of lookup: +-- SPEC lookup Char# Char# Char# +-- SPEC lookup Char# Char# a +-- use lookup Int# Int# Int# + +{-# SPECIALISE data Tree Int# Float# #-} +{-# SPECIALISE data Tree Char# a #-} + +{-# SPECIALISE lookup :: (Char#->Char#->Bool) -> (Char#->Char#->Bool) + -> Char# -> Char# -> Tree Char# Char# -> Char# #-} +{-# SPECIALISE lookup :: (Char#->Char#->Bool) -> (Char#->Char#->Bool) + -> Char# -> a -> Tree Char# a -> a #-} + +tree1 = case (lookup eqInt# ltInt# 1# 1# (Leaf 1# 1#)) of i# -> I# i# +tree2 k = Leaf k 1# +tree3 a = case 'k' of C# k# -> Leaf k# a + +{- These should cause errors -} + +{- *** # SPECIALISE data Tree Char# a #-} -- duplicate +{- *** # SPECIALISE data Tree Char# Int #-} -- boxed type +{- *** # SPECIALISE data Tree a b #-} -- no spec + + diff --git a/ghc/tests/specialise/code001/Use.hs b/ghc/tests/specialise/code001/Use.hs new file mode 100644 index 000000000000..191ba32a5200 --- /dev/null +++ b/ghc/tests/specialise/code001/Use.hs @@ -0,0 +1,33 @@ +module Use ( + + UseTree, + + lookup1, lookup2, lookup3, tree1 + + ) where + +import Spec ( Tree(..), lookup) + +data UseTree a = UseTree (Tree Char# a) + + -- specialised version of UseTree Int# will be created + -- however, since the a is not a direct component this is + -- identical to the original version! + -- ToDo: avoid creating such versions? + + -- this data declaration does not in itself require specialisations of Tree + -- these will only be required by code which constructs the values placed + -- inside a use of this data declaration + +{- These should be ok -} + +lookup1 = case (lookup eqInt# ltInt# 1# 1# (Leaf 1# 1#)) of i# -> I# i# + +{- These should cause specialisation errors, unless added to Spec.hs -} + +tree1 = UseTree (Leaf (case 'k' of C# k# -> k#) 1#) + +lookup2 = case (lookup eqInt# ltInt# 1# 1.0# (Leaf 1# 1.0#)) of f# -> F# f# + +lookup3 = case (lookup (==) (<) 1 1.0# (Leaf 1 1.0#)) of f# -> F# f# + diff --git a/ghc/tests/specialise/code002/Jmakefile b/ghc/tests/specialise/code002/Jmakefile new file mode 100644 index 000000000000..89e24d1f7c8c --- /dev/null +++ b/ghc/tests/specialise/code002/Jmakefile @@ -0,0 +1,8 @@ +SRCS_HS=Spec.hs Use.hs +OBJS_O= Spec.o Use.o + +all : $(OBJS_O) + +NoFibHaskellCompile(code002,Spec,hs) +NoFibHaskellCompile(code002,Use,hs) + diff --git a/ghc/tests/specialise/code002/Spec.hs b/ghc/tests/specialise/code002/Spec.hs new file mode 100644 index 000000000000..9553133f4b71 --- /dev/null +++ b/ghc/tests/specialise/code002/Spec.hs @@ -0,0 +1,55 @@ +module Spec ( + + Tree(..), + + tree1, tree2, tree3, + + lookup + + ) where + +data Tree k a = Leaf k a + | Branch k (Tree k a) (Tree k a) + +lookup eq lt k def (Leaf k1 v1) + = if eq k k1 then v1 else def +lookup eq lt k def (Branch k1 t1 t2) + = if lt k k1 then lookup eq lt k def t1 + else lookup eq lt k def t2 + +-- Versions of Tree: +-- SPEC Tree Int# Float# +-- SPEC Tree Char# a +-- use Tree Int# Int#, +-- use Tree a Int#, +-- use Tree Char# a (already requested) +-- use Tree Char# Char# (via lookup SPEC) + +-- Versions of lookup: +-- SPEC lookup Char# Char# Char# +-- SPEC lookup Char# Char# a +-- use lookup Int# Int# Int# + +{-# SPECIALISE data Tree Int# Float# #-} +{-# SPECIALISE data Tree Char# a #-} + +{-# SPECIALISE lookup :: (Char#->Char#->Bool) -> (Char#->Char#->Bool) + -> Char# -> Char# -> Tree Char# Char# -> Char# #-} +{-# SPECIALISE lookup :: (Char#->Char#->Bool) -> (Char#->Char#->Bool) + -> Char# -> a -> Tree Char# a -> a #-} + +tree1 = case (lookup eqInt# ltInt# 1# 1# (Leaf 1# 1#)) of i# -> I# i# +tree2 k = Leaf k 1# +tree3 a = case 'k' of C# k# -> Leaf k# a + +{- These should cause errors -} + +{- *** # SPECIALISE data Tree Char# a #-} -- duplicate +{- *** # SPECIALISE data Tree Char# Int #-} -- boxed type +{- *** # SPECIALISE data Tree a b #-} -- no spec + +{- Essential Specialisations -} +{-# SPECIALISE data Tree a Float# #-} +{-# SPECIALISE data Tree Char# Int# #-} +{-# SPECIALISE lookup :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> Float# -> Tree b Float# -> Float# #-} +{-# SPECIALISE lookup :: (Int# -> Int# -> Bool) -> (Int# -> Int# -> Bool) -> Int# -> Float# -> Tree Int# Float# -> Float# #-} diff --git a/ghc/tests/specialise/code002/Use.hs b/ghc/tests/specialise/code002/Use.hs new file mode 100644 index 000000000000..fe89f0f13a24 --- /dev/null +++ b/ghc/tests/specialise/code002/Use.hs @@ -0,0 +1,28 @@ +module Use ( + + UseTree, + + lookup1, lookup2, lookup3, tree1, + + Tree, lookup + + ) where + +import Spec ( Tree(..), lookup) + +data UseTree a = UseTree (Tree Char# a) + + -- this data declaration does not in itself require specialisations of Tree + -- these will only be required by code which constructs the values placed + -- inside a use of this data declaration + +{- These should be ok -} + +lookup1 = case (lookup eqInt# ltInt# 1# 1# (Leaf 1# 1#)) of i# -> I# i# + +tree1 = UseTree (Leaf (case 'k' of C# k# -> k#) 1#) + +lookup2 = case (lookup eqInt# ltInt# 1# 1.0# (Leaf 1# 1.0#)) of f# -> F# f# + +lookup3 = case (lookup (==) (<) 1 1.0# (Leaf 1 1.0#)) of f# -> F# f# + diff --git a/ghc/tests/specialise/code003/Jmakefile b/ghc/tests/specialise/code003/Jmakefile new file mode 100644 index 000000000000..33b3aa0fc567 --- /dev/null +++ b/ghc/tests/specialise/code003/Jmakefile @@ -0,0 +1,8 @@ +SRCS_HS=PreludeNum.hs +OBJS_O= PreludeNum.o + +all : $(OBJS_O) + +NoFibHaskellCompile(code003,PreludeNum,hs) + + diff --git a/ghc/tests/specialise/code003/PreludeNum.hs b/ghc/tests/specialise/code003/PreludeNum.hs new file mode 100644 index 000000000000..f6037123b09e --- /dev/null +++ b/ghc/tests/specialise/code003/PreludeNum.hs @@ -0,0 +1,50 @@ +module PreludeNum ( + + double, compute1, compute2 + + ) where + +{- Preliminaries ... -} + +{- patError# { Int# } (built into compiler) -} +local_map f [] = [] +local_map f (x:xs) = (f x) : local_map f xs + + +{- Here we go ... -} + +instance Eq Int# where + x == y = eqInt# x y + x /= y = neInt# x y + +instance Read Int# where + readsPrec p s = map (\ (I# i#, s) -> (i#, s)) (readsPrec p s) + readList s = map (\ (x, s) -> (local_map (\ (I# i#) -> i#) x, s)) (readList s) + +instance Show Int# where + showsPrec p x = showsPrec p (I# x) + showList l = showList (local_map I# l) + +instance Num Int# where + (+) x y = plusInt# x y + (-) x y = minusInt# x y + negate x = negateInt# x + (*) x y = timesInt# x y + abs n = if n `geInt#` 0# then n else (negateInt# n) + + signum n | n `ltInt#` 0# = negateInt# 1# + | n `eqInt#` 0# = 0# + | otherwise = 1# + + fromInteger (J# a# s# d#) + = integer2Int# a# s# d# + + fromInt (I# i#) = i# + +double x = x * x + x * x - x * x + x * x - x * x + +compute1 n = 1# + double n +compute2 n = (1::Int) + double n + + + diff --git a/ghc/tests/specialise/jmake.multi b/ghc/tests/specialise/jmake.multi new file mode 100644 index 000000000000..dea3b45f8924 --- /dev/null +++ b/ghc/tests/specialise/jmake.multi @@ -0,0 +1,12 @@ +HC_OPTS=-O -unregisterised -g -darity-checks -debug -keep-hc-files-too -odump spec001.dump + +SRCS_HS=Main.hs PreludeSpec001.hs +OBJS_O= Main.o PreludeSpec001.o + +NoFibMultiModuleCompileAndRun(spec001,-i spec001.stdin -o1 spec001.stdout) + +NoFibHaskellCompile(spec001,Main,hs) +NoFibHaskellCompile(spec001,PreludeSpec001,hs) + +HaskellDependTarget( $(SRCS_HS) ) + diff --git a/ghc/tests/specialise/spec001/Jmakefile b/ghc/tests/specialise/spec001/Jmakefile new file mode 100644 index 000000000000..172ff743ba0b --- /dev/null +++ b/ghc/tests/specialise/spec001/Jmakefile @@ -0,0 +1,2 @@ +NoFibOneModuleCompileAndRun(spec001,-i spec001.stdin -o1 spec001.stdout) + diff --git a/ghc/tests/specialise/spec001/Main.hs b/ghc/tests/specialise/spec001/Main.hs new file mode 100644 index 000000000000..20847786dbf2 --- /dev/null +++ b/ghc/tests/specialise/spec001/Main.hs @@ -0,0 +1,40 @@ +module Main where + +data AList a = ANil | ACons a (AList a) + +listtoalist [] = ANil +listtoalist (x:xs) = ACons x (listtoalist xs) + +alisttolist ANil = [] +alisttolist (ACons a as) = (a : alisttolist as) + +mapalist f ANil = ANil +mapalist f (ACons a as) = ACons (f a) (mapalist f as) + +tochar (C# c#) = c# +fromchar c# = C# c# +incchar c# = chr# (ord# c# +# 1#) + +doalist as0 + = let as1# = mapalist{-BChar-} tochar as0 + as2# = mapalist{-CharChar-} incchar as1# + as3 = mapalist{-CharB-} fromchar as2# + in as3 + +dolist xs = alisttolist (doalist (listtoalist xs)) + +main = do + input <- getContents + putStr (unlines (map dolist (lines input))) + + +data AListChar = ANilChar | AConsChar Char# AListChar + +mapalistBChar f ANil = ANilChar +mapalistBChar f (ACons a as) = AConsChar (f a) (mapalistBChar f as) + +mapalistCharChar f ANilChar = ANilChar +mapalistCharChar f (AConsChar a as) = AConsChar (f a) (mapalistCharChar f as) + +mapalistCharB f ANilChar = ANil +mapalistCharB f (AConsChar a as) = ACons (f a) (mapalistCharB f as) diff --git a/ghc/tests/specialise/spec001/spec001.stdin b/ghc/tests/specialise/spec001/spec001.stdin new file mode 100644 index 000000000000..3da1ec26e9c8 --- /dev/null +++ b/ghc/tests/specialise/spec001/spec001.stdin @@ -0,0 +1 @@ +HelloWorld diff --git a/ghc/tests/specialise/spec001/spec001.stdout b/ghc/tests/specialise/spec001/spec001.stdout new file mode 100644 index 000000000000..6cec388d6598 --- /dev/null +++ b/ghc/tests/specialise/spec001/spec001.stdout @@ -0,0 +1 @@ +IfmmpXpsme diff --git a/ghc/tests/specialise/spec002/Jmakefile b/ghc/tests/specialise/spec002/Jmakefile new file mode 100644 index 000000000000..9efbe0b9b641 --- /dev/null +++ b/ghc/tests/specialise/spec002/Jmakefile @@ -0,0 +1 @@ +NoFibOneModuleCompileAndRun(spec002,-i spec002.stdin -o1 spec002.stdout) diff --git a/ghc/tests/specialise/spec002/Main.hs b/ghc/tests/specialise/spec002/Main.hs new file mode 100644 index 000000000000..b310e3830633 --- /dev/null +++ b/ghc/tests/specialise/spec002/Main.hs @@ -0,0 +1,23 @@ +-- Generation of BigTuples ... + +module Main where + +-- import Other (bigtuple2, untuple2) + +bigtuple2 = bigtuple1 +untuple2 = untuple1 + +main = do + input <- getContents + putStr (unlines (map dolist (lines input))) + +dolist l = untuple1 (bigtuple1 l) ++ ['\n'] ++ untuple2 (bigtuple2 l) + +bigtuple1 (a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:q:r:s:t:u:v:w:x:y:z:a':b':c':d':e':f':g':h':i':j':k':l':m':n':rest) + = (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z,a',b',c',d',e',f',g',h',i',j',k',l',m',n') : bigtuple1 rest +bigtuple1 _ = [] + +untuple1 ((a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z,a',b',c',d',e',f',g',h',i',j',k',l',m',n'):rest) + = a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:q:r:s:t:u:v:w:x:y:z:a':b':c':d':e':f':g':h':i':j':k':l':m':n': untuple1 rest +untuple1 [] + = [] diff --git a/ghc/tests/specialise/spec002/Other.hs b/ghc/tests/specialise/spec002/Other.hs new file mode 100644 index 000000000000..f434d3c307b4 --- /dev/null +++ b/ghc/tests/specialise/spec002/Other.hs @@ -0,0 +1,12 @@ +module Other (bigtuple2, untuple2) where + +bigtuple2 (a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:q:r:s:t:u:v:w:x:y:z:a':b':c':d':e':f':g':h':i':j':k':l':m':n':rest) + = (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z,a',b',c',d',e',f',g',h',i',j',k',l',m',n') : bigtuple2 rest +bigtuple2 _ = [] + +untuple2 ((a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z,a',b',c',d',e',f',g',h',i',j',k',l',m',n'):rest) + = a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:q:r:s:t:u:v:w:x:y:z:a':b':c':d':e':f':g':h':i':j':k':l':m':n': untuple2 rest +untuple2 [] + = [] + +data ATuple a b c d e f g h i j k l m n o p = ATuple a b c d e f g h i j k l m n o p diff --git a/ghc/tests/specialise/spec002/spec002.stdin b/ghc/tests/specialise/spec002/spec002.stdin new file mode 100644 index 000000000000..a868a8c6547b --- /dev/null +++ b/ghc/tests/specialise/spec002/spec002.stdin @@ -0,0 +1,2 @@ +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN!!! +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN!!! diff --git a/ghc/tests/specialise/spec002/spec002.stdout b/ghc/tests/specialise/spec002/spec002.stdout new file mode 100644 index 000000000000..86a0dab52a88 --- /dev/null +++ b/ghc/tests/specialise/spec002/spec002.stdout @@ -0,0 +1,4 @@ +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN +abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN diff --git a/ghc/tests/specialise/spec003/Jmakefile b/ghc/tests/specialise/spec003/Jmakefile new file mode 100644 index 000000000000..c349e285f0d4 --- /dev/null +++ b/ghc/tests/specialise/spec003/Jmakefile @@ -0,0 +1,10 @@ +SRCS_HS=Main.hs PreludeNum.hs +OBJS_O= Main.o PreludeNum.o + +NoFibMultiModuleCompileAndRun(spec003,-i spec003.stdin -o1 spec003.stdout) + +NoFibHaskellCompile(spec003,Main,hs) +NoFibHaskellCompile(spec003,PreludeNum,hs) + +NoFibDependTarget(spec003, $(SRCS_HS)) + diff --git a/ghc/tests/specialise/spec003/Main.hs b/ghc/tests/specialise/spec003/Main.hs new file mode 100644 index 000000000000..086ac9f72bb8 --- /dev/null +++ b/ghc/tests/specialise/spec003/Main.hs @@ -0,0 +1,10 @@ +-- Generation of BigTuples ... + +module Main where + +import PreludeNum + +main = putStr (show values) + +values = (I# f1, I# f2, I# f3) + diff --git a/ghc/tests/specialise/spec003/PreludeNum.hs b/ghc/tests/specialise/spec003/PreludeNum.hs new file mode 100644 index 000000000000..291030876f17 --- /dev/null +++ b/ghc/tests/specialise/spec003/PreludeNum.hs @@ -0,0 +1,58 @@ +module PreludeNum (f1, f2, fac, f3, fac_two) where + +{- Preliminaries ... -} + +{- patError# { Int# } (built into compiler) -} +local_map f [] = [] +local_map f (x:xs) = (f x) : local_map f xs + +instance Eq Int# where + x == y = eqInt# x y + x /= y = neInt# x y + +instance Read Int# where + readsPrec p s = map (\ (I# i#, s) -> (i#, s)) (readsPrec p s) + readList s = map (\ (x, s) -> (local_map (\ (I# i#) -> i#) x, s)) (readList s) + +instance Show Int# where + showsPrec p x = showsPrec p (I# x) + showList l = showList (local_map I# l) + +instance Num Int# where + (+) x y = plusInt# x y + (-) x y = minusInt# x y + negate x = negateInt# x + (*) x y = timesInt# x y + abs n = if n `geInt#` 0# then n else (negateInt# n) + + signum n | n `ltInt#` 0# = negateInt# 1# + | n `eqInt#` 0# = 0# + | otherwise = 1# + + fromInteger (J# a# s# d#) + = integer2Int# a# s# d# + + fromInt (I# i#) = i# + + +first (a, b) = a +second (a, b) = b + +{- Here we go ... -} + +fac 0 = 1 +fac n = n * (fac (n - 1)) + +{-# INLINE f1 #-} +f1 = fac 10# + +f2 = f1 * f1 + +fac_two n two = case n of 0 -> (1, 1) + n -> (n * (first (fac_two (n - 1) two)), 2) + +f3 = let (res1, two1) = fac_two (10::Int#) (two2::Int#) + (res2, two2) = fac_two (10::Int) (two1::Int) + in + res1 + two2 + diff --git a/ghc/tests/specialise/spec003/spec003.stdin b/ghc/tests/specialise/spec003/spec003.stdin new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/ghc/tests/specialise/spec003/spec003.stdout b/ghc/tests/specialise/spec003/spec003.stdout new file mode 100644 index 000000000000..e69de29bb2d1 -- GitLab