content: -- Lazy evaluation machine
  --
  -- LamMachine is a variant of the machine described in
  -- "Deriving a Lazy Abstract Machine" (1997) by Peter Sestoft 
  
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeSynonymInstances #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE BangPatterns #-}
  
  --module LamMachineV2 where
  
  import Data.List
  import Data.Word
  import Data.Int
  import Data.Monoid
  import Data.Maybe
  import Data.Bits
  import Data.String
  import qualified Data.Vector as PV
  import qualified Data.Vector.Mutable as V
  import qualified Data.Vector.Unboxed.Mutable as UV
  import qualified Data.Vector.Unboxed as PUV
  import Control.Arrow hiding ((<+>))
  import Control.Category hiding ((.), id)
  import Control.Monad
  import Control.Monad.Writer
  import Control.Monad.ST
  import Debug.Trace
  import qualified Text.Show.Pretty as P
  import System.Environment
  
  import LambdaCube.Compiler.Pretty
  
  -----------------------------------------
  
  class HasLen v where
      len :: v -> Int
  
  class (HasLen v, Monad m) => VecLike v m where
      type VElem v
      new     :: Int -> m v
      append  :: v -> (Int, [VElem v]) -> m v
      read_   :: v -> Int -> m (VElem v)
      freezedRead :: v -> m (Int -> VElem v)
      write   :: v -> Int -> VElem v -> m v
      modify  :: v -> Int -> (VElem v -> VElem v) -> m v
      vToList :: v -> m [VElem v]
  
  -----------------
  
  data Vec s a = Vec !Int !(V.STVector s a)
  
  instance HasLen (Vec s a) where
      len (Vec n _) = n
  
  instance VecLike (Vec s a) (ST s) where
      type VElem (Vec s a) = a
  
      new n | n < 0 = error $ "new: " ++ show n
      new n = Vec 0 <$> V.unsafeNew n
  
      append (Vec n v@(V.length -> m)) (k, xs) = do
          let !nk = n + k
          v' <- if m >= nk then return v else V.unsafeGrow v (2 * nk - m)
          zipWithM_ (V.unsafeWrite v') [n..] xs
          return $ Vec nk v'
  
      read_ (Vec _ v) i = V.unsafeRead v i
  
      freezedRead (Vec _ v) = PV.unsafeFreeze v <&> PV.unsafeIndex
  
      write x@(Vec _ v) i a = V.unsafeWrite v i a >> return x
  
      modify x@(Vec _ v) i a = V.unsafeModify v a i >> return x
  
      vToList (Vec n v) = mapM (V.unsafeRead v) [0..n-1]
  
  --------------------------------------------------------------------------- data structures
  
  data Lit
      = LInt   !Int
      | LChar  !Char
      | LFloat !Double
      deriving Eq
  
  data Exp
      = Var_ !DB
      | Lam  VarInfo Exp
      | App  Exp Exp
      | Con  ConIndex [Exp]
      | Case CaseInf Exp [Exp]
      | Lit  !Lit
      | Delta !Op [Exp]
      deriving (Show)
  
  pattern Var i  = Var_ (Pos i)
  pattern Free i = Var_ (Neg i)
  
  type DB = Int
  type ConIndex = (ConInfo, Int)
  type CaseInf = (CaseInfo, [Int])
  
  data Op
      = Round | ISqrt
      | Add | Sub | Mod | LessEq | EqInt
      | YOp | SeqOp
      deriving (Eq, Show)
  
  pattern Op1 op x    = Delta op [x]
  pattern Op2 op x y  = Delta op [x, y]
  
  pattern Y s a       = Op1 YOp (Lam s a)
  pattern Seq a b     = Op2 SeqOp a b
  pattern Int i       = Lit (LInt i)
  
  infixl 4 `App`
  
  data EnvPiece
      = EApp !EExp
      | ECase CaseInf ![EExp]
      | EDelta !Op ![Lit] ![EExp]
      | Update_ !DB
      deriving (Eq, Show)
  
  data HNF
      = HLam VarInfo !EExp
      | HCon ConIndex ![DB]
      | HLit !Lit
      | HVar_ !DB
      | HPiece !EnvPiece !HNF
      | HLet !Int ![EExp] !HNF
      deriving (Eq, Show)
  
  zipWith' f (x: xs) (y: ys) = f x y !: zipWith' f xs ys
  zipWith' _ _ _ = []
  {-
  f <$!> [] = []
  f <$!> (a: as) = f a :! (f <$!> as)
  -}
  a !: as = a `seq` as `seq` (a: as)
  
  [] ++! xs = xs
  (x: xs) ++! ys = x !: (xs ++! ys)
  
  pattern Update i = Update_ (Pos i)
  
  pattern HVar i  = HVar_ (Pos i)
  pattern HFree i = HVar_ (Neg i)
  
  pattern Neg i <- (getNeg -> Just i)
    where Neg i =  negate i - 1
  
  getNeg i | i < 0 = Just $ negate i - 1
  getNeg _ = Nothing
  
  pattern Pos :: Int -> Int
  pattern Pos i <- (getPos -> Just i)
    where Pos i =  i
  
  getPos i | i >= 0 = Just i
  getPos _ = Nothing
  
  data EExp
      = ExpC !Int ![EExp] !HNF
      | ErrExp
      deriving (Eq, Show)
  
  pattern SExp :: HNF -> EExp
  pattern SExp e <- ExpC 0 _ e
    where SExp = ExpC 0 []
  
  pattern ERef r = SExp (HVar_ r)
  
  pattern LExp n ls v = ExpC n ls (HVar_ v)
  
  -------------------------------------- max db index
  
  newtype MDB = MDB {getMDB :: Int}
      deriving (Eq, Show)
  
  instance Monoid MDB where
      mempty = MDB 0
  #if !MIN_VERSION_base(4,11,0)
      MDB n `mappend` MDB m = MDB $ n `max` m
  #else
  instance Semigroup MDB where
      MDB n <> MDB m = MDB $ n `max` m
  #endif
  
  ------------------------------------- rearrange De Bruijn indices
  
  class Rearrange a where
      rearrange :: (Int -> Int) -> Int -> a -> a
  
  instance Rearrange a => Rearrange [a] where
      rearrange f i xs = rearrange f i <$!> xs
  
  instance Rearrange EExp
    where
      rearrange _ _ ErrExp = ErrExp
      rearrange f l_ (ExpC n ls e) = ExpC n (rearrange f l ls) $ rearrange f l e
        where
          l = l_ + n
  
  instance Rearrange EnvPiece
    where
      rearrange f l = \case
          EApp e          -> EApp $ rearrange f l e
          ECase is@(_, i) es -> ECase is $ zipWith' (rearrange f . (l +)) i es
          EDelta o ls es  -> EDelta o ls $ rearrange f l es
          Update_ i       -> Update_ $ atL f l i
  
  instance Rearrange HNF
    where
      rearrange f l = \case
          HLam i e    -> HLam i $ rearrange f (l+1) e
          HCon i ns   -> HCon i $ atL f l <$!> ns
          HVar_ i     -> HVar_ $ atL f l i
          HPiece p e  -> HPiece (rearrange f l p) $ rearrange f l e
          x@HLit{}    -> x
  
  instance Rearrange Exp
    where
      rearrange f l = \case
          Var_ i      -> Var_ $ atL f l i
          Lam i e     -> Lam i $ rearrange f (l+1) e
          App e e'    -> App (rearrange f l e) (rearrange f l e')
          Con i es    -> Con i $ rearrange f l es
          Case is@(_, i) e es -> Case is (rearrange f l e) $ zipWith (rearrange f . (l +)) i es
          Delta d es  -> Delta d $ rearrange f l es
          x           -> x
  
  ----------
  
  rearrange' f = rearrange f 0
  
  up _ 0 = id
  up l n = rearrange (+n) l
  
  up' = up 0
  
  -----------------------------------------
  
  (<&>) = flip (<$>)
  
  addI f l i | i < l = return 
  addI f l i = f (i-l)
  
  atL f l i | i < l = i
  atL f l i = aadd l $ f (i-l)
  
  aadd l (Pos i) = l + i
  aadd l i = i
  
  class FVs a where
      fv :: Monad m => (Int -> b -> m b) -> Int -> a -> b -> m b
      sfv :: (Int -> Int) -> Int -> a -> a
      open :: Int -> Int -> a -> a
  
  instance FVs a => FVs [a] where
      fv l f [] = return
      fv l f (x: xs) = fv l f x >=> fv l f xs
  
      sfv l f xs = sfv l f <$!> xs
  
      open l f xs = open l f <$!> xs
  
  instance (FVs a, FVs b) => FVs (a, b) where
      fv l f (a, b) = fv l f a >=> fv l f b
  
      sfv f l (a, b) = (sfv f l a, sfv f l b)
  
      open f i (a, b) = (open f i a, open f i b)
  
  instance FVs EExp where
      fv f l ErrExp = return
      fv f l (ExpC n ls e) = fv f l' ls >=> fv f l' e
        where l' = l + n
  
      sfv f l ErrExp = ErrExp
      sfv f l (ExpC n ls e) = ExpC n (sfv f l' ls) (sfv f l' e)
        where l' = l + n
  
      open f l ErrExp = ErrExp
      open f l (ExpC n ls e) = ExpC n (open f l' ls) (open f l' e)
        where l' = l + n
  
  instance FVs EnvPiece where
  
      fv f l = \case
          EApp e          -> fv f l e
          ECase (_, i) es -> foldr (>=>) return $ zipWith (fv f . (l +)) i es
          EDelta o ls es  -> fv f l es
          Update_ i       -> addI f l i
  
      sfv f l = \case
          EApp e          -> EApp $ sfv f l e
          ECase is@(_, i) es -> ECase is $ zipWith' (sfv f . (l +)) i es
          EDelta o ls es  -> EDelta o ls $ sfv f l es
          Update_ i       -> Update_ $ atL f l i
  
      open f l = \case
          EApp e          -> EApp $ open f l e
          ECase is@(_, i) es -> ECase is $ zipWith' (open f . (l +)) i es
          EDelta o ls es  -> EDelta o ls $ open f l es
          Update_ i       -> Update_ $ openL f l i
  
  instance FVs HNF where
  
      fv f l = \case
          HLam i e    -> fv f (l+1) e
          HCon i ns   -> foldr (>=>) return $ addI f l <$!> ns
          HVar_ i     -> addI f l i
          HPiece p e  -> fv f l p >=> fv f l e
          HLit{}      -> return
  
      sfv f l = \case
          HLam i e    -> HLam i $ sfv f (l+1) e
          HCon i ns   -> HCon i $ atL f l <$!> ns
          HVar_ i     -> HVar_ $ atL f l i
          HPiece p e  -> HPiece (sfv f l p) $ sfv f l e
          x@HLit{}    -> x
  
      open f l = \case
          HLam i e    -> HLam i $ open f (l+1) e
          HCon i ns   -> HCon i $ openL f l <$!> ns
          HVar_ i     -> HVar_ $ openL f l i
          HPiece p e  -> HPiece (open f l p) $ open f l e
          x@HLit{}    -> x
  
  openL f l (Neg i) | i >= f = i - f + l
  openL f l i = i
  
  -----------------------------------------
  
  type GCConfig = (Int, Int, Int, Int)
  
  defaultConfig = (20000, 10000, max 0 $ 10000 - 20, 20)
  
  hnf = hnf_ defaultConfig
  
  hnf_ gcconfig e_
       = open ii 0 $ steps gcconfig -- $ join (trace . ("\n------------\n" ++) . ppShow)
          $ preprocess e
    where
      (e, MDB ii) = runWriter $ closeExp ii 0 e_
  
      closeExp f l = \case
          Free i      -> tell (MDB $ i + 1) >> return (Free i)
          Var i       -> return $ if i >= l then Free $ i - l + f else Var i
          Lam i e     -> Lam i <$> closeExp f (l+1) e
          App e e'    -> App <$> closeExp f l e <*> closeExp f l e'
          Con i es    -> Con i <$> traverse (closeExp f l) es
          Case is@(_, i) e es -> Case is <$> closeExp f l e <*> zipWithM (\ns -> closeExp f (l + ns)) i es
          Delta d es  -> Delta d <$> traverse (closeExp f l) es
          x           -> return x
  
  preprocess :: Exp -> EExp
  preprocess = \case
      Lit l       -> SExp $ HLit l
      Var_ i      -> SExp $ HVar_ i
      Lam i e     -> SExp $ HLam i $ hnf e
      Y s e       -> ExpC (n+1) (ls ++ [({-s,-} SExp f)]) (HVar n)
        where ExpC n ls f = hnf e
      Delta d (e: es) -> add' (EDelta d [] $ preprocess <$!> es) $ preprocess e
      App e f         -> add' (EApp $ letify "u" $ preprocess f) $ preprocess e
      Case is@(_, i) e es -> add' (ECase is $ zipWith' (\ns -> if ns == 0 then preprocess else hnf) i es) $ preprocess e
      Con i es        -> foldl (app2 f) (SExp $ HCon i mempty) $ letify "r" . preprocess <$> es
        where
          f (HCon i vs) (HVar_ v) = HCon i $ vs ++ [v]
    where
      add' p (ExpC n ls e) = ExpC n ls $ HPiece (up' n p) e
  
      app2 g e@(ExpC n ls f) e'@(ExpC n' ls' f') = ExpC (n+n') (up n n' ls ++! up 0 n ls') f''
        where
          f'' = g (up n n' f) (up 0 n f')
  
      letify :: Info String -> EExp -> EExp
      letify s e@LExp{} = e
      letify s (ExpC n ls e) = LExp (n+1) (up n 1 $ ls <> [({-s,-} SExp e)]) n
  
  -------------------------------------------------
  
  nogc_mark = -1
  
  type Vecs s = (Vec s EExp, Vec s EExp)
  
  steps :: GCConfig -> EExp -> EExp
  steps (gc1, gc2, gc3, gc4) e = runST (init e)
    where
      init :: forall s . EExp -> ST s EExp
      init (ExpC n ls e) = do
          v1 <- new n
          v2 <- new gc4
          v1' <- append v1 (n, ls)
          trace "-----" $ vsteps (n, 0, []) (v1', v2) [] e
        where
          vsteps :: (Int, Int, [Int]) -> Vecs s -> [EnvPiece] -> HNF -> ST s EExp
  
          vsteps sn ls ps (HPiece p e) = vsteps sn ls (p: ps) e
  
          vsteps sn ls@(v1@(len -> n), v2@(len -> n')) ps e@(HVar_ i)
              | i < 0 || i >= n + n' = final sn ls ps e
              | i < n = do
                  (adjust (n + n') -> e) <- read_ v1 i
                  if isHNF e
                    then addLets sn ls ps e
                    else write v1 i ErrExp >>= \v1 -> addLets sn (v1, v2) (Update i: ps) e
              | i < n + n' = do
                  (adjust (n + n') -> e) <- read_ v2 (i-n)
                  if isHNF e
                    then addLets sn ls ps e
                    else write v2 (i-n) ErrExp >>= \v2 -> addLets sn (v1, v2) (Update i: ps) e
          vsteps sn@(gc1, gc2, argh) ls@(v1@(len -> n), v2@(len -> n')) (p: ps) e
              | Update i <- p = if i < n
                  then do
                      v1' <- write v1 i $ SExp e
                      vsteps (gc1, gc2, i: argh) (v1', v2) ps e
                  else do
                      v2' <- write v2 (i - n) $ SExp e
                      vsteps sn (v1, v2') ps e
              | Just x <- dx (n + n') p e = addLets sn ls ps x
          vsteps sn ls ps e = final sn ls ps e
  
          final sn v ps e = majorGC sn v ps e $ \sn' (v1@(len -> n), _) ps' e' -> do
              ls' <- vToList v1
              return $ ExpC n ls' $ foldl (flip HPiece) e' ps'
  
          dx len (EApp (LExp n ls z)) (HLam i (ExpC n' ls' e))
              = Just $ ExpC (n + n') (rearrange' upFun ls ++! rearrange' fu ls') $ rearrange' fu e
                where
                  z' = if z < 0 then z else if z < n then z + len else z - n
                  fu i | i <  n'   = i + n + len
                       | i == n'   = z'
                       | otherwise = i - (1 + n')
  
                  upFun i = if i < n then i + len else i - n
  
          dx len (ECase _ cs) (HCon (_, i) vs@(length -> n))
              | nn == 0 = Just e
              | otherwise = Just $ adjust' (\i -> if i < n' then i + len else if i < nn then vs !! (nn - 1 - i) else i - nn) e
            where
              !nn = n + n'
              !e@(ExpC n' _ _) = cs !! i
          dx len (EDelta SeqOp [] [f]) x
              | isHNF' x = Just $ adjust len f
              | otherwise = Nothing
          dx len (EDelta o lits (ExpC n ls f: fs)) (HLit l)
              = Just $ adjust len $ ExpC n ls $ HPiece (EDelta o (l: lits) fs) f
          dx len (EDelta o lits []) (HLit l)
              = Just $ SExp $ delta o $ l: lits
          dx _ _ _ = Nothing
  
          addLets sn ls ps (SExp e) = vsteps sn ls ps e
          addLets sn ls@(v1, v2) ps (ExpC n' xs e) = do
              v2' <- append v2 (n', xs)
              mkGC sn (v1, v2') ps e
  
          mkGC sn@(mg, sn_, xx) v@(len -> n, len -> n') ps e
              | n' < gc2          = vsteps (mg, sn_ + 1, xx) v ps e
              | n + n' - mg < gc1 = minorGC sn v ps e
              | otherwise         = majorGC sn v ps e vsteps
  
          adjust _ e@SExp{} = e
          adjust n e@(ExpC n' _ _) = adjust' (\i -> if i < n' then i + n else i - n') e
  
          adjust' fu (ExpC n' xs e) = ExpC n' (rearrange' fu xs) (rearrange' fu e)
  
          minorGC :: (Int, Int, [Int]) -> Vecs s -> [EnvPiece] -> HNF -> ST s EExp
          minorGC (mg, sn, argh) (v1@(len -> n), v2@(len -> n')) ps e = do
            fv2 <- freezedRead v2
            genericGC_ fv2 n n' $ \mark co -> do
              let cc (xx, acc) i = do
                      e <- read_ v1 i
                      (same, xx') <- fv (\i (same, b) -> (,) False <$> mark i b) n e (True, xx)
                      return (xx', if same then acc else i: acc)
  
              let !la = length argh
              (xx', argh') <- foldM cc (0, []) argh
              let !la' = length argh'
              s <- fv mark n (ps, e) xx'
              append v1 (s, []) >>= \vv -> co vv $ \fvi v1'@(len -> n'') ->
                  trace ("minor gc: " ++ show (n - la) ++ " + " ++ show (la - la') ++ " + " ++ show la' ++ " + " ++ show xx' ++ " + " ++ show (n' - xx') ++ " - " ++ show (n + n' - n'')) $ do
                      v1'' <- foldM (\v i -> modify v i $ sfv fvi n) v1' argh'
                      v2' <- new gc3
                      vsteps (mg, sn + 1, []) (v1'', v2') (sfv fvi n ps) (sfv fvi n e)
  
          majorGC :: (Int, Int, [Int]) -> Vecs s -> [EnvPiece] -> HNF
                  -> ((Int, Int, [Int]) -> Vecs s -> [EnvPiece] -> HNF -> ST s e)
                  -> ST s e
          majorGC (_, sn, argh) v@(v1@(len -> n), v2@(len -> n')) ps e cont = do
            fv1 <- freezedRead v1
            fv2 <- freezedRead v2
            let read2 i = if i < n then fv1 i else fv2 (i - n)
            genericGC_ read2 0 (n + n') $ \mark co -> do
              s <- fv mark 0 (ps, e) 0
              new s >>= \v -> append v (s, []) >>= \vv -> co vv $ 
                \fvi v1'@(len -> n'') ->
                  trace ("major gc: " ++ show n ++ " + " ++ show n' ++ " - " ++ show (n + n' - n'')) $ do
                      v2' <- new gc3
                      cont (n'', sn + 1, []) (v1', v2') (sfv fvi 0 ps) (sfv fvi 0 e)
  
          genericGC_ read_ n len cont = do
              vi <- UV.replicate len nogc_mark
              cont (mark vi read_ n []) $ \vv cont -> do
                  (PUV.unsafeIndex -> fvi) <- PUV.unsafeFreeze vi
                  let sweep i v | i == len = return v
                      sweep i v = do
                          let !ma = fvi i
                          if ma == nogc_mark then sweep (i+1) v else
                              case read_ i of
                                ERef r | r >= n -> sweep (i+1) v
                                e -> sweep (i+1) =<< write v (ma + n) (sfv fvi n e)
                  cont fvi =<< sweep 0 vv
           where
              mark vi read_ n acc i t = do
                  ma <- UV.unsafeRead vi i
                  if ma /= nogc_mark then writes ma >> return t else
                      case read_ i of
                        ERef r | r >= n -> mark vi read_ n (i: acc) (r - n) t
                        e -> do
                          writes t
                          UV.unsafeWrite vi i t
                          fv (mark vi read_ n []) n e $ t+1
                where
                  writes t = forM_ acc $ \i -> UV.unsafeWrite vi i t
  
  delta ISqrt             [LInt i] = HLit $ LInt $ round $ sqrt $ fromIntegral i
  delta LessEq    [LInt j, LInt i] = mkBool $ i <= j
  delta EqInt     [LInt j, LInt i] = mkBool $ i == j
  delta Add       [LInt j, LInt i] = HLit $ LInt $ i + j
  delta Sub       [LInt j, LInt i] = HLit $ LInt $ i - j
  delta Mod       [LInt j, LInt i] = HLit $ LInt $ i `mod` j
  delta o ls = error $ "delta: " ++ show o ++ "\n" ++ show ls
  
  mkBool b = HCon (if b then ("True", 1) else ("False", 0)) mempty
  
  isHNF (SExp x) = isHNF' x
  isHNF _ = False
  
  isHNF' HVar_{} = False
  isHNF' HPiece{} = False
  isHNF' _ = True
  
  --------------------------------------------------------------- pretty print
  
  newtype Info a = Info {getInfo :: a}
  
  instance Eq (Info a) where _ == _ = True
  instance Show a => Show (Info a) where show (Info s) = show s
  instance IsString a => IsString (Info a) where fromString = Info . fromString
  
  type VarInfo = Info String
  type ConInfo = String
  type CaseInfo = [(String, [String])]
  
  instance PShow Lit where
      pShow (LInt i)   = pShow i
      pShow (LChar i)  = pShow i
      pShow (LFloat i) = pShow i
  
  instance Show Lit where show = ppShow
  
  shLet [] x = x
  shLet ls x = foldl (flip DFreshName) (DLet' (foldr1 DSemi $ zipWith (\i (_, e) -> DOp "=" (Infix (-1)) (dVar i) e) [0..] ls) x) (Just . getInfo . fst <$> ls)
  
  shCase cn e xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of"))
      $ foldr1 DSemi
      [ foldr DFreshName
          (DArr_ "->" (foldl DApp (text a) $ dVar <$> reverse [0..length n - 1])
                      b
          )
          $ Just <$> n
      | ((a, n), b) <- zip cn xs]
  
  shLam n b = DFreshName (Just n) $ showLam (DVar 0) b
  
  showLam x (DFreshName u d) = DFreshName u $ showLam (DUp 0 x) d
  showLam x (DLam xs y) = DLam (DSep (InfixR 11) x xs) y
  showLam x y = DLam x y
  
  instance PShow HNF where
      pShow = \case
          HLam n e -> shLam (getInfo n) $ pShow e
          HCon (s, _) is -> foldl DApp (text s) $ dVar <$> is
          HLit l -> pShow l
          HVar_ i -> dVar i
          HPiece p e -> showPiece (pShow e) p
  
  dVar (Pos i) = DVar i
  dVar (Neg i) = text $ "v" ++ show i
  
  instance PShow EExp where
      pShow ErrExp = text "_|_"
      pShow (ExpC _ ls e) = shLet ((,) "x" . pShow <$> ls) $ pShow e
  
  showPiece e = \case
      EApp x -> e `DApp` pShow x
      ECase (cns, _) xs -> shCase cns e $ pShow <$> xs
      Update_ i -> DOp "@" (InfixR 14) (dVar i) e
      EDelta o ls es -> shDelta o $ (pShow <$> ls) ++ e: (pShow <$> es)
  {-
  instance PShow Exp where
      pShow = \case
          Var i -> DVar i
          Free i -> text $ "v" ++ show i
          Lam n e -> shLam (getInfo n) $ pShow e
          App a b -> pShow a `DApp` pShow b
          Con (s, _) is -> foldl DApp (text s) $ pShow <$> is
          Case (cns, _) e xs -> shCase cns (pShow e) $ pShow <$> xs
          Lit l -> pShow l
          Delta o es -> shDelta o $ pShow <$> es
  -}
  --shDelta ISqrt [x]    =
  shDelta SeqOp [a, b] = DOp "`seq`" (Infix 1) a b
  shDelta EqInt [x, y] = DOp "==" (Infix 4) x y
  shDelta Add [x, y]   = DOp "+" (InfixL 6) x y
  shDelta Sub [x, y]   = DOp "-" (InfixL 6) x y
  shDelta Mod [x, y]   = DOp "`mod`" (InfixL 7) x y
  shDelta o xs = foldl DApp (text $ show o) xs
  
  ---------------------------------------------------------------------------------------- examples
  
  --pPrint = putStrLn . ppShow
  
  pattern F = Con ("False", 0) []
  pattern T = Con ("True", 1) []
  pattern ENil = Con ("[]", 0) []
  pattern ECons a b = Con ("ECons", 1) [a, b]
  
  mkCase a b c = Case (a, map (length . snd) a) b c
  
  caseBool x f t = mkCase [("False", []), ("True", [])] x [f, t]
  caseList x n c = mkCase [("[]", []), ("ECons", ["c", "cs"])] x [n, c]
  
  id_ = Lam "x" (Var 0)
  
  if_ b t f = caseBool b f t
  
  not_ x = if_ x F T
  
  test = id_ `App` id_ `App` id_ `App` id_ `App` Int 13
  
  test' = id_ `App` (id_ `App` Int 14)
  
  foldr_ f e = Y "g" $ Lam "as" $ caseList (Var 0) (up' 2 e) (up' 4 f `App` Var 1 `App` (Var 3 `App` Var 0))
  
  filter_ p = foldr_ (Lam "y" $ Lam "ys" $ if_ (up' 2 p `App` Var 1) (ECons (Var 1) (Var 0)) (Var 0)) ENil
  
  and2 a b = if_ a b F
  
  and_ = foldr_ (Lam "a" $ Lam "b" $ and2 (Var 1) (Var 0)) T
  
  map_ f = foldr_ (Lam "z" $ Lam "zs" $ ECons (up' 2 f `App` Var 1) (Var 0)) ENil
  
  neq a b = not_ $ Op2 EqInt a b
  
  from_ = Y "from" $ Lam "n" $ ECons (Var 0) $ Var 1 `App` Op2 Add (Var 0) (Int 1)
  
  undefined_ = Y "undefined" $ Var 0
  
  idx = Y "idx" $ Lam "xs" $ Lam "n" $ caseList (Var 1) undefined_ $ if_ (Op2 EqInt (Var 2) $ Int 0) (Var 1) $ Var 4 `App` Var 0 `App` (Op2 Sub (Var 2) $ Int 1)
  
  t = idx `App` (from_ `App` Int 3) `App` Int 5
  
  takeWhile_ = Y "takeWhile" $ Lam "p" $ Lam "xs" $ caseList (Var 0) ENil $ if_ (Var 3 `App` Var 1) (ECons (Var 1) $ Var 4 `App` Var 3 `App` Var 0) ENil
  
  sum_ = foldr_ (Lam "a" $ Lam "b" $ Op2 Add (Var 1) (Var 0)) (Int 0)
  
  sum' = Y "sum" $ Lam "xs" $ caseList (Var 0) (Int 0) $ Op2 Add (Var 1) $ Var 3 `App` Var 0
  
  infixl 4 `sApp`
  
  sApp a b = Lam "s" (Seq (Var 0) (up' 1 a `App` Var 0)) `App` b
  
  {-
  accsum acc [] = acc
  accsum acc (x: xs) = let z = acc + x `seq` accsum z xs
  -}
  accsum = Y "accsum" $ Lam "acc" $ Lam "xs" $ caseList (Var 0) (Var 1) $ Var 4 `sApp` Op2 Add (Var 3) (Var 1) `App` Var 0
  
  fromTo = Y "fromTo" $ Lam "begin" $ Lam "end" $ ECons (Var 1) $ if_ (Op2 EqInt (Var 0) (Var 1)) ENil $ Var 2 `App` Op2 Add (Var 1) (Int 1) `App` Var 0
  
  from = Y "from" $ Lam "begin" $ ECons (Var 0) $ Var 1 `App` Op2 Add (Var 0) (Int 1)
  
  t' n = sum' `App` (fromTo `App` Int 0 `App` Int n)
  
  t'' n = accsum `App` Int 0 `App` (fromTo `App` Int 0 `App` Int n)
  
  t_opt n = Y "optsum" (Lam "i" $ if_ (Op2 EqInt (Int n) (Var 0)) (Var 0) (Op2 Add (Var 0) $ Var 1 `App` Op2 Add (Int 1) (Var 0))) `App` Int 0
  
  t_seqopt n = Y "seqoptsum" (Lam "i" $ Lam "j" $ if_ (Op2 EqInt (Int n) (Var 0)) (Op2 Add (Int n) (Var 1)) (Var 2 `sApp` Op2 Add (Var 0) (Var 1) `sApp` Op2 Add (Int 1) (Var 0))) `App` Int 0 `App` Int 0
  
  mod_ = Op2 Mod
  
  isqrt = Op1 ISqrt
  
  le = Op2 LessEq
  
  primes = Y "primes"
      $ ECons (Int 2) $ ECons (Int 3)
      $ filter_ (Lam "n" $ and_ `App` (map_ (Lam "p" $ neq (Int 0) $ mod_ (Var 1) (Var 0)) `App` (takeWhile_ `App` (Lam "x" $ le (Var 0) $ isqrt $ Var 1) `App` Var 1))) `App` (from `App` Int 5)
  -- primes = 2:3: filter (\n -> and $ map (\p -> n `mod` p /= 0) (takeWhile (\x -> x <= iSqrt n) primes)) (from 5)
  
  
  nthPrime n = idx `App` primes `App` (Int $ n-1)
  
  
  twice = Lam "f" $ Lam "x" $ Var 1 `App` (Var 1 `App` Var 0)
  twice2 = Lam "f" $ Lam "x" $ Var 1 `sApp` (Var 1 `App` Var 0)
  
  inc = Lam "n" $ Op2 Add (Int 1) (Var 0)
  
  test'' = Lam "f" (Int 4) `App` Int 3
  
  twiceTest n = (Lam "twice" $ (iterate (`App` Var 0) (Var 0) !! n) `App` inc `App` Int 0) `App` twice
  twiceTest2 n = (Lam "twice" $ (iterate (`App` Var 0) (Var 0) !! n) `App` inc `App` Int 0) `App` twice2
  
  tests =
      [ t test (Int 13)
      , t test' (Int 14)
      , t test'' (Int 4)
      , t (t' 10) (Int 55)
      , t (t'' 10) (Int 55)
      , t (nthPrime 6) (Int 13)
      ]
    where t = (,)
  
  evalTests = case [(a, b) | (hnf -> a, hnf -> b) <- tests, a /= b] of
      [] -> True
      (a, b): _ -> error $ "tests:\n" ++ ppShow a ++ "\n------ /= -------\n" ++ ppShow b 
  
  
  main | evalTests = do
      [s, read -> m, read -> m', read -> g3, n] <- getArgs
      putStrLn . (++"\n---------------") . ppShow $ 
          hnf_ (m, m', max 0 $ m' - g3, g3) $ prog s $ read n
  
  prog = \case
      "prime" -> nthPrime
      "seq" -> t''
      "sum" -> t'
      "opt" -> t_opt
      "seqopt" -> t_seqopt
      "twice" -> twiceTest
      "twice2" -> twiceTest2
  
  