refactoring

1 files changed, 123 insertions, 117 deletions

diff --git a/prototypes/LamMachine.hs b/prototypes/LamMachine.hs
index 6fbd3f73..0a80ea2c 100644
--- a/prototypes/LamMachine.hs
+++ b/prototypes/LamMachine.hs
@@ -47,16 +47,32 @@ data Op2 = AppOp | SeqOp | Add | Sub | Mod | LessEq | EqInt
 data Exp = Exp_ !FV !Exp_
     deriving (Eq, Show)
 
--------------------
-
 data EnvPiece
-    = ELet   Exp
-    | EDLet1 DExp
-    | ECase_  FV [String] [Exp]
-    | EOp2_1 Op2 Exp
-    | EOp2_2 Op2 Exp
+    = ELet   !Exp
+    | EDLet1 !DExp
+    | ECase_ !FV ![String] ![Exp]
+    | EOp2_1 !Op2 !Exp
+    | EOp2_2 !Op2 !Exp
     deriving (Eq, Show)
 
+data DExp
+    = DExpNil   -- variable
+    | DExpCons_ !FV !EnvPiece !DExp
+    deriving (Eq, Show)
+
+data DEnv
+    = DEnvNil
+    | DEnvCons !EnvPiece !DEnv
+    deriving (Eq, Show)
+
+-- state of the machine
+data MSt = MSt !DEnv !Exp
+    deriving (Eq, Show)
+
+--------------------------------------------------------------------- pattern synonyms
+
+infixr 4 `DEnvCons`, `DExpCons`
+
 pattern ECase op e <- ECase_ u op (map (upp u) -> e)
   where ECase op b = ECase_ u op bz where (u, bz) = deltas b
 
@@ -78,11 +94,6 @@ getEnvPiece = \case
 
 uppS (SFV _ x) (Exp_ u a) = Exp_ (expand x u) a
 
-data DExp
-    = DExpNil   -- variable
-    | DExpCons_ FV EnvPiece DExp
-    deriving (Eq, Show)
-
 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
@@ -93,7 +104,7 @@ pattern DExpCons a b <- (getDExpCons -> (a, b))
 
 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      -- ???
+uppEP u (EnvPiece (SFV n x) y) = EnvPiece (SFV n $ onTail (u `expand`) n x) y
 
 upP i j = uppEP $ mkUp i j
 
@@ -103,99 +114,10 @@ uppDE :: FV -> Nat -> DExp -> DExp
 uppDE a _ DExpNil = DExpNil
 uppDE a n (DExpCons_ u x y) = DExpCons_ (onTail (expand a) n u) x y
 
-data DEnv
-    = DEnvNil
-    | DEnvCons EnvPiece DEnv
-    deriving (Eq, Show)
-
--- state of the machine
-data MSt = MSt DEnv Exp
-    deriving (Eq, Show)
-
-infixr 4 `DEnvCons`, `DExpCons`
-
 dDown i DExpNil = Just DExpNil
 dDown i (DExpCons_ u a b) = DExpCons_ <$> downFV i u <*> pure a <*> pure b
 
---------------------------------------------------------------------- toolbox: pretty print
-
-class ViewShow a where
-    viewShow :: Bool -> a -> Doc
-
-instance ViewShow Exp where
-  viewShow vi = pShow where
-    pShow e@(Exp_ fv x) = showFE green vi fv $
-      case {-if vi then Exp_ (selfContract fv) x else-} e of
-        Var (Nat i)  -> DVar i
-        Let a b     -> shLet (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
-        Y e         -> "Y" `DApp` pShow e
-        InHNF x     -> DBrace (pShow x)
-        Op1 o x     -> text (show o) `DApp` pShow x
-        Op2 o x y   -> shOp2 o (pShow x) (pShow y)
-        Case cn e xs -> shCase cn (pShow e) (pShow <$> xs)
-        Exp_ u Var_ -> onblue $ pShow' u
-        e -> error $ "pShow @Exp: " ++ show e
-
-glueTo = DGlue (InfixR 40)
-
-shCase cn e xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of"))
-                        $ foldr1 DSemi [DArr_ "->" (text a) b | (a, b) <- zip cn xs]
-
-shOp2 AppOp x y = DApp x y
-shOp2 EqInt x y = DOp "==" (Infix 4) x y
-shOp2 Add x y   = DOp "+" (InfixL 6) x y
-shOp2 o x y     = text (show o) `DApp` x `DApp` y
-
-showFE c True fv | fv /= mempty = DGlue (InfixL 40) (c $ pShow' fv)
-showFE _ _ _ = id
-
-pShow' = pShow
-
-instance ViewShow MSt where
-    viewShow vi (MSt env e) = g (onred $ white $ pShow e) env
-      where
-        pShow = viewShow vi
-
-        g y DEnvNil = y
-        g y z@(DEnvCons p env) = flip g env $ {-showFE red vi (case p of EnvPiece f _ -> f) $-} case p of
-            EDLet1 x -> shLet y (h x)
-            ELet x -> shLet (pShow x) y
-            ECase cns xs -> shCase cns y (pShow <$> xs)
-            EOp2_1 op x -> shOp2 op y (pShow x)
-            EOp2_2 op x -> shOp2 op (pShow x) y
-
-        h DExpNil = onred $ white "*" --TODO?
-        h z@(DExpCons p (h -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of
-            EDLet1 x -> shLet y (h x)
-            ELet x -> shLet (pShow x) y
-            ECase cns xs -> shCase cns y (pShow <$> xs)
-            EOp2_1 op x -> shOp2 op y (pShow x)
-            EOp2_2 op x -> shOp2 op (pShow x) y
-
-instance PShow MSt where pShow = viewShow False
-
-
-shUps a b = DPreOp (-20) (SimpleAtom $ show a) b
-shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) 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 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
-
-
---------------------------------------------------------------------- pattern synonyms
+---------------------------------------------------------------------
 
 pattern Int i       <- Exp_ _ (Int_ i)
   where Int i       =  Exp_ mempty $ Int_ i
@@ -215,8 +137,20 @@ pattern Case a b c  <- Exp_ u (Case_ a (upp u -> b) (map (upp u) -> c))
 pattern Let i x    <- App (Lam x) i
   where Let i (down 0 -> Just x) = x
         Let i x     = App (Lam x) i
+
+pattern InHNF a    <- (getHNF -> Just a)
+  where InHNF a@Int{}        = a
+        InHNF a@Lam{}        = a
+        InHNF a@(Op1 HNF_ _) = a
+        InHNF a              = Op1 HNF_ a
+
+getHNF x = case x of
+    Int{} -> Just x
+    Lam{} -> Just x
+    Op1 HNF_ a -> Just a
+    _ -> Nothing
+
 pattern Y a         = Op1 YOp a
-pattern InHNF a     = Op1 HNF_ a
 pattern App a b     = Op2 AppOp a b
 pattern Seq a b     = Op2 SeqOp a b
 
@@ -270,9 +204,6 @@ hnf = justResult . initSt
 
 ----------------
 
-inHNF (InHNF a) = InHNF a
-inHNF a = InHNF a
-
 type GenSteps e
     = (MSt -> e)
    -> (StepTag -> (MSt -> e) -> MSt -> e)
@@ -287,9 +218,6 @@ focusNotUsed _ = True
 steps :: forall e . Int -> GenSteps e
 steps lev nostep bind cont (MSt vs e) = case e of
 
-    Int{} -> step "int hnf" $ MSt vs $ InHNF e
-    Lam{} -> step "lam hnf" $ MSt vs $ InHNF e
-
     Con cn i xs
         | lz == 0 || focusNotUsed (MSt vs e) -> step "con hnf" $ MSt vs $ InHNF e
         | otherwise -> step "copy con" $ MSt (foldr DEnvCons vs $ ELet <$> zs) $ InHNF $ Con cn i xs'  -- share complex constructor arguments
@@ -312,7 +240,7 @@ steps lev nostep bind cont (MSt vs e) = case e of
 
         DEnvNil -> bind "whnf" nostep $ MSt DEnvNil $ InHNF a
 
-        ELet x `DEnvCons` vs -> step "goUp" $ MSt vs $ inHNF $ Let x $ InHNF a
+        ELet x `DEnvCons` vs -> step "goUp" $ MSt vs $ InHNF $ Let x $ InHNF a
         x `DEnvCons` vs | Let y e <- a -> step "pakol" $ MSt (upP 0 1 x `DEnvCons` ELet y `DEnvCons` vs) e
         x `DEnvCons` vs -> case x of
             EOp2_1 SeqOp b -> case a of
@@ -320,16 +248,16 @@ steps lev nostep bind cont (MSt vs e) = case e of
                 Lam{}   -> step "seq" $ MSt vs b   -- TODO: remove a
                 Con{}   -> step "seq" $ MSt vs b   -- TODO: remove a
                 _       -> step "seq hnf" $ MSt vs $ InHNF $ Seq (InHNF a) b
-            EOp2_1 AppOp b -> case a of
-                Lam x | usedVar 0 x -> step "app"    $ MSt (ELet b `DEnvCons` vs) x
-                      | otherwise   -> step "appdel" $ MSt vs x   -- TODO: remove b
-                _     -> step "app hnf" $ MSt vs $ InHNF $ App (InHNF a) b
             ECase cns cs -> case a of
                 Con cn i es -> step "case" $ MSt vs $ foldl App (cs !! i) es  -- TODO: remove unused cases
                 _           -> step "case hnf" $ MSt vs $ InHNF $ Case cns (InHNF a) cs
+            EOp2_1 AppOp b -> case a of
+                Lam (down 0 -> Just x) -> step "appdel" $ MSt vs x   -- TODO: remove b
+                Lam x -> step "app"    $ MSt (ELet b `DEnvCons` vs) x
+                _     -> step "app hnf" $ MSt vs $ InHNF $ App (InHNF a) b
             EOp2_1 op b -> step "op2_2 hnf" $ MSt (EOp2_2 op (InHNF a) `DEnvCons` vs) b
             EOp2_2 op b -> case (b, a) of
-                (InHNF (Int e), Int f) -> step "op-done" $ MSt vs (int op e f)
+                (Int e, Int f) -> step "op-done" $ MSt vs (int op e f)
                   where
                     int Add a b = Int $ a + b
                     int Sub a b = Int $ a - b
@@ -337,7 +265,7 @@ steps lev nostep bind cont (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
                 _ -> step "op2 hnf" $ MSt vs $ InHNF $ Op2 op b (InHNF a)
-            EDLet1 (dDown 0 -> Just d) -> zipUp a vs d
+            EDLet1 (dDown 0 -> Just d) -> zipUp (InHNF a) vs d
             EDLet1 d -> zipUp (up 0 1 a) (ELet (InHNF a) `DEnvCons` vs) d
 
   where
@@ -368,6 +296,84 @@ simple = \case
 
 delElem i xs = take i xs ++ drop (i+1) xs
 
+--------------------------------------------------------------------- toolbox: pretty print
+
+class ViewShow a where
+    viewShow :: Bool -> a -> Doc
+
+instance ViewShow Exp where
+  viewShow vi = pShow where
+    pShow e@(Exp_ fv x) = showFE green vi fv $
+      case {-if vi then Exp_ (selfContract fv) x else-} e of
+        Var (Nat i)  -> DVar i
+        Let a b     -> shLet (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
+        Y e         -> "Y" `DApp` pShow e
+        InHNF x     -> DBrace (pShow x)
+        Op1 o x     -> text (show o) `DApp` pShow x
+        Op2 o x y   -> shOp2 o (pShow x) (pShow y)
+        Case cn e xs -> shCase cn (pShow e) (pShow <$> xs)
+        Exp_ u Var_ -> onblue $ pShow' u
+        e -> error $ "pShow @Exp: " ++ show e
+
+glueTo = DGlue (InfixR 40)
+
+shCase cn e xs = DPreOp (-20) (ComplexAtom "case" (-10) e (SimpleAtom "of"))
+                        $ foldr1 DSemi [DArr_ "->" (text a) b | (a, b) <- zip cn xs]
+
+shOp2 AppOp x y = DApp x y
+shOp2 EqInt x y = DOp "==" (Infix 4) x y
+shOp2 Add x y   = DOp "+" (InfixL 6) x y
+shOp2 o x y     = text (show o) `DApp` x `DApp` y
+
+showFE c True fv | fv /= mempty = DGlue (InfixL 40) (c $ pShow' fv)
+showFE _ _ _ = id
+
+pShow' = pShow
+
+instance ViewShow MSt where
+    viewShow vi (MSt env e) = g (onred $ white $ pShow e) env
+      where
+        pShow = viewShow vi
+
+        g y DEnvNil = y
+        g y z@(DEnvCons p env) = flip g env $ {-showFE red vi (case p of EnvPiece f _ -> f) $-} case p of
+            EDLet1 x -> shLet y (h x)
+            ELet x -> shLet (pShow x) y
+            ECase cns xs -> shCase cns y (pShow <$> xs)
+            EOp2_1 op x -> shOp2 op y (pShow x)
+            EOp2_2 op x -> shOp2 op (pShow x) y
+
+        h DExpNil = onred $ white "*" --TODO?
+        h z@(DExpCons p (h -> y)) = showFE blue vi (case p of EnvPiece f _ -> f) $ case p of
+            EDLet1 x -> shLet y (h x)
+            ELet x -> shLet (pShow x) y
+            ECase cns xs -> shCase cns y (pShow <$> xs)
+            EOp2_1 op x -> shOp2 op y (pShow x)
+            EOp2_2 op x -> shOp2 op (pShow x) y
+
+instance PShow MSt where pShow = viewShow False
+
+
+shUps a b = DPreOp (-20) (SimpleAtom $ show a) b
+shUps' a x b = DPreOp (-20) (SimpleAtom $ show a ++ show x) 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 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
+
+
 ---------------------------------------------------------------------------------------- examples
 
 pPrint = putStrLn . ppShow