remove unused tests.
+++ /dev/null
-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.
+++ /dev/null
-TOP = ..
-include $(TOP)/mk/boilerplate.mk
-
-SUBDIRS = $(wildcard spec* code* clausify*)
-
-include $(TOP)/mk/target.mk
+++ /dev/null
-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) )
+++ /dev/null
--- 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
+++ /dev/null
-(a = a = a) = (a = a = a) = (a = a = a)
+++ /dev/null
-prop> a <=
-prop>
\ No newline at end of file
+++ /dev/null
-NoFibOneModuleCompileAndRun(clausify001,-i clausify001.stdin -o1 clausify001.stdout)
+++ /dev/null
--- 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
+++ /dev/null
-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)
+++ /dev/null
--- 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
-
+++ /dev/null
-(a = a = a) = (a = a = a) = (a = a = a)
+++ /dev/null
-prop> a <=
-prop>
\ No newline at end of file
+++ /dev/null
-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))
+++ /dev/null
-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)
+++ /dev/null
--- 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
-
+++ /dev/null
-(a = a = a) = (a = a = a) = (a = a = a)
+++ /dev/null
-prop> a <=
-prop>
\ No newline at end of file
+++ /dev/null
-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))
+++ /dev/null
-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)
+++ /dev/null
--- 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
-
+++ /dev/null
-(a = a = a) = (a = a = a) = (a = a = a)
+++ /dev/null
-prop> a <=
-prop>
\ No newline at end of file
+++ /dev/null
-SRCS_HS=Spec.hs Use.hs
-OBJS_O= Spec.o Use.o
-
-all : $(OBJS_O)
-
-NoFibHaskellCompile(code001,Spec,hs)
-NoFibHaskellCompile(code001,Use,hs)
-
+++ /dev/null
-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
-
-
+++ /dev/null
-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#
-
+++ /dev/null
-SRCS_HS=Spec.hs Use.hs
-OBJS_O= Spec.o Use.o
-
-all : $(OBJS_O)
-
-NoFibHaskellCompile(code002,Spec,hs)
-NoFibHaskellCompile(code002,Use,hs)
-
+++ /dev/null
-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# #-}
+++ /dev/null
-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#
-
+++ /dev/null
-SRCS_HS=PreludeNum.hs
-OBJS_O= PreludeNum.o
-
-all : $(OBJS_O)
-
-NoFibHaskellCompile(code003,PreludeNum,hs)
-
-
+++ /dev/null
-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
-
-
-
+++ /dev/null
-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) )
-
+++ /dev/null
-NoFibOneModuleCompileAndRun(spec001,-i spec001.stdin -o1 spec001.stdout)
-
+++ /dev/null
-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)
+++ /dev/null
-HelloWorld
+++ /dev/null
-IfmmpXpsme
+++ /dev/null
-NoFibOneModuleCompileAndRun(spec002,-i spec002.stdin -o1 spec002.stdout)
+++ /dev/null
--- 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 []
- = []
+++ /dev/null
-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
+++ /dev/null
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN!!!
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN!!!
+++ /dev/null
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNabcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN
-abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMN
+++ /dev/null
-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))
-
+++ /dev/null
--- Generation of BigTuples ...
-
-module Main where
-
-import PreludeNum
-
-main = putStr (show values)
-
-values = (I# f1, I# f2, I# f3)
-
+++ /dev/null
-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
-
projects / ghc-hetmet.git / commitdiff