diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2005 Thomas Jäger
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject
+to the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY
+KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE
+WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Main.hs b/Main.hs
new file mode 100644
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,48 @@
+module Main where
+
+import Plugin.Pl.Common
+import Plugin.Pl.Optimize
+import Plugin.Pl.Parser
+import Plugin.Pl.Transform
+
+import Data.List (intersperse)
+import System.Environment (getArgs)
+import System.Console.GetOpt
+
+data Flag = Verbose 
+  deriving Eq
+
+options :: [OptDescr Flag]
+options = [ Option ['v'] ["verbose"] (NoArg Verbose) "verbose results"]
+
+header :: String
+header = "Usage: pointfree [OPTION...] query"
+
+parseArgs :: [String] -> IO ([Flag], [String])
+parseArgs args =
+  case getOpt Permute options args of
+    (flags, nonOptions, []) -> return (flags, nonOptions)
+    (_, _, errs) -> ioError (userError (concat errs ++ usageInfo header options))
+
+main :: IO ()
+main = do
+  args <- getArgs
+  (flags, nonOptions) <- parseArgs args
+  if null nonOptions
+     then putStrLn $ usageInfo header options
+     else let query = concat $ intersperse " " nonOptions
+              verbose = Verbose `elem` flags
+          in pf query verbose
+
+pf :: String -> Bool -> IO ()
+pf input verbose = case parsePF input of
+  Right d ->
+    if verbose
+       then do putStrLn "Transformed to pointfree style:"
+               let d' = mapTopLevel transform d
+               print $ d'
+               putStrLn "Optimized expression:"
+               mapM_ print $ mapTopLevel' optimize d'
+       else print $ last $ mapTopLevel' optimize $ mapTopLevel transform d
+  Left err -> putStrLn err
+
diff --git a/Plugin/Pl/Common.hs b/Plugin/Pl/Common.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/Common.hs
@@ -0,0 +1,149 @@
+{-# OPTIONS -fvia-C #-}
+
+module Plugin.Pl.Common (
+        Fixity(..), Expr(..), Pattern(..), Decl(..), TopLevel(..),
+        bt, sizeExpr, mapTopLevel, mapTopLevel', getExpr,
+        operators, opchars, reservedOps, lookupOp, lookupFix, minPrec, maxPrec,
+        comp, flip', id', const', scomb, cons, nil, fix', if', readM,
+        makeList, getList,
+        Assoc(..),
+        module Data.Maybe,
+        module Control.Arrow,
+        module Data.List,
+        module Control.Monad,
+        module GHC.Base
+    ) where
+
+import Data.Maybe (isJust, fromJust)
+import Data.List (intersperse, minimumBy)
+import qualified Data.Map as M
+
+import Control.Monad
+import Control.Arrow (first, second, (***), (&&&), (|||), (+++))
+
+import Text.ParserCombinators.Parsec.Expr (Assoc(..))
+
+import GHC.Base (assert)
+
+
+-- The rewrite rules can be found at the end of the file Rules.hs
+
+-- Not sure if passing the information if it was used as infix or prefix
+-- is worth threading through the whole thing is worth the effort,
+-- but it stays that way until the prettyprinting algorithm gets more
+-- sophisticated.
+data Fixity = Pref | Inf deriving Show
+
+instance Eq Fixity where
+  _ == _ = True
+
+instance Ord Fixity where
+  compare _ _ = EQ
+
+data Expr
+  = Var Fixity String
+  | Lambda Pattern Expr
+  | App Expr Expr
+  | Let [Decl] Expr
+  deriving (Eq, Ord)
+
+data Pattern
+  = PVar String 
+  | PCons Pattern Pattern
+  | PTuple Pattern Pattern
+  deriving (Eq, Ord)
+
+data Decl = Define { 
+  declName :: String, 
+  declExpr :: Expr
+} deriving (Eq, Ord)
+
+data TopLevel = TLD Bool Decl | TLE Expr deriving (Eq, Ord)
+
+mapTopLevel :: (Expr -> Expr) -> TopLevel -> TopLevel
+mapTopLevel f tl = case getExpr tl of (e, c) -> c $ f e
+
+mapTopLevel' :: Functor f => (Expr -> f Expr) -> TopLevel -> f TopLevel
+mapTopLevel' f tl = case getExpr tl of (e, c) -> fmap c $ f e
+
+getExpr :: TopLevel -> (Expr, Expr -> TopLevel)
+getExpr (TLD True (Define foo e)) = (Let [Define foo e] (Var Pref foo), 
+                                     \e' -> TLD False $ Define foo e')
+getExpr (TLD False (Define foo e)) = (e, \e' -> TLD False $ Define foo e')
+getExpr (TLE e)      = (e, TLE)
+
+sizeExpr :: Expr -> Int
+sizeExpr (Var _ _) = 1
+sizeExpr (App e1 e2) = sizeExpr e1 + sizeExpr e2 + 1
+sizeExpr (Lambda _ e) = 1 + sizeExpr e
+sizeExpr (Let ds e) = 1 + sum (map sizeDecl ds) + sizeExpr e where
+  sizeDecl (Define _ e') = 1 + sizeExpr e'
+
+comp, flip', id', const', scomb, cons, nil, fix', if' :: Expr
+comp   = Var Inf  "."
+flip'  = Var Pref "flip"
+id'    = Var Pref "id"
+const' = Var Pref "const"
+scomb  = Var Pref "ap"
+cons   = Var Inf  ":"
+nil    = Var Pref "[]"
+fix'   = Var Pref "fix"
+if'    = Var Pref "if'"
+
+makeList :: [Expr] -> Expr
+makeList = foldr (\e1 e2 -> cons `App` e1 `App` e2) nil
+
+-- Modularity is a drag
+getList :: Expr -> ([Expr], Expr)
+getList (c `App` x `App` tl) | c == cons = first (x:) $ getList tl
+getList e = ([],e)
+
+bt :: a
+bt = undefined
+
+shift, minPrec, maxPrec :: Int
+shift = 0
+maxPrec = shift + 10
+minPrec = 0
+
+-- operator precedences are needed both for parsing and prettyprinting
+operators :: [[(String, (Assoc, Int))]]
+operators = (map . map . second . second $ (+shift))
+  [[inf "." AssocRight 9, inf "!!" AssocLeft 9],
+   [inf name AssocRight 8 | name <- ["^", "^^", "**"]],
+   [inf name AssocLeft 7
+     | name <- ["*", "/", "`quot`", "`rem`", "`div`", "`mod`", ":%", "%"]],
+   [inf name AssocLeft 6  | name <- ["+", "-"]],
+   [inf name AssocRight 5 | name <- [":", "++"]],
+   [inf name AssocNone 4 
+     | name <- ["==", "/=", "<", "<=", ">=", ">", "`elem`", "`notElem`"]],
+   [inf "&&" AssocRight 3],
+   [inf "||" AssocRight 2],
+   [inf ">>" AssocLeft 1, inf ">>=" AssocLeft 1, inf "=<<" AssocRight 1],
+   [inf name AssocRight 0 | name <- ["$", "$!", "`seq`"]]
+  ] where
+  inf name assoc fx = (name, (assoc, fx))
+
+opchars :: [Char]
+opchars = "!@#$%^*./|=-+:?<>&"
+
+reservedOps :: [String]
+reservedOps = ["->", "..", "="]
+
+opFM :: M.Map String (Assoc, Int)
+opFM = (M.fromList $ concat operators)
+
+lookupOp :: String -> Maybe (Assoc, Int)
+lookupOp k = M.lookup k opFM
+
+lookupFix :: String -> (Assoc, Int)
+lookupFix str = case lookupOp $ str of
+  Nothing -> (AssocLeft, 9 + shift)
+  Just x  -> x
+
+readM :: (Monad m, Read a) => String -> m a
+readM s = case [x | (x,t) <- reads s, ("","")  <- lex t] of
+            [x] -> return x
+            []  -> fail "readM: No parse."
+            _   -> fail "readM: Ambiguous parse."
+
diff --git a/Plugin/Pl/Optimize.hs b/Plugin/Pl/Optimize.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/Optimize.hs
@@ -0,0 +1,105 @@
+{-# OPTIONS -fvia-C -O2 -optc-O3 #-}
+module Plugin.Pl.Optimize (
+    optimize,
+  ) where
+
+import Plugin.Pl.Common
+import Plugin.Pl.Rules
+import Plugin.Pl.PrettyPrinter
+
+import Data.List (nub)
+import Control.Monad.State
+
+cut :: [a] -> [a]
+cut = take 1
+
+toMonadPlus :: MonadPlus m => Maybe a -> m a
+toMonadPlus Nothing = mzero
+toMonadPlus (Just x)= return x
+
+type Size = Double
+-- This seems to be a better size for our purposes,
+-- despite being "a little" slower because of the wasteful uglyprinting
+sizeExpr' :: Expr -> Size 
+sizeExpr' e = fromIntegral (length $ show e) + adjust e where
+  -- hackish thing to favor some expressions if the length is the same:
+  -- (+ x) --> (x +)
+  -- x >>= f --> f =<< x
+  -- f $ g x --> f (g x)
+  adjust :: Expr -> Size
+  adjust (Var _ str) -- Just n <- readM str = log (n*n+1) / 4
+                     | str == "uncurry"    = -4
+--                     | str == "s"          = 5
+                     | str == "flip"       = 0.1
+                     | str == ">>="        = 0.05
+                     | str == "$"          = 0.01
+                     | str == "subtract"   = 0.01
+                     | str == "ap"         = 2
+                     | str == "liftM2"     = 1.01
+                     | str == "return"     = -2
+                     | str == "zipWith"    = -4
+                     | str == "const"      = 0 -- -2
+                     | str == "fmap"       = -1
+  adjust (Lambda _ e') = adjust e'
+  adjust (App e1 e2)  = adjust e1 + adjust e2
+  adjust _ = 0
+
+optimize :: Expr -> [Expr]
+optimize e = result where
+  result :: [Expr]
+  result = map (snd . fromJust) . takeWhile isJust . 
+    iterate ((=<<) simpleStep) $ Just (sizeExpr' e, e)
+
+  simpleStep :: (Size, Expr) -> Maybe (Size, Expr)
+  simpleStep t = do 
+    let chn = let ?first = True in step (snd t)
+        chnn = let ?first = False in step =<< chn
+        new = filter (\(x,_) -> x < fst t) . map (sizeExpr' &&& id) $ 
+                snd t: chn ++ chnn
+    case new of
+      [] -> Nothing
+      (new':_) -> return new'
+
+step :: (?first :: Bool) => Expr -> [Expr]
+step e = nub $ rewrite rules e
+ 
+rewrite :: (?first :: Bool) => RewriteRule -> Expr -> [Expr]
+rewrite rl e = case rl of
+    Up r1 r2     -> let e'  = cut $ rewrite r1 e
+                        e'' = rewrite r2 =<< e'
+                    in if null e'' then e' else e''
+    OrElse r1 r2 -> let e'  = rewrite r1 e
+                    in if null e' then rewrite r2 e else e' 
+    Then r1 r2   -> rewrite r2 =<< nub (rewrite r1 e)
+    Opt  r       -> e: rewrite r e
+    If   p  r    -> if null (rewrite p e) then mzero else rewrite r e
+    Hard r       -> if ?first then rewrite r e else mzero
+    Or rs        -> (\x -> rewrite x e) =<< rs
+    RR {}        -> rewDeep rl e
+    CRR {}       -> rewDeep rl e
+    Down {}      -> rewDeep rl e
+    
+  where -- rew = ...; rewDeep = ...
+
+rewDeep :: (?first :: Bool) => RewriteRule -> Expr -> [Expr]
+rewDeep rule e = rew rule e `mplus` case e of
+    Var _ _    -> mzero
+    Lambda _ _ -> error "lambda: optimizer only works for closed expressions"
+    Let _ _    -> error "let: optimizer only works for closed expressions"
+    App e1 e2  -> ((`App` e2) `map` rewDeep rule e1) `mplus`
+                  ((e1 `App`) `map` rewDeep rule e2)
+
+rew :: (?first :: Bool) => RewriteRule -> Expr -> [Expr]
+rew (RR r1 r2) e = toMonadPlus $ fire r1 r2 e 
+rew (CRR r) e = toMonadPlus $ r e
+rew (Or rs) e = (\x -> rew x e) =<< rs
+rew (Down r1 r2) e
+  = if null e'' then e' else e'' where
+    e'  = cut $ rew r1 e
+    e'' = rewDeep r2 =<< e'
+rew r@(Then   {}) e = rewrite r e
+rew r@(OrElse {}) e = rewrite r e
+rew r@(Up     {}) e = rewrite r e
+rew r@(Opt    {}) e = rewrite r e
+rew r@(If     {}) e = rewrite r e
+rew r@(Hard   {}) e = rewrite r e
diff --git a/Plugin/Pl/Parser.hs b/Plugin/Pl/Parser.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/Parser.hs
@@ -0,0 +1,229 @@
+{-# OPTIONS -fvia-C -O2 -optc-O3 #-}
+--
+-- Todo, use Language.Haskell
+--
+-- Doesn't handle string literals?
+--
+module Plugin.Pl.Parser (parsePF) where
+
+import Plugin.Pl.Common
+
+import Text.ParserCombinators.Parsec
+import Text.ParserCombinators.Parsec.Expr
+import Text.ParserCombinators.Parsec.Language
+import qualified Text.ParserCombinators.Parsec.Token as T
+
+-- is that supposed to be done that way?
+tp :: T.TokenParser ()
+tp = T.makeTokenParser $ haskellStyle { 
+  reservedNames = ["if","then","else","let","in"]
+}
+
+parens :: Parser a -> Parser a
+parens = T.parens tp
+
+brackets :: Parser a -> Parser a
+brackets = T.brackets tp
+
+symbol :: String -> Parser String
+symbol = T.symbol tp
+
+atomic :: Parser String
+atomic = try (show `fmap` T.natural tp) <|> T.identifier tp
+
+reserved :: String -> Parser ()
+reserved = T.reserved tp
+
+charLiteral :: Parser Char
+charLiteral = T.charLiteral tp
+
+stringLiteral :: Parser String
+stringLiteral = T.stringLiteral tp
+
+table :: [[Operator Char st Expr]]
+table = addToFirst def $ map (map inf) operators where
+  addToFirst y (x:xs) = ((y:x):xs)
+  addToFirst _ _ = assert False bt
+  
+  def :: Operator Char st Expr
+  def = Infix (try $ do
+      name <- parseOp  
+      guard $ not $ isJust $ lookupOp name
+      spaces
+      return $ \e1 e2 -> App (Var Inf name) e1 `App` e2
+    ) AssocLeft
+
+  inf :: (String, (Assoc, Int)) -> Operator Char st Expr
+  inf (name, (assoc, _)) = Infix (try $ do 
+      string name
+      notFollowedBy $ oneOf opchars
+      spaces
+      let name' = if head name == '`' 
+                  then tail . reverse . tail . reverse $ name 
+                  else name
+      return $ \e1 e2 -> App (Var Inf name') e1 `App` e2
+    ) assoc
+
+
+parseOp :: CharParser st String
+parseOp = (between (char '`') (char '`') $ many1 (letter <|> digit))
+  <|> try (do 
+    op <- many1 $ oneOf opchars
+    guard $ not $ op `elem` reservedOps
+    return op)
+
+pattern :: Parser Pattern
+pattern = buildExpressionParser ptable ((PVar `fmap` 
+                       (    atomic 
+                        <|> (symbol "_" >> return ""))) 
+                        <|> parens pattern)
+    <?> "pattern" where
+  ptable = [[Infix (symbol ":" >> return PCons) AssocRight],
+            [Infix (symbol "," >> return PTuple) AssocNone]]
+
+lambda :: Parser Expr
+lambda = do
+    symbol "\\"
+    vs <- many1 pattern
+    symbol "->"
+    e <- myParser False
+    return $ foldr Lambda e vs
+  <?> "lambda abstraction"
+
+var :: Parser Expr
+var = try (makeVar `fmap` atomic <|> 
+           parens (try unaryNegation <|> try rightSection
+                   <|> try (makeVar `fmap` many1 (char ',')) 
+                   <|> tuple) <|> list <|> (Var Pref . show) `fmap` charLiteral
+                   <|> stringVar `fmap` stringLiteral)
+        <?> "variable" where
+  makeVar v | Just _ <- lookupOp v = Var Inf v -- operators always want to
+                                               -- be infixed
+            | otherwise            = Var Pref v
+  stringVar :: String -> Expr
+  stringVar str = makeList $ (Var Pref . show) `map` str
+
+list :: Parser Expr
+list = msum (map (try . brackets) plist) <?> "list" where
+  plist = [
+    foldr (\e1 e2 -> cons `App` e1 `App` e2) nil `fmap` 
+      (myParser False `sepBy` symbol ","),
+    do e <- myParser False
+       symbol ".."
+       return $ Var Pref "enumFrom" `App` e,
+    do e <- myParser False
+       symbol ","
+       e' <- myParser False
+       symbol ".."
+       return $ Var Pref "enumFromThen" `App` e `App` e',
+    do e <- myParser False
+       symbol ".."
+       e' <- myParser False
+       return $ Var Pref "enumFromTo" `App` e `App` e',
+    do e <- myParser False
+       symbol ","
+       e' <- myParser False
+       symbol ".."
+       e'' <- myParser False
+       return $ Var Pref "enumFromThenTo" `App` e `App` e' `App` e''
+    ] 
+
+tuple :: Parser Expr
+tuple = do
+    elts <- myParser False `sepBy` symbol ","
+    guard $ length elts /= 1
+    let name = Var Pref $ replicate (length elts - 1) ','
+    return $ foldl App name elts
+  <?> "tuple"
+
+unaryNegation :: Parser Expr
+unaryNegation = do
+    symbol "-"
+    e <- myParser False
+    return $ Var Pref "negate" `App` e
+  <?> "unary negation"
+
+rightSection :: Parser Expr
+rightSection = do
+    v <- Var Inf `fmap` parseOp
+    spaces
+    let rs e = flip' `App` v `App` e
+    option v (rs `fmap` myParser False)
+  <?> "right section"
+    
+
+myParser :: Bool -> Parser Expr
+myParser b = lambda <|> expr b
+
+expr :: Bool -> Parser Expr
+expr b = buildExpressionParser table (term b) <?> "expression"
+
+decl :: Parser Decl
+decl = do
+  f <- atomic 
+  args <- pattern `endsIn` symbol "="
+  e <- myParser False
+  return $ Define f (foldr Lambda e args)
+
+letbind :: Parser Expr
+letbind = do
+  reserved "let"
+  ds <- decl `sepBy` symbol ";"
+  reserved "in"
+  e <- myParser False
+  return $ Let ds e
+
+ifexpr :: Parser Expr
+ifexpr = do
+  reserved "if"
+  p <- myParser False
+  reserved "then"
+  e1 <- myParser False
+  reserved "else"
+  e2 <- myParser False
+  return $ if' `App` p `App` e1 `App` e2
+
+term :: Bool -> Parser Expr
+term b = application <|> lambda <|> letbind <|> ifexpr <|>
+    (guard b >> (notFollowedBy (noneOf ")") >> return (Var Pref "")))
+  <?> "simple term"
+
+application :: Parser Expr
+application = do
+    e:es <- many1 $ var <|> parens (myParser True)
+    return $ foldl App e es
+  <?> "application"
+
+endsIn :: Parser a -> Parser b -> Parser [a]
+endsIn p end = do
+  xs <- many p
+  end
+  return $ xs
+
+input :: Parser TopLevel
+input = do
+  spaces
+  tl <- try (do 
+      f    <- atomic
+      args <- pattern `endsIn` symbol "="
+      e    <- myParser False
+      return $ TLD True $ Define f (foldr Lambda e args)
+    ) <|> TLE `fmap` myParser False
+  eof
+  return tl
+
+parsePF :: String -> Either String TopLevel
+parsePF inp = case runParser input () "" inp of
+    Left err -> Left $ show err
+    Right e  -> Right $ mapTopLevel postprocess e
+
+
+postprocess :: Expr -> Expr
+postprocess (Var f v) = (Var f v)
+postprocess (App e1 (Var Pref "")) = postprocess e1
+postprocess (App e1 e2) = App (postprocess e1) (postprocess e2)
+postprocess (Lambda v e) = Lambda v (postprocess e)
+postprocess (Let ds e) = Let (mapDecl postprocess `map` ds) $ postprocess e where
+  mapDecl :: (Expr -> Expr) -> Decl -> Decl
+  mapDecl f (Define foo e') = Define foo $ f e'
+
diff --git a/Plugin/Pl/PrettyPrinter.hs b/Plugin/Pl/PrettyPrinter.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/PrettyPrinter.hs
@@ -0,0 +1,149 @@
+{-# OPTIONS -fvia-C -fno-warn-orphans #-}
+module Plugin.Pl.PrettyPrinter (Expr) where
+
+-- Dummy export to make ghc -Wall happy
+
+import Plugin.Pl.Common
+
+instance Show Decl where
+  show (Define f e) = f ++ " = " ++ show e
+  showList ds = (++) $ concat $ intersperse "; " $ map show ds
+
+instance Show TopLevel where
+  showsPrec p (TLE e) = showsPrec p e
+  showsPrec p (TLD _ d) = showsPrec p d
+
+data SExpr
+  = SVar !String
+  | SLambda ![Pattern] !SExpr
+  | SLet ![Decl] !SExpr
+  | SApp !SExpr !SExpr
+  | SInfix !String !SExpr !SExpr
+  | LeftSection !String !SExpr  -- (x +)
+  | RightSection !String !SExpr -- (+ x)
+  | List ![SExpr]
+  | Tuple ![SExpr]
+  | Enum !Expr !(Maybe Expr) !(Maybe Expr)
+
+{-# INLINE toSExprHead #-}
+toSExprHead :: String -> [Expr] -> Maybe SExpr
+toSExprHead hd tl
+  | all (==',') hd, length hd+1 == length tl 
+  = Just . Tuple . reverse $ map toSExpr tl
+  | otherwise = case (hd,reverse tl) of
+      ("enumFrom", [e])              -> Just $ Enum e Nothing   Nothing
+      ("enumFromThen", [e,e'])       -> Just $ Enum e (Just e') Nothing
+      ("enumFromTo", [e,e'])         -> Just $ Enum e Nothing   (Just e')
+      ("enumFromThenTo", [e,e',e'']) -> Just $ Enum e (Just e') (Just e'')
+      _                              -> Nothing
+
+toSExpr :: Expr -> SExpr
+toSExpr (Var _ v) = SVar v
+toSExpr (Lambda v e) = case toSExpr e of
+  (SLambda vs e') -> SLambda (v:vs) e'
+  e'              -> SLambda [v] e'
+toSExpr (Let ds e) = SLet ds $ toSExpr e
+toSExpr e | Just (hd,tl) <- getHead e, Just se <- toSExprHead hd tl = se
+toSExpr e | (ls, tl) <- getList e, tl == nil
+  = List $ map toSExpr ls
+toSExpr (App e1 e2) = case e1 of
+  App (Var Inf v) e0 
+    -> SInfix v (toSExpr e0) (toSExpr e2)
+  Var Inf v | v /= "-"
+    -> LeftSection v (toSExpr e2)
+
+  Var _ "flip" | Var Inf v <- e2, v == "-" -> toSExpr $ Var Pref "subtract"
+    
+  App (Var _ "flip") (Var pr v)
+    | v == "-"  -> toSExpr $ Var Pref "subtract" `App` e2
+    | v == "id" -> RightSection "$" (toSExpr e2)
+    | Inf <- pr -> RightSection v (toSExpr e2)
+  _ -> SApp (toSExpr e1) (toSExpr e2)
+
+getHead :: Expr -> Maybe (String, [Expr])
+getHead (Var _ v) = Just (v, [])
+getHead (App e1 e2) = second (e2:) `fmap` getHead e1
+getHead _ = Nothing
+
+instance Show Expr where
+  showsPrec p = showsPrec p . toSExpr
+
+instance Show SExpr where
+  showsPrec _ (SVar v) = (getPrefName v ++)
+  showsPrec p (SLambda vs e) = showParen (p > minPrec) $ ('\\':) . 
+    foldr (.) id (intersperse (' ':) (map (showsPrec $ maxPrec+1) vs)) .
+    (" -> "++) . showsPrec minPrec e
+  showsPrec p (SApp e1 e2) = showParen (p > maxPrec) $
+    showsPrec maxPrec e1 . (' ':) . showsPrec (maxPrec+1) e2
+  showsPrec _ (LeftSection fx e) = showParen True $ 
+    showsPrec (snd (lookupFix fx) + 1) e . (' ':) . (getInfName fx++)
+  showsPrec _ (RightSection fx e) = showParen True $ 
+    (getInfName fx++) . (' ':) . showsPrec (snd (lookupFix fx) + 1) e
+  showsPrec _ (Tuple es) = showParen True $
+    (concat `id` intersperse ", " (map show es) ++)
+  
+  showsPrec _ (List es) 
+    | Just cs <- mapM ((=<<) readM . fromSVar) es = shows (cs::String)
+    | otherwise = ('[':) . 
+      (concat `id` intersperse ", " (map show es) ++) . (']':)
+    where fromSVar (SVar str) = Just str
+          fromSVar _          = Nothing
+  showsPrec _ (Enum fr tn to) = ('[':) . shows fr . 
+    showsMaybe (((',':) . show) `fmap` tn) . (".."++) . 
+    showsMaybe (show `fmap` to) . (']':)
+      where showsMaybe = maybe id (++)
+  showsPrec _ (SLet ds e) = ("let "++) . shows ds . (" in "++) . shows e
+
+
+  showsPrec p (SInfix fx e1 e2) = showParen (p > fixity) $
+    showsPrec f1 e1 . (' ':) . (getInfName fx++) . (' ':) . 
+    showsPrec f2 e2 where
+      fixity = snd $ lookupFix fx
+      (f1, f2) = case fst $ lookupFix fx of
+        AssocRight -> (fixity+1, fixity + infixSafe e2 AssocLeft fixity)
+        AssocLeft  -> (fixity + infixSafe e1 AssocRight fixity, fixity+1)
+        AssocNone  -> (fixity+1, fixity+1)
+
+      -- This is a little bit awkward, but at least seems to produce no false
+      -- results anymore
+      infixSafe :: SExpr -> Assoc -> Int -> Int
+      infixSafe (SInfix fx'' _ _) assoc fx'
+        | lookupFix fx'' == (assoc, fx') = 1
+        | otherwise = 0
+      infixSafe _ _ _ = 0 -- doesn't matter
+
+instance Show Pattern where
+  showsPrec _ (PVar v) = (v++)
+  showsPrec _ (PTuple p1 p2) = showParen True $
+    showsPrec 0 p1 . (", "++) . showsPrec 0 p2
+  showsPrec p (PCons p1 p2) = showParen (p>5) $
+    showsPrec 6 p1 . (':':) . showsPrec 5 p2
+  
+isOperator :: String -> Bool
+isOperator = all (`elem` opchars)
+
+getInfName :: String -> String
+getInfName str = if isOperator str then str else "`"++str++"`"
+
+getPrefName :: String -> String
+getPrefName str = if isOperator str || ',' `elem` str then "("++str++")" else str
+
+instance Eq Assoc where
+  AssocLeft  == AssocLeft  = True
+  AssocRight == AssocRight = True
+  AssocNone  == AssocNone  = True
+  _          == _          = False
+
+{-
+instance Show Assoc where
+  show AssocLeft  = "AssocLeft"
+  show AssocRight = "AssocRight"
+  show AssocNone  = "AssocNone"
+
+instance Ord Assoc where
+  AssocNone <= _ = True
+  _ <= AssocNone = False
+  AssocLeft <= _ = True
+  _ <= AssocLeft = False
+  _ <= _ = True
+-}
diff --git a/Plugin/Pl/Rules.hs b/Plugin/Pl/Rules.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/Rules.hs
@@ -0,0 +1,764 @@
+{-# OPTIONS -fvia-C #-}
+{-# OPTIONS -fno-warn-name-shadowing #-}
+-- 6.4 gives a name shadow warning I haven't tracked down.
+
+--
+-- | This marvellous module contributed by Thomas J\344ger
+--
+module Plugin.Pl.Rules (RewriteRule(..), rules, fire) where
+
+import Lib.Serial (readM)
+
+import Plugin.Pl.Common
+
+import Data.Array
+import qualified Data.Set as S
+
+import Control.Monad.Fix (fix)
+
+--import PlModule.PrettyPrinter
+
+-- Next time I do somthing like this, I'll actually think about the combinator
+-- language before, instead of producing something ad-hoc like this:
+data RewriteRule 
+  = RR Rewrite Rewrite
+  | CRR (Expr -> Maybe Expr)
+  | Down RewriteRule RewriteRule
+  | Up RewriteRule RewriteRule
+  | Or [RewriteRule]
+  | OrElse RewriteRule RewriteRule
+  | Then RewriteRule RewriteRule
+  | Opt RewriteRule
+  | If RewriteRule RewriteRule
+  | Hard RewriteRule
+
+-- No MLambda here because we only consider closed Terms (no alpha-renaming!).
+data MExpr
+  = MApp !MExpr !MExpr
+  | Hole !Int
+  | Quote !Expr
+  deriving Eq
+
+--instance Show MExpr where
+--  show = show . fromMExpr
+
+data Rewrite = Rewrite {
+  holes :: MExpr,
+  rid :: Int -- rlength - 1
+} --deriving Show
+
+-- What are you gonna do when no recursive modules are possible?
+class RewriteC a where
+  getRewrite :: a -> Rewrite 
+
+instance RewriteC MExpr where
+  getRewrite rule = Rewrite {
+    holes   = rule,
+    rid = 0
+  }
+
+type ExprArr = Array Int Expr
+
+myFire :: ExprArr -> MExpr -> MExpr
+myFire xs (MApp e1 e2) = MApp (myFire xs e1) (myFire xs e2)
+myFire xs (Hole h) = Quote $ xs ! h
+myFire _ me = me
+
+nub' :: Ord a => [a] -> [a]
+nub' = S.toList . S.fromList
+
+uniqueArray :: Ord v => Int -> [(Int, v)] -> Maybe (Array Int v)
+uniqueArray n lst 
+  | length (nub' lst) == n = Just $ array (0,n-1) lst
+  | otherwise = Nothing              
+
+match :: Rewrite -> Expr -> Maybe ExprArr
+match (Rewrite hl rid') e  = uniqueArray rid' =<< matchWith hl e
+
+fire' :: Rewrite -> ExprArr -> MExpr
+fire' (Rewrite hl _)   = (`myFire` hl)
+
+fire :: Rewrite -> Rewrite -> Expr -> Maybe Expr
+fire r1 r2 e = (fromMExpr . fire' r2) `fmap` match r1 e
+
+matchWith :: MExpr -> Expr -> Maybe [(Int, Expr)]
+matchWith (MApp e1 e2) (App e1' e2') = 
+  liftM2 (++) (matchWith e1 e1') (matchWith e2 e2')
+matchWith (Quote e) e' = if e == e' then Just [] else Nothing
+matchWith (Hole k) e = Just [(k,e)]
+matchWith _ _ = Nothing
+
+fromMExpr :: MExpr -> Expr
+fromMExpr (MApp e1 e2)  = App (fromMExpr e1) (fromMExpr e2)
+fromMExpr (Hole _)      = Var Pref "Hole" -- error "Hole in MExpr"
+fromMExpr (Quote e)     = e
+
+instance RewriteC a => RewriteC (MExpr -> a) where
+  getRewrite rule = Rewrite {
+    holes = holes . getRewrite . rule . Hole $ pid,
+    rid   = pid + 1
+  } where 
+    pid = rid $ getRewrite (bt :: a)
+
+-- Yet another pointless transformation
+transformM :: Int -> MExpr -> MExpr
+transformM _ (Quote e) = constE `a` Quote e
+transformM n (Hole n') = if n == n' then idE else constE `a` Hole n'
+transformM n (Quote (Var _ ".") `MApp` e1 `MApp` e2)
+  | e1 `hasHole` n && not (e2 `hasHole` n) 
+  = flipE `a` compE `a` e2 `c` transformM n e1
+transformM n e@(MApp e1 e2) 
+  | fr1 && fr2 = sE `a` transformM n e1 `a` transformM n e2
+  | fr1        = flipE `a` transformM n e1 `a` e2
+  | fr2, Hole n' <- e2, n' == n = e1
+  | fr2        = e1 `c` transformM n e2
+  | otherwise  = constE `a` e
+  where
+    fr1 = e1 `hasHole` n
+    fr2 = e2 `hasHole` n
+
+hasHole :: MExpr -> Int -> Bool
+hasHole (MApp e1 e2) n = e1 `hasHole` n || e2 `hasHole` n
+hasHole (Quote _)   _ = False
+hasHole (Hole n')   n = n == n'
+
+--
+-- haddock doesn't like n+k patterns, so rewrite them
+--
+getVariants, getVariants' :: Rewrite -> [Rewrite]
+getVariants' r@(Rewrite _ 0)  = [r]
+getVariants' r@(Rewrite e nk)
+    | nk >= 1    = r : getVariants (Rewrite e' (nk-1))
+    | otherwise  = error "getVariants' : nk went negative"
+    where
+        e' = decHoles $ transformM 0 e
+
+        decHoles (Hole n')    = Hole (n'-1)
+        decHoles (MApp e1 e2) = decHoles e1 `MApp` decHoles e2
+        decHoles me           = me
+
+getVariants = getVariants' -- r = trace (show vs) vs where vs = getVariants' r
+
+rr, rr0, rr1, rr2 :: RewriteC a => a -> a -> RewriteRule
+-- use this rewrite rule and rewrite rules derived from it by iterated
+-- pointless transformation
+rrList :: RewriteC a => a -> a -> [RewriteRule]
+rrList r1 r2 = zipWith RR (getVariants r1') (getVariants r2') where
+  r1' = getRewrite r1
+  r2' = getRewrite r2
+
+rr  r1 r2 = Or          $ rrList r1 r2
+rr1 r1 r2 = Or . take 2 $ rrList r1 r2
+rr2 r1 r2 = Or . take 3 $ rrList r1 r2
+
+-- use only this rewrite rule
+rr0 r1 r2 = RR r1' r2' where
+  r1' = getRewrite r1
+  r2' = getRewrite r2
+  
+down, up :: RewriteRule -> RewriteRule
+down = fix . Down
+up   = fix . Up
+
+
+idE, flipE, bindE, extE, returnE, consE, appendE, nilE, foldrE, foldlE, fstE,
+  sndE, dollarE, constE, uncurryE, curryE, compE, headE, tailE, sE, commaE, 
+  fixE, foldl1E, notE, equalsE, nequalsE, plusE, multE, zeroE, oneE, lengthE, 
+  sumE, productE, concatE, concatMapE, joinE, mapE, fmapE, fmapIE, subtractE, 
+  minusE, liftME, apE, liftM2E, seqME, zipE, zipWithE, 
+  crossE, firstE, secondE, andE, orE, allE, anyE :: MExpr
+idE        = Quote $ Var Pref "id"
+flipE      = Quote $ Var Pref "flip"
+constE     = Quote $ Var Pref "const"
+compE      = Quote $ Var Inf "."
+sE         = Quote $ Var Pref "ap"
+fixE       = Quote $ Var Pref "fix"
+bindE      = Quote $ Var Inf  ">>="
+extE       = Quote $ Var Inf  "=<<"
+returnE    = Quote $ Var Pref "return"
+consE      = Quote $ Var Inf  ":"
+nilE       = Quote $ Var Pref "[]"
+appendE    = Quote $ Var Inf  "++"
+foldrE     = Quote $ Var Pref "foldr"
+foldlE     = Quote $ Var Pref "foldl"
+fstE       = Quote $ Var Pref "fst"
+sndE       = Quote $ Var Pref "snd"
+dollarE    = Quote $ Var Inf  "$"
+uncurryE   = Quote $ Var Pref "uncurry"
+curryE     = Quote $ Var Pref "curry"
+headE      = Quote $ Var Pref "head"
+tailE      = Quote $ Var Pref "tail"
+commaE     = Quote $ Var Inf  ","
+foldl1E    = Quote $ Var Pref "foldl1"
+equalsE    = Quote $ Var Inf  "=="
+nequalsE   = Quote $ Var Inf  "/="
+notE       = Quote $ Var Pref "not"
+plusE      = Quote $ Var Inf  "+"
+multE      = Quote $ Var Inf  "*"
+zeroE      = Quote $ Var Pref "0"
+oneE       = Quote $ Var Pref "1"
+lengthE    = Quote $ Var Pref "length"
+sumE       = Quote $ Var Pref "sum"
+productE   = Quote $ Var Pref "product"
+concatE    = Quote $ Var Pref "concat"
+concatMapE = Quote $ Var Pref "concatMap"
+joinE      = Quote $ Var Pref "join"
+mapE       = Quote $ Var Pref "map"
+fmapE      = Quote $ Var Pref "fmap"
+fmapIE     = Quote $ Var Inf  "fmap"
+subtractE  = Quote $ Var Pref "subtract"
+minusE     = Quote $ Var Inf  "-"
+liftME     = Quote $ Var Pref "liftM"
+liftM2E    = Quote $ Var Pref "liftM2"
+apE        = Quote $ Var Inf  "ap"
+seqME      = Quote $ Var Inf  ">>"
+zipE       = Quote $ Var Pref "zip"
+zipWithE   = Quote $ Var Pref "zipWith"
+crossE     = Quote $ Var Inf  "***"
+firstE     = Quote $ Var Pref "first"
+secondE    = Quote $ Var Pref "second"
+andE       = Quote $ Var Pref "and"
+orE        = Quote $ Var Pref "or"
+allE       = Quote $ Var Pref "all"
+anyE       = Quote $ Var Pref "any"
+
+
+
+a, c :: MExpr -> MExpr -> MExpr
+a       = MApp
+c e1 e2 = compE `a` e1 `a` e2
+infixl 9 `a`
+infixr 8 `c`
+
+
+collapseLists :: Expr -> Maybe Expr
+collapseLists (Var _ "++" `App` e1 `App` e2)
+  | (xs,x) <- getList e1, x==nil,
+    (ys,y) <- getList e2, y==nil = Just $ makeList $ xs ++ ys
+collapseLists _ = Nothing
+
+data Binary = forall a b c. (Read a, Show a, Read b, Show b, Read c, Show c) => BA (a -> b -> c)
+
+evalBinary :: [(String, Binary)] -> Expr -> Maybe Expr
+evalBinary fs (Var _ f' `App` Var _ x' `App` Var _ y')
+  | Just (BA f) <- lookup f' fs = (Var Pref . show) `fmap` liftM2 f (readM x') (readM y')
+evalBinary _ _ = Nothing
+
+data Unary = forall a b. (Read a, Show a, Read b, Show b) => UA (a -> b)
+
+evalUnary :: [(String, Unary)] -> Expr -> Maybe Expr
+evalUnary fs (Var _ f' `App` Var _ x')
+  | Just (UA f) <- lookup f' fs = (Var Pref . show . f) `fmap` readM x'
+evalUnary _ _ = Nothing
+
+assocR, assocL, assoc :: [String] -> Expr -> Maybe Expr
+-- (f `op` g) `op` h --> f `op` (g `op` h)
+assocR ops (Var f1 op1 `App` (Var f2 op2 `App` e1 `App` e2) `App` e3)
+  | op1 == op2 && op1 `elem` ops 
+  = Just (Var f1 op1 `App` e1 `App` (Var f2 op2 `App` e2 `App` e3))
+assocR _ _ = Nothing
+
+-- f `op` (g `op` h) --> (f `op` g) `op` h
+assocL ops (Var f1 op1 `App` e1 `App` (Var f2 op2 `App` e2 `App` e3))
+  | op1 == op2 && op1 `elem` ops 
+  = Just (Var f1 op1 `App` (Var f2 op2 `App` e1 `App` e2) `App` e3)
+assocL _ _ = Nothing
+
+-- op f . op g --> op (f `op` g)
+assoc ops (Var _ "." `App` (Var f1 op1 `App` e1) `App` (Var f2 op2 `App` e2))
+  | op1 == op2 && op1 `elem` ops
+  = Just (Var f1 op1 `App` (Var f2 op2 `App` e1 `App` e2))
+assoc _ _ = Nothing
+
+commutative :: [String] -> Expr -> Maybe Expr
+commutative ops (Var f op `App` e1 `App` e2) 
+  | op `elem` ops = Just (Var f op `App` e2 `App` e1)
+commutative ops (Var _ "flip" `App` e@(Var _ op)) | op `elem` ops = Just e
+commutative _ _ = Nothing
+
+-- TODO: Move rules into a file.
+{-# INLINE simplifies #-}
+simplifies :: RewriteRule
+simplifies = Or [
+  -- (f . g) x --> f (g x)
+  rr0 (\f g x -> (f `c` g) `a` x)
+      (\f g x -> f `a` (g `a` x)),
+  -- id x --> x
+  rr0 (\x -> idE `a` x)
+      (\x -> x),
+  -- flip (flip x) --> x
+  rr  (\x -> flipE `a` (flipE `a` x))
+      (\x -> x),
+  -- flip id x . f --> flip f x
+  rr0 (\f x -> (flipE `a` idE `a` x) `c` f)
+      (\f x -> flipE `a` f `a` x),
+  -- id . f --> f
+  rr0 (\f -> idE `c` f)
+      (\f -> f),
+  -- f . id --> f
+  rr0 (\f -> f `c` idE)
+      (\f -> f),
+  -- const x y --> x
+  rr0 (\x y -> constE `a` x `a` y)
+      (\x _ -> x),
+  -- not (not x) --> x
+  rr  (\x -> notE `a` (notE `a` x))
+      (\x -> x),
+  -- fst (x,y) --> x
+  rr  (\x y -> fstE `a` (commaE `a` x `a` y))
+      (\x _ -> x),
+  -- snd (x,y) --> y
+  rr  (\x y -> sndE `a` (commaE `a` x `a` y))
+      (\_ y -> y),
+  -- head (x:xs) --> x
+  rr  (\x xs -> headE `a` (consE `a` x `a` xs))
+      (\x _  -> x),
+  -- tail (x:xs) --> xs
+  rr  (\x xs -> tailE `a` (consE `a` x `a` xs))
+      (\_ xs -> xs),
+  -- uncurry f (x,y) --> f x y
+  rr1 (\f x y -> uncurryE `a` f `a` (commaE `a` x `a` y))
+      (\f x y -> f `a` x `a` y),
+  -- uncurry (,) --> id
+  rr  (uncurryE `a` commaE)
+      (idE),
+  -- uncurry f . s (,) g --> s f g
+  rr1 (\f g -> (uncurryE `a` f) `c` (sE `a` commaE `a` g))
+      (\f g -> sE `a` f `a` g),
+  -- curry fst --> const
+  rr (curryE `a` fstE) (constE),
+  -- curry snd --> const id
+  rr (curryE `a` sndE) (constE `a` idE),
+  -- s f g x --> f x (g x)
+  rr0 (\f g x -> sE `a` f `a` g `a` x)
+      (\f g x -> f `a` x `a` (g `a` x)),
+  -- flip f x y --> f y x
+  rr0 (\f x y -> flipE `a` f `a` x `a` y)
+      (\f x y -> f `a` y `a` x),
+  -- flip (=<<) --> (>>=)
+  rr0 (flipE `a` extE)
+      bindE,
+
+  -- TODO: Think about map/fmap
+  -- fmap id --> id
+  rr (fmapE `a` idE)
+     (idE),
+  -- map id --> id
+  rr (mapE `a` idE)
+     (idE),
+  -- (f . g) . h --> f . (g . h)
+  rr0 (\f g h -> (f `c` g) `c` h)
+      (\f g h -> f `c` (g `c` h)),
+  -- fmap f . fmap g -> fmap (f . g)
+  rr0 (\f g -> fmapE `a` f `c` fmapE `a` g)
+      (\f g -> fmapE `a` (f `c` g)),
+  -- map f . map g -> map (f . g)
+  rr0 (\f g -> mapE `a` f `c` mapE `a` g)
+      (\f g -> mapE `a` (f `c` g))
+  
+  ]
+
+onceRewrites :: RewriteRule
+onceRewrites = Hard $ Or [
+  -- ($) --> id
+  rr0 (dollarE)
+      idE,
+  -- concatMap --> (=<<)
+  rr concatMapE extE,
+  -- concat    --> join
+  rr concatE joinE,
+  -- liftM --> fmap
+  rr liftME fmapE,
+  -- map --> fmap
+  rr mapE fmapE,
+  -- subtract -> flip (-)
+  rr  subtractE
+      (flipE `a` minusE)
+  ]
+
+-- Now we can state rewrite rules in a nice high level way
+-- Rewrite rules should be as pointful as possible since the pointless variants
+-- will be derived automatically.
+rules :: RewriteRule
+rules = Or [
+  -- f (g x) --> (f . g) x
+  Hard $
+  rr  (\f g x -> f `a` (g `a` x)) 
+      (\f g x -> (f `c` g) `a` x),
+  -- (>>=) --> flip (=<<)
+  Hard $
+  rr  bindE
+      (flipE `a` extE),
+  -- (.) id --> id
+  rr (compE `a` idE)
+     idE,
+  -- (++) [x] --> (:) x
+  rr  (\x -> appendE `a` (consE `a` x `a` nilE))
+      (\x -> consE `a` x),
+  -- (=<<) return --> id
+  rr  (extE `a` returnE)
+      idE,
+  -- (=<<) f (return x) -> f x
+  rr  (\f x -> extE `a` f `a` (returnE `a` x))
+      (\f x -> f `a` x),
+  -- (=<<) ((=<<) f . g) --> (=<<) f . (=<<) g
+  rr  (\f g -> extE `a` ((extE `a` f) `c` g))
+      (\f g -> (extE `a` f) `c` (extE `a` g)),
+  -- flip (f . g) --> flip (.) g . flip f
+  Hard $
+  rr  (\f g -> flipE `a` (f `c` g))
+      (\f g -> (flipE `a` compE `a` g) `c` (flipE `a` f)),
+  -- flip (.) f . flip id --> flip f 
+  rr  (\f -> (flipE `a` compE `a` f) `c` (flipE `a` idE))
+      (\f -> flipE `a` f),
+  -- flip (.) f . flip flip --> flip (flip . f)
+  rr  (\f -> (flipE `a` compE `a` f) `c` (flipE `a` flipE))
+      (\f -> flipE `a` (flipE `c` f)),
+  -- flip (flip (flip . f) g) --> flip (flip . flip f) g
+  rr1 (\f g -> flipE `a` (flipE `a` (flipE `c` f) `a` g))
+      (\f g -> flipE `a` (flipE `c` flipE `a` f) `a` g),
+  
+  -- flip (.) id --> id
+  rr (flipE `a` compE `a` idE)
+     idE,
+  -- (.) . flip id --> flip flip
+  rr  (compE `c` (flipE `a` idE))
+      (flipE `a` flipE),
+  -- s const x y --> y
+  rr  (\x y -> sE `a` constE `a` x `a` y)
+      (\_ y -> y),
+  -- s (const . f) g --> f
+  rr1 (\f g -> sE `a` (constE `c` f) `a` g)
+      (\f _ -> f),
+  -- s (const f) --> (.) f
+  rr  (\f -> sE `a` (constE `a` f))
+      (\f -> compE `a` f),
+  -- s (f . fst) snd --> uncurry f
+  rr  (\f -> sE `a` (f `c` fstE) `a` sndE)
+      (\f -> uncurryE `a` f),
+  -- fst (join (,) x) --> x
+  rr (\x -> fstE `a` (joinE `a` commaE `a` x))
+     (\x -> x),
+  -- snd (join (,) x) --> x
+  rr (\x -> sndE `a` (joinE `a` commaE `a` x))
+     (\x -> x),
+  -- The next two are `simplifies', strictly speaking, but invoked rarely.
+  -- uncurry f (x,y) --> f x y
+--  rr  (\f x y -> uncurryE `a` f `a` (commaE `a` x `a` y))
+--      (\f x y -> f `a` x `a` y),
+  -- curry (uncurry f) --> f
+  rr (\f -> curryE `a` (uncurryE `a` f))
+     (\f -> f),
+  -- uncurry (curry f) --> f
+  rr (\f -> uncurryE `a` (curryE `a` f))
+     (\f -> f),
+  -- (const id . f) --> const id
+  rr  (\f -> (constE `a` idE) `c` f)
+      (\_ -> constE `a` idE),
+  -- const x . f --> const x
+  rr (\x f -> constE `a` x `c` f)
+     (\x _ -> constE `a` x),
+  -- fix f --> f (fix x)
+  Hard $
+  rr0 (\f -> fixE `a` f)
+      (\f -> f `a` (fixE `a` f)),
+  -- f (fix f) --> fix x
+  Hard $
+  rr0 (\f -> f `a` (fixE `a` f))
+      (\f -> fixE `a` f),
+  -- fix f --> f (f (fix x))
+  Hard $ 
+  rr0 (\f -> fixE `a` f)
+      (\f -> f `a` (f `a` (fixE `a` f))),
+  -- fix (const f) --> f
+  rr (\f -> fixE `a` (constE `a` f)) 
+     (\f -> f),
+  -- flip const x --> id
+  rr  (\x -> flipE `a` constE `a` x)
+      (\_ -> idE),
+  -- const . f --> flip (const f)
+  Hard $ 
+  rr  (\f -> constE `c` f)
+      (\f -> flipE `a` (constE `a` f)),
+  -- not (x == y) -> x /= y
+  rr2 (\x y -> notE `a` (equalsE `a` x `a` y))
+      (\x y -> nequalsE `a` x `a` y),
+  -- not (x /= y) -> x == y
+  rr2 (\x y -> notE `a` (nequalsE `a` x `a` y))
+      (\x y -> equalsE `a` x `a` y),
+  If (Or [rr plusE plusE, rr minusE minusE, rr multE multE]) $ down $ Or [
+    -- 0 + x --> x
+    rr  (\x -> plusE `a` zeroE `a` x)
+        (\x -> x),
+    -- 0 * x --> 0
+    rr  (\x -> multE `a` zeroE `a` x)
+        (\_ -> zeroE),
+    -- 1 * x --> x
+    rr  (\x -> multE `a` oneE `a` x)
+        (\x -> x),
+    -- x - x --> 0
+    rr  (\x -> minusE `a` x `a` x)
+        (\_ -> zeroE),
+    -- x - y + y --> x
+    rr  (\y x -> plusE `a` (minusE `a` x `a` y) `a` y)
+        (\_ x -> x),
+    -- x + y - y --> x
+    rr  (\y x -> minusE `a` (plusE `a` x `a` y) `a` y)
+        (\_ x -> x),
+    -- x + (y - z) --> x + y - z
+    rr  (\x y z -> plusE `a` x `a` (minusE `a` y `a` z))
+        (\x y z -> minusE `a` (plusE `a` x `a` y) `a` z),
+    -- x - (y + z) --> x - y - z
+    rr  (\x y z -> minusE `a` x `a` (plusE `a` y `a` z))
+        (\x y z -> minusE `a` (minusE `a` x `a` y) `a` z),
+    -- x - (y - z) --> x + y - z
+    rr  (\x y z -> minusE `a` x `a` (minusE `a` y `a` z))
+        (\x y z -> minusE `a` (plusE `a` x `a` y) `a` z)
+  ],
+
+  Hard onceRewrites,
+  -- join (fmap f x) --> f =<< x
+  rr (\f x -> joinE `a` (fmapE `a` f `a` x))
+     (\f x -> extE `a` f `a` x),
+  -- (=<<) id --> join
+  rr (extE `a` idE) joinE,
+  -- join --> (=<<) id
+  Hard $
+  rr joinE (extE `a` idE),
+  -- join (return x) --> x
+  rr (\x -> joinE `a` (returnE `a` x))
+     (\x -> x),
+  -- (return . f) =<< m --> fmap f m
+  rr (\f m -> extE `a` (returnE `c` f) `a` m)
+     (\f m -> fmapIE `a` f `a` m),
+  -- (x >>=) . (return .) . f  --> flip (fmap . f) x
+  rr (\f x -> bindE `a` x `c` (compE `a` returnE) `c` f)
+     (\f x -> flipE `a` (fmapIE `c` f) `a` x),
+  -- (>>=) (return f) --> flip id f
+  rr (\f -> bindE `a` (returnE `a` f))
+     (\f -> flipE `a` idE `a` f),
+  -- liftM2 f x --> ap (f `fmap` x)
+  Hard $
+  rr (\f x -> liftM2E `a` f `a` x)
+     (\f x -> apE `a` (fmapIE `a` f `a` x)),
+  -- liftM2 f (return x) --> fmap (f x)
+  rr (\f x -> liftM2E `a` f `a` (returnE `a` x))
+     (\f x -> fmapIE `a` (f `a` x)),
+  -- f `fmap` return x --> return (f x)
+  rr (\f x -> fmapE `a` f `a` (returnE `a` x))
+     (\f x -> returnE `a` (f `a` x)),
+  -- (=<<) . flip (fmap . f) --> flip liftM2 f
+  Hard $
+  rr (\f -> extE `c` flipE `a` (fmapE `c` f))
+     (\f -> flipE `a` liftM2E `a` f),
+  
+  -- (.) -> fmap
+  Hard $ 
+  rr compE fmapE,
+
+  -- map f (zip xs ys) --> zipWith (curry f) xs ys
+  Hard $
+  rr (\f xs ys -> mapE `a` f `a` (zipE `a` xs `a` ys))
+     (\f xs ys -> zipWithE `a` (curryE `a` f) `a` xs `a` ys),
+  -- zipWith (,) --> zip (,)
+  rr (zipWithE `a` commaE) zipE,
+
+  -- all f --> and . map f
+  Hard $
+  rr (\f -> allE `a` f)
+     (\f -> andE `c` mapE `a` f),
+  -- and . map f --> all f
+  rr (\f -> andE `c` mapE `a` f)
+     (\f -> allE `a` f),
+  -- any f --> or . map f
+  Hard $
+  rr (\f -> anyE `a` f)
+     (\f -> orE `c` mapE `a` f),
+  -- or . map f --> any f
+  rr (\f -> orE `c` mapE `a` f)
+     (\f -> anyE `a` f),
+
+  -- return f `ap` x --> fmap f x
+  rr (\f x -> apE `a` (returnE `a` f) `a` x)
+     (\f x -> fmapIE `a` f `a` x),
+  -- ap (f `fmap` x) --> liftM2 f x
+  rr (\f x -> apE `a` (fmapIE `a` f `a` x))
+     (\f x -> liftM2E `a` f `a` x),
+  -- f `ap` x --> (`fmap` x) =<< f
+  Hard $
+  rr (\f x -> apE `a` f `a` x)
+     (\f x -> extE `a` (flipE `a` fmapIE `a` x) `a` f),
+  -- (`fmap` x) =<< f --> f `ap` x
+  rr (\f x -> extE `a` (flipE `a` fmapIE `a` x) `a` f)
+     (\f x -> apE `a` f `a` x),
+  -- (x >>=) . flip (fmap . f) -> liftM2 f x
+  rr (\f x -> bindE `a` x `c` flipE `a` (fmapE `c` f))
+     (\f x -> liftM2E `a` f `a` x),
+
+  -- (f =<< m) x --> f (m x) x
+  rr0 (\f m x -> extE `a` f `a` m `a` x)
+      (\f m x -> f `a` (m `a` x) `a` x),
+  -- (fmap f g x) --> f (g x)
+  rr0 (\f g x -> fmapE `a` f `a` g `a` x)
+      (\f g x -> f `a` (g `a` x)),
+  -- return x y --> y
+  rr  (\y x -> returnE `a` x `a` y)
+      (\y _ -> y),
+  -- liftM2 f g h x --> g x `h` h x
+  rr0 (\f g h x -> liftM2E `a` f `a` g `a` h `a` x)
+      (\f g h x -> f `a` (g `a` x) `a` (h `a` x)),
+  -- ap f id --> join f
+  rr  (\f -> apE `a` f `a` idE)
+      (\f -> joinE `a` f),
+
+  -- (=<<) const q --> flip (>>) q
+  Hard $ -- ??
+  rr (\q p -> extE `a` (constE `a` q) `a` p)
+     (\q p -> seqME `a` p `a` q),
+  -- p >> q --> const q =<< p
+  Hard $
+  rr (\p q -> seqME `a` p `a` q)
+     (\p q -> extE `a` (constE `a` q) `a` p),
+
+  -- experimental support for Control.Arrow stuff 
+  -- (costs quite a bit of performace)
+  -- uncurry ((. g) . (,) . f) --> f *** g
+  rr (\f g -> uncurryE `a` ((flipE `a` compE `a` g) `c` commaE `c` f))
+     (\f g -> crossE `a` f `a` g),
+  -- uncurry ((,) . f) --> first f
+  rr (\f -> uncurryE `a` (commaE `c` f))
+     (\f -> firstE `a` f),
+  -- uncurry ((. g) . (,)) --> second g
+  rr (\g -> uncurryE `a` ((flipE `a` compE `a` g) `c` commaE))
+     (\g -> secondE `a` g),
+  -- I think we need all three of them:
+  -- uncurry (const f) --> f . snd
+  rr (\f -> uncurryE `a` (constE `a` f))
+     (\f -> f `c` sndE),
+  -- uncurry const --> fst
+  rr (uncurryE `a` constE)
+     (fstE),
+  -- uncurry (const . f) --> f . fst
+  rr (\f -> uncurryE `a` (constE `c` f))
+     (\f -> f `c` fstE),
+
+  -- TODO is this the right place?
+  -- [x] --> return x
+  Hard $
+  rr (\x -> consE `a` x `a` nilE)
+     (\x -> returnE `a` x),
+  -- list destructors
+  Hard $ 
+  If (Or [rr consE consE, rr nilE nilE]) $ Or [
+    down $ Or [
+      -- length [] --> 0
+      rr (lengthE `a` nilE)
+         zeroE,
+      -- length (x:xs) --> 1 + length xs
+      rr (\x xs -> lengthE `a` (consE `a` x `a` xs))
+         (\_ xs -> plusE `a` oneE `a` (lengthE `a` xs))
+    ],
+    -- map/fmap elimination
+    down $ Or [
+      -- map f (x:xs) --> f x: map f xs
+      rr (\f x xs -> mapE `a` f `a` (consE `a` x `a` xs))
+         (\f x xs -> consE `a` (f `a` x) `a` (mapE `a` f `a` xs)),
+      -- fmap f (x:xs) --> f x: Fmap f xs
+      rr (\f x xs -> fmapE `a` f `a` (consE `a` x `a` xs))
+         (\f x xs -> consE `a` (f `a` x) `a` (fmapE `a` f `a` xs)),
+      -- map f []     --> []
+      rr (\f -> mapE `a` f `a` nilE)
+         (\_ -> nilE),
+      -- fmap f []     --> []
+      rr (\f -> fmapE `a` f `a` nilE)
+         (\_ -> nilE)
+    ],
+    -- foldr elimination
+    down $ Or [
+      -- foldr f z (x:xs) --> f x (foldr f z xs)
+      rr (\f x xs z -> (foldrE `a` f `a` z) `a` (consE `a` x `a` xs))
+         (\f x xs z -> (f `a` x) `a` (foldrE `a` f `a` z `a` xs)),
+      -- foldr f z [] --> z
+      rr (\f z -> foldrE `a` f `a` z `a` nilE)
+         (\_ z -> z)
+    ],
+    -- foldl elimination
+    down $ Opt (CRR $ assocL ["."]) `Then` Or [
+      -- sum xs --> foldl (+) 0 xs
+      rr (\xs -> sumE `a` xs)
+         (\xs -> foldlE `a` plusE `a` zeroE `a` xs),
+      -- product xs --> foldl (*) 1 xs
+      rr (\xs -> productE `a` xs)
+         (\xs -> foldlE `a` multE `a` oneE `a` xs),
+      -- foldl1 f (x:xs) --> foldl f x xs
+      rr (\f x xs -> foldl1E `a` f `a` (consE `a` x `a` xs))
+         (\f x xs -> foldlE `a` f `a` x `a` xs),
+      -- foldl f z (x:xs) --> foldl f (f z x) xs
+      rr (\f z x xs -> (foldlE `a` f `a` z) `a` (consE `a` x `a` xs))
+         (\f z x xs -> foldlE `a` f `a` (f `a` z `a` x) `a` xs),
+      -- foldl f z [] --> z
+      rr (\f z -> foldlE `a` f `a` z `a` nilE)
+         (\_ z -> z),
+      -- special rule:
+      -- foldl f z [x] --> f z x
+      rr (\f z x -> foldlE `a` f `a` z `a` (returnE `a` x))
+         (\f z x -> f `a` z `a` x),
+      rr (\f z x -> foldlE `a` f `a` z `a` (consE `a` x `a` nilE))
+         (\f z x -> f `a` z `a` x)
+    ] `OrElse` (
+      -- (:) x --> (++) [x]
+      Opt (rr0 (\x -> consE `a` x)
+         (\x -> appendE `a` (consE `a` x `a` nilE))) `Then`
+      -- More special rule: (:) x . (++) ys --> (++) (x:ys)
+      up (rr0 (\x ys -> (consE `a` x) `c` (appendE `a` ys))
+         (\x ys -> appendE `a` (consE `a` x `a` ys)))
+      )
+  ],
+
+  -- Complicated Transformations
+  CRR (collapseLists),
+  up $ Or [CRR (evalUnary unaryBuiltins), CRR (evalBinary binaryBuiltins)],
+  up $ CRR (assoc assocOps),
+  up $ CRR (assocL assocOps),
+  up $ CRR (assocR assocOps),
+  Up (CRR (commutative commutativeOps)) $ down $ Or [CRR $ assocL assocLOps,
+                                                     CRR $ assocR assocROps],
+
+  Hard $ simplifies
+  ] `Then` Opt (up simplifies)
+assocLOps, assocROps, assocOps :: [String]
+assocLOps = ["+", "*", "&&", "||", "max", "min"]
+assocROps = [".", "++"]
+assocOps  = assocLOps ++ assocROps
+
+commutativeOps :: [String]
+commutativeOps = ["*", "+", "==", "/=", "max", "min"]
+
+unaryBuiltins :: [(String,Unary)]
+unaryBuiltins = [
+    ("not",    UA (not    :: Bool -> Bool)),
+    ("negate", UA (negate :: Integer -> Integer)),
+    ("signum", UA (signum :: Integer -> Integer)),
+    ("abs",    UA (abs    :: Integer -> Integer))
+  ]
+
+binaryBuiltins :: [(String,Binary)]
+binaryBuiltins = [
+    ("+",    BA ((+)  :: Integer -> Integer -> Integer)),
+    ("-",    BA ((-)  :: Integer -> Integer -> Integer)),
+    ("*",    BA ((*)  :: Integer -> Integer -> Integer)),
+    ("^",    BA ((^)  :: Integer -> Integer -> Integer)),
+    ("<",    BA ((<)  :: Integer -> Integer -> Bool)),
+    (">",    BA ((>)  :: Integer -> Integer -> Bool)),
+    ("==",   BA ((==) :: Integer -> Integer -> Bool)),
+    ("/=",   BA ((/=) :: Integer -> Integer -> Bool)),
+    ("<=",   BA ((<=) :: Integer -> Integer -> Bool)),
+    (">=",   BA ((>=) :: Integer -> Integer -> Bool)),
+    ("div",  BA (div  :: Integer -> Integer -> Integer)),
+    ("mod",  BA (mod  :: Integer -> Integer -> Integer)),
+    ("max",  BA (max  :: Integer -> Integer -> Integer)),
+    ("min",  BA (min  :: Integer -> Integer -> Integer)),
+    ("&&",   BA ((&&) :: Bool -> Bool -> Bool)),
+    ("||",   BA ((||) :: Bool -> Bool -> Bool))
+  ]
+
diff --git a/Plugin/Pl/Transform.hs b/Plugin/Pl/Transform.hs
new file mode 100644
--- /dev/null
+++ b/Plugin/Pl/Transform.hs
@@ -0,0 +1,119 @@
+{-# OPTIONS -fvia-C -O2 -optc-O3 #-}
+module Plugin.Pl.Transform (
+    transform,
+  ) where
+
+import Plugin.Pl.Common
+import Plugin.Pl.PrettyPrinter
+
+import qualified Data.Map as M
+
+import Data.Graph (stronglyConnComp, flattenSCC, flattenSCCs)
+import Control.Monad.State
+
+{-
+nub :: Ord a => [a] -> [a]
+nub = nub' S.empty where
+  nub' _ [] = []
+  nub' set (x:xs)
+    | x `S.member` set = nub' set xs
+    | otherwise = x: nub' (x `S.insert` set) xs
+-}
+
+occursP :: String -> Pattern -> Bool
+occursP v (PVar v') = v == v'
+occursP v (PTuple p1 p2) = v `occursP` p1 || v `occursP` p2
+occursP v (PCons  p1 p2) = v `occursP` p1 || v `occursP` p2
+
+freeIn :: String -> Expr -> Int
+freeIn v (Var _ v') = fromEnum $ v == v'
+freeIn v (Lambda pat e) = if v `occursP` pat then 0 else freeIn v e
+freeIn v (App e1 e2) = freeIn v e1 + freeIn v e2
+freeIn v (Let ds e') = if v `elem` map declName ds then 0 
+  else freeIn v e' + sum [freeIn v e | Define _ e <- ds]
+
+isFreeIn :: String -> Expr -> Bool
+isFreeIn v e = freeIn v e > 0
+
+tuple :: [Expr] -> Expr
+tuple es  = foldr1 (\x y -> Var Inf "," `App` x `App` y) es
+
+tupleP :: [String] -> Pattern
+tupleP vs = foldr1 PTuple $ PVar `map` vs
+
+dependsOn :: [Decl] -> Decl -> [Decl]
+dependsOn ds d = [d' | d' <- ds, declName d' `isFreeIn` declExpr d]
+  
+unLet :: Expr -> Expr
+unLet (App e1 e2) = App (unLet e1) (unLet e2)
+unLet (Let [] e) = unLet e
+unLet (Let ds e) = unLet $
+  (Lambda (tupleP $ declName `map` dsYes) (Let dsNo e)) `App`
+    (fix' `App` (Lambda (tupleP $ declName `map` dsYes)
+                        (tuple  $ declExpr `map` dsYes)))
+    where
+  comps = stronglyConnComp [(d',d',dependsOn ds d') | d' <- ds]
+  dsYes = flattenSCC $ head comps
+  dsNo = flattenSCCs $ tail comps
+  
+unLet (Lambda v e) = Lambda v (unLet e)
+unLet (Var f x) = Var f x
+
+type Env = M.Map String String
+
+-- It's a pity we still need that for the pointless transformation.
+-- Otherwise a newly created id/const/... could be bound by a lambda
+-- e.g. transform' (\id x -> x) ==> transform' (\id -> id) ==> id
+alphaRename :: Expr -> Expr
+alphaRename e = alpha e `evalState` M.empty where
+  alpha :: Expr -> State Env Expr
+  alpha (Var f v) = do fm <- get; return $ Var f $ maybe v id (M.lookup v fm)
+  alpha (App e1 e2) = liftM2 App (alpha e1) (alpha e2)
+  alpha (Let _ _) = assert False bt
+  alpha (Lambda v e') = inEnv $ liftM2 Lambda (alphaPat v) (alpha e')
+
+  -- act like a reader monad
+  inEnv :: State s a -> State s a
+  inEnv (State f) = State $ \s -> (fst $ f s, s)
+
+  alphaPat (PVar v) = do
+    fm <- get
+    let v' = "$" ++ show (M.size fm)
+    put $ M.insert v v' fm
+    return $ PVar v'
+  alphaPat (PTuple p1 p2) = liftM2 PTuple (alphaPat p1) (alphaPat p2)
+  alphaPat (PCons p1 p2) = liftM2 PCons (alphaPat p1) (alphaPat p2)
+
+
+transform :: Expr -> Expr
+transform = transform' . alphaRename . unLet
+
+transform' :: Expr -> Expr
+transform' (Let {}) = assert False bt
+transform' (Var f v) = Var f v
+transform' (App e1 e2) = App (transform' e1) (transform' e2)
+transform' (Lambda (PTuple p1 p2) e) 
+  = transform' $ Lambda (PVar "z") $ 
+      (Lambda p1 $ Lambda p2 $ e) `App` f `App` s where
+    f = Var Pref "fst" `App` Var Pref "z"
+    s = Var Pref "snd" `App` Var Pref "z"
+transform' (Lambda (PCons p1 p2) e) 
+  = transform' $ Lambda (PVar "z") $ 
+      (Lambda p1 $ Lambda p2 $ e) `App` f `App` s where
+    f = Var Pref "head" `App` Var Pref "z"
+    s = Var Pref "tail" `App` Var Pref "z"
+transform' (Lambda (PVar v) e) = transform' $ getRidOfV e where
+  getRidOfV (Var f v') | v == v'   = id'
+                       | otherwise = const' `App` Var f v'
+  getRidOfV l@(Lambda pat _) = assert (not $ v `occursP` pat) $ 
+    getRidOfV $ transform' l
+  getRidOfV (Let {}) = assert False bt
+  getRidOfV e'@(App e1 e2) 
+    | fr1 && fr2 = scomb `App` getRidOfV e1 `App` getRidOfV e2
+    | fr1 = flip' `App` getRidOfV e1 `App` e2
+    | Var _ v' <- e2, v' == v = e1
+    | fr2 = comp `App` e1 `App` getRidOfV e2
+    | True = const' `App` e'
+    where
+      fr1 = v `isFreeIn` e1
+      fr2 = v `isFreeIn` e2
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,10 @@
+Pointfree refactoring tool
+==========================
+
+Stand-alone command-line version of the point-less plugin for lambdabot. Detailed information about the use of this tool is available at http://haskell.org/haskellwiki/Pointfree.
+
+Integration with GHCi: Make sure that the directory containing the pointfree executable is in your PATH environment variable and add the following line to your GHCi configuration file:
+
+:def pf \str -> return $ ":! pointfree \"" ++ str ++ "\""
+
+Or modify the line to point directly to the executable. Invoke pointfree with commands like :pf \x y -> x + y
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+#!/usr/bin/env runhaskell
+
+import Distribution.Simple
+main = defaultMain
diff --git a/pointfree.cabal b/pointfree.cabal
new file mode 100644
--- /dev/null
+++ b/pointfree.cabal
@@ -0,0 +1,15 @@
+name:                pointfree
+version:             1.0
+synopsis:            Pointfree refactoring tool
+description:         Stand-alone command-line version of the point-less plugin for lambdabot.
+license:             OtherLicense
+license-file:        LICENSE
+author:              Thomas Jäger
+homepage:            http://haskell.org/haskellwiki/Pointfree
+category:            Tool
+build-depends:       base, parsec, mtl
+
+executable:          pointfree
+main-is:             Main.hs
+ghc-options:         -Wall -O -funbox-strict-fields -fglasgow-exts
+
diff --git a/test/Makefile b/test/Makefile
new file mode 100644
--- /dev/null
+++ b/test/Makefile
@@ -0,0 +1,9 @@
+all:	
+	#ghc -package HUnit -i.. -O --make -fglasgow-exts -funfolding-use-threshold -o Test Test.hs
+	ghc -Wall -cpp -funbox-strict-fields -i.. --make -O -fglasgow-exts -o Test Test.hs
+
+tests:	all
+	./Test tests
+
+clean:
+	rm *.o *.hi
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,261 @@
+module Main where
+
+#define READLINE
+#if __GLASGOW_HASKELL__ > 602
+import Test.HUnit
+import Test.QuickCheck hiding (test)
+#else
+import HUnit
+import Debug.QuickCheck hiding (test)
+#endif
+
+import Plugin.Pl.Common
+import Plugin.Pl.Transform
+import Plugin.Pl.Parser
+import Plugin.Pl.PrettyPrinter
+import Plugin.Pl.Optimize
+
+import Data.List ((\\))
+import Data.Char (isSpace)
+
+import Control.Monad.Error
+
+import System.IO (hSetBuffering, stdout, BufferMode(NoBuffering))
+import System.Environment (getArgs)
+
+#ifdef READLINE
+import System.Console.Readline (readline, addHistory, initialize)
+#endif
+
+import Debug.Trace
+
+instance Arbitrary Expr where
+  arbitrary = sized $ \size -> frequency $ zipWith (,) [1,size,size]
+    [arbVar,
+     liftM2 Lambda arbPat arbitrary,
+     let se = resize (size `div` 2) arbitrary in liftM2 App se se ] 
+  coarbitrary = error "Expr.coarbitrary"
+
+arbVar :: Gen Expr
+arbVar = oneof [(Var Pref . return) `fmap` choose ('a','z'), 
+                (Var Inf .  return) `fmap` elements (opchars\\"=")]
+
+arbPat :: Gen Pattern
+arbPat = sized $ \size -> 
+  let
+    spat = resize (size `div` 5) arbPat
+  in
+    frequency $ zipWith (,) [1,size,size] [
+      (PVar . return) `fmap` choose ('a','z'),
+      liftM2 PTuple spat spat,
+      liftM2 PCons  spat spat]
+
+propRoundTrip :: Expr -> Bool
+propRoundTrip e = Right (TLE e) == parsePF (show e)
+
+-- hacking qc2 functionality (?) in here
+propRoundTrip' :: Expr -> Property
+propRoundTrip' e = not (propRoundTrip e) ==> trace (show $ findMin e) False
+    where
+  findMin e' = case filter (not . propRoundTrip) $ subExpr e' of
+    [] -> e'
+    (x:_) -> findMin x
+
+propMonotonic1 :: Expr -> Expr -> Expr -> Bool
+propMonotonic1 e e1 e2 = App e e1 `compare` App e e2 == e1 `compare` e2
+
+propMonotonic2 :: Expr -> Expr -> Expr -> Bool
+propMonotonic2 e e1 e2 = App e1 e `compare` App e2 e == e1 `compare` e2
+
+subExpr :: Expr -> [Expr]
+subExpr (Var _ _) = []
+subExpr (Lambda v e) = [e] ++ Lambda v `map` subExpr e
+subExpr (App e1 e2) = [e1, e2] 
+  ++ App e1 `map` subExpr e2 ++ (`App` e2) `map` subExpr e1
+subExpr (Let {}) = bt
+
+sizeTest :: IO ()
+sizeTest = quickCheck $ \e -> collect (sizeExpr e) (propRoundTrip e)
+
+quick :: Config
+quick = Config
+  { configMaxTest = 100
+  , configMaxFail = 1000
+  , configSize    = const 40
+  , configEvery   = \n _ -> let sh = show n in sh ++ [ '\b' | _ <- sh ]
+  }
+
+myTest :: IO ()
+myTest = check quick propRoundTrip'
+
+qcTests :: IO ()
+qcTests = do
+  quickCheck propRoundTrip
+  quickCheck propMonotonic1
+  quickCheck propMonotonic2
+
+pf :: String -> IO ()
+pf inp = case parsePF inp of
+  Right d -> do 
+    putStrLn "Your expression:"
+    print d
+    putStrLn "Transformed to pointfree style:"
+    let d' = mapTopLevel transform d
+    print $ d'
+    putStrLn "Optimized expression:"
+    mapM_ print $ mapTopLevel' optimize d'
+  Left err -> putStrLn $ err
+
+mapTopLevel' :: Functor f => (Expr -> f Expr) -> TopLevel -> f TopLevel
+mapTopLevel' f tl = case getExpr tl of (e, c) -> fmap c $ f e
+
+pf' :: String -> IO ()
+pf' = putStrLn . (id ||| show) . parsePF
+
+-- NB: this is a special case of (import Control.Monad.Reader)
+-- ap :: m (a -> b) -> m a -> m b
+s :: (t -> a -> b) -> (t -> a) -> t -> b
+s f g x = f x $ g x  
+
+unitTest :: String -> [String] -> Test
+unitTest inp out = TestCase $ do
+  d <- case parsePF inp of
+    Right x -> return x
+    Left err -> fail $ "Parse error on input " ++ inp ++ ": " ++ err
+  let d' = mapTopLevel (last . optimize . transform) d
+  foldr1 mplus [assertEqual (inp++" failed.") o (show d') | o <- out]
+
+unitTests :: Test
+unitTests = TestList [
+  unitTest "foldr (++) []" ["join"],
+  unitTest "flip flip [] . ((:) .)" ["(return .)"],
+  unitTest "\\x -> x - 2" ["subtract 2"],
+  unitTest "\\(x,_) (y,_) -> x == y" ["(. fst) . (==) . fst"],
+  unitTest "\\x y z -> return x >>= \\x' -> return y >>= \\y' -> return z >>= \\z' -> f x' y' z'" ["f"],
+  unitTest "let (x,y) = (1,2) in y" ["2"],
+  unitTest "fix . const" ["id"],
+  unitTest "all f . map g" ["all (f . g)"],
+  unitTest "any f . map g" ["any (f . g)"],
+  unitTest "liftM2 ($)" ["ap"],
+  unitTest "\\f -> f x" ["($ x)"],
+  unitTest "flip (-)" ["subtract"],
+  unitTest "\\xs -> [f x | x <- xs, p x]" ["map f . filter p"],
+  unitTest "all id" ["and"],
+  unitTest "any id" ["or"],
+  unitTest "and . map f" ["all f"],
+  unitTest "or . map f" ["any f"],
+  unitTest "return ()" ["return ()"],
+  unitTest "f (fix f)" ["fix f"],
+  unitTest "concat ([concat (map h (k a))])" ["h =<< k a"],
+  unitTest "uncurry (const f)" ["f . snd"],
+  unitTest "uncurry const" ["fst"],
+  unitTest "uncurry (const . f)" ["f . fst"],
+  unitTest "\\a b -> a >>= \\x -> b >>= \\y -> return (x,y)" ["liftM2 (,)"],
+  unitTest "\\b a -> a >>= \\x -> b >>= \\y -> return (x,y)" ["flip liftM2 (,)"],
+  unitTest "curry snd" ["const id"],
+  unitTest "\\x -> return x y" ["const y"],
+  unitTest "\\x -> f x x" ["join f"],
+  unitTest "join (+) 1" ["2"],
+  unitTest "fmap f g x" ["f (g x)"],
+  unitTest "liftM2 (+) f g 0" ["f 0 + g 0", "g 0 + f 0"],
+  unitTest "return 1 x" ["x"],
+  unitTest "f =<< return x" ["f x"],
+  unitTest "(=<<) id" ["join"],
+  unitTest "zipWith (,)" ["zip"],
+  unitTest "map fst . zip [1..]" ["zipWith const [1..]"],
+  unitTest "curry . uncurry" ["id"],
+  unitTest "uncurry . curry" ["id"],
+  unitTest "curry fst" ["const"],
+  unitTest "return x >> y" ["y"],
+  -- What were they smoking when they decided >> should be infixl
+  unitTest "a >>= \\_ -> b >>= \\_ -> return $ const (1 + 2) $ a + b" ["a >> (b >> return 3)"],
+  unitTest "foo = m >>= \\x -> return 1" ["foo = m >> return 1"],
+  unitTest "foo m = m >>= \\x -> return 1" ["foo = (>> return 1)"],
+  unitTest "return (+) `ap` return 1 `ap` return 2" ["return 3"],
+  unitTest "liftM2 (+) (return 1) (return 2)" ["return 3"],
+  unitTest "(. ((return .) . (+))) . (>>=)" ["flip (fmap . (+))"],
+  unitTest "\\a b -> a >>= \\x -> b >>= \\y -> return $ x + y" ["liftM2 (+)"],
+  unitTest "ap (flip const . f)" ["id"],
+  unitTest "uncurry (flip (const . flip (,) (snd t))) . ap (,) id" ["flip (,) (snd t)"],
+  unitTest "foo = (1, fst foo)" ["foo = (1, 1)"],
+  unitTest "foo = (snd foo, 1)" ["foo = (1, 1)"],
+  unitTest "map (+1) [1,2,3]" ["[2, 3, 4]"],
+  unitTest "snd . (,) (\\x -> x*x)" ["id"],
+  unitTest "return x >>= f" ["f x"],
+  unitTest "m >>= return" ["m"],
+  unitTest "m >>= \\x -> f x >>= g" ["m >>= f >>= g", "g =<< f =<< m"],
+  unitTest "\\x -> 1:2:3:4:x" ["([1, 2, 3, 4] ++)"],
+  unitTest "\\(x:xs) -> x"  ["head"],
+  unitTest "\\(x:xs) -> xs" ["tail"],
+  unitTest "\\(x,y)  -> x"  ["fst"],
+  unitTest "\\(x,y)  -> y"  ["snd"],
+  unitTest "\\x -> x" ["id"],
+  unitTest "\\x y -> x" ["const"],
+  unitTest "\\f x y -> f y x" ["flip"],
+  unitTest "t f g x = f x (g x)" ["t = ap"],
+  unitTest "(+2).(+3).(+4)" ["(9 +)"],
+  unitTest "head $ fix (x:)" ["x"],
+  unitTest "head $ tail $ let xs = x:ys; ys = y:ys in xs" ["y"],
+  unitTest "head $ tail $ let ys = y:ys in let xs = x:ys in xs" ["y"],
+  unitTest "2+3*4-3*3" ["5"],
+  unitTest "foldr (+) x [1,2,3,4]" ["10 + x", "x + 10"],
+  unitTest "foldl (+) x [1,2,3,4]" ["10 + x", "x + 10"],
+  unitTest "head $ fst (x:xs, y:ys)" ["x"],
+  unitTest "snd $ (,) 2 3" ["3"],
+  unitTest "\\id x -> id" ["const"],
+  unitTest "\\y -> let f x = foo x; g = f in g y" ["foo"],
+  unitTest "neq x y = not $ x == y" ["neq = (/=)"],
+  unitTest "not (x /= y)" ["x == y"],
+  unitTest "\\x x -> x" ["const id"],
+  unitTest "\\(x, x) -> x" ["snd"],
+  unitTest "not $ not 4" ["4"],
+  unitTest "\\xs -> foldl (+) 0 (1:2:xs)" ["foldl (+) 3"],
+  unitTest "\\x -> foldr (+) x [0,1,2,3]" ["(6 +)"],
+  unitTest "foldr (+) 0 [x,y,z]" ["x + y + z"],
+  unitTest "foldl (*) 0 [x,y,z]" ["0"],
+  unitTest "length \"abcdefg\"" ["7"],
+  unitTest "ap (f x . fst) snd" ["uncurry (f x)"],
+  unitTest "sum [1,2,3,x]" ["6 + x", "x + 6"],
+  unitTest "p x = product [1,2,3,x]" ["p = (6 *)"],
+  unitTest "(concat .) . map" ["(=<<)"],
+  unitTest "let f ((a,b),(c,d)) = a + b + c + d in f ((1,2),(3,4))" ["10"],
+  unitTest "let x = const 3 y; y = const 4 x in x + y" ["7"] -- yay!
+  ]
+
+main :: IO ()
+main = do 
+  hSetBuffering stdout NoBuffering
+  args <- getArgs
+  case args of
+    ("tests":_) -> doTests
+    xs          -> do 
+        mapM_ pf xs
+#ifdef READLINE
+        initialize
+#endif
+        pfloop
+
+
+pfloop :: IO ()
+pfloop = do
+#ifdef READLINE 
+  line' <- readline "pointless> "
+#else
+  line' <- Just `fmap` getLine
+#endif
+  case line' of
+    Just line 
+      | all isSpace line -> pfloop
+      | otherwise        -> do
+#ifdef READLINE
+          addHistory line
+#endif
+          pf line
+          pfloop
+    Nothing   -> putStrLn "Bye."
+
+doTests :: IO ()
+doTests = do
+  runTestTT unitTests
+--  qcTests 
+  return ()