1 files changed, 86 insertions, 191 deletions

diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs
index f88062b0..e95960d2 100644
--- a/prototypes/LamMachine.hs
+++ b/prototypes/LamMachine.hs
@@ -11,43 +11,51 @@
 module LamMachine where
 
 import Data.List
+import Data.Word
+import Data.Int
+import Data.Monoid
 import Data.Maybe
-import Control.Arrow
+import Control.Arrow hiding ((<+>))
 import Control.Category hiding ((.), id)
---import Debug.Trace
+import Control.Monad
+import Debug.Trace
 
 import LambdaCube.Compiler.Pretty
 
+import FreeVars
+
 --------------------------------------------------------------------- data structures
 
 data Exp_
     = Var_
     | Int_ !Int     -- ~ constructor with 0 args
-    | Lam_ Exp
-    | Con_ String Int [Exp]
-    | Case_ [String]{-for pretty print-} Exp [Exp]  -- --> simplify
-    | Op1_ !Op1 Exp
-    | Op2_ !Op2 Exp Exp
-
-data Op1 = YOp | Round
+    | Lam_ !Exp
+    | Op1_ !Op1 !Exp
+    | Con_ String !Int [Exp]
+    | Case_ [String]{-for pretty print-} !Exp ![Exp]  -- --> simplify
+    | Op2_ !Op2 !Exp !Exp
+    deriving Eq
+
+data Op1 = HNF_ !Int | YOp | Round
     deriving (Eq, Show)
 
 data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt
     deriving (Eq, Show)
 
 -- cached and compressed free variables set
-type FV = [Int]
-
-data Exp = Exp !FV Exp_
+data Exp = Exp_ !FV !Exp_
+    deriving Eq
 
 -- state of the machine
-data MSt = MSt Exp Exp [Exp]
+data MSt = MSt Exp Exp ![Exp]
+    deriving Eq
 
 --------------------------------------------------------------------- toolbox: pretty print
 
 instance PShow Exp where
-    pShow e@(Exp _ x) = case e of -- shUps' u t $ case Exp [] t x of
-        Var i       -> DVar i
+    pShow e@(Exp_ fv _) = --(("[" <> pShow fv <> "]") <+>) $
+      case e of
+        Var (Nat 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)
@@ -55,6 +63,7 @@ instance PShow Exp where
         Con s i xs  -> foldl DApp (text s) $ pShow <$> xs
         Int i       -> pShow i
         Y e         -> "Y" `DApp` pShow e
+        Op1 (HNF_ i) x -> DGlue (InfixL 40) (onred $ white $ if i == -1 then "this" else pShow i) $ DBrace (pShow x)
         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)
@@ -63,8 +72,7 @@ instance PShow Exp where
                         $ foldr1 DSemi [DArr_ "->" (text a) (pShow b) | (a, b) <- zip cn 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
+    pShow (MSt as b bs) = pShow $ foldl (flip Let) (Let (HNF (-1) b) as) bs
 
 shUps a b = DPreOp (-20) (SimpleAtom $ show a) b
 shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) b
@@ -84,48 +92,29 @@ showLet x y = DLet' x y
 
 --------------------------------------------------------------------- pattern synonyms
 
-pattern Int i       <- Exp _ (Int_ i)
-  where Int i       =  Exp [0] $ Int_ 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 a    =  dup1 (Op1_ op) a
-pattern Var i       <- Exp (varIndex -> i) Var_
-  where Var 0       =  Exp [1] Var_
-        Var i       =  Exp [0, i, i+1] Var_
-pattern Lam i       <- Exp u (Lam_ (upp ((+1) <$> u) -> i))
-  where Lam i       =  dupLam i
-pattern Con a b i   <- Exp u (Con_ a b (map (upp u) -> i))
-  where Con a b []  =  Exp [0] $ Con_ a b []
-        Con a b [x]  =  dup1 (Con_ a b . (:[])) x
-        Con a b [x, y] = Exp s $ Con_ a b [xz, yz] where (s, xz, yz) = delta2 x y
-        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 Int i       <- Exp_ _ (Int_ i)
+  where Int i       =  Exp_ mempty $ Int_ 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_ (delUnused ab) x
+pattern Var' i      =  Exp_ (VarFV i) Var_
+pattern Var i       =  Var' i
+pattern Lam i       <- Exp_ u (Lam_ (upp (incFV u) -> i))
+  where Lam (Exp_ vs ax) = Exp_ (del1 vs) $ Lam_ $ 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 i x     = App (Lam x) i
 pattern Y a         = Op1 YOp a
+pattern HNF i a     = Op1 (HNF_ i) a
 pattern App a b     = Op2 AppOp a b
 pattern Seq a b     = Op2 SeqOp a b
 
 infixl 4 `App`
 
-varIndex (_: i: _) = i
-varIndex _ = 0
-
-dupLam (Exp vs ax) = Exp (f vs) $ Lam_ $ Exp (g vs) ax
-  where
-    f (0: nus) = 0 .: map (+(-1)) nus
-    f us = map (+(-1)) us
-
-    g xs@(0: _) = [0, 1, altersum xs + 1]
-    g xs = [altersum xs]
-
-dup1 f (Exp ab x) = Exp ab $ f $ Exp [altersum ab] x
-
-altersum [x] = x
-altersum (a: b: cs) = a - b + altersum cs
-
 initSt :: Exp -> MSt
 initSt e = MSt (Var 0) e []
 
@@ -136,98 +125,50 @@ size (MSt xs _ ys) = length (getLets xs) + length ys
     getLets (Let x y) = x: getLets y
     getLets x = [x]
 
---------------------------------------------------------------------- toolbox: de bruijn index shifting
-
-upp [k] ys = ys
-upp (x: y: xs) ys = upp xs (up x (y - x) ys)
-
-up i 0 e = e
-up i num (Exp us x) = Exp (f i (i + num) us) x
+delta2 (Exp_ ua a) (Exp_ ub b) = (s, Exp_ (delFV ua s) a, Exp_ (delFV ub s) b)
   where
-    f l n [s]
-        | l >= s    = [s]
-        | otherwise = [l, n, s+n-l]
-    f l n us_@(l': n': us)
-        | l <  l'   = l : n: map (+(n-l)) us_
-        | l <= n'   = l': n' + n - l: map (+(n-l)) us
-        | otherwise = l': n': f l n us
+    s = ua <> ub
 
--- free variables set
-fvs (Exp us _) = gen 0 us  where
-    gen i (a: xs) = [i..a-1] ++ gen' xs
-    gen' [] = []
-    gen' (a: xs) = gen a xs
-
-(.:) :: Int -> [Int] -> [Int]
-a .: (x: y: xs) | a == x = y: xs
-a .: xs = a: xs
-
-usedVar i (Exp us _) = f us where
-    f [fv] = i < fv
-    f (l: n: us) = i < l || i >= n && f us
-
-down i (Exp us e) = Exp <$> f us <*> pure e where
-    f [fv]
-        | i < fv = Nothing
-        | otherwise = Just [fv]
-    f vs@(j: vs'@(n: us))
-        | i < j  = Nothing
-        | i < n  = Just $ j .: map (+(-1)) vs'
-        | otherwise = (j:) . (n .:) <$> f us
-
-delta2 (Exp (add0 -> ua) a) (Exp (add0 -> ub) b) = (add0 s, Exp (dLadders 0 ua s) a, Exp (dLadders 0 ub s) b)
+deltas [] = (mempty, [])
+deltas [Exp_ x e] = (x, [Exp_ (delUnused x) e]) 
+deltas [Exp_ ua a, Exp_ ub b] = (s, [Exp_ (delFV ua s) a, Exp_ (delFV ub s) b])
   where
-    s = iLadders ua ub
-
-deltas [] = ([0], [])
-deltas es = (add0 s, [Exp (dLadders 0 u s) e | (u, Exp _ e) <- zip xs es])
+    s = ua <> ub
+deltas es = (s, [Exp_ (delFV u s) e | (u, Exp_ _ e) <- zip xs es])
   where
-    xs = [add0 ue | Exp ue _ <- es]
+    xs = [ue | Exp_ ue _ <- es]
 
-    s = foldr1 iLadders xs
+    s = mconcat xs
 
-iLadders :: [Int] -> [Int] -> [Int]
-iLadders x [] = x
-iLadders [] x = x
-iLadders x@(a: b: us) x'@(a': b': us')
-    | b <= a' = addL a b $ iLadders us x'
-    | b' <= a = addL a' b' $ iLadders x us'
-    | otherwise = addL (min a a') c $ iLadders (addL c b us) (addL c b' us')
-  where
-    c = min b b'
+upp :: FV -> Exp -> Exp
+upp a (Exp_ b e) = Exp_ (compFV a b) e
 
-addL a b cs | a == b = cs
-addL a b (c: cs) | b == c = a: cs
-addL a b cs = a: b: cs
+up l n (Exp_ us x) = Exp_ (upFV l n us) x
+
+-- free variables set
+fvs (Exp_ us _) = usedFVs us
 
-add0 [] = [0]
-add0 (0: cs) = cs
-add0 cs = 0: cs
+usedVar i (Exp_ us _) = usedFV i us
 
-dLadders :: Int -> [Int] -> [Int] -> [Int]
-dLadders s [] x = [s]
-dLadders s x@(a: b: us) x'@(a': b': us')
-    | b' <= a  = addL s (s + b' - a') $ dLadders (s + b' - a') x us'
-    | a' <  a  = addL s (s + a - a') $ dLadders (s + a - a') x (addL a b' us')
-    | a' == a  = dLadders (s + b - a) us (addL b b' us')
+down i (Exp_ us e) = Exp_ <$> downFV i us <*> pure e
 
 ---------------------------
 
-tryRemoves xs = tryRemoves_ (Var <$> xs)
+tryRemoves xs = tryRemoves_ (Var' <$> xs)
 
 tryRemoves_ [] dt = dt
-tryRemoves_ (Var i: vs) dt = maybe (tryRemoves_ vs dt) (\(is, st) -> tryRemoves_ (is ++ catMaybes (down i <$> vs)) st) $ tryRemove_ i dt
+tryRemoves_ (Var' i: vs) dt = maybe (tryRemoves_ vs dt) (\(is, st) -> tryRemoves_ (is ++ catMaybes (down i <$> vs)) st) $ tryRemove_ i dt
   where
     tryRemove_ i (MSt xs e es) = (\a b (is, c) -> (is, MSt a b c)) <$> down (i+1) xs <*> down i e <*> downDown i es
 
     downDown i [] = Just ([], [])
-    downDown 0 (x: xs) = Just (Var <$> fvs x, xs)
+    downDown 0 (x: xs) = Just (Var' <$> fvs x, xs)
     downDown i (x: xs) = (\x (is, xs) -> (up 0 1 <$> is, x: xs)) <$> down (i-1) x <*> downDown (i-1) xs
 
 ----------------------------------------------------------- machine code begins here
 
 justResult :: MSt -> MSt
-justResult = steps id (const ($)) (const (.))
+justResult = steps 0 id (const ($)) (const (.))
 
 hnf = justResult . initSt
 
@@ -242,23 +183,23 @@ type GenSteps e
 
 type StepTag = String
 
-steps :: forall e . GenSteps e
-steps nostep {-ready-} bind cont dt@(MSt t e vs) = case e of
+steps :: forall e . Int -> GenSteps e
+steps lev nostep {-ready-} bind cont dt@(MSt t e vs) = case e of
 
     Int{} -> nostep dt --ready "hnf int"
     Lam{} -> nostep dt --ready "hnf lam"
 
     Con cn i xs
-        | lz /= 0 -> step "copy con" $ MSt (up 1 lz t) (Con cn i xs') $ zs ++ vs  -- share complex constructor arguments
+        | lz > 0 -> step "copy con" $ MSt (up 1 lz t) (Con cn i xs') $ zs ++ vs  -- share complex constructor arguments
         | otherwise -> nostep dt --ready "hnf con"
       where
-        lz = length zs
+        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
 
-    Var i -> lookupHNF_ rec "var" const i dt
+    Var i -> lookupHNF_ nostep "var" const i dt
 
     Seq a b -> case a of
         Int{}   -> step "seq" $ MSt t b vs
@@ -297,27 +238,29 @@ steps nostep {-ready-} bind cont dt@(MSt t e vs) = case e of
         (_, Int{}) -> step "op2" $ MSt (up 1 1 t) (Op2 op (Var 0) y) $ x: vs
         _          -> step "op2" $ MSt (up 1 2 t) (Op2 op (Var 0) (Var 1)) $ x: y: vs
   where
-    rec = steps nostep bind cont
+    rec i = steps i nostep bind cont
 
     step :: StepTag -> MSt -> e
-    step t = bind t rec
+    step t = bind t (rec lev)
 
     hnf :: (MSt -> e) -> MSt -> e
-    hnf f = cont "hnf" f rec
+    hnf f = cont "hnf" f (rec $ 1 + lev)
+
+    hnfTag (MSt a b c) = MSt a (HNF lev b) c
 
     -- lookup var in head normal form
-    lookupHNF_ :: (MSt -> e) -> StepTag -> (Exp -> Exp -> Exp) -> Int -> MSt -> e
-    lookupHNF_ end msg f i dt = bind msg (hnf shiftLookup) $ iterate shiftL dt !! (i+1)
+    lookupHNF_ :: (MSt -> e) -> StepTag -> (Exp -> Exp -> Exp) -> Nat -> MSt -> e
+    lookupHNF_ end msg f i@(Nat i') dt = bind msg (hnf shiftLookup) $ iterate shiftL (hnfTag dt) !! (i'+1)
       where
         shiftLookup dt@(MSt _ e _)
-            = case iterate shiftR dt !! (i+1) of
-                MSt xs z es -> bind "shiftR" (tryRemove i) $ MSt xs (f (up 0 (i+1) e) z) es
+            = case iterate shiftR dt !! (i'+1) of
+                MSt xs (HNF lev z) es -> bind "shiftR" (tryRemove i) $ MSt xs (f (up 0 (i+1) e) z) es
 
         tryRemove i st = {-maybe (end st)-} (bind "remove" end) $ tryRemoves [i] st
 
     -- lookup & step
-    lookupHNF' :: StepTag -> (Exp -> Exp -> Exp) -> Int -> MSt -> e
-    lookupHNF' msg f i dt = lookupHNF_ rec msg f i dt
+    lookupHNF' :: StepTag -> (Exp -> Exp -> Exp) -> Nat -> MSt -> e
+    lookupHNF' msg f i dt = lookupHNF_ (rec lev) msg f i dt
 
     shiftL (MSt xs x (e: es)) = MSt (Let x xs) e es
 
@@ -348,9 +291,9 @@ if_ b t f = caseBool b f t
 
 not_ x = caseBool x T F
 
-test = runMachinePure (id_ `App` id_ `App` id_ `App` id_ `App` Con "()" 0 [])
+test = hnf (id_ `App` id_ `App` id_ `App` id_ `App` Int 13)
 
-test' = runMachinePure (id_ `App` (id_ `App` Con "()" 0 []))
+test' = hnf (id_ `App` (id_ `App` Int 14))
 
 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))
 
@@ -401,60 +344,12 @@ primes = 2:3: filter (\n -> and $ map (\p -> n `mod` p /= 0) (takeWhile (\x -> x
 main = primes !! 3000
 -}
 
+tests
+    =   test == hnf (Int 13)
+    &&  test' == hnf (Int 14)
+    &&  hnf (Lam (Int 4) `App` Int 3) == hnf (Int 4)
+    &&  hnf (t' 10) == hnf (Int 55)
+    &&  hnf (t'' 10) == hnf (Int 55)
 
 
--------------------------------------------------------------
-
-{- alternative presentation
-
-sect [] xs = xs
-sect xs [] = xs
-sect (x:xs) (y:ys) = (x || y): sect xs ys
-
-diffUps a b = diffUps' 0 (back a) (back b)
-
-diffUps' n u [] = (+(-n)) <$> u
-diffUps' n [] _ = []
-diffUps' n (x: xs) (y: ys)
-    | x < y = (x - n): diffUps' n xs (y: ys)
-    | x == y = diffUps' (n+1) xs ys
-
-back = map fst . filter (not . snd) . zip [0..]
-
-mkUps = f 0
-  where
-    f i [] = []
-    f i (x: xs) = insertUp (Up (x-i) 1) $ f (i+1) xs
-
-showUps us n = foldr f (replicate n True) us where
-    f (Up l n) is = take l is ++ replicate n False ++ drop l is
-
-deltaUps_ (map $ uncurry showUps -> us) = (mkUps $ back s, [mkUps $ u `diffUps` s | u <- us])
-  where
-    s = foldr1 sect $ us
-
-joinUps a b = foldr insertUp b a
-
-diffUpsTest xs
-    | and $ zipWith (\a (b, _) -> s `joinUps` a == b) ys xs = show (s, ys)
-    | otherwise = error $ unlines $ map (show . toLadder) xs ++ "----": map show xs ++ "-----": show s: show s_: "-----": map show ys ++ "------": map (show . joinUps s) ys
-  where
-    (s, ys) = deltaUps_ xs
-    s_ = foldr1 iLadders $ toLadder <$> xs
-
-diffUpsTest' = diffUpsTest [x,y] --diffUpsTest x y
-
---x = ([Up 8 2], 200)
---y = ([], 28)
-x = ([Up 1 2, Up 3 4, Up 8 2], 200)
-y = ([Up 2 2, Up 5 1, Up 6 2, Up 7 2], 28)
-
--- TODO: remove
-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
--}