use splay lists

4 files changed, 406 insertions, 273 deletions

diff --git a/prototypes/FreeVars.hs b/prototypes/FreeVars.hs
index eefea309..71c0a99c 100644
--- a/prototypes/FreeVars.hs
+++ b/prototypes/FreeVars.hs
@@ -6,15 +6,27 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# language TemplateHaskell #-}  -- for testing
+{-# LANGUAGE NoMonomorphismRestriction #-}
 
-module FreeVars where
+module FreeVars
+    ( SFV(..), FV, Nat(..), pattern Nat
+    , HasFV (..), Lens
+    , up, down, usedVar, appLens, lComp, lConst
+    , FVCache(..), LamFV(..), VarFV(..)
+    , pattern CacheFV
+
+    , expand, fv, primContract
+    )
+    where
 
 import Data.List
 import Data.Word
@@ -57,51 +69,24 @@ instance Num Nat where
     abs _ = error "abs @Nat"
     signum _ = error "signum @Nat"
 
+instance Monoid Nat where
+    mempty = 0
+    Nat a `mappend` Nat b = Nat (a + b)
+
 instance PShow Nat where pShow (Nat i) = pShow i
 instance Show Nat where show = ppShow
 
 ----------------------------------------------------------------------------------
 
-data D1 a = D1 a
-    deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
-
-data D2 a = D2 a a
-    deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
-
-data D3 a = D3 a a a
-    deriving (Functor, Foldable, Traversable, Eq, Ord, Show)
-
-instance Arbitrary a => Arbitrary (D1 a) where arbitrary = D1 <$> arbitrary
-instance Arbitrary a => Arbitrary (D2 a) where arbitrary = D2 <$> arbitrary <*> arbitrary
-instance Arbitrary a => Arbitrary (D3 a) where arbitrary = D3 <$> arbitrary <*> arbitrary <*> arbitrary
-
-----------------------------------------------------------------------------------
-
-class Monoid a => Expandable a where
+-- Expand monoid
+newtype Expand = Expand {getExpand :: FV}
+    deriving (Eq, Show, Arbitrary)
 
-    expandT :: Traversable t => a -> t a -> t a
-    expandT = fmap . expand
-
-    expand :: a -> a -> a
-    expand u = runIdentity . expandT u . Identity
-
-    primContractT :: Traversable t => a -> t a -> t a
-    primContractT = fmap . primContract
-
-    primContract :: a -> a -> a
-    primContract u = runIdentity . primContractT u . Identity
-
-    contract :: a -> a -> a
-    contract a b = primContract (a <> b) a
-
-    selfContract :: a -> a
-    selfContract a = primContract a a
-
-diffT :: (Traversable t, Expandable a) => t a -> (a, t a)
-diffT u = (s, primContractT s u)
-  where
-    s = fold u
+instance Monoid Expand where
+    mempty = Expand $ fO 0
+    Expand a `mappend` Expand b = Expand (a `expand` b)
 
+{-
 diffTest u = u == uncurry expandT (diffT u)
 
 assocTestL (D3 a b c) = (abc, D3 a'' b'' c'') == diffT (D3 a b c)
@@ -115,13 +100,7 @@ assocTestR (D3 a b c) = (abc, D3 a'' b'' c'') == diffT (D3 a b c)
     (bc, D2 b' c') = diffT $ D2 b c
     (abc, D2 a'' bc') = diffT $ D2 a bc
     D2 b'' c'' = expandT bc' $ D2 b' c'
-
-class StreamLike a where
-    type StreamElem a
-
-    sDrop :: Nat -> a -> a
-
-    sIndex :: a -> Nat -> StreamElem a
+-}
 
 ----------------------------------------------------------------------------------
 
@@ -194,45 +173,53 @@ instance Monoid FV where
 prop_monoid_FV = prop_Monoid (T :: T FV)
 prop_mappend_normal_FV (a :: FV) b = testNormalFV (a <> b)
 
-instance Expandable FV where
-    expand _ FE = FE
-    expand FE _ = FE
-    expand (FV a b xs) (FV c d ys)
-        | c + d <= b  = fv (a + c) d       $ expand (FV 0 (b - (c + d)) xs) ys
-        | c <= b      = fv (a + c) (b - c) $ expand xs (FV 0 (d - (b - c)) ys)
-        | otherwise   = fv (a + b) 0       $ expand xs (FV (c - b) d ys)
-
-    primContract x FE = FE
-    primContract (FV a' b' us') (FV a b us)
-        | a' + b' <= a = fv b'       0 $ primContract us' (FV (a - (a' + b')) b us)
-        | otherwise    = fv (a - a') b $ primContract (FV 0 ((a' + b') - (a + b)) us') us
-
-    selfContract xs = fv 0 (altersum xs) FE
-      where
-        altersum FE = 0
-        altersum (FV _ a cs) = a + altersum cs
+expand :: FV -> FV -> FV
+expand _ FE = FE
+expand FE _ = FE
+expand (FV a b xs) (FV c d ys)
+    | c + d <= b  = fv (a + c) d       $ expand (FV 0 (b - (c + d)) xs) ys
+    | c <= b      = fv (a + c) (b - c) $ expand xs (FV 0 (d - (b - c)) ys)
+    | otherwise   = fv (a + b) 0       $ expand xs (FV (c - b) d ys)
+
+primContract :: FV -> FV -> FV
+primContract x FE = FE
+primContract (FV a' b' us') (FV a b us)
+    | a' + b' <= a = fv b'       0 $ primContract us' (FV (a - (a' + b')) b us)
+    | otherwise    = fv (a - a') b $ primContract (FV 0 ((a' + b') - (a + b)) us') us
+
+contract :: FV -> FV -> FV
+contract a b = primContract (a <> b) a
+
+--    selfContract a = primContract a a
+selfContract :: FV -> FV
+selfContract xs = fv 0 (altersum xs) FE
+  where
+    altersum FE = 0
+    altersum (FV _ a cs) = a + altersum cs
 
 prop_expand_normal_FV (a :: FV) b = testNormalFV (expand a b)
 prop_contract_normal_FV (a :: FV) b = testNormalFV (contract a b)
 
-prop_diffTestFV1 = diffTest :: D1 FV -> Bool
-prop_diffTestFV2 = diffTest :: D2 FV -> Bool
-prop_diffTestFV3 = diffTest :: D3 FV -> Bool
-
-prop_assocTestL_FV = assocTestL :: D3 FV -> Bool
-prop_assocTestR_FV = assocTestR :: D3 FV -> Bool
+prop_monoid_Expand_FV = prop_Monoid (T :: T Expand)
+{-
+--prop_diffTestFV1 = diffTest :: D1 FV -> Bool
+--prop_diffTestFV2 = diffTest :: D2 FV -> Bool
+--prop_diffTestFV3 = diffTest :: D3 FV -> Bool
 
-instance StreamLike FV where
-    type StreamElem FV = Bool
+--prop_assocTestL_FV = assocTestL :: D3 FV -> Bool
+--prop_assocTestR_FV = assocTestR :: D3 FV -> Bool
+-}
 
-    sIndex FE i = False
-    sIndex (FV n l us) i = i >= n && (i < l || sIndex us (i - l - n))
+sIndex :: FV -> Nat -> Bool
+sIndex FE i = False
+sIndex (FV n l us) i = i >= n && (i < l || sIndex us (i - l - n))
 
-    sDrop _ FE = FE
-    sDrop n (FV i j us)
-        | i + j <= n   = sDrop (n - (i + j)) us
-        | n <= i       = FV (i - n) j us
-        | otherwise    = FV 0 (j - (n - i)) us
+sDrop :: Nat -> FV -> FV
+sDrop _ FE = FE
+sDrop n (FV i j us)
+    | i + j <= n   = sDrop (n - (i + j)) us
+    | n <= i       = FV (i - n) j us
+    | otherwise    = FV 0 (j - (n - i)) us
 
 ------------------------------------------------
 
@@ -244,14 +231,6 @@ onTail f n (FV i j us)
     | n <= i       = fv n 0 $ f $ FV (i - n) j us
     | otherwise    = fv i (n - i) $ f $ FV 0 (j - (n - i)) us
 
--- usedFVs s = filter (sIndex s) [0..]
--- TODO: remove
-usedFVs :: FV -> [Nat]
-usedFVs = f 0
-  where
-    f _ FE = []
-    f s (FV i a xs) = [s+i..(s+i+a)-1] ++ f (s+i+a) xs
-
 -- downFV i u = if sIndex u i then Just $ fv 0 i (FO 1) `contract` u else Nothing
 downFV :: Nat -> FV -> Maybe FV
 downFV i FE = Just FE
@@ -265,7 +244,7 @@ fO i = FV i 10000 FE
 
 mkUp l n = fv 0 l $ fO n
 
---upFV l n = expand (fv 0 l $ FO n)
+--upFV l n = expand (mkUp l n)
 upFV :: Nat -> Nat -> FV -> FV
 upFV l n FE = FE
 upFV l n (FV n' l' us)
@@ -273,16 +252,77 @@ upFV l n (FV n' l' us)
     | l' <= l - n' = FV n' l' $ upFV (l - n' - l') n us
     | otherwise    = FV n' (l - n') $ FV n (l' - (l - n')) us
 
-pattern VarFV i <- FV i _ _
-  where VarFV i =  FV i 1 FE
+--------------------------------------------
+
+type Lens a b = a -> (b, b -> a)
+
+(l1 `lComp` l2) (l1 -> (l2 -> (y, fy), fx)) = (y, fx . fy)
 
-incFV :: FV -> FV
-incFV = FV{-ok-} 0 1
+lConst e = (mempty, const e)
 
--- compact u = r where (_, D2 r _) = cDiffT $ D2 (SFV 0 u) (SFV 1 FE)
-compact :: FV -> FV
-compact xs@(FV 0 _ _) = selfContract xs
-compact xs = fv 1 0 $ selfContract xs
+lId x = (x, id)
+
+lApp' f (a, b) = b (f a)
+
+------------
+
+class HasFV a where
+    fvLens :: Lens a FV
+
+appLens fx (fvLens -> (y, fy)) = (y, fx . fy)
+
+up l n = lApp' (upFV l n) . fvLens
+
+down i (fvLens -> (ux, fx)) = fx <$> downFV i ux
+
+usedVar :: HasFV x => Nat -> x -> Bool
+usedVar i x = sIndex (fst $ fvLens x :: FV) i
+
+instance HasFV FV where
+    fvLens = lId
+
+instance (HasFV a, HasFV b) => HasFV (a, b) where
+    fvLens (fvLens -> (ux, x'), fvLens -> (uy, y')) = (s, \s' -> (x' $ s' `expand` primContract s ux, y' $ s' `expand` primContract s uy)) where
+        s = ux <> uy
+
+--prop_HasFV_D2 (a :: FV) b = contractFV (D2 a b) == diffT (D2 a b)
+--prop_HasFV_D2' (s :: FV) a b = expandFV s (D2 a b) == expandT s (D2 a b)
+
+newtype LamFV u = LamFV {getLamFV :: u}
+    deriving (Eq, Show)
+
+instance HasFV a => HasFV (LamFV a) where
+    fvLens (LamFV (fvLens -> x@(ux, fx))) = (sDrop 1 ux, \s -> LamFV $ lApp' (onTail (const s) 1) x)
+
+--prop_LamFV (u :: FV) = contractFV (LamFV u) == (sDrop 1 u, LamFV $ onTail selfContract 1 u)
+--prop_LamFV' s (u :: FV) = expandFV s (LamFV u) == LamFV (fv 0 1 s `expand` u)
+
+data FVCache a b = FVCache !a !b
+    deriving (Eq, Show)
+
+instance Functor (FVCache a) where
+    fmap f (FVCache a b) = FVCache a (f b)
+
+instance HasFV (FVCache FV x) where
+    fvLens (FVCache u x) = (u, \u -> FVCache u x)
+
+pattern CacheFV a <- FVCache u (lApp' (expand u) . fvLens -> a)
+  where CacheFV (fvLens -> x@(ua, fa)) = FVCache ua $ lApp' selfContract x
+
+instance HasFV a => HasFV [a] where
+    fvLens [] = lConst []
+    fvLens [fvLens -> (u, fx)] = (u, \s -> [fx s])
+    fvLens [fvLens -> (u, fx), fvLens -> (u', fy)] = (s, \s' -> [fx $ s' `expand` primContract s u, fy $ s' `expand` primContract s u' ])
+      where
+        s = u <> u'
+    fvLens (unzip . map fvLens -> (us, fs)) = let
+        s = mconcat us in (s, \s -> zipWith (\f u -> f $ s `expand` primContract s u) fs us)
+
+newtype VarFV = VarFV Nat
+    deriving (Eq, Show)
+
+instance HasFV VarFV where
+    fvLens (VarFV i) = (FV i 1 FE, \(FV i _ _) -> VarFV i)
 
 ---------------------------------------------------------------------------------- skewed free vars set
 
@@ -290,10 +330,6 @@ compact xs = fv 1 0 $ selfContract xs
 data SFV = SFV !Nat !FV
     deriving (Eq, Show)
 
-padSFV (SFV n x) = SFV n $ fv 0 n $ sDrop n x
-
-fromSFV (SFV n u) = sDrop n u
-
 instance PShow SFV where pShow (SFV n x) = pShow n <> pShow x
 
 instance Arbitrary SFV where
@@ -302,22 +338,22 @@ instance Arbitrary SFV where
 instance Monoid SFV where
     mempty = SFV 0 mempty
 
-    SFV m b `mappend` SFV n a = SFV (n + m) $ b <> fv m 0 a
+    SFV m b `mappend` SFV n a = SFV (n + m) $ sDrop n b <> a
 
 prop_monoid_SFV = prop_Monoid (T :: T SFV)
 
-instance Expandable SFV where
-
-    expandT (padSFV -> SFV n b) = flip evalState b . traverse (\(SFV n a) -> state $ \u -> (SFV n $ u `expand` a, sDrop n u))
-
-    primContractT (padSFV -> SFV _ b) = flip evalState b . traverse (\(SFV n a) -> state $ \u -> (SFV n $ u `primContract` a, sDrop n u))
+instance HasFV SFV where
+    fvLens (SFV n u) = (u, SFV n)
+{-
+--prop_diffTest1_SFV = diffTest :: D1 SFV -> Bool
+--prop_diffTest2_SFV = diffTest :: D2 SFV -> Bool
+--prop_diffTest3_SFV = diffTest :: D3 SFV -> Bool
 
-prop_diffTest1_SFV = diffTest :: D1 SFV -> Bool
-prop_diffTest2_SFV = diffTest :: D2 SFV -> Bool
-prop_diffTest3_SFV = diffTest :: D3 SFV -> Bool
+--prop_assocTestL_SFV = assocTestL :: D3 SFV -> Bool
+--prop_assocTestR_SFV = assocTestR :: D3 SFV -> Bool
+-}
 
-prop_assocTestL_SFV = assocTestL :: D3 SFV -> Bool
-prop_assocTestR_SFV = assocTestR :: D3 SFV -> Bool
+-----------------------------------------------------
 
 return []
 main = $quickCheckAll
diff --git a/prototypes/Inspector.hs b/prototypes/Inspector.hs
index 1d88577e..317fc326 100644
--- a/prototypes/Inspector.hs
+++ b/prototypes/Inspector.hs
@@ -139,7 +139,7 @@ programs = cycle $ map stepList
     , iterate (\x -> x `App` x) id_ !! 5
     , twiceTest 2
     , twiceTest 3
-    , twiceTest2
+    , twiceTest2 2
     , t' 20
     , t'' 20
     ]
@@ -149,7 +149,7 @@ main = do
   hSetBuffering stdout NoBuffering
   getArgs >>= \case
     ["twice"] -> pPrint $ hnf $ twiceTest 3
-    ["twice2"] -> pPrint $ hnf twiceTest2
+    ["twice2"] -> pPrint $ hnf $ twiceTest2 3
     [b, n] ->
         putStrLn $ ppShow $ hnf $ case b of
             "lazy" -> t' $ read n
diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs
index d878bcb4..f5375d7f 100644
--- a/prototypes/LamMachine.hs
+++ b/prototypes/LamMachine.hs
@@ -7,7 +7,10 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module LamMachine where
 
@@ -16,6 +19,8 @@ import Data.Word
 import Data.Int
 import Data.Monoid
 import Data.Maybe
+--import Data.Foldable (toList)
+import qualified SplayList as F
 import Control.Arrow hiding ((<+>))
 import Control.Category hiding ((.), id)
 import Control.Monad
@@ -28,20 +33,20 @@ import FreeVars
 --------------------------------------------------------------------- data structures
 
 data Lit
-    = LInt  !Int
-    | LChar !Char
+    = LInt   !Int
+    | LChar  !Char
     | LFloat !Double
     deriving Eq
 
-data Exp_
-    = Var_
-    | Lam_ VarInfo !Exp
-    | Let_ VarInfo !Exp !Exp
-    | Con_  ConInfo !Int [Exp]
-    | Case_ CaseInfo !Exp ![Exp]
-    | Lit_ !Lit
-    | Op1_ !Op1 !Exp
-    | Op2_ !Op2 !Exp !Exp
+data Exp
+    = Var_  !VarFV
+    | Lam_  VarInfo  !(FVCache FV (LamFV Exp))
+    | Let_  VarInfo  !(FVCache FV (Exp, LamFV Exp))
+    | Con_  ConInfo !Int (FVCache FV [Exp])
+    | Case_ CaseInfo !(FVCache FV (Exp, [Exp]))
+    | Lit  !Lit
+    | Op1  !Op1 !Exp
+    | Op2_ !Op2 !(FVCache FV (Exp, Exp))
     deriving (Eq, Show)
 
 data Op1 = HNFMark | YOp | Round
@@ -55,29 +60,54 @@ pattern App a b     = Op2 AppOp a b
 pattern Seq a b     = Op2 SeqOp a b
 pattern Int i       = Lit (LInt i)
 
-infixl 4 `App`
+pattern Var i       = Var_ (VarFV i)
+pattern Lam n i     = Lam_ n (CacheFV (LamFV i))
+pattern Let n i x   <- Let_ n (CacheFV (i, LamFV x))
+  where Let _ _ (down 0 -> Just x) = x
+        Let n i x   =  Let_ n (CacheFV (i, LamFV x))
+pattern Con a b i   = Con_ a b (CacheFV i)
+pattern Case a b c  = Case_ a (CacheFV (b, c))
+pattern Op2 op a b  = Op2_ op (CacheFV (a, b))
 
--- cached and compressed free variables set
-data Exp = Exp !FV !Exp_
-    deriving (Eq, Show)
+infixl 4 `App`
 
 data EnvPiece
-    = ELet   VarInfo !Exp
-    | EDLet1 VarInfo !DExp
-    | ECase_ CaseInfo !FV ![Exp]
-    | EOp2_1 !Op2 !Exp
-    | EOp2_2 !Op2 !Exp
+    = ELet_   VarInfo !Exp
+    | EDLet1_ VarInfo !(LamFV DExp)
+    | ECase_ CaseInfo !(FVCache FV [Exp])
+    | EOp2_1_ !Op2 !Exp
+    | EOp2_2_ !Op2 !Exp
     deriving (Eq, Show)
 
-data DExp
-    = DExpNil   -- variable
-    | DExpCons_ !FV !EnvPiece !DExp
-    deriving (Eq, Show)
+pattern ELet i x   = ELet_ i x
+pattern EDLet1 i x = EDLet1_ i (LamFV x)
+pattern ECase op b = ECase_ op (CacheFV b)
+pattern EOp2_1 i x = EOp2_1_ i x
+pattern EOp2_2 i x = EOp2_2_ i x
 
-data DEnv
-    = DEnvNil
-    | DEnvCons !EnvPiece !DEnv
-    deriving (Eq, Show)
+type DEnv = F.SplayList EnvPiece
+
+pattern DEnvNil = F.Nil
+
+pattern DEnvCons :: EnvPiece -> DEnv -> DEnv
+pattern DEnvCons p e = F.Cons p e
+
+instance F.Measured EnvPiece where
+    type Measure EnvPiece = Nat
+    measure = \case
+        ELet_{} -> 1
+        _ -> 0
+--instance HasSFV DExp where
+
+
+type DExp = DEnv
+
+pattern DExpNil = DEnvNil
+
+pattern DExpCons :: EnvPiece -> DExp -> DExp
+pattern DExpCons p e = F.Snoc e p
+
+infixr 4 `DEnvCons`, `DExpCons`
 
 -- state of the machine
 data MSt = MSt !DEnv !Exp
@@ -89,122 +119,40 @@ type VarInfo = String
 type ConInfo = String
 type CaseInfo = [(String, [String])]
 
---------------------------------------------------------------------- pattern synonyms
-
-infixr 4 `DEnvCons`, `DExpCons`
+--------------------------------------------------------------------- instances
+
+instance HasFV Exp where
+    fvLens = \case
+        Op1    op e -> appLens (Op1 op) e
+        Op2_   op e -> appLens (Op2_ op) e
+        Con_ x op e -> appLens (Con_ x op) e
+        Case_  op e -> appLens (Case_ op) e
+        Let_   op e -> appLens (Let_ op) e
+        Lam_   op e -> appLens (Lam_ op) e
+        Var_      e -> appLens Var_ e
+        Lit l       -> lConst $ Lit l
+
+instance HasFV EnvPiece where
+    fvLens = \case
+        EOp2_1_ op e -> appLens (EOp2_1_ op) e
+        EOp2_2_ op e -> appLens (EOp2_2_ op) e
+        ECase_  op e -> appLens (ECase_ op) e
+        ELet_   op e -> appLens (ELet_ op) e
+        EDLet1_ op e -> appLens (EDLet1_ op) e
 
-pattern ECase op e <- ECase_ op u (map (upp u) -> e)
-  where ECase op b = ECase_ op u bz where (u, bz) = deltas b
-
-pattern EnvPiece sfv p <- (getEnvPiece -> (sfv, p))
-  where EnvPiece sfv@(SFV n u') = \case
-            EOp2_1 op e -> EOp2_1 op (uppS sfv e)
-            EOp2_2 op e -> EOp2_2 op (uppS sfv e)
-            ECase_ s u es -> ECase_ s (expand u' u) es
-            ELet n (Exp u e) -> ELet n (Exp (sDrop 1 u' `expand` u) e)
-            EDLet1 n z -> EDLet1 n $ uppDE u' 1 z
-
-getEnvPiece = \case
-    EOp2_1 op (Exp u e) -> (SFV 0 u, EOp2_1 op (Exp (selfContract u) e))
-    EOp2_2 op (Exp u e) -> (SFV 0 u, EOp2_2 op (Exp (selfContract u) e))
-    ECase_ s u es -> (SFV 0 u, ECase_ s (selfContract u) es)
-    ELet n (Exp u e) -> (SFV 1 $ fv 1 0 u, ELet n $ Exp (selfContract u) e)
-    EDLet1 n DExpNil -> (mempty, EDLet1 n DExpNil)
-    EDLet1 n (DExpCons_ u x y) -> (SFV 0 $ sDrop 1 u, EDLet1 n $ DExpCons_ (onTail selfContract 1 u) x y)
-
-uppS (SFV _ x) (Exp u a) = Exp (expand x u) a
-
-pattern DExpCons :: EnvPiece -> DExp -> DExp
-pattern DExpCons a b <- (getDExpCons -> (a, b))
-  where DExpCons (EnvPiece ux a) DExpNil = DExpCons_ (fromSFV s) (EnvPiece ux' a) DExpNil
-          where (s, D1 ux') = diffT $ D1 ux
-        DExpCons (ELet _ a) (dDown 0 -> Just d) = d
-        DExpCons (EnvPiece ux a) (DExpCons_ u x y) = DExpCons_ (fromSFV s) (EnvPiece ux' a) (DExpCons_ u' x y)
-          where (s, D2 (SFV 0 u') ux') = diffT $ D2 (SFV 0 u) ux
-
-getDExpCons (DExpCons_ u x@(EnvPiece (SFV n _) _) b) = (uppEP u x, uppDE u n b)
-
-uppEP u (EnvPiece (SFV n x) y) = EnvPiece (SFV n $ onTail (u `expand`) n x) y
-
-upP i j = uppEP $ mkUp i j
-
-incFV' (SFV n u) = SFV (n + 1) $ incFV u
-
-uppDE :: FV -> Nat -> DExp -> DExp
-uppDE a _ DExpNil = DExpNil
-uppDE a n (DExpCons_ u x y) = DExpCons_ (onTail (expand a) n u) x y
-
-dDown i DExpNil = Just DExpNil
-dDown i (DExpCons_ u a b) = DExpCons_ <$> downFV i u <*> pure a <*> pure b
-
----------------------------------------------------------------------
-
-pattern Lit i       <- Exp _ (Lit_ i)
-  where Lit i       =  Exp mempty $ Lit_ i
-pattern Op2 op a b  <- Exp u (Op2_ op (upp u -> a) (upp u -> b))
-  where Op2 op a b  =  Exp s $ Op2_ op az bz where (s, az, bz) = delta2 a b
-pattern Op1 op a    <- Exp u (Op1_ op (upp u -> a))
-  where Op1 op (Exp ab x) = Exp ab $ Op1_ op $ Exp (selfContract ab) x
-pattern Var' i      =  Exp (VarFV i) Var_
-pattern Var i       =  Var' i
-pattern Lam n i           <- Exp u (Lam_ n (upp (incFV u) -> i))
-  where Lam n (Exp vs ax) = Exp (sDrop 1 vs) $ Lam_ n $ Exp (compact vs) ax
-pattern Con a b i   <- Exp u (Con_ a b (map (upp u) -> i))
-  where Con a b x   =  Exp s $ Con_ a b bz where (s, bz) = deltas x
-pattern Case a b c  <- Exp u (Case_ a (upp u -> b) (map (upp u) -> c))
-  where Case cn a b =  Exp s $ Case_ cn az bz where (s, az: bz) = deltas $ a: b
-
-pattern Let n i x   <- Exp u (Let_ n (upp u -> i) (upp (incFV u) -> x))
-  where Let _ _ (down 0 -> Just x) = x
-        Let n a b   =  Exp s (Let_ n a' b') where (s, a', Lam _ b') = delta2 a $ Lam n b
+---------------------------
 
-pattern InHNF a    <- (getHNF -> Just a)
-  where InHNF a@Lit{}        = a
-        InHNF a@Lam{}        = a
+pattern InHNF a <- (getHNF -> Just a)
+  where InHNF a@Lit{}           = a
+        InHNF a@Lam{}           = a
         InHNF a@(Op1 HNFMark _) = a
-        InHNF a              = Op1 HNFMark a
+        InHNF a                 = Op1 HNFMark a
 
 getHNF x = case x of
-    Lit{} -> Just x
-    Lam{} -> Just x
+    Lit{}         -> Just x
+    Lam{}         -> Just x
     Op1 HNFMark a -> Just a
-    _ -> Nothing
-
-delta2 (Exp ua a) (Exp ub b) = (s, Exp ua' a, Exp ub' b)
-  where
-    (s, ua', ub') = delta2' ua ub
-
-delta2' ua ub = (s, primContract s ua, primContract s ub)
-  where
-    s = ua <> ub
-
-deltas [] = (mempty, [])
-deltas [Exp x e] = (x, [Exp (selfContract x) e]) 
-deltas [Exp ua a, Exp ub b] = (s, [Exp (primContract s ua) a, Exp (primContract s ub) b])
-  where
-    s = ua <> ub
-deltas es = (s, [Exp (primContract s u) e | (u, Exp _ e) <- zip xs es])
-  where
-    xs = [ue | Exp ue _ <- es]
-
-    s = mconcat xs
-
-upp :: FV -> Exp -> Exp
-upp a (Exp b e) = Exp (expand a b) e
-
-up l n (Exp us x) = Exp (upFV l n us) x
-
--- free variables set
---fvs (Exp us _) = usedFVs us
-
-usedVar i (Exp us _) = sIndex us i
-
-usedVar' i DExpNil = False
-usedVar' i (DExpCons_ u _ _) = sIndex u i
-
-down i (Exp us e) = Exp <$> downFV i us <*> pure e
-
----------------------------
+    _             -> Nothing
 
 initSt :: Exp -> MSt
 initSt e = MSt DEnvNil e
@@ -221,30 +169,27 @@ hnf = justResult . initSt
 data StepTag = Begin String | End String | Step String
   deriving Show
 
-type GenSteps e
-    = e
-   -> (StepTag -> MSt -> e)
-   -> MSt -> e
-
-focusNotUsed (MSt (EDLet1 _ x `DEnvCons` _) _) = not $ usedVar' 0 x
+focusNotUsed (EDLet1 _ x `DEnvCons` _) = False --not $ usedVar 0 x
 focusNotUsed _ = True
 
 inHNF :: MSt -> Bool
 inHNF (MSt _ (InHNF _)) = True
 inHNF _ = False
 
-steps :: forall e . GenSteps e
+steps :: forall e . e -> (StepTag -> MSt -> e) -> MSt -> e
 steps nostep bind (MSt vs e) = case e of
 
+    e | EDLet1 _ (down 0 -> Just d) `DEnvCons` vs <- vs -> zipUp e vs d
+
     Con cn i xs
-        | lz == 0 || focusNotUsed (MSt vs e) -> step (cn ++ " hnf") $ MSt vs $ InHNF e
+        | focusNotUsed vs || lz == 0 -> step (cn ++ " hnf") $ MSt vs $ InHNF e
         | otherwise -> step (cn ++ " copy") $ MSt (foldr DEnvCons vs $ ELet "" <$> zs) $ InHNF $ Con cn i xs'  -- share complex constructor arguments
       where
         lz = Nat $ length zs
         (xs', concat -> zs) = unzip $ f 0 xs
         f i [] = []
         f i (x: xs) | simple x = (up 0 lz x, []): f i xs
-                    | otherwise = (Var' i, [up 0 (lz - i - 1) x]): f (i+1) xs
+                    | otherwise = (Var i, [up 0 (lz - i - 1) x]): f (i+1) xs
 
     -- TODO: handle recursive constants
     Y x             -> step "Y"     $ MSt vs $ App x (Y x)
@@ -257,14 +202,15 @@ steps nostep bind (MSt vs e) = case e of
 
         DEnvNil -> nostep
 
-        ELet n x `DEnvCons` vs -> step "goUp" $ MSt vs $ InHNF $ Let n x $ InHNF a
-        x `DEnvCons` vs | Let n y e <- a -> step "pakol" $ MSt (upP 0 1 x `DEnvCons` ELet n y `DEnvCons` vs) e
+        ELet n x `DEnvCons` vs -> step "goUp" $ MSt vs $ InHNF $ Let n x $ InHNF a  -- TODO: speed up?
+        x `DEnvCons` vs | Let n y e <- a -> step "pakol" $ MSt (up 0 1 x `DEnvCons` ELet n y `DEnvCons` vs) e   -- TODO: speed up
         x `DEnvCons` vs -> case x of
             ECase cns cs -> end "case" $ case a of
                 Con cn i es -> MSt vs $ foldl App (cs !! i) es  -- TODO: remove unused cases
                 _           -> MSt vs $ InHNF $ Case cns (InHNF a) cs
             EOp2_1 AppOp b -> end "AppOp" $ case a of
                 Lam _ (down 0 -> Just x) -> MSt vs x   -- TODO: remove b
+                -- TODO: optimize out Var 0 application
                 Lam n x -> MSt (ELet n b `DEnvCons` vs) x
                 _       -> MSt vs $ InHNF $ App (InHNF a) b
             EOp2_1 SeqOp b -> end "SeqOp" $ case a of
@@ -282,17 +228,17 @@ steps nostep bind (MSt vs e) = case e of
                     int LessEq a b = if a <= b then T else F
                     int EqInt a b = if a == b then T else F
                 _ -> MSt vs $ InHNF $ Op2 op b (InHNF a)
-            EDLet1 _ (dDown 0 -> Just d) -> zipUp (InHNF a) vs d
             EDLet1 n d -> zipUp (up 0 1 a) (ELet n (InHNF a) `DEnvCons` vs) d
 
   where
-    zipDown 0 e (ELet n z `DEnvCons` zs) = MSt (EDLet1 n e `DEnvCons` zs) z
-    zipDown j e (z@ELet{} `DEnvCons` zs) = zipDown (j-1) (z `DExpCons` e) zs
-    zipDown j e (z `DEnvCons` zs) = zipDown j (z `DExpCons` e) zs
+    zipDown j e (F.split (> j) -> (t, ELet n z `DEnvCons` zs))
+        = MSt (EDLet1 n (f e t) `DEnvCons` zs) z
+      where
+        f e t = t <> e
 
-    zipUp x xs DExpNil = end "var" $ MSt xs x
-    zipUp x xs (DExpCons a@ELet{} as) = zipUp (up 0 1 x) (a `DEnvCons` xs) as
-    zipUp x xs (DExpCons a as) = zipUp x (a `DEnvCons` xs) as
+    zipUp x xs e = end "var" $ MSt (e <> xs) $ up 0 n x
+      where
+        n = F.measure e
 
     begin t = bind (Begin t)
     next t  = bind (Step t)
@@ -318,7 +264,7 @@ class ViewShow a where
 
 instance ViewShow Exp where
   viewShow vi = pShow where
-    pShow e@(Exp fv x) = showFE green vi fv $
+    pShow e = showFE green vi (fst $ fvLens e :: FV) $
       case {-if vi then Exp_ (selfContract fv) x else-} e of
         Var (Nat i)  -> DVar i
         Let n a b   -> shLet n (pShow a) $ pShow b
@@ -366,7 +312,7 @@ instance ViewShow MSt where
             EOp2_2 op x -> shOp2 op (pShow x) y
 
         h n DExpNil = onred $ white $ DVar n
-        h n z@(DExpCons p (h (adj p n) -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of
+        h n z@(DExpCons p (h (adj p n) -> y)) = showFE blue vi (fst $ fvLens p :: FV) $ case p of
             EDLet1 n x -> shLet n y (h 0 x)
             ELet n x -> shLet n (pShow x) y
             ECase cns xs -> shCase cns y pShow xs
@@ -446,7 +392,7 @@ sum' = Y $ Lam "sum" $ Lam "xs" $ caseList (Var 0) (Int 0) $ Lam "y" $ Lam "ys"
 
 infixl 4 `sApp`
 
-sApp a b = Seq b (App a b)
+sApp a b = Lam "s" (Seq (Var 0) (a `App` Var 0)) `App` b
 
 {-
 accsum acc [] = acc
@@ -477,14 +423,14 @@ inc = Lam "n" $ Op2 Add (Var 0) (Int 1)
 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 = twice2 `App` twice2 `App` twice2 `App` twice2 `App` inc `App` Int 0
+twiceTest2 n = (Lam "twice" $ (iterate (`App` Var 0) (Var 0) !! n) `App` inc `App` Int 0) `App` twice2
 
 tests
     =   hnf test == hnf (Int 13)
     &&  hnf test' == hnf (Int 14)
     &&  hnf test'' == hnf (Int 4)
     &&  hnf (t' 10) == hnf (Int 55)
-    &&  hnf (t'' 10) == hnf (Int 55)
+--    &&  hnf (t'' 10) == hnf (Int 55)
 
 
 
diff --git a/prototypes/SplayList.hs b/prototypes/SplayList.hs
new file mode 100644
index 00000000..fee995ed
--- /dev/null
+++ b/prototypes/SplayList.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module SplayList
+    ( SplayList (..)
+    , pattern Cons, pattern Snoc
+    , Measured (..)
+    , split
+    ) where
+
+import Prelude hiding (null)
+import Control.Applicative hiding (empty)
+import Control.Monad
+import Control.Arrow
+
+import Data.Function
+import Data.Data
+import Data.Maybe
+import Data.Monoid
+
+import FreeVars
+
+------------------------------------------------------------------------
+
+data SplayList a
+    = Nil
+    | Singleton a
+    | Append_ !(Measure a) !FV (SplayList a) (SplayList a)
+    deriving (Typeable)
+
+deriving instance (Show a, Show (Measure a)) => Show (SplayList a)
+
+toList = go []
+  where
+    go i    Nil = i
+    go i   (Singleton a) = a: i
+    go acc (Append l r) = go (go acc r) l
+
+instance (Measured a, Eq a)  => Eq (SplayList a)  where (==)    = (==)    `on` toList
+instance (Measured a, Ord a) => Ord (SplayList a) where compare = compare `on` toList
+
+--------------------------------------------
+
+class (HasFV a, Measure a ~ Nat) => Measured a where
+    type Measure a :: *
+    measure :: a -> Measure a
+
+instance Measured a => Monoid (SplayList a) where
+    mempty  = Nil
+    Nil `mappend` ys  = ys
+    xs  `mappend` Nil = xs
+    xs  `mappend` ys  = Append xs ys
+
+instance (Measured a, HasFV a) => HasFV (SplayList a) where
+    fvLens = \case
+        Nil -> lConst Nil
+        Singleton (fvLens -> (s, f)) -> (s, Singleton . f)
+        Append_ n s l r -> (s, \s -> Append_ n s l r)
+
+instance (Measured a) => Measured (SplayList a) where
+    type Measure (SplayList a) = Measure a
+    measure Nil = mempty
+    measure (Singleton a) = measure a
+    measure (Append_ n _ _ _) = n
+
+--------------------------------------------
+
+getAppend (Append_ _ s x@(fvLens -> ~(ux, x')) z@(fvLens -> ~(uz, z')))
+    = Just (x' $ fv 0 (measure z) s `expand` ux, z' $ s `expand` uz)
+getAppend _ = Nothing
+
+pattern Append :: () => Measured a => SplayList a -> SplayList a -> SplayList a
+pattern Append l r <- (getAppend -> Just (l, r))
+  where Append x@(fvLens -> (ux, x')) z@(fvLens -> (uz, z')) = Append_ us s (x' ux') (z' uz')
+          where
+            SFV us s = SFV (measure x) ux <> SFV mz uz
+
+            mz = measure z
+
+            ux' = fv 0 mz s `primContract` ux
+            uz' = s `primContract` uz
+
+pattern Cons a as <- (viewl -> Just (a, ascendL -> as))
+  where Cons a as = Singleton a <> as
+
+viewl Nil = Nothing
+viewl xs = Just $ go [] xs
+  where
+    go xs (Singleton a) = (a, xs)
+    go xs (Append l r)  = go (r: xs) l
+
+ascendL [] = Nil
+ascendL (x: xs) = go x xs
+  where
+    go !a = \case
+        [] -> a
+        b: [] -> a `app` b
+        b: c: xs -> go (a `app` Append b c) xs
+
+    Append a b `app` c = Append a (Append b c)
+    a `app` b = Append a b
+
+pattern Snoc as a <- (viewr -> Just (a, ascendR -> as))
+  where Snoc as a = as <> Singleton a
+
+viewr Nil = Nothing
+viewr xs = Just $ go [] xs
+  where
+    go xs (Singleton a) = (a, xs)
+    go xs (Append l r) = go (l: xs) r
+
+ascendR [] = Nil
+ascendR (x: xs) = go x xs
+  where
+    go !c = \case
+        [] -> c
+        a: [] -> a `app` c
+        b: a: xs -> go (Append a b `app` c) xs
+
+    a `app` Append b c = Append (Append a b) c
+    a `app` b = Append a b
+
+-- | Split a list at the point where the predicate on the measure changes from False to True.
+split :: Measured a => (Nat -> Bool) -> SplayList a -> (SplayList a, SplayList a)
+split _ Nil = (Nil, Nil)
+split p xs
+    | p mempty       = (Nil, xs)
+    | p (measure xs) = go mempty [] [] xs
+    | otherwise      = (xs, Nil)
+  where
+    go m ls rs = \case
+        Append l r
+            | p n       -> go m ls (r: rs) l
+            | otherwise -> go n (l: ls) rs r
+          where
+            n = m <> measure l
+
+        xs  | p (m <> measure xs) -> (ascendR ls, ascendL $ xs: rs)
+            | otherwise           -> (ascendR $ xs: ls, ascendL rs)
+