diff --git a/SSTG.cabal b/SSTG.cabal
--- a/SSTG.cabal
+++ b/SSTG.cabal
@@ -1,5 +1,5 @@
 name:                SSTG
-version:             0.1.0.3
+version:             0.1.0.4
 synopsis:            STG Symbolic Execution
 description:         Prototype of STG-based Symbolic Execution for Haskell.
 homepage:            https://github.com/AntonXue/SSTG#readme
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -24,10 +24,10 @@
             error str
         LoadOkay state -> do
             putStrLn" **************** INIT ***************"
-            -- putStrLn "Initial state:"
-            -- putStrLn $ pprStateStr state
-            let lds = execute1 200 state
+            putStrLn "Initial state:"
+            putStrLn $ pprStateStr state
             putStrLn "*************** BEGIN ***************"
+            let lds = execute1 40 state
             putStrLn $ pprLivesDeadsStr lds
         LoadGuess state cands -> do
             putStrLn $ pprStateStr state
diff --git a/src/SSTG/Core/Execution/Models.hs b/src/SSTG/Core/Execution/Models.hs
--- a/src/SSTG/Core/Execution/Models.hs
+++ b/src/SSTG/Core/Execution/Models.hs
@@ -52,7 +52,7 @@
 newtype Stack = Stack [Frame] deriving (Show, Eq, Read)
 
 -- | Stack Frame
-data Frame = AltFrame    Var [Alt] Locals
+data Frame = CaseFrame   Var [Alt] Locals
            | ApplyFrame  [Atom]    Locals
            | UpdateFrame MemAddr
            deriving (Show, Eq, Read)
@@ -178,8 +178,8 @@
 -- | Lookup Value
 lookupValue :: Var -> Locals -> Globals -> Maybe Value
 lookupValue var locals globals = case lookupLocals var locals of
-    Nothing  -> lookupGlobals var globals
-    mb_value -> mb_value
+    Nothing -> lookupGlobals var globals
+    mb_val  -> mb_val
 
 -- | Lookup Heap by Variable
 vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)
@@ -187,13 +187,13 @@
     val <- lookupValue var locals globals
     case val of
         LitVal _    -> Nothing
-        MemVal addr -> lookupHeap addr heap >>= \hobj -> return (addr, hobj)
+        MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)
 
 -- | MemAddr Type
 memAddrType :: MemAddr -> Heap -> Maybe Type
 memAddrType addr heap = do
     hobj <- lookupHeap addr heap
-    return $ case hobj of
+    Just $ case hobj of
         Blackhole           -> Bottom
         LitObj lit          -> litType lit
         SymObj (Symbol s _) -> varType s
diff --git a/src/SSTG/Core/Execution/Namer.hs b/src/SSTG/Core/Execution/Namer.hs
--- a/src/SSTG/Core/Execution/Namer.hs
+++ b/src/SSTG/Core/Execution/Namer.hs
@@ -34,10 +34,10 @@
 
 -- | Frame Names
 frameNames :: Frame -> [Name]
-frameNames (UpdateFrame _)         = []
-frameNames (ApplyFrame as lcs)     = concatMap atomNames as ++ localsNames lcs
-frameNames (AltFrame var alts lcs) = varNames var ++ (concatMap altNames alts)
-                                                  ++ localsNames lcs
+frameNames (UpdateFrame _)          = []
+frameNames (ApplyFrame as lcs)      = concatMap atomNames as ++ localsNames lcs
+frameNames (CaseFrame var alts lcs) = varNames var ++ (concatMap altNames alts)
+                                                   ++ localsNames lcs
 
 -- | Alt Names
 altNames :: Alt -> [Name]
diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs
--- a/src/SSTG/Core/Execution/Rules.hs
+++ b/src/SSTG/Core/Execution/Rules.hs
@@ -22,8 +22,8 @@
           | RuleUpdateCThunk
           | RuleUpdateDLit | RuleUpdateDValPtr
 
-          | RuleAltCCaseNonVal
-          | RuleAltDLit | RuleAltDValPtr
+          | RuleCaseCCaseNonVal
+          | RuleCaseDLit | RuleCaseDValPtr
 
           | RuleApplyCFunThunk  | RuleApplyCFunAppOver
           | RuleApplyDReturnFun | RuleApplyDReturnSym
@@ -213,53 +213,53 @@
   -- Stack Independent Rules
 
   -- Atom Lit
-  | Evaluate (Atom (LitAtom lit)) _ <- code = do
-    return ( RuleAtomLit
-           , [state { state_code = Return (LitVal lit) }])
+  | Evaluate (Atom (LitAtom lit)) _ <- code =
+       Just (RuleAtomLit
+            ,[state { state_code = Return (LitVal lit) }])
 
   -- Atom Lit Pointer
   | Evaluate (Atom (VarAtom var)) locals <- code
   , Just (_, hobj) <- vlookupHeap var locals globals heap
-  , LitObj lit     <- hobj = do
-    return ( RuleAtomLitPtr
-           , [state { state_code = Evaluate (Atom (LitAtom lit)) locals }])
+  , LitObj lit     <- hobj =
+       Just (RuleAtomLitPtr
+            ,[state { state_code = Evaluate (Atom (LitAtom lit)) locals }])
 
   -- Rule Atom Val Pointer
   | Evaluate (Atom (VarAtom var)) locals <- code
   , Just (addr, hobj) <- vlookupHeap var locals globals heap
-  , isHeapValueForm hobj = do
-    return ( RuleAtomValPtr
-           , [state { state_code = Return (MemVal addr) }])
+  , isHeapValueForm hobj =
+       Just (RuleAtomValPtr
+            ,[state { state_code = Return (MemVal addr) }])
 
   -- Rule Atom Uninterpreted
   | Evaluate (Atom (VarAtom uvar)) locals <- code
-  , Nothing <- vlookupHeap uvar locals globals heap = do
+  , Nothing <- vlookupHeap uvar locals globals heap =
     let pass_in = LiftAct uvar locals globals heap confs
-    let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in
-    return ( RuleAtomUnInt
-           , [state { state_heap    = heap'
+        LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in
+    in Just (RuleAtomUnInt
+            ,[state { state_heap    = heap'
                     , state_globals = globals'
                     , state_code    = Evaluate (Atom (VarAtom uvar)) locals'
                     , state_names   = confs' }])
 
   -- Prim Function App
-  | Evaluate (PrimApp pfun args) locals <- code = do
+  | Evaluate (PrimApp pfun args) locals <- code =
     let pass_in = LiftAct args locals globals heap confs
-    let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
-    let eval    = SymLitEval pfun (map valueToLit vals)
-    return ( RulePrimApp
-           , [state { state_heap    = heap'
+        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
+        eval    = SymLitEval pfun (map valueToLit vals)
+    in Just (RulePrimApp
+            ,[state { state_heap    = heap'
                     , state_globals = globals'
                     , state_code    = Evaluate (Atom (LitAtom eval)) locals'
                     , state_names   = confs' }])
 
   -- | Rule Con App
-  | Evaluate (ConApp dcon args) locals <- code = do
+  | Evaluate (ConApp dcon args) locals <- code =
     let pass_in = LiftAct args locals globals heap confs
-    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-    let (heapf, addr) = allocHeap (ConObj dcon vals) heap'
-    return ( RuleConApp
-           , [state { state_heap    = heapf
+        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
+        (heapf, addr) = allocHeap (ConObj dcon vals) heap'
+    in Just (RuleConApp
+            ,[state { state_heap    = heapf
                     , state_globals = globals'
                     , state_code    = Return (MemVal addr)
                     , state_names   = confs' }])
@@ -268,12 +268,12 @@
   | Evaluate (FunApp fun args) locals <- code
   , Just (_, hobj)              <- vlookupHeap fun locals globals heap
   , FunObj params expr fun_locs <- hobj
-  , length params == length args = do
+  , length params == length args =
     let pass_in   = LiftAct args locals globals heap confs
-    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-    let fun_locs' = insertLocalsList (zip params vals) fun_locs
-    return ( RuleFunAppExact
-           , [state { state_heap    = heap'
+        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
+        fun_locs' = insertLocalsList (zip params vals) fun_locs
+    in Just (RuleFunAppExact
+            ,[state { state_heap    = heap'
                     , state_globals = globals'
                     , state_code    = Evaluate expr fun_locs'
                     , state_names   = confs' }])
@@ -282,15 +282,15 @@
   | Evaluate (FunApp fun args) locals <- code
   , Just (_, hobj)              <- vlookupHeap fun locals globals heap
   , FunObj params expr fun_locs <- hobj
-  , (_, Left ex_ps)             <- unevenZip params args = do
+  , (_, Left ex_ps)             <- unevenZip params args =
     let pass_in   = LiftAct args locals globals heap confs
-    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-    let fun_locs' = insertLocalsList (zip params vals) fun_locs
-    -- New Fun Object.
-    let pobj      = FunObj ex_ps expr fun_locs'
-    let (heapf, paddr) = allocHeap pobj heap'
-    return ( RuleFunAppUnder
-           , [state { state_heap    = heapf
+        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
+        fun_locs' = insertLocalsList (zip params vals) fun_locs
+        -- New Fun Object.
+        pobj      = FunObj ex_ps expr fun_locs'
+        (heapf, paddr) = allocHeap pobj heap'
+    in Just (RuleFunAppUnder
+            ,[state { state_heap    = heapf
                     , state_globals = globals'
                     , state_code    = Return (MemVal paddr)
                     , state_names   = confs' }])
@@ -298,106 +298,102 @@
   -- Rule Fun App Symbolic
   | Evaluate (FunApp sfun args) locals <- code
   , Just (_, hobj)         <- vlookupHeap sfun locals globals heap
-  , SymObj (Symbol svar _) <- hobj = do
+  , SymObj (Symbol svar _) <- hobj =
     let sname = freshSeededName (varName svar) confs
-    let svar' = Var sname (foldl AppTy (varType svar) (map atomType args))
-    let sym   = Symbol svar' (Just (FunApp sfun args, locals))
-    let (heap', addr) = allocHeap (SymObj sym) heap
-    return ( RuleFunAppSym
-           , [state { state_heap  = heap'
+        svar' = Var sname (foldl AppTy (varType svar) (map atomType args))
+        sym   = Symbol svar' (Just (FunApp sfun args, locals))
+        (heap', addr) = allocHeap (SymObj sym) heap
+    in Just (RuleFunAppSym
+            ,[state { state_heap  = heap'
                     , state_code  = Return (MemVal addr)
                     , state_names = sname : confs }])
 
   -- Rule Fun App ConObj
   | Evaluate (FunApp cvar []) locals <- code
   , Just (addr, hobj) <- vlookupHeap cvar locals globals heap
-  , ConObj _ _        <- hobj = do
-    return ( RuleFunAppConPtr
-           , [state { state_code = Return (MemVal addr) }])
+  , ConObj _ _        <- hobj =
+       Just (RuleFunAppConPtr
+            ,[state { state_code = Return (MemVal addr) }])
 
   -- Rule Fun App Uninterpreted
   | Evaluate (FunApp ufun args) locals <- code
-  , Nothing  <- vlookupHeap ufun locals globals heap = do
+  , Nothing  <- vlookupHeap ufun locals globals heap =
     let pass_in = LiftAct ufun locals globals heap confs
-    let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in
-    return ( RuleFunAppUnInt
-           , [ state { state_heap    = heap'
-                     , state_globals = globals'
-                     , state_code    = Evaluate (FunApp ufun args) locals'
-                     , state_names   = confs' }])
+        LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in
+    in Just (RuleFunAppUnInt
+            ,[state { state_heap    = heap'
+                    , state_globals = globals'
+                    , state_code    = Evaluate (FunApp ufun args) locals'
+                    , state_names   = confs' }])
 
   -- Rule Let
-  | Evaluate (Let bnd expr) locals <- code = do
+  | Evaluate (Let bnd expr) locals <- code =
     let pass_in = LiftAct bnd locals globals heap confs
-    let LiftAct _ locals' globals' heap' confs' = liftBinding pass_in
-    return ( RuleLet
-           , [state { state_heap    = heap'
+        LiftAct _ locals' globals' heap' confs' = liftBinding pass_in
+    in Just (RuleLet
+            ,[state { state_heap    = heap'
                     , state_globals = globals'
                     , state_code    = Evaluate expr locals'
                     , state_names   = confs' }])
 
   -- Rule Case Lit
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
-  , (Alt _ _ expr):_ <- matchLitAlts lit alts = do
-    -- Account for cvar.
+  , (Alt _ _ expr):_ <- matchLitAlts lit alts =
     let locals' = insertLocals cvar (LitVal lit) locals
-    return ( RuleCaseLit
-           , [state { state_code = Evaluate expr locals' }])
+    in Just (RuleCaseLit
+            ,[state { state_code = Evaluate expr locals' }])
 
   -- Rule Case Con Pointer
   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code
   , Just (addr, hobj)     <- vlookupHeap mvar locals globals heap
   , ConObj dcon vals      <- hobj
   , (Alt _ params expr):_ <- matchDataAlts dcon alts
-  , length params == length vals = do
-    -- Account for cvar.
+  , length params == length vals =
     let llist   = (cvar, MemVal addr) : zip params vals
-    let locals' = insertLocalsList llist locals
-    return ( RuleCaseConPtr
-           , [state { state_code = Evaluate expr locals' }])
+        locals' = insertLocalsList llist locals
+    in Just (RuleCaseConPtr
+            ,[state { state_code = Evaluate expr locals' }])
 
   -- Rule Case Any Lit
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
   , []               <- matchLitAlts lit alts
-  , (Alt _ _ expr):_ <- defaultAlts alts = do
-    -- Account for cvar.
+  , (Alt _ _ expr):_ <- defaultAlts alts =
     let locals' = insertLocals cvar (LitVal lit) locals
-    return ( RuleCaseAnyLit
-           , [state { state_code = Evaluate expr locals' }])
+    in Just (RuleCaseAnyLit
+            ,[state { state_code = Evaluate expr locals' }])
 
   -- Rule Case Any Con Pointer
   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code
   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap
   , ConObj dcon _     <- hobj
   , []                <- matchDataAlts dcon alts
-  , (Alt _ _ expr):_  <- defaultAlts alts = do
-    -- Account for cvar.
+  , (Alt _ _ expr):_  <- defaultAlts alts =
     let llist   = (cvar, (MemVal addr)) : []
-    let locals' = insertLocalsList llist locals
-    return ( RuleCaseAnyConPtr
-           , [state { state_code = Evaluate expr locals' }])
+        locals' = insertLocalsList llist locals
+    in Just (RuleCaseAnyConPtr
+            ,[state { state_code = Evaluate expr locals' }])
 
   -- Rule Case Sym
   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code
   , Just (addr, hobj)     <- vlookupHeap mvar locals globals heap
   , SymObj _              <- hobj
   , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)
-  , length (acon_alts ++ def_alts) > 0 = do
+  , length (acon_alts ++ def_alts) > 0 =
     let acon_ins   = map (\a -> LiftAct (mvar, addr, cvar, a)
                                         locals globals heap confs) acon_alts
-    let acon_lifts = map liftSymAlt acon_ins
-    let def_ins    = map (\a -> LiftAct (mvar, addr, cvar, a)
+        acon_lifts = map liftSymAlt acon_ins
+        def_ins    = map (\a -> LiftAct (mvar, addr, cvar, a)
                                         locals globals heap confs) def_alts
-    let def_lifts  = map liftSymAlt def_ins
-    -- Make AltCon states first.
-    let acon_sts   = map (liftedAltToState state) acon_lifts
-    -- Make DEFAULT states next.
-    let all_pcons  = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts
-    let negs       = negatePathCons all_pcons
-    let def_lifts' = map (\(LiftAct (e, _) l g h c) ->
+        def_lifts  = map liftSymAlt def_ins
+        -- Make AltCon states first.
+        acon_sts   = map (liftedAltToState state) acon_lifts
+        -- Make DEFAULT states next.
+        all_pcons  = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts
+        negs       = negatePathCons all_pcons
+        def_lifts' = map (\(LiftAct (e, _) l g h c) ->
                            (LiftAct (e, negs) l g h c)) def_lifts
-    let def_sts    = map (liftedAltToState state) def_lifts'
-    return (RuleCaseSym, acon_sts ++ def_sts)
+        def_sts    = map (liftedAltToState state) def_lifts'
+    in Just (RuleCaseSym, acon_sts ++ def_sts)
 
   -- Stack Dependent Rules
 
@@ -405,17 +401,17 @@
   | Stack frames                         <- stack
   , Evaluate (Atom (VarAtom var)) locals <- code
   , Just (addr, hobj)       <- vlookupHeap var locals globals heap
-  , FunObj [] expr fun_locs <- hobj = do  -- Thunk form.
-    return ( RuleUpdateCThunk
-           , [state { state_stack = Stack (UpdateFrame addr : frames)
+  , FunObj [] expr fun_locs <- hobj = -- Thunk form.
+       Just (RuleUpdateCThunk
+            ,[state { state_stack = Stack (UpdateFrame addr : frames)
                     , state_heap  = insertHeap addr Blackhole heap
                     , state_code  = Evaluate expr fun_locs }])
 
   -- Rule Update Frame Delete Lit
   | Stack (UpdateFrame frm_addr : rest) <- stack
-  , Return (LitVal lit)                 <- code = do
-    return ( RuleUpdateDLit
-           , [state { state_stack = Stack rest
+  , Return (LitVal lit)                 <- code =
+       Just (RuleUpdateDLit
+            ,[state { state_stack = Stack rest
                     , state_heap  = insertHeap frm_addr (LitObj lit) heap
                     , state_code  = Return (LitVal lit) }])
 
@@ -423,39 +419,39 @@
   | Stack (UpdateFrame frm_addr : rest) <- stack
   , Return (MemVal addr)                <- code
   , Just hobj <- lookupHeap addr heap
-  , isHeapValueForm hobj = do
-    return ( RuleUpdateDValPtr
-           , [state { state_stack = Stack rest
+  , isHeapValueForm hobj =
+       Just (RuleUpdateDValPtr
+            ,[state { state_stack = Stack rest
                     , state_heap  = insertHeap frm_addr hobj heap
                     , state_code  = Return (MemVal addr) }])
 
-  -- Rule Alt Frame Create Case Non LitVal or MemVal
+  -- Rule Case Frame Create Case Non LitVal or MemVal
   | Stack frames                          <- stack
   , Evaluate (Case mxpr cvar alts) locals <- code
-  , not (isExprValueForm mxpr locals globals heap) = do
-    return ( RuleAltCCaseNonVal
-           , [state { state_stack = Stack (AltFrame cvar alts locals : frames)
+  , not (isExprValueForm mxpr locals globals heap) =
+       Just (RuleCaseCCaseNonVal
+            ,[state { state_stack = Stack (CaseFrame cvar alts locals : frames)
                     , state_code  = Evaluate mxpr locals }])
 
-    -- Rule Alt Frame Delete Lit
-  | Stack (AltFrame cvar alts frm_locs : rest) <- stack
-  , Return (LitVal lit)                        <- code = do
+    -- Rule Case Frame Delete Lit
+  | Stack (CaseFrame cvar alts frm_locs : rest) <- stack
+  , Return (LitVal lit)                         <- code =
     let mxpr = Atom (LitAtom lit)
-    return ( RuleAltDLit
-           , [state { state_stack = Stack rest
+    in Just (RuleCaseDLit
+            ,[state { state_stack = Stack rest
                     , state_code  = Evaluate (Case mxpr cvar alts) frm_locs }])
 
-  -- Rule Alt Frame Delete Heap Value
-  | Stack (AltFrame cvar alts frm_locs : rest) <- stack
-  , Return (MemVal addr)                       <- code
+  -- Rule Case Frame Delete Heap Value
+  | Stack (CaseFrame cvar alts frm_locs : rest) <- stack
+  , Return (MemVal addr)                        <- code
   , Just hobj <- lookupHeap addr heap
-  , isHeapValueForm hobj = do
+  , isHeapValueForm hobj =
     let vname     = freshSeededName (varName cvar) confs
-    let vvar      = Var vname (varType cvar)
-    let mxpr      = Atom (VarAtom vvar)
-    let frm_locs' = insertLocals vvar (MemVal addr) frm_locs
-    return ( RuleAltDValPtr
-           , [state { state_stack = Stack rest
+        vvar      = Var vname (varType cvar)
+        mxpr      = Atom (VarAtom vvar)
+        frm_locs' = insertLocals vvar (MemVal addr) frm_locs
+    in Just (RuleCaseDValPtr
+            ,[state { state_stack = Stack rest
                     , state_code  = Evaluate (Case mxpr cvar alts) frm_locs'
                     , state_names = vname : confs }])
 
@@ -463,9 +459,9 @@
   | Stack frames                      <- stack
   , Evaluate (FunApp fun args) locals <- code
   , Just (_, hobj)          <- vlookupHeap fun locals globals heap
-  , FunObj [] expr fun_locs <- hobj = do
-    return ( RuleApplyCFunThunk
-           , [state { state_stack = Stack (ApplyFrame args locals : frames)
+  , FunObj [] expr fun_locs <- hobj =
+       Just (RuleApplyCFunThunk
+            ,[state { state_stack = Stack (ApplyFrame args locals : frames)
                     , state_code  = Evaluate expr fun_locs }])
 
   -- Rule Apply Frame Create Function Over Application
@@ -473,12 +469,12 @@
   , Evaluate (FunApp fun args) locals <- code
   , Just (_, hobj)              <- vlookupHeap fun locals globals heap
   , FunObj params expr fun_locs <- hobj
-  , (_, Right ex_as)            <- unevenZip params args = do
+  , (_, Right ex_as)            <- unevenZip params args =
     let pass_in   = LiftAct args locals globals heap confs
-    let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
-    let fun_locs' = insertLocalsList (zip params vals) fun_locs
-    return ( RuleApplyCFunAppOver
-           , [state { state_stack   = Stack (ApplyFrame ex_as locals' : frames)
+        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
+        fun_locs' = insertLocalsList (zip params vals) fun_locs
+    in Just (RuleApplyCFunAppOver
+            ,[state { state_stack   = Stack (ApplyFrame ex_as locals' : frames)
                     , state_heap    = heap'
                     , state_globals = globals'
                     , state_code    = Evaluate expr fun_locs'
@@ -488,13 +484,13 @@
   | Stack (ApplyFrame args frm_locs : rest) <- stack
   , Return (MemVal addr)                    <- code
   , Just hobj    <- lookupHeap addr heap
-  , FunObj _ _ _ <- hobj = do
-    ftype <- memAddrType addr heap
+  , FunObj _ _ _ <- hobj
+  , Just ftype   <- memAddrType addr heap =
     let fname     = freshName VarNSpace confs
-    let fvar      = Var fname ftype
-    let frm_locs' = insertLocals fvar (MemVal addr) frm_locs
-    return ( RuleApplyDReturnFun
-           , [state { state_stack = Stack rest
+        fvar      = Var fname ftype
+        frm_locs' = insertLocals fvar (MemVal addr) frm_locs
+    in Just (RuleApplyDReturnFun
+            ,[state { state_stack = Stack rest
                     , state_code  = Evaluate (FunApp fvar args) frm_locs'
                     , state_names = fname : confs }])
 
@@ -502,17 +498,17 @@
   | Stack (ApplyFrame args frm_locs : rest) <- stack
   , Return (MemVal addr)                    <- code
   , Just hobj             <- lookupHeap addr heap
-  , SymObj (Symbol sym _) <- hobj = do
+  , SymObj (Symbol sym _) <- hobj =
     let sname     = freshSeededName (varName sym) confs
-    let svar      = Var sname (varType sym)
-    let frm_locs' = insertLocals svar (MemVal addr) frm_locs
-    return ( RuleApplyDReturnSym
-           , [state { state_stack = Stack rest
+        svar      = Var sname (varType sym)
+        frm_locs' = insertLocals svar (MemVal addr) frm_locs
+    in Just (RuleApplyDReturnSym
+            ,[state { state_stack = Stack rest
                     , state_code  = Evaluate (FunApp svar args) frm_locs'
                     , state_names = sname : confs }])
 
   -- State is Value Form
-  | isStateValueForm state = return (RuleIdentity, [state])
+  | isStateValueForm state = Just (RuleIdentity, [state])
 
   -- Everything Broke!!!
   | otherwise = Nothing
diff --git a/src/SSTG/Utils/PrettyPrint.hs b/src/SSTG/Utils/PrettyPrint.hs
--- a/src/SSTG/Utils/PrettyPrint.hs
+++ b/src/SSTG/Utils/PrettyPrint.hs
@@ -112,8 +112,8 @@
         acc_strs   = "Stack" : frame_strs
 
 pprFrameStr :: Frame -> String
-pprFrameStr (AltFrame var alts locals) = injNewLine acc_strs
-  where header   = "AltFrame"
+pprFrameStr (CaseFrame var alts locals) = injNewLine acc_strs
+  where header   = "CaseFrame"
         var_str  = pprVarStr var
         alts_str = pprAltsStr alts
         locs_str = pprLocalsStr locals