content: {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  --
  -- | This marvellous module contributed by Thomas J\344ger
  --
  module Plugin.Pl.Rules (RewriteRule(..), rules, fire) where
  
  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 --> x
    rr  (\y x -> returnE `a` x `a` y)
        (\_ x -> x),
    -- 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))
    ]
  
  