add reducer prototype with fast de bruijn index shifting (not ready yet)

1 files changed, 696 insertions, 0 deletions

diff --git a/prototypes/ShiftReducer.hs b/prototypes/ShiftReducer.hs
new file mode 100644
index 00000000..ae515b08
--- /dev/null
+++ b/prototypes/ShiftReducer.hs
@@ -0,0 +1,696 @@
+{-# language ScopedTypeVariables #-}
+{-# language LambdaCase #-}
+{-# language TypeOperators #-}
+{-# language TypeFamilies #-}
+{-# language ViewPatterns #-}
+{-# language PatternGuards #-}
+{-# language PatternSynonyms #-}
+{-# language RankNTypes #-}
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language GADTs #-}
+{-# language DeriveFunctor #-}
+{-# language DeriveGeneric #-}
+{-# language DefaultSignatures #-}
+{-# language FlexibleInstances #-}
+{-# language FlexibleContexts #-}
+{-# language TemplateHaskell #-}  -- for testing
+{-# language NoMonomorphismRestriction #-}
+
+import Data.Monoid
+import Data.Maybe
+import Data.List
+import Data.Map (Map)
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Control.Monad
+import Control.Arrow hiding (app)
+import Test.QuickCheck
+import Test.QuickCheck.Function
+import GHC.Generics
+import Debug.Trace
+
+------------------------------------------------------------ utils
+
+iterateN i f x = iterate f x !! i
+
+(<&>) = flip (<$>)
+
+data Void
+
+instance Eq Void where (==) = error "(==) @Void"
+instance Show Void where show = error "show @Void"
+
+{- used later?
+-- supplementary data: data with no semantic relevance
+newtype SData a = SData a
+instance Show (SData a) where show _ = "SData"
+instance Eq (SData a) where _ == _ = True
+instance Ord (SData a) where _ `compare` _ = EQ
+-}
+
+------------------------------------------------------------ streams
+
+-- streams with constant tails
+-- invariant property: Repeat is used when possible (see cons)
+data Stream a
+    = Cons a (Stream a)  
+    | Repeat a
+    deriving (Eq, Show, Functor)    -- Functor is not proper, may break invariant
+
+-- smart constructor to construct normal form of streams
+cons b (Repeat b') | b == b' = Repeat b'
+cons b x = Cons b x
+
+-- stream head
+sHead (Cons a _) = a
+sHead (Repeat a) = a
+
+-- stream tail
+sTail (Cons _ a) = a
+sTail (Repeat a) = Repeat a
+
+instance Applicative Stream where
+    pure a = Repeat a
+    -- (<*>) is not proper, may break invariant
+    Repeat f <*> Repeat a = Repeat $ f a
+    x <*> y = Cons{-should be cons-} (sHead x $ sHead y) (sTail x <*> sTail y)
+
+foldStream :: (b -> a -> a) -> (b -> a) -> Stream b -> a
+foldStream f g (Cons b u) = f b (foldStream f g u)
+foldStream f g (Repeat b) = g b
+
+-- final value in the stream
+limes :: Stream a -> a
+limes = foldStream const id
+
+-- replace limes by given stream
+sCont :: Eq a => Stream a -> (a -> Stream a) -> Stream a
+sCont as f = foldStream cons f as
+
+-- semantics of Stream
+streamToList :: Stream a -> [a]
+streamToList = foldStream (:) repeat
+
+streamToFun :: Stream a -> Int -> a
+streamToFun u i = streamToList u !! i
+
+sFromList :: Eq a => [a] -> a -> Stream a
+sFromList xs b = foldr cons (Repeat b) xs
+
+instance (Arbitrary a, Eq a) => Arbitrary (Stream a) where
+    arbitrary = sFromList <$> arbitrary <*> arbitrary
+
+-- iterate on stream
+sIterate :: Eq a => (a -> a) -> a -> Stream a
+sIterate f x
+    | y == x = Repeat x
+    | otherwise = Cons x $ sIterate f y
+  where
+    y = f x
+
+sCatMaybes :: Stream (Maybe a) -> [a]
+sCatMaybes = foldStream (\m s -> maybe s (:s) m) (maybe [] repeat)
+
+---------------------------------------------------------- operations involving Boolean streams
+
+mergeStreams :: Eq a => Stream Bool -> Stream a -> Stream a -> Stream a
+mergeStreams (Cons True u)  as bs = cons (sHead as) $ mergeStreams u (sTail as) bs
+mergeStreams (Cons False u) as bs = cons (sHead bs) $ mergeStreams u as (sTail bs)
+mergeStreams (Repeat True)  as bs = as
+mergeStreams (Repeat False) as bs = bs
+
+sFilter :: Stream Bool -> [a] -> [a]
+sFilter (Cons True  u) is = take 1 is ++ sFilter u (drop 1 is)
+sFilter (Cons False u) is =              sFilter u (drop 1 is)
+sFilter (Repeat True)  is = is
+sFilter (Repeat False) is = []
+
+-- sFilter for streams
+-- the first stream is used when no more element can pass the filter
+filterStream :: Eq a => Stream a -> Stream Bool -> Stream a -> Stream a
+filterStream d (Cons True s)  as = cons (sHead as) $ filterStream d s $ sTail as
+filterStream d (Cons False s) as =                   filterStream d s $ sTail as
+filterStream d (Repeat True)  as = as
+filterStream d (Repeat False) as = d
+
+sOr :: Stream Bool -> Stream Bool -> Stream Bool
+sOr (Cons b u) (Cons b' u') = cons (b || b') $ sOr u u'
+sOr (Repeat False) u = u
+sOr (Repeat True)  u = Repeat True
+sOr u (Repeat False) = u
+sOr u (Repeat True)  = Repeat True
+
+prop_sOr_idemp a = sOr a a == a
+prop_sOr_comm a b = sOr a b == sOr b a
+
+dbAnd a b = not <$> sOr (not <$> a) (not <$> b)
+
+instance Monoid (Stream Bool) where
+    mempty = Repeat False
+    mappend = sOr
+
+prop_StreamBool_monoid_left  (a :: Stream Bool)     = mempty <> a == a
+prop_StreamBool_monoid_right (a :: Stream Bool)     = a <> mempty == a
+prop_StreamBool_monoid_assoc (a :: Stream Bool) b c = (a <> b) <> c == a <> (b <> c)
+
+-- composition of (Stream Bool) values (by sFilter semantics)
+sComp :: Stream Bool -> Stream Bool -> Stream Bool
+sComp bs as = mergeStreams bs as $ Repeat False
+
+prop_sComp a b xs = sFilter (sComp a b) xs == (sFilter b . sFilter a) xs
+prop_sComp_trans a b (getNonNegative -> i) = indexTrans (sComp a b) i == (indexTrans a =<< indexTrans b i)
+
+filterDBUsed :: Stream Bool -> Stream Bool -> Stream Bool
+filterDBUsed = filterStream $ Repeat False
+
+--prop_filterDBUsed bs = mergeStreams bs xs ys sOr b a `sComp` filterDBUsed (sOr b a) a  == a
+
+prop_filterDBUsed a b = sOr b a `sComp` filterDBUsed (sOr b a) a  == a
+
+compress s = filterDBUsed s s
+
+
+--takeUps :: Int -> Stream Bool -> Stream Bool
+--takeUps i = (`sComp` sFromList (replicate i True) False)
+
+--prop_takeUps (getNonNegative -> n) u = streamToList (takeUps n u) == normSem (take n $ streamToList u)
+
+--takeUps' :: Int -> Stream Bool -> Stream Bool
+--takeUps' i = sComp $ sFromList (replicate i True) False
+
+--prop_takeUps' u (getNonNegative -> n) = streamToList (takeUps' n u) == head (dropWhile ((< n) . length . filter id) (inits $ streamToList u) ++ [streamToList u])
+
+--------------------------------------------------------------- indices
+
+-- index of the first appearance of the limes
+limesIndex :: Stream a -> Int
+limesIndex = foldStream (const (+1)) (const 0)
+
+-- indices at which the stream value is True
+trueIndices :: Stream Bool -> [Int]
+trueIndices s = sFilter s [0..]
+
+prop_trueIndices (getExpDB -> u) = all (streamToFun u) $ trueIndices u
+
+invTrueIndices :: [Int] -> Stream Bool
+invTrueIndices = f 0 where
+    f i [] = Repeat False
+    f i (k: ks) = iterateN (k - i) (cons False) $ cons True $ f (k + 1) ks
+
+prop_invTrueIndices (map getNonNegative . Set.toList -> ks) = trueIndices (invTrueIndices ks) == ks
+prop_invTrueIndices' (getExpDB -> u) = u == invTrueIndices (trueIndices u)
+
+-- a Boolean stream can be seen as an index transformation function for indices 0..n
+indexTrans :: Stream Bool -> Int -> Maybe Int
+indexTrans s i = ((Just <$> sFilter s [0..]) ++ repeat Nothing) !! i
+
+-- inverse of indexTrans
+invIndexTrans :: Stream Bool -> Int -> Maybe Int
+invIndexTrans s i = case dropWhile ((< i) . snd) $ zip [0..] $ sFilter s [0..] of
+    ((x, i'): _) | i' == i -> Just x
+    _ -> Nothing
+
+prop_invIndexTrans u (getNonNegative -> i) = maybe True (==i) (indexTrans u i >>= invIndexTrans u)
+
+diffDBs as = (u, filterDBUsed u <$> as) where u = mconcat as
+
+
+------------------------------------------------------------ used/unused de bruijn indices
+
+-- which de bruijn indicies are used?
+-- semantics of DBUsed is given by trueIndices
+-- True: use index; False: skip index
+type DBUsed = Stream Bool
+
+-- invariant property: limes is False
+-- finite indicies are used; lambda expressions are decorated with this
+newtype ExpDB = ExpDB { getExpDB :: DBUsed }
+    deriving (Eq, Show)
+
+instance Arbitrary ExpDB where
+    arbitrary = ExpDB . flip sFromList False <$> arbitrary
+
+-- invariant property: limes is True
+-- finite indicies are not used; good for index shifting transformations
+newtype ShiftDB = ShiftDB { getShiftDB :: DBUsed }
+    deriving (Eq, Show)
+
+instance Arbitrary ShiftDB where
+    arbitrary = ShiftDB . flip sFromList True <$> arbitrary
+
+------------------------------------------------------------ de bruijn index shifting layer
+
+-- transformation on De-Bruijn indices
+--      Shift s i   ~   (fromJust . indexTrans s) <$> i
+data Shift a = Shift DBUsed a
+  deriving (Eq, Functor)
+
+instance Show a => Show (Shift a) where
+    show (Shift s a) = foldStream (:) (:":") ((\b -> if b then 'x' else '_') <$> s) ++ show a
+
+strip (Shift _ x) = x
+
+{-
+instance Applicative Shift where
+    pure = Shift (Repeat False)
+    Shift uf f <*> Shift ua a = Shift (uf <> ua) (f a)
+
+instance Monad Shift where
+    return = pure
+    Shift ux x >>= f = up ux $ f x
+
+--prop_UExpmonadAssoc (x :: Shift ()) (apply -> f) (apply -> g) = ((x >>= f) >>= g) == (x >>= (\x' -> f x' >>= g))
+-}
+
+class GetDBUsed a where
+    getDBUsed :: a -> DBUsed
+
+instance GetDBUsed ExpDB where
+    getDBUsed = getExpDB
+
+instance GetDBUsed (Shift a) where
+    getDBUsed (Shift u _) = u
+
+mkShift :: GetDBUsed a => a -> Shift a
+mkShift e = Shift (getDBUsed e) e
+
+instance (Arbitrary a, GetDBUsed a) => Arbitrary (Shift a) where
+    arbitrary = upToShift <$> arbitrary
+
+----------------
+
+-- for testing
+-- generate a DBUsed with a given number of used indicies
+data Up a = Up DBUsed a
+    deriving (Show)
+
+upToShift :: GetDBUsed a => Up a -> Shift a
+upToShift (Up u x) = Shift (sComp u $ getDBUsed x) x
+
+instance (Arbitrary a, GetDBUsed a) => Arbitrary (Up a) where
+    arbitrary = do
+        f <- arbitrary
+        u <- flip sFromList True . concatMap ((++ [True]) . (`replicate` False) . getNonNegative)
+                <$> replicateM (limesIndex $ getDBUsed f) arbitrary
+        return $ Up u f
+
+class GetDBUsed a => ShiftLike a where
+    setDBUsed :: DBUsed -> a -> a
+
+modDBUsed :: ShiftLike a => (DBUsed -> DBUsed) -> a -> a
+modDBUsed f e = setDBUsed (f $ getDBUsed e) e
+
+up :: ShiftLike a => DBUsed -> a -> a
+up x = modDBUsed (sComp x)
+
+down :: ShiftLike a => DBUsed -> a -> Maybe a
+down a e = case filterDBUsed (not <$> a) (getDBUsed e) of
+    Repeat False -> Just $ modDBUsed (filterDBUsed a) e
+    _ -> Nothing
+
+up_ :: ShiftLike a => Int -> Int -> a -> a
+up_ i j = up (iterateN i (cons True) $ iterateN j (cons False) (Repeat True))
+
+down_ :: ShiftLike a => Int -> a -> Maybe a
+down_ i = down (iterateN i (cons True) $ cons False (Repeat True))
+
+instance ShiftLike (Shift a) where
+    setDBUsed x (Shift _ a) = Shift x a
+
+prop_upDown (Up u ((`Shift` ()) . getExpDB -> e))
+    = down u (up u e) == Just e
+prop_downNothing ((`Shift` ()) . getExpDB -> e) (getNonNegative -> i)
+    = if i `elem` trueIndices (getDBUsed e) then down_ i e == Nothing else isJust (down_ i e)
+
+------------------------------------------------------------ substitutions
+
+type Substs a = Map Int a
+
+substsKeys :: Substs a -> Stream Bool
+substsKeys = invTrueIndices . Map.keys
+
+substsStream :: Eq a => Substs a -> Stream (Maybe a)
+substsStream = elemsUps . Map.toList
+
+elemsUps :: Eq a => [(Int, a)] -> Stream (Maybe a)
+elemsUps = f 0 where
+    f i [] = Repeat Nothing
+    f i ((k, a): ks) = iterateN (k - i) (cons Nothing) $ cons (Just a) $ f (k + 1) ks
+
+streamSubsts :: Stream (Maybe a) -> Substs a
+streamSubsts = Map.fromDistinctAscList . upsElems
+
+upsElems :: Stream (Maybe a) -> [(Int, a)]
+upsElems = f 0 where
+    f _ (Repeat Nothing) = []
+    f i (Cons Nothing u) = f (i+1) u
+    f i (Cons (Just a) u) = (i, a): f (i+1) u
+
+expandSubsts :: (Eq a, ShiftLike a) => Stream Bool -> Substs a -> Substs a
+expandSubsts u m = streamSubsts $ (\x -> mergeStreams u x $ Repeat Nothing) $ substsStream $ up u <$> m
+
+filterSubsts :: (Eq a, ShiftLike a) => Stream Bool -> Substs a -> Substs a
+filterSubsts u m = streamSubsts $ filterStream (Repeat Nothing) u $ substsStream $ modDBUsed (filterDBUsed u) <$> m
+
+------------------------------------------------------------ let expressions (substitutions + expression)
+
+data Let e a = Let (Substs e) a
+  deriving (Eq, Show, Functor)
+
+instance (GetDBUsed e, GetDBUsed a) => GetDBUsed (Let e a) where
+    getDBUsed (Let m e) = getDBUsed $ ShiftLet (getDBUsed e <> mconcat (Map.elems $ getDBUsed <$> m)) m e
+
+pattern ShiftLet :: DBUsed -> Substs a -> b -> Shift (Let a b)
+pattern ShiftLet u m e <- (getShiftLet -> (u, m, e)) where ShiftLet u m e = Shift (filterDBUsed (not <$> substsKeys m) u) (Let m e)
+
+getShiftLet (Shift u (Let m e)) = (mergeStreams (substsKeys m) (Repeat True) u, m, e)
+
+-- TODO: remove Eq a
+pattern PShiftLet :: () => (Eq a, ShiftLike a, ShiftLike b) => Substs a -> b -> Shift (Let a b)
+pattern PShiftLet m e <- (pushShiftLet -> Let m e) where
+    PShiftLet m e = ShiftLet u (filterSubsts u m) $ modDBUsed (filterDBUsed u) e
+      where
+        u = getDBUsed e <> mconcat (Map.elems $ getDBUsed <$> m)
+
+pushShiftLet (ShiftLet u m e) = Let (expandSubsts u m) (up u e)
+
+mkLet :: (Eq a, ShiftLike a, ShiftLike b) => Substs a -> b -> Shift (Let a b)
+mkLet m e = PShiftLet (Map.filterWithKey (\k _ -> streamToFun c k) m) e
+  where
+    -- determine which let expressions are used (garbage collection)
+    -- TODO: speed this up somehow
+    c = limes $ sIterate f $ getDBUsed e
+      where
+        f x = dbAnd ks $ x <> mconcat (sCatMaybes $ filterStream (Repeat Nothing) x us)
+        ks = substsKeys m
+        us = substsStream $ getDBUsed <$> m
+
+transportIntoLet (Let m _) e = up (not <$> substsKeys m) e
+
+----------------------------------------------------------------- MaybeLet
+
+data MaybeLet a b c
+    = HasLet (Let a (Shift c))
+    | NoLet b
+    deriving (Show, Eq)
+
+type MaybeLet' a b = MaybeLet a b b
+
+maybeLet :: (Eq a, ShiftLike a) => Shift (Let a (Shift b)) -> Shift (MaybeLet' a b)
+maybeLet l@(Shift u (Let m e))
+    | Map.null m = up u $ NoLet <$> e
+    | otherwise  = HasLet <$> l
+
+joinLets :: (Eq a, ShiftLike a) => MaybeLet' a (MaybeLet' a b) -> MaybeLet' a b
+joinLets (NoLet e) = e
+joinLets (HasLet (Let m (Shift s' (NoLet e)))) = HasLet $ Let m $ Shift s' e
+joinLets (HasLet (Let m (Shift s' (HasLet (Let m' e)))))
+    = HasLet $ Let (expandSubsts (not <$> substsKeys sm) m <> sm) se
+      where
+        (PShiftLet sm se) = Shift s' (Let m' e)
+
+instance (GetDBUsed a, GetDBUsed b, GetDBUsed c) => GetDBUsed (MaybeLet a b c) where
+    getDBUsed = \case
+        NoLet a  -> getDBUsed a
+        HasLet x -> getDBUsed x
+
+-- used in testing
+fromLet (Shift u (NoLet e)) = Shift u e
+
+------------------------------------------------------------ literals
+
+data Lit
+    = LInt Int
+    | LChar Char
+    -- ...
+    deriving (Eq)
+
+instance Show Lit where
+    show = \case
+        LInt i -> show i
+        LChar c -> show c
+
+------------------------------------------------------------ expressions
+
+data Exp_ a b c d e
+    = ELit_  Lit
+    | EVar_  a   -- a = () means that the variable de bruijn index is 0 (the only possible index if the exprssion is compact)
+                 -- a = Int is the de bruijn index (in cases when the exprssion is not compactified)
+    | ELamD_ b   -- lambda with unused argument
+                 -- b  is usually (Exp_ a b c d e)
+    | ELam_  c   -- lambda with used argument
+                 -- c  usually contains a MaybeLet layer
+    | EApp_  d d -- application
+                 -- d  usually contains a Shift layer
+    | RHS_   e   -- marks the beginning of right hand side (parts right to the equal sign) in fuction definitions
+                 -- e  is usually (Exp_ a b c d e)
+                 -- e = Void  means that this constructor cannot be used
+  deriving (Eq, Show) --, Generic)
+
+--------------------------------------------------------
+
+type WithLet a = MaybeLet (Shift LHSExp) a a
+
+-- right-hand-side expression (no RHS constructors inside)
+newtype Exp = Exp (Exp_ () Exp (WithLet Exp) (Shift Exp) Void)
+  deriving (Eq)
+
+pattern ELit l   = Exp (ELit_ l)
+pattern EApp a b = Exp (EApp_ a b)
+pattern ELam i   = Exp (ELam_ i)
+pattern ELamD i  = Exp (ELamD_ i)
+pattern EVar i   = Exp (EVar_ i)
+
+pattern EInt i = ELit (LInt i)
+
+-- left-hand-side expression (allows RHS constructor)
+newtype LHSExp = LHSExp (Exp_ () LHSExp (WithLet LHSExp) (Shift LHSExp) Exp)
+  deriving (Eq, Show)
+
+pattern RHS i   = LHSExp (RHS_ i)
+
+--------------------------------------------------------
+
+type SExp = Shift Exp
+type LExp = WithLet Exp
+
+-- SLExp is *the* expression type in the user API
+type SLExp = Shift (WithLet Exp)
+
+sFun p s xs c = parens $ \c -> s ++ foldr (\f c -> ' ': f c) c xs
+  where
+    parens x
+        | p < 10 = x c
+        | otherwise = '(': x (')': c)
+
+instance Show Exp where
+    showsPrec p = \case
+        ELit i   -> shows i
+        EApp a b -> sFun p "EApp" [showsPrec 10 a, showsPrec 10 b]
+        ELam a   -> sFun p "ELam" [showsPrec 10 a]
+        ELamD a  -> sFun p "ELamD" [showsPrec 10 a]
+        EVar ()  -> ("EVar" ++)
+
+instance GetDBUsed Exp where
+    getDBUsed = \case
+        EApp (Shift ua a) (Shift ub b) -> ua <> ub
+        ELit{} -> mempty
+        EVar{} -> cons True mempty
+        ELamD e -> sTail $ getDBUsed e
+        ELam e  -> sTail $ getDBUsed e
+
+instance Arbitrary Exp where
+    arbitrary = (\(Shift _ (NoLet e)) -> e) . getSimpleExp <$> arbitrary
+--    shrink = genericShrink
+
+-- SLExp without let and shifting; for testing
+newtype SimpleExp = SimpleExp { getSimpleExp :: SLExp }
+    deriving (Eq, Show)
+
+instance Arbitrary SimpleExp where
+    arbitrary = fmap SimpleExp $ oneof
+        [ var . getNonNegative <$> arbitrary
+        , Int <$> arbitrary
+        , app <$> (getSimpleExp <$> arbitrary) <*> (getSimpleExp <$> arbitrary)
+        , lam <$> (getSimpleExp <$> arbitrary)
+        ]
+
+getLit :: SLExp -> Maybe Lit
+getLit (Shift _ (NoLet (ELit l))) = Just l
+getLit (Shift _ (HasLet (Let _ (Shift _ (ELit l))))) = Just l
+getLit _ = Nothing
+
+pattern Int i <- (getLit -> Just (LInt i)) where Int = Shift mempty . NoLet . EInt
+
+var :: Int -> SLExp
+var i = fmap NoLet $ up_ 0 i $ mkShift $ EVar ()
+
+prop_upVar (getNonNegative -> k) (getNonNegative -> n) (getNonNegative -> i) = up_ k n (var i) == var (if k <= i then n + i else i)
+prop_downVar (getNonNegative -> k) (getNonNegative -> i) = down_ k (var i) == case compare k i of LT -> Just (var $ i-1); EQ -> Nothing; GT -> Just (var i)
+
+lam :: SLExp -> SLExp
+lam (Shift u e) = Shift (sTail u) $ if sHead u then eLam e else eLamD e
+  where
+    eLam (NoLet e) = NoLet $ ELam $ NoLet e
+    -- TODO: improve this by let-floating
+    eLam x = NoLet $ ELam x
+
+    eLamD (NoLet e) = NoLet $ ELamD e
+    -- TODO: review
+    eLamD (HasLet (Let m (Shift u e))) = HasLet $ {-gc?-}Let (filterSubsts ul m) $ Shift (filterDBUsed ul u) $ ELamD e
+      where
+        ul = Cons False $ Repeat True
+
+app :: SLExp -> SLExp -> SLExp
+app (Shift ua (NoLet a)) (Shift ub (NoLet b))
+    = Shift u $ NoLet $ EApp (Shift (filterDBUsed u ua) a) (Shift (filterDBUsed u ub) b)
+  where u = ua <> ub
+app x y = f x y
+  where
+    f :: SLExp -> SLExp -> SLExp
+    f (Shift ula la) (Shift ulb (HasLet lb)) = g app ula la ulb lb
+    f (Shift ulb (HasLet lb)) (Shift ula la) = g (flip app) ula la ulb lb
+
+    g :: (SLExp -> SLExp -> SLExp) -> DBUsed -> LExp -> DBUsed -> Let (Shift LHSExp) (Shift Exp) -> SLExp
+    g app ula la ulb lb
+        = up u $ lets {-Shift u $-}
+    --      app (Shift ula' la) (Shift ulb' lb)
+    --      app (Shift ula' la) (Let mb eb)
+            mb {-HasLet $ Let mb $-} $
+                app xa (fmap NoLet eb)
+      where
+        (u, [ula', ulb']) = diffDBs [ula, ulb]
+        lb'@(Let mb eb) = pushShiftLet $ Shift ulb' lb
+        xa = transportIntoLet lb' $ Shift ula' la
+
+lets :: Substs (Shift LHSExp) -> SLExp -> SLExp
+lets m e = fmap joinLets $ maybeLet $ mkLet m e
+
+-- TODO
+instance Arbitrary LExp where
+    arbitrary = NoLet <$> arbitrary
+
+let1 :: Int -> SLExp -> SLExp -> SLExp
+let1 i (Shift u (NoLet x)) = lets $ Map.singleton i $ Shift u $ RHS x
+let1 i (Shift u (HasLet l)) = lets $ m <> Map.singleton i' (RHS <$> e)
+  where
+    (Let m e) = pushShiftLet $ Shift u l
+    (Just i') = indexTrans (not <$> substsKeys m) i
+
+---------------------------------------------------------
+{-
+newtype ExpS = ExpS (Exp_ Int ExpS (MaybeLet SExp ExpS Exp) SExp)
+  deriving (Eq, Show)
+
+pushShift :: SExp -> ExpS
+pushShift (Shift u e) = ExpS $ case e of
+    EApp a b -> EApp_ (up u a) (up u b)
+    ELit i -> ELit_ i
+    EVar{} -> EVar_ $ fromJust $ indexTrans u 0
+    ELamD e -> ELamD_ $ pushShift $ Shift (cons False u) e
+    ELam (NoLet e) -> ELam_ $ NoLet $ pushShift $ Shift (cons True u) e
+    LHS a b -> LHS_ a (up u <$> b) -- ??? $ SData (pushShift $ Shift u c)
+--    Delta x -> Delta_ $ SData x
+
+prop_var (getNonNegative -> i) = case pushShift (fromLet $ var i) of
+    ExpS (EVar_ i') -> i == i'
+    _ -> False
+
+prop_app (getSimpleExp -> a) (getSimpleExp -> b) = case pushShift $ fromLet $ app a b of
+    ExpS (EApp_ a' b') -> (a', b') == (fromLet a, fromLet b)
+    _ -> False
+
+--prop_lam (getNonNegative -> i) = elimShift undefined undefined undefined (==i) (var i)
+
+--prop_pushShift (Shift u e) =
+
+---------------------------------------------------------
+
+newtype ExpL = ExpL (Exp_ Int SLExp SLExp SLExp)
+  deriving (Eq, Show)
+{-
+pushLet :: LExp -> ExpL
+pushLet (NoLet e) = ExpL $ case e of
+    EInt i -> EInt_ i
+    EApp a b -> EApp_ (NoLet <$> a) (NoLet <$> b)
+    EVar{} -> EVar_ 0
+--    ELam a -> ELam_ $ mkShift a
+    ELamD a -> ELamD_ $ NoLet <$> mkShift a
+pushLet (HasLet (Let m e)) = ExpL $ case pushShift e of
+    ExpS e' -> case e' of
+        EApp_ a b -> EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b))
+        EInt_ i -> EInt_ i
+        EVar_ i -> EVar_ i
+-}
+pushLet' :: SLExp -> ExpL
+pushLet' (Shift u l) = case l of
+    NoLet e -> {-case pushShift (Shift u e) of
+      ExpS e -> -} ExpL $ case e of
+        ELit i -> ELit_ i
+        EApp a b -> EApp_ (NoLet <$> up u a) (NoLet <$> up u b)
+        EVar () -> EVar_ $ fromJust $ indexTrans u 0
+        ELam a -> ELam_ $ Shift (cons True u) a
+    --    ELamD_ a -> ELamD_ $ NoLet a
+        LHS a b -> LHS_ a ((fmap NoLet . up u) <$> b)
+    HasLet l -> case Shift u l of
+      PShiftLet m e -> case pushShift e of
+        ExpS e' -> case e' of
+            EApp_ a b -> ExpL $ EApp_ (fmap HasLet (mkLet m a)) (fmap HasLet (mkLet m b))
+            ELit_ i -> ExpL $ ELit_ i
+            EVar_ i -> case Map.lookup i m of
+                Nothing -> ExpL $ EVar_ i
+                Just x -> pushLet' $ lets m $ NoLet <$> x
+            LHS_ a b -> error "efun"
+--            Delta_ f -> ExpL $ Delta_ f
+
+---------------------------------------------------------
+
+hnf :: SLExp -> ExpL
+hnf e = case pushLet' e of
+    (ExpL (LHS_ "add" [_, _])) -> error "ok"
+    x@(ExpL (EApp_ a b)) -> case hnf a of
+        ExpL (ELam_ a) -> hnf $ let1 0 b a
+        ExpL (LHS_ n acc) -> hnf $ LHS n (_ b: acc)
+        _ -> x
+    x -> x
+
+-----------------------------------------------------------------------------------
+
+idE :: SLExp
+idE = lam $ var 0
+
+add :: SLExp
+add = NoLet <$> mkShift (LHS "add" []) -- $ ELam $ NoLet $ ELam $ NoLet $ Delta f)
+  where
+    f [Int i, Int j] = Int $ i + j
+
+example1 = app (idE) (Int 10)
+
+example2 = app (app add (Int 10)) (Int 5)
+
+
+--     = fun name args  $ \x -> \y -> rhs e
+
+
+----------------------------------------------------------------- run all tests
+-}
+return []
+runTests = $quickCheckAll
+
+{-
+TODO
+
+-   primes example running
+-   speed up eliminators with caching
+-   write performance tests
+-   speed up Boolean streams with compression
+-   check that all operations is available and efficient
+    -   up, down
+    -   subst
+    -   constructions
+        -   lam, pi, app, var, lit, ...
+    -   eliminations
+-   intergrate into the compiler
+-}
+