refactoring

1 files changed, 85 insertions, 123 deletions

diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs
index b869285e..5dce0829 100644
--- a/prototypes/LamMachine.hs
+++ b/prototypes/LamMachine.hs
@@ -27,7 +27,6 @@ data Exp_
     | Y_ Exp
     | Int_ Int
     | Lam_ Exp
-    | Let_ Exp Exp
 
     | App_ Exp Exp
     | Seq_ Exp Exp
@@ -46,79 +45,108 @@ data Op2 = Add | Sub | Mod | LessEq | EqInt
 data Exp = Exp {dbUps :: [Up], maxFreeVars :: Int, expexp :: Exp_ }
 
 -- state of the machine
-data MSt = MSt [(FreeVars, Exp)]  -- TODO: use finger tree instead of list
+data MSt = MSt Exp   -- TODO: use finger tree instead of lets?
                Exp
-               [Exp]  -- TODO: use finger tree instead of list
+               [Exp]  -- TODO: use finger tree instead of list?
 
 --------------------------------------------------------------------- toolbox: pretty print
 
 instance PShow Exp where
     pShow e@(Exp u t x) = case e of -- shUps' u t $ case Exp [] t x of
-        Var i -> DVar i
-        App a b -> DApp (pShow a) (pShow b)
-        Seq a b -> DOp "`seq`" (Infix 1) (pShow a) (pShow b)
-        Lam e -> shLam_ True $ pShow e
-        Let a b -> shLet_ (pShow a) $ pShow b
-        Con s i xs -> foldl DApp (text s) $ pShow <$> xs
-        Int i -> pShow i
-        Op1 o x -> text (show o) `DApp` pShow x
+        Var i       -> DVar i
+        Let a b     -> shLet (pShow a) $ pShow b
+        App a b     -> DApp (pShow a) (pShow b)
+        Seq a b     -> DOp "`seq`" (Infix 1) (pShow a) (pShow b)
+        Lam e       -> shLam $ pShow e
+        Con s i xs  -> foldl DApp (text s) $ pShow <$> xs
+        Int i       -> pShow i
+        Op1 o x     -> text (show o) `DApp` pShow x
         Op2 EqInt x y -> DOp "==" (Infix 4) (pShow x) (pShow y)
         Op2 Add x y -> DOp "+" (InfixL 6) (pShow x) (pShow y)
-        Op2 o x y -> text (show o) `DApp` pShow x `DApp` pShow y
-        Y e -> "Y" `DApp` pShow e
-        Case e xs -> DPreOp (-20) (ComplexAtom "case" (-10) (pShow e) (SimpleAtom "of")) $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- xs]
+        Op2 o x y   -> text (show o) `DApp` pShow x `DApp` pShow y
+        Y e         -> "Y" `DApp` pShow e
+        Case e xs   -> DPreOp (-20) (ComplexAtom "case" (-10) (pShow e) (SimpleAtom "of"))
+                        $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- xs]
+
+instance PShow MSt where
+    pShow (MSt as b bs) = case foldl (flip (:)) (DBrace (pShow b): [pShow x |  x <- bs]) $ [pShow as] of
+        x: xs -> foldl (flip shLet) x xs
 
 shUps a b = DPreOp (-20) (SimpleAtom $ show a) b
 shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b
 
-shLam_ usedVar b = DFreshName usedVar $ showLam (DVar 0) b
+shLam b = DFreshName True $ 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
 
-shLet i a b = DLet' (DLet "=" (blue $ shVar i) $ DUp i a) (DUp i b)
+shLet a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b
 
 showLet x (DFreshName u d) = DFreshName u $ showLet (DUp 0 x) d
 showLet x (DLet' xs y) = DLet' (DSemi x xs) y
 showLet x y = DLet' x y
 
-shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b
-
-instance PShow MSt where
-    pShow (MSt as b bs) = case foldl (flip (:)) (DBrace (pShow b): [pShow x |  x <- bs]) [pShow x | EPP x <- as] of
-        x: xs -> foldl (flip shLet_) x xs
-
 
 --------------------------------------------------------------------- toolbox: free variables
 
-maxFreeVars' (Exp u k _) = upsFreeVars' u k
-
-upsFreeVars xs s = foldr rearr s xs
-
-upsFreeVars' xs s = foldr rearr' s xs
+maxFreeVars' (Exp xs s _) = foldl' f s xs
   where
-    rearr' (Up l n) m
-        | l >= m = m      -- TODO: remove
-        | otherwise = n + m
+    f m (Up l n) = n + m
 
-upVarIndex xs s = foldr rearr' s xs
+upVarIndex xs s = foldr f s xs
   where
-    rearr' (Up l n) i
+    f (Up l n) i
         | l > i = i
         | otherwise = n + i
 
+upp u x = foldr up x u
+
+up' l n = up $ Up l n
+
+up :: Up -> Exp -> Exp
+up (Up i 0) e = e
+up u@(Up i num) e@(Exp us s x) = Exp (insertUp_ s u us) s x
+
+insertUp_ s u@(Up i _) []
+    | i >= s = []
+    | otherwise = [u]
+insertUp_ s u@(Up l n) us_@(u'@(Up l' n'): us)
+    | l < l' = u: us_
+    | l >= l' && l <= l' + n' = Up l' (n' + n): us
+    | otherwise = u': insertUp_ s (Up (l-n') n) us
 
 -- TODO: remove
-instance HasFreeVars Exp where
-    getFreeVars (Exp us fv e) = upsFreeVars us $ FreeVars $ 2^fv - 1
+insertUp (Up l 0) us = us
+insertUp u [] = [u]
+insertUp u@(Up l n) us_@(u'@(Up l' n'): us)
+    | l < l' = u: us_
+    | l >= l' && l <= l' + n' = Up l' (n' + n): us
+    | otherwise = u': insertUp (Up (l-n') n) us
 
+-- TODO: remove if possible
 fvs (Exp us fv _) = gen 0 $ foldr f [fv] us  where
     f (Up l n) xs = l: l+n: map (+n) xs
     gen i (a: xs) = [i..a-1] ++ gen' xs
     gen' [] = []
     gen' (a: xs) = gen a xs
 
+usedVar' i (Exp us fv _) = f i us where
+    f i [] = i < fv
+    f i (Up l n: us)
+        | l > i = f i us
+        | i < l + n = False
+        | otherwise = f (n + i) us
+
+down i0 e0@(Exp us fv e) = f i0 us where
+    f i []
+        | i < fv = Nothing
+        | otherwise = Just $ Exp [] fv e
+    f i (u@(Up j n): us)
+        | i < j = up' (j-1) n <$> f i us
+        | i >= j + n = up u <$> f (i-n) us
+        | otherwise = Just $ up' j (n-1) $ Exp us fv e
+
 upss u (Exp _ i e) = Exp u i e
 
 dup2 f ax bx = Exp s (maxFreeVars' az `max` maxFreeVars' bz) $ f az bz  where
@@ -149,11 +177,6 @@ dupLam f e@(Exp a fv ax) = Exp (ff a) (max 0 $ fv - 1) $ f $ Exp (gg a) fv ax
     ff (Up 0 n: us) = insertUp (Up 0 $ n - 1) $ incUp (-1) <$> us
     ff us = incUp (-1) <$> us
 
--- (\x -> e) f           x = f in e
-dupLet f z w = case Lam w `App` z of
-    Exp a fv (App_ (Exp b fv' (Lam_ c)) d) -> Exp a fv $ Let_ d c 
-
-
 pattern Int i <- Exp _ _ (Int_ i)
   where Int i =  Exp [] 0 $ Int_ i
 pattern App a b <- Exp u _ (App_ (upp u -> a) (upp u -> b))
@@ -169,24 +192,14 @@ pattern Var i <- Exp u _ (Var_ (upVarIndex u -> i))
         Var i =  Exp [Up 0 i] 1 $ Var_ 0
 pattern Lam i <- Exp u _ (Lam_ (upp (incUp 1 <$> u) -> i))
   where Lam i =  dupLam Lam_ i
-pattern Let i x <- Exp u _ (Let_ (upp u -> i) (upp (incUp 1 <$> u) -> x))
-  where Let i x =  dupLet Let_ i x
 pattern Y i <- Exp u _ (Y_ (upp u -> i))
   where Y i =  dup1 Y_ i
 pattern Con a b i <- Exp u _ (Con_ a b (map (upp u) -> i))
   where Con a b i =  dupCon (Con_ a b) i
 pattern Case a b <- Exp u _ (Case_ (upp u -> a) (map (second $ upp u) -> b))
   where Case a b =  dupCase Case_ a b
---pattern Ups op a <- Exp _ (Ups_ op a)
---  where Ups op a =  Exp (
-
-upp u x = foldr up x u
-
-up :: Up -> Exp -> Exp
-up u@(Up i num) e@(Exp us s x)
-    | dbGE'' i e = e
-    | otherwise = addUp u e
 
+pattern Let i x = App (Lam x) i
 
 infixl 4 `App`
 
@@ -197,8 +210,6 @@ data Up = Up !Int{-level-} !Int{-num-}
 
 incUp t (Up l n) = Up (l+t) n
 
-rearr (Up l n) = rearrangeFreeVars (RFUp n) l
-
 showUps us n = foldr f (replicate n True) us where
     f (Up l n) is = take l is ++ replicate n False ++ drop l is
 
@@ -261,46 +272,11 @@ diffUpsTest' = diffUpsTest [x,y] --diffUpsTest x y
     x = ([Up 1 2, Up 3 4, Up 8 2], 20)
     y = ([Up 2 2, Up 5 1, Up 6 2, Up 7 2], 18)
 
-insertUp u@(Up l 0) us = us
-insertUp u@(Up l n) [] = [u]
-insertUp u@(Up l n) us_@(u'@(Up l' n'): us)
-    | l < l' = u: us_
-    | l >= l' && l <= l' + n' = Up l' (n' + n): us
-    | otherwise = u': insertUp (Up (l-n') n) us
-
-addUp u (Exp us k e) = Exp (insertUp u us) k e  -- TODO: remove excess ups?
-
-ups' a b = ups $ Up a b
-
-ups :: Up -> [(FreeVars, Exp)] -> [(FreeVars, Exp)]
-ups l [] = []
-ups l@(Up i _) xs@((s,  e): es)
-    | dbGE i s = xs
-    | otherwise = eP (up l e) $ ups (incUp 1 l) es
-
-eP x [] = [(getFreeVars x,  x)]
-eP x xs@((s, _):_) = (getFreeVars x <> lowerFreeVars s,  x): xs
-
-pattern EPP x <- (_,  x)
+getLets (Let x y) = x: getLets y
+getLets x = [x]
 
 ---------------------------
 
-down i x | usedVar i x = Nothing
-down i x = Just $ down_ i x
-
-dbGE' l m = l >= m
-
-dbGE'' l m = dbGE' l $ maxFreeVars' m
-
-down_ i e
-    | dbGE'' i e = e
-down_ i0 e0@(Exp us ii e) = f i0 us e where
-    f i [] e = error $ "-- - -  -- " ++ show (i0, i) ++ "     " ++ ppShow e0  --(pushUps e) --"show down_ i e
-    f i (u@(Up j n): us) e
-        | i < j = addUp (Up (j-1) n) $ f i us e
-        | i >= j + n = addUp u $ f (i-n) us e
-        | otherwise = addUp (Up j $ n-1) $ Exp us ii e
-
 tryRemoves xs = tryRemoves_ (Var <$> xs)
 tryRemoves_ [] dt = dt
 tryRemoves_ (Var i: vs) dt
@@ -312,30 +288,16 @@ tryRemove i x = fromMaybe x $ tryRemove_ i x
 
 tryRemove_ i dt@(MSt xs e es)
     | Just e' <- down i e
-    , Just xs' <- downUp i xs
+    , Just xs' <- down (i+1) xs
     , Just es' <- downDown i es
     = Just $ MSt xs' e' es'
     | otherwise
     = Nothing
 
-downEP i ( x) =  down i x
-downEP_ i (s,  x) = (delVar i s, down_ i x)
-
-downUp i [] = Just []
-downUp i x@((s, _): _)
-    | usedVar (i+1) s = Nothing
-    | otherwise = Just $ downUp_ i x
-
-downUp_ i [] = []
-downUp_ i (x: xs)
-    | x' <- downEP_ (i+1) x
-    , xs' <- downUp_ (i+1) xs
-    = x': xs'
-
 downDown i [] = Just []
 downDown 0 (_: xs) = Just xs
 downDown i (x: xs)
-    | Just x' <- downEP (i-1) x
+    | Just x' <- down (i-1) x
     , Just xs' <- downDown (i-1) xs
     = Just $ x': xs'
     | otherwise = Nothing
@@ -382,14 +344,14 @@ step dt@(MSt t e vs) = case e of
     Lam{} -> return dt
 
     Con cn i xs
-        | lz /= 0 -> return $ MSt (ups' 1 lz t) (Con cn i xs') $ zs ++ vs  -- share complex constructor arguments
+        | lz /= 0 -> return $ MSt (up' 1 lz t) (Con cn i xs') $ zs ++ vs  -- share complex constructor arguments
         | otherwise -> return dt
       where
         lz = length zs
         (xs', concat -> zs) = unzip $ f 0 xs
         f i [] = []
-        f i (x: xs) | simple x = (up (Up 0 lz) x, []): f i xs
-                    | otherwise = (Var i, [up (Up 0 (lz - i - 1)) x]): f (i+1) xs
+        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
 
     Var i -> lookupHNF "var" (\e _ -> e) i dt
 
@@ -398,22 +360,22 @@ step dt@(MSt t e vs) = case e of
         Lam{} -> stepMsg "seq" $ tryRemoves (fvs a) $ MSt t b vs
         Con{} -> stepMsg "seq" $ tryRemoves (fvs a) $ MSt t b vs
         Var i -> lookupHNF' "seqvar" (\e (Seq _ b) -> b) i dt
-        _      -> stepMsg "seqexp" $ MSt (ups' 1 1 t) (Seq (Var 0) $ up (Up 0 1) b) $  a: vs
+        _      -> stepMsg "seqexp" $ MSt (up' 1 1 t) (Seq (Var 0) $ up' 0 1 b) $  a: vs
 
     -- TODO: handle recursive constants
-    Y (Lam x) -> stepMsg "Y" $ MSt (ups' 1 1 t) x $ e: vs
+    Y (Lam x) -> stepMsg "Y" $ MSt (up' 1 1 t) x $ e: vs
 
     App a b -> case a of
-        Lam x | usedVar 0 x
-                -> stepMsg "app" $ MSt (ups' 1 1 t) x $ b: vs
+        Lam x | usedVar' 0 x
+                -> stepMsg "app" $ MSt (up' 1 1 t) x $ b: vs
         Lam x   -> stepMsg "appdel" $ tryRemoves (fvs b) $ MSt t x vs
         Var i   -> lookupHNF' "appvar" (\e (App _ y) -> App e y) i dt
-        _       -> stepMsg "appexp" $ MSt (ups' 1 1 t) (App (Var 0) $ up (Up 0 1) b) $  a: vs
+        _       -> stepMsg "appexp" $ MSt (up' 1 1 t) (App (Var 0) $ up' 0 1 b) $  a: vs
 
     Case a cs -> case a of
         Con cn i es -> stepMsg "case" $ tryRemoves (nub $ foldMap (fvs . snd) $ delElem i cs) $ (MSt t (foldl App (snd $ cs !! i) es) vs)
         Var i -> lookupHNF' "casevar" (\e (Case _ cs) -> Case e cs) i dt
-        _     -> stepMsg "caseexp" $ MSt (ups' 1 1 t) (Case (Var 0) $ second (up (Up 0 1)) <$> cs) $ a: vs
+        _     -> stepMsg "caseexp" $ MSt (up' 1 1 t) (Case (Var 0) $ second (up' 0 1) <$> cs) $ a: vs
 
     Op2 op x y -> case (x, y) of
         (Int e, Int f) -> return $ MSt t (int op e f) vs
@@ -425,9 +387,9 @@ step dt@(MSt t e vs) = case e of
             int EqInt a b = if a == b then T else F
         (Var i, _) -> lookupHNF' "op2-1var" (\e (Op2 op _ y) -> Op2 op e y) i dt
         (_, Var i) -> lookupHNF' "op2-2var" (\e (Op2 op x _) -> Op2 op x e) i dt
-        (Int{}, _) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op x (Var 0)) $ y: vs
-        (_, Int{}) -> stepMsg "op2" $ MSt (ups' 1 1 t) (Op2 op (Var 0) y) $ x: vs
-        _          -> stepMsg "op2" $ MSt (ups' 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs
+        (Int{}, _) -> stepMsg "op2" $ MSt (up' 1 1 t) (Op2 op x (Var 0)) $ y: vs
+        (_, Int{}) -> stepMsg "op2" $ MSt (up' 1 1 t) (Op2 op (Var 0) y) $ x: vs
+        _          -> stepMsg "op2" $ MSt (up' 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs
 
 stepMsg :: MachineMonad m => String -> MSt -> m MSt
 stepMsg msg dt = do
@@ -435,15 +397,15 @@ stepMsg msg dt = do
     collectSizeStat $ size dt
     step dt
 
-hnf e = stepMsg "hnf" $ MSt [] e []
+hnf e = stepMsg "hnf" $ MSt (Var 0) e []
 
-size (MSt xs _ ys) = length xs + length ys
+size (MSt xs _ ys) = length (getLets xs) + length ys
 
-shiftL (MSt xs x (e: es)) = MSt (eP x xs) e es
-shiftR (MSt (EPP x: xs) e es) = MSt xs x $ e: es
+shiftL (MSt xs x (e: es)) = MSt (Let x xs) e es
+shiftR (MSt (Let x xs) e es) = MSt xs x $ e: es
 
 shiftLookup f n dt@(MSt _ e _) = repl $ iterate shiftR dt !! (n+1) where
-    repl (MSt xs z es) = MSt xs (f (up (Up 0 (n+1)) e) z) es
+    repl (MSt xs z es) = MSt xs (f (up' 0 (n+1) e) z) es
 
 -- lookup var in head normal form
 lookupHNF msg f i dt = tryRemove i . shiftLookup f i <$> stepMsg msg (iterate shiftL dt !! (i+1))
@@ -478,7 +440,7 @@ test = runMachinePure (id_ `App` id_ `App` id_ `App` id_ `App` Con "()" 0 [])
 
 test' = runMachinePure (id_ `App` (id_ `App` Con "()" 0 []))
 
-foldr_ f e = Y $ Lam $ Lam $ caseList (Var 0) (up (Up 0 2) e) (Lam $ Lam $ up (Up 0 4) f `App` Var 1 `App` (Var 3 `App` Var 0))
+foldr_ f e = Y $ Lam $ Lam $ caseList (Var 0) (up' 0 2 e) (Lam $ Lam $ up' 0 4 f `App` Var 1 `App` (Var 3 `App` Var 0))
 
 filter_ p = foldr_ (Lam $ Lam $ if_ (p `App` Var 1) (Cons (Var 1) (Var 0)) (Var 0)) Nil