--- /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 $(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