diff --git a/SSTG.cabal b/SSTG.cabal
--- a/SSTG.cabal
+++ b/SSTG.cabal
@@ -1,5 +1,5 @@
 name:                SSTG
-version:             0.1.1.4
+version:             0.1.1.5
 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
@@ -58,7 +58,7 @@
     -- Get command line arguments.
     (proj:src:tail_args) <- getArgs
     -- Make bindings.
-    bindss <- mkTargetBindsList proj src
+    bindss <- mkTargetBindss proj src
     -- Configure entry.
     let entry = if length tail_args > 0 then tail_args !! 0 else "main"
     -- Get the flags.
diff --git a/src/SSTG/Core/Execution/Engine.hs b/src/SSTG/Core/Execution/Engine.hs
--- a/src/SSTG/Core/Execution/Engine.hs
+++ b/src/SSTG/Core/Execution/Engine.hs
@@ -42,8 +42,8 @@
     -- Globals and Heap are loaded together. They are still beta forms now.
     heap0 = empty_heap
     (glist, heap1, binds_addrss) = initGlobals bindss heap0
-    globals0 = insertGlobalsList glist empty_globals
-    (heap2, localss) = liftBindsList binds_addrss globals0 heap1
+    globals0 = insertGlobalsVals glist empty_globals
+    (heap2, localss) = liftBindsAddrss binds_addrss globals0 heap1
     binds_locs = zip bindss localss
     -- Code loading. Completes heap and globals with symbolic injection.
     matches = entryMatches entry binds_locs
@@ -57,7 +57,7 @@
                    , state_globals = globals
                    , state_code = code
                    , state_names = []
-                   , state_paths = empty_pathcons }
+                   , state_path = empty_pathcons }
 
     -- Gather information on all variables.
     state = state0 { state_names = allNames (Program bindss) }
@@ -67,35 +67,35 @@
 allocBinds (Binds _ kvs) heap = (heap', addrs)
   where
     hfakes = map (const Blackhole) kvs
-    (heap', addrs) = allocHeapList hfakes heap
+    (heap', addrs) = allocHeapObjs hfakes heap
 
 -- | Allocate List of `Binds`s
-allocBindsList :: [Binds] -> Heap -> (Heap, [[MemAddr]])
-allocBindsList [] heap = (heap, [])
-allocBindsList (b:bs) heap = (heapf, addrs : as)
+allocBindss :: [Binds] -> Heap -> (Heap, [[MemAddr]])
+allocBindss [] heap = (heap, [])
+allocBindss (bind:bs) heap = (heapf, addrs : as)
   where
-    (heap', addrs) = allocBinds b heap
-    (heapf, as) = allocBindsList bs heap'
+    (heap', addrs) = allocBinds bind heap
+    (heapf, as) = allocBindss bs heap'
 
--- | Binds Address to Name Values
-bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Value)]
+-- | Binds Address to Name Vals
+bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Val)]
 bindsAddrsToVarVals (Binds _ kvs, addrs) = zip (map fst kvs) mem_vals
   where
     mem_vals = map (\a -> MemVal a) addrs
 
 -- | Initialize Globals
-initGlobals :: [Binds] -> Heap -> ([(Var, Value)], Heap, [(Binds, [MemAddr])])
+initGlobals :: [Binds] -> Heap -> ([(Var, Val)], Heap, [(Binds, [MemAddr])])
 initGlobals bindss heap = (var_vals, heap', binds_addrss)
   where
-    (heap', addrss) = allocBindsList bindss heap
+    (heap', addrss) = allocBindss bindss heap
     binds_addrss = zip bindss addrss
     var_vals = concatMap bindsAddrsToVarVals binds_addrss
 
 -- | Force Atom Lookup
-forceLookupValue :: Atom -> Locals -> Globals -> Value
-forceLookupValue (LitAtom lit) _ _ = LitVal lit
-forceLookupValue (VarAtom var) locals globals =
-    case lookupValue var locals globals of
+forceLookupVal :: Atom -> Locals -> Globals -> Val
+forceLookupVal (LitAtom lit) _ _ = LitVal lit
+forceLookupVal (VarAtom var) locals globals =
+    case lookupVal var locals globals of
         Just val -> val
         Nothing -> LitVal BlankAddr  -- An error, but I want to not crash.
 
@@ -104,27 +104,27 @@
 forceRhsObj (FunForm prms expr) locals _ = FunObj prms expr locals
 forceRhsObj (ConForm dcon args) locals globals = ConObj dcon arg_vals
   where
-    arg_vals = map (\a -> forceLookupValue a locals globals) args
+    arg_vals = map (\a -> forceLookupVal a locals globals) args
 
 -- | Lift `Binds`.
-liftBinds :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)
-liftBinds (Binds rec kvs, addrs) globals heap = (heap', locals)
+liftBindsAddrs :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)
+liftBindsAddrs (Binds rec kvs, addrs) globals heap = (heap', locals)
   where
     (vars, rhss) = unzip kvs
     mem_vals = map (\a -> MemVal a) addrs
     e_locs = empty_locals
-    r_locs = insertLocalsList (zip vars mem_vals) e_locs
+    r_locs = insertLocalsVals (zip vars mem_vals) e_locs
     locals = case rec of { Rec -> r_locs; NonRec -> e_locs }
     hobjs = map (\r -> forceRhsObj r locals globals) rhss
-    heap' = insertHeapObjList (zip addrs hobjs) heap
+    heap' = insertHeapObjs (zip addrs hobjs) heap
 
 -- | Lift Binds List
-liftBindsList :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])
-liftBindsList [] _ heap = (heap, [])
-liftBindsList (bm:bms) globals heap = (heapf, locals : ls)
+liftBindsAddrss :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])
+liftBindsAddrss [] _ heap = (heap, [])
+liftBindsAddrss (bind_addr:bms) globals heap = (heapf, locals : ls)
   where
-    (heap', locals) = liftBinds bm globals heap
-    (heapf, ls) = liftBindsList bms globals heap'
+    (heap', locals) = liftBindsAddrs bind_addr globals heap
+    (heapf, ls) = liftBindsAddrss bms globals heap'
 
 -- | Return a sub-list of binds in which the entry candidate appears.
 entryMatches :: String -> [(Binds, Locals)] -> [(Binds, Locals)]
@@ -144,18 +144,18 @@
 loadCode ent (ConForm _ _) locals globals heap = (code, globals, heap)
   where
     code = Evaluate (Atom (VarAtom ent)) locals
-loadCode ent (FunForm params expr) locals globals heap = (code, globals, heap')
+loadCode ent (FunForm params expr) locals globals heap = (code,globals,heap')
   where
     actuals = traceArgs params expr locals globals heap
     confs = map varName actuals
-    names' = freshSeededNameList confs confs
+    names' = freshSeededNames confs confs
     adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals))
     -- Throw the parameters on heap as symbolic objects
     sym_objs = map (\p -> SymObj (Symbol p Nothing)) adjusted
-    (heap', addrs) = allocHeapList sym_objs heap
+    (heap', addrs) = allocHeapObjs sym_objs heap
     -- make Atom representations for arguments and shove into locals.
     mem_vals = map (\a -> MemVal a) addrs
-    locals' = insertLocalsList (zip adjusted mem_vals) locals
+    locals' = insertLocalsVals (zip adjusted mem_vals) locals
     args = map (\p -> VarAtom p) adjusted
     -- Set up code
     code = Evaluate (FunApp ent args) locals'
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
@@ -2,7 +2,7 @@
 module SSTG.Core.Execution.Rules
     ( Rule(..)
     , reduce
-    , isStateValueForm
+    , isStateValForm
     ) where
 
 import SSTG.Core.Language
@@ -35,40 +35,40 @@
 
 -- | Does not include `LitObj`. i.e. if something points to this, we have
 -- nothing to do in terms of reducitons.
-isHeapValueForm :: HeapObj -> Bool
-isHeapValueForm (SymObj _) = True
-isHeapValueForm (ConObj _ _) = True
-isHeapValueForm (FunObj (_:_) _ _) = True
-isHeapValueForm _ = False
+isHeapValForm :: HeapObj -> Bool
+isHeapValForm (SymObj _) = True
+isHeapValForm (ConObj _ _) = True
+isHeapValForm (FunObj (_:_) _ _) = True
+isHeapValForm _ = False
 
 -- | Either a `Lit` or points to a `Heap` value (not LitObj!). If we find
 -- nothing in the `Heap`, then this means we can still upcast the var to a
 -- symbolic that we create additional mappings to in the `Globals`.
-isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool
-isExprValueForm (Atom (LitAtom _)) _ _ _ = True
-isExprValueForm (Atom (VarAtom var)) locals globals heap =
+isExprValForm :: Expr -> Locals -> Globals -> Heap -> Bool
+isExprValForm (Atom (LitAtom _)) _ _ _ = True
+isExprValForm (Atom (VarAtom var)) locals globals heap =
     case vlookupHeap var locals globals heap of
-        Just (_, hobj) -> isHeapValueForm hobj
+        Just (_, hobj) -> isHeapValForm hobj
         Nothing -> False
-isExprValueForm _ _ _ _ = False
+isExprValForm _ _ _ _ = False
 
 -- | Is the `State` in a normal form that cannot be reduced further?
-isStateValueForm :: State -> Bool
-isStateValueForm state
+isStateValForm :: State -> Bool
+isStateValForm state
   | Nothing <- popStack (state_stack state)
   , Return (LitVal _) <- (state_code state) = True
 
   | Nothing <- popStack (state_stack state)
   , Return (MemVal addr) <- (state_code state)
   , Just hobj <- lookupHeap addr (state_heap state)
-  , isHeapValueForm hobj = True
+  , isHeapValForm hobj = True
 
   | otherwise = False
 
--- | `Value` to `Lit`.
-valueToLit :: Value -> Lit
-valueToLit (LitVal lit) = lit
-valueToLit (MemVal addr) = AddrLit (memAddrInt addr)
+-- | `Val` to `Lit`.
+valToLit :: Val -> Lit
+valToLit (LitVal lit) = lit
+valToLit (MemVal addr) = AddrLit (memAddrInt addr)
 
 -- | Uneven `zip` of two `List`s, with the leftover stored.
 unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])
@@ -87,36 +87,36 @@
   where
     sname = freshSeededName (varName var) confs
     svar = Var sname (varType var)
-    (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap
-    globals' = insertGlobals (var, MemVal addr) globals
+    (heap', addr) = allocHeapObj (SymObj (Symbol svar Nothing)) heap
+    globals' = insertGlobalsVal (var, MemVal addr) globals
     confs' = sname : confs
     pass_out = LiftAct addr locals globals' heap' confs'
 
 -- | Lift `Atom` if necessary (i.e. uinterpreted / out-of-scope).
-liftAtom :: LiftAct Atom -> LiftAct Value
+liftAtom :: LiftAct Atom -> LiftAct Val
 liftAtom (LiftAct atom locals globals heap confs) = pass_out
   where
     pass_out = LiftAct aval locals globals' heap' confs'
     (aval, globals', heap', confs') = case atom of
         LitAtom lit -> (LitVal lit, globals, heap, confs)
-        VarAtom var -> case lookupValue var locals globals of
+        VarAtom var -> case lookupVal var locals globals of
             Just val -> (val, globals, heap, confs)
             Nothing -> let pass_in = LiftAct var locals globals heap confs
                            LiftAct addr _ g' h' c' = liftUnInt pass_in
                        in (MemVal addr, g', h', c')
 
 -- | Lift a list of `Atom`s.
-liftAtomList :: LiftAct [Atom] -> LiftAct [Value]
-liftAtomList (LiftAct [] locals globals heap confs) = pass_out
+liftAtoms :: LiftAct [Atom] -> LiftAct [Val]
+liftAtoms (LiftAct [] locals globals heap confs) = pass_out
   where
     pass_out = LiftAct [] locals globals heap confs
-liftAtomList (LiftAct (atom:as) locals globals heap confs) = pass_out
+liftAtoms (LiftAct (atom:as) locals globals heap confs) = pass_out
   where
     pass_in = LiftAct atom locals globals heap confs
     pass_rest = LiftAct as locals' globals' heap' confs'
     pass_out = LiftAct (val : vs) localsf globalsf heapf confsf
     LiftAct val locals' globals' heap' confs' = liftAtom pass_in
-    LiftAct vs localsf globalsf heapf confsf = liftAtomList pass_rest
+    LiftAct vs localsf globalsf heapf confsf = liftAtoms pass_rest
 
 -- | Lift `BindRhs`.
 liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj
@@ -127,43 +127,43 @@
   where
     pass_in = LiftAct args locals globals heap confs
     pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs'
-    LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
+    LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in
 
 -- | Lift `BindRhs` list.
-liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj]
-liftBindRhsList (LiftAct [] locals globals heap confs) = pass_out
+liftBindRhss :: LiftAct [BindRhs] -> LiftAct [HeapObj]
+liftBindRhss (LiftAct [] locals globals heap confs) = pass_out
   where
     pass_out = LiftAct [] locals globals heap confs
-liftBindRhsList (LiftAct (rhs:rs) locals globals heap confs) = pass_out
+liftBindRhss (LiftAct (rhs:rs) locals globals heap confs) = pass_out
   where
     pass_in = LiftAct rhs locals globals heap confs
     pass_rest = LiftAct rs locals' globals' heap' confs'
     pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf
     LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in
-    LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest
+    LiftAct hos localsf globalsf heapf confsf = liftBindRhss pass_rest
 
 -- | Lift `Binds`.
 liftBinds :: LiftAct Binds -> LiftAct ()
 liftBinds (LiftAct (Binds NonRec kvs) locals globals heap confs) = pass_out
   where
-    (heapf, addrs) = allocHeapList hobjs heap'
+    (heapf, addrs) = allocHeapObjs hobjs heap'
     mem_vals = map MemVal addrs
-    localsf = insertLocalsList (zip (map fst kvs) mem_vals) locals'
+    localsf = insertLocalsVals (zip (map fst kvs) mem_vals) locals'
     pass_in = LiftAct (map snd kvs) locals globals heap confs
     pass_out = LiftAct () localsf globals' heapf confs'
-    LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in
+    LiftAct hobjs locals' globals' heap' confs' = liftBindRhss pass_in
 liftBinds (LiftAct (Binds Rec kvs) locals globals heap confs) = pass_out
   where
     hfakes = map (const Blackhole) kvs
     -- Allocate dummy BLACKHOLEs
-    (heap', addrs) = allocHeapList hfakes heap
+    (heap', addrs) = allocHeapObjs hfakes heap
     mem_vals = map MemVal addrs
     -- Use the reigstered loca BLACKHOLEs to construct the locals closure.
-    locals' = insertLocalsList (zip (map fst kvs) mem_vals) locals
-    heapf = insertHeapObjList (zip addrs hobjs) heap''
+    locals' = insertLocalsVals (zip (map fst kvs) mem_vals) locals
+    heapf = insertHeapObjs (zip addrs hobjs) heap''
     pass_in = LiftAct (map snd kvs) locals' globals heap' confs
     pass_out = LiftAct () localsf globals' heapf confs'
-    LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in
+    LiftAct hobjs localsf globals' heap'' confs' = liftBindRhss pass_in
 
 -- | `Default` `Alt` branches in a `Case`.
 defaultAlts :: [Alt] -> [Alt]
@@ -190,13 +190,13 @@
 liftSymAlt (LiftAct args locals globals heap confs) = pass_out
   where
     (mvar, addr, cvar, Alt ac params expr) = args
-    snames = freshSeededNameList (map varName params) confs
+    snames = freshSeededNames (map varName params) confs
     svars = map (\(p, n) -> Var n (varType p)) (zip params snames)
     hobjs = map (\s -> SymObj (Symbol s Nothing)) svars
-    (heap', addrs) = allocHeapList hobjs heap
+    (heap', addrs) = allocHeapObjs hobjs heap
     mem_vals = map MemVal addrs
     kvs = (cvar, MemVal addr) : zip params mem_vals
-    locals' = insertLocalsList kvs locals
+    locals' = insertLocalsVals kvs locals
     mexpr = Atom (VarAtom mvar)
     conss = [Constraint (ac, params) mexpr locals' True]
     confs' = snames ++ confs
@@ -207,12 +207,12 @@
 liftedAltToState state (LiftAct args locals globals heap confs) = state'
   where
     (expr, conss) = args
-    pcons = state_paths state
+    pcons = state_path state
     state' = state { state_heap = heap
                    , state_globals = globals
                    , state_code = Evaluate expr locals
                    , state_names = confs
-                   , state_paths = insertPathConsList conss pcons }
+                   , state_path = insertPathConss conss pcons }
 
 -- | Reduce the state if it matches some type of reduction `Rule`. Return
 -- `Nothing` to denote that rule application has completely failed.
@@ -240,7 +240,7 @@
   -- Rule Atom Val Pointer
   | Evaluate (Atom (VarAtom var)) locals <- code
   , Just (addr, hobj) <- vlookupHeap var locals globals heap
-  , isHeapValueForm hobj =
+  , isHeapValForm hobj =
     Just (RuleAtomValPtr
          ,[state { state_code = Return (MemVal addr) }])
 
@@ -258,8 +258,8 @@
   -- Prim Function App
   | Evaluate (PrimApp pfun args) locals <- code =
     let pass_in = LiftAct args locals globals heap confs
-        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
-        eval = LitEval pfun (map valueToLit vals)
+        LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in
+        eval = LitEval pfun (map valToLit vals)
     in Just (RulePrimApp
             ,[state { state_heap = heap'
                     , state_globals = globals'
@@ -269,8 +269,8 @@
   -- Rule Con App
   | Evaluate (ConApp dcon args) locals <- code =
     let pass_in = LiftAct args locals globals heap confs
-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-        (heapf, addr) = allocHeap (ConObj dcon vals) heap'
+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in
+        (heapf, addr) = allocHeapObj (ConObj dcon vals) heap'
     in Just (RuleConApp
             ,[state { state_heap = heapf
                     , state_globals = globals'
@@ -283,8 +283,8 @@
   , FunObj params expr fun_locs <- hobj
   , length params == length args =
     let pass_in = LiftAct args locals globals heap confs
-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-        fun_locs' = insertLocalsList (zip params vals) fun_locs
+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in
+        fun_locs' = insertLocalsVals (zip params vals) fun_locs
     in Just (RuleFunAppExact
             ,[state { state_heap = heap'
                     , state_globals = globals'
@@ -297,11 +297,11 @@
   , FunObj params expr fun_locs <- hobj
   , (_, Left ex_params) <- unevenZip params args =
     let pass_in = LiftAct args locals globals heap confs
-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in
-        fun_locs' = insertLocalsList (zip params vals) fun_locs
+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in
+        fun_locs' = insertLocalsVals (zip params vals) fun_locs
         -- New Fun Object.
         pobj = FunObj ex_params expr fun_locs'
-        (heapf, paddr) = allocHeap pobj heap'
+        (heapf, paddr) = allocHeapObj pobj heap'
     in Just (RuleFunAppUnder
             ,[state { state_heap = heapf
                     , state_globals = globals'
@@ -315,7 +315,7 @@
     let sname = freshSeededName (varName svar) confs
         svar' = Var sname (foldl AppTy (varType svar) (map atomType args))
         sym = Symbol svar' (Just (FunApp sfun args, locals))
-        (heap', addr) = allocHeap (SymObj sym) heap
+        (heap', addr) = allocHeapObj (SymObj sym) heap
     in Just (RuleFunAppSym
             ,[state { state_heap = heap'
                     , state_code = Return (MemVal addr)
@@ -352,7 +352,7 @@
   -- Rule Case Lit
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
   , (Alt _ _ expr):_ <- matchLitAlts lit alts =
-    let locals' = insertLocals (cvar, LitVal lit) locals
+    let locals' = insertLocalsVal (cvar, LitVal lit) locals
     in Just (RuleCaseLit
             ,[state { state_code = Evaluate expr locals' }])
 
@@ -363,7 +363,7 @@
   , (Alt _ params expr):_ <- matchDataAlts dcon alts
   , length params == length vals =
     let kvs = (cvar, MemVal addr) : zip params vals
-        locals' = insertLocalsList kvs locals
+        locals' = insertLocalsVals kvs locals
     in Just (RuleCaseConPtr
             ,[state { state_code = Evaluate expr locals' }])
 
@@ -371,7 +371,7 @@
   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code
   , [] <- matchLitAlts lit alts
   , (Alt _ _ expr):_ <- defaultAlts alts =
-    let locals' = insertLocals (cvar, LitVal lit) locals
+    let locals' = insertLocalsVal (cvar, LitVal lit) locals
     in Just (RuleCaseAnyLit
             ,[state { state_code = Evaluate expr locals' }])
 
@@ -381,7 +381,7 @@
   , ConObj dcon _ <- hobj
   , [] <- matchDataAlts dcon alts
   , (Alt _ _ expr):_ <- defaultAlts alts =
-    let locals' = insertLocals (cvar, MemVal addr) locals
+    let locals' = insertLocalsVal (cvar, MemVal addr) locals
     in Just (RuleCaseAnyConPtr
             ,[state { state_code = Evaluate expr locals' }])
 
@@ -403,7 +403,7 @@
         all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts
         negatives = map negateConstraint all_conss
         def_lifts' = map (\(LiftAct (e, _) l g h c) ->
-                                    (LiftAct (e, negatives) l g h c)) def_lifts
+                           (LiftAct (e, negatives) l g h c)) def_lifts
         def_sts = map (liftedAltToState state) def_lifts'
     in Just (RuleCaseSym, acon_sts ++ def_sts)
 
@@ -431,7 +431,7 @@
   | Just (UpdateFrame frm_addr, stack') <- popStack stack
   , Return (MemVal addr) <- code
   , Just hobj <- lookupHeap addr heap
-  , isHeapValueForm hobj =
+  , isHeapValForm hobj =
     Just (RuleUpdateDValPtr
          ,[state { state_stack = stack'
                  , state_heap = insertHeapRedir (frm_addr, addr) heap
@@ -439,7 +439,7 @@
 
   -- Rule Case Frame Create Case Non LitVal or MemVal
   | Evaluate (Case mexpr cvar alts) locals <- code
-  , not (isExprValueForm mexpr locals globals heap) =
+  , not (isExprValForm mexpr locals globals heap) =
     let frame = CaseFrame cvar alts locals
     in Just (RuleCaseCCaseNonVal
             ,[state { state_stack = pushStack frame stack
@@ -453,15 +453,15 @@
             ,[state { state_stack = stack'
                     , state_code = Evaluate cexpr frm_locs }])
 
-  -- Rule Case Frame Delete Heap Value
+  -- Rule Case Frame Delete Heap Val
   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack
   , Return (MemVal addr) <- code
   , Just hobj <- lookupHeap addr heap
-  , isHeapValueForm hobj =
+  , isHeapValForm hobj =
     let vname = freshSeededName (varName cvar) confs
         vvar = Var vname (varType cvar)
         cexpr = Case (Atom (VarAtom vvar)) cvar alts
-        frm_locs' = insertLocals (vvar, MemVal addr) frm_locs
+        frm_locs' = insertLocalsVal (vvar, MemVal addr) frm_locs
     in Just (RuleCaseDValPtr
             ,[state { state_stack = stack'
                     , state_code = Evaluate cexpr frm_locs'
@@ -482,8 +482,8 @@
   , FunObj params expr fun_locs <- hobj
   , (_, Right ex_args) <- unevenZip params args =
     let pass_in = LiftAct args locals globals heap confs
-        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in
-        fun_locs' = insertLocalsList (zip params vals) fun_locs
+        LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in
+        fun_locs' = insertLocalsVals (zip params vals) fun_locs
         frame = ApplyFrame ex_args locals'
     in Just (RuleApplyCFunAppOver
             ,[state { state_stack = pushStack frame stack
@@ -500,7 +500,7 @@
   , Just ftype <- memAddrType addr heap =
     let fname = freshName VarNSpace confs
         fvar = Var fname ftype
-        frm_locs' = insertLocals (fvar, MemVal addr) frm_locs
+        frm_locs' = insertLocalsVal (fvar, MemVal addr) frm_locs
     in Just (RuleApplyDReturnFun
             ,[state { state_stack = stack'
                     , state_code = Evaluate (FunApp fvar args) frm_locs'
@@ -513,14 +513,14 @@
   , SymObj (Symbol svar _) <- hobj =
     let sname = freshSeededName (varName svar) confs
         svar' = Var sname (varType svar)
-        frm_locs' = insertLocals (svar', MemVal addr) frm_locs
+        frm_locs' = insertLocalsVal (svar', MemVal addr) frm_locs
     in Just (RuleApplyDReturnSym
             ,[state { state_stack = stack'
                     , state_code = Evaluate (FunApp svar' args) frm_locs'
                     , state_names = sname : confs }])
 
-  -- State is Value Form
-  | isStateValueForm state = Just (RuleIdentity, [state])
+  -- State is Val Form
+  | isStateValForm state = Just (RuleIdentity, [state])
 
   -- Everything Broke!!!
   | otherwise = Nothing
diff --git a/src/SSTG/Core/Execution/Stepping.hs b/src/SSTG/Core/Execution/Stepping.hs
--- a/src/SSTG/Core/Execution/Stepping.hs
+++ b/src/SSTG/Core/Execution/Stepping.hs
@@ -57,8 +57,8 @@
 pass rule_states = (lives, \prev -> prev ++ deads)
   where
     stepped = concatMap step rule_states
-    lives = filter (not . isStateValueForm . snd) stepped
-    deads = filter (isStateValueForm . snd) stepped
+    lives = filter (not . isStateValForm . snd) stepped
+    deads = filter (isStateValForm . snd) stepped
 
 -- | Run bounded breadth-first-search of the execution space with an `Int` to
 -- denote the maximum number of steps to take.
@@ -70,7 +70,7 @@
     execution = foldl (\acc s -> s <*> acc) start passes
 
 -- | Run bounded breadth-first-search of the execution state with an `Int` to
--- denote the maximum number of steps to take. We keep track of a list to track
+-- denote the maximum number of steps to take. We keep a list to track
 -- a history of all the execution snapshots. As it stands, this is currently
 -- very NOT optimized.
 runBoundedBFSLogged :: Int -> State -> [([LiveState], [DeadState])]
diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs
--- a/src/SSTG/Core/Execution/Support.hs
+++ b/src/SSTG/Core/Execution/Support.hs
@@ -13,7 +13,7 @@
     , Stack
     , Frame(..)
     , MemAddr
-    , Value(..)
+    , Val(..)
     , Locals
     , Heap
     , HeapObj(..)
@@ -36,31 +36,31 @@
 
     , empty_locals
     , lookupLocals
-    , insertLocals
-    , insertLocalsList
+    , insertLocalsVal
+    , insertLocalsVals
     , localsToList
 
     , empty_heap
     , lookupHeap
     , insertHeapObj
-    , insertHeapObjList
+    , insertHeapObjs
     , insertHeapRedir
-    , allocHeap
-    , allocHeapList
+    , allocHeapObj
+    , allocHeapObjs
     , heapToList
 
     , empty_globals
     , lookupGlobals
-    , insertGlobals
-    , insertGlobalsList
+    , insertGlobalsVal
+    , insertGlobalsVals
     , globalsToList
 
     , empty_pathcons
     , insertPathCons
-    , insertPathConsList
-    , pathconsToList
+    , insertPathConss
+    , pathConsToList
 
-    , lookupValue
+    , lookupVal
     , vlookupHeap
     , memAddrType
     ) where
@@ -100,12 +100,12 @@
                    , state_globals :: !Globals
                    , state_code :: !Code
                    , state_names :: ![Name]
-                   , state_paths :: !PathCons
+                   , state_path :: !PathCons
                    } deriving (Show, Eq, Read)
 
 -- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the
--- source from which the symbolic variable was generated. For instance, this is
--- useful during symbolic function application.
+-- source from which the symbolic variable was generated. For instance, this
+-- is useful during symbolic function application.
 data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)
 
 -- | State status.
@@ -126,15 +126,15 @@
 -- | Memory address for things on the `Heap`.
 newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord)
 
--- | A `Value` is something that we aim to reduce our current expression down
+-- | A `Val` is something that we aim to reduce our current expression down
 -- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or
 -- `ConObj`, which are "returned" from expression evaluation in this form.
-data Value = LitVal Lit
-           | MemVal MemAddr
-           deriving (Show, Eq, Read)
+data Val = LitVal Lit
+         | MemVal MemAddr
+         deriving (Show, Eq, Read)
 
--- | Locals binds a `Var`'s `Name` to its some `Value`.
-newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)
+-- | Locals binds a `Var`'s `Name` to its some `Val`.
+newtype Locals = Locals (M.Map Name Val) deriving (Show, Eq, Read)
 
 -- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address
 -- that was allocated. This allows us to consistently allocate fresh addresses
@@ -145,7 +145,7 @@
 -- | Heap objects.
 data HeapObj = LitObj Lit
              | SymObj Symbol
-             | ConObj DataCon [Value]
+             | ConObj DataCon [Val]
              | FunObj [Var] Expr Locals
              | Blackhole
              deriving (Show, Eq, Read)
@@ -153,12 +153,12 @@
 -- | Globals are statically loaded at the time when a `State` is loaded.
 -- However, because uninterpreted / out-of-scope variables are made symbolic
 -- at runtime, it can be modified during execution.
-newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read)
+newtype Globals = Globals (M.Map Name Val) deriving (Show, Eq, Read)
 
 -- | Evaluation of the current expression. We are either evaluating, or ready
--- to return with some `Value`.
+-- to return with some `Val`.
 data Code = Evaluate Expr Locals
-          | Return Value
+          | Return Val
           deriving (Show, Eq, Read)
 
 -- | Path constraints are the conjunctive normal form of `Constraint`s.
@@ -200,7 +200,7 @@
 -- | `Stack` pop.
 popStack :: Stack -> Maybe (Frame, Stack)
 popStack (Stack []) = Nothing
-popStack (Stack (frame:frames)) = Just (frame, Stack frames)
+popStack (Stack (frame:fs)) = Just (frame, Stack fs)
 
 -- | `Stack` push.
 pushStack :: Frame -> Stack -> Stack
@@ -215,19 +215,19 @@
 empty_locals = Locals M.empty
 
 -- | `Locals` lookup.
-lookupLocals :: Var -> Locals -> Maybe Value
+lookupLocals :: Var -> Locals -> Maybe Val
 lookupLocals var (Locals lmap) = M.lookup (varName var) lmap
 
 -- | `Locals` insertion.
-insertLocals :: (Var, Value) -> Locals -> Locals
-insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)
+insertLocalsVal :: (Var, Val) -> Locals -> Locals
+insertLocalsVal (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)
 
 -- | List insertion into `Locals`.
-insertLocalsList :: [(Var, Value)] -> Locals -> Locals
-insertLocalsList kvs locals = foldr insertLocals locals kvs
+insertLocalsVals :: [(Var, Val)] -> Locals -> Locals
+insertLocalsVals kvs locals = foldr insertLocalsVal locals kvs
 
 -- | `Locals` to key value pairs.
-localsToList :: Locals -> [(Name, Value)]
+localsToList :: Locals -> [(Name, Val)]
 localsToList (Locals lmap) = M.toList lmap
 
 -- | Empty `Heap`.
@@ -246,28 +246,28 @@
 insertHeapObj (k, v) (Heap hmap prev) = Heap (M.insert k (Right v) hmap) prev
 
 -- | Insert a list of `HeapObj` at specified `MemAddr` locations.
-insertHeapObjList :: [(MemAddr, HeapObj)] -> Heap -> Heap
-insertHeapObjList kvs heap = foldr insertHeapObj heap kvs
+insertHeapObjs :: [(MemAddr, HeapObj)] -> Heap -> Heap
+insertHeapObjs kvs heap = foldr insertHeapObj heap kvs
 
 -- | Insert a redirection `MemAddr` into the `Heap`.
 insertHeapRedir :: (MemAddr, MemAddr) -> Heap -> Heap
 insertHeapRedir (a, r) (Heap hmap prev) = Heap (M.insert a (Left r) hmap) prev
 
 -- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`.
-allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)
-allocHeap hobj (Heap hmap prev) = (heap', addr)
+allocHeapObj :: HeapObj -> Heap -> (Heap, MemAddr)
+allocHeapObj hobj (Heap hmap prev) = (heap', addr)
   where
     addr = MemAddr ((memAddrInt prev) + 1)
     heap' = insertHeapObj (addr, hobj) (Heap hmap addr)
 
 -- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the
 -- `MemAddr` at which they have been allocated at.
-allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr])
-allocHeapList [] heap = (heap, [])
-allocHeapList (hobj:hobjs) heap = (heapf, addr : as)
+allocHeapObjs :: [HeapObj] -> Heap -> (Heap, [MemAddr])
+allocHeapObjs [] heap = (heap, [])
+allocHeapObjs (hobj:hs) heap = (heapf, addr : as)
   where
-    (heap', addr) = allocHeap hobj heap
-    (heapf, as) = allocHeapList hobjs heap'
+    (heap', addr) = allocHeapObj hobj heap
+    (heapf, as) = allocHeapObjs hs heap'
 
 -- | `Heap` to key value pairs.
 heapToList :: Heap -> [(MemAddr, Either MemAddr HeapObj)]
@@ -278,21 +278,21 @@
 empty_globals = Globals M.empty
 
 -- | `Globals` lookup.
-lookupGlobals :: Var -> Globals -> Maybe Value
+lookupGlobals :: Var -> Globals -> Maybe Val
 lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap
 
 -- | `Globals` insertion.
-insertGlobals :: (Var, Value) -> Globals -> Globals
-insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)
+insertGlobalsVal :: (Var, Val) -> Globals -> Globals
+insertGlobalsVal (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)
 
--- | Insert a list of `Var` and `Value` pairs into `Globals`. This would
+-- | Insert a list of `Var` and `Val` pairs into `Globals`. This would
 -- typically occur for new symbolic variables created from uninterpreted /
 -- out-of-scope variables during runtime.
-insertGlobalsList :: [(Var, Value)] -> Globals -> Globals
-insertGlobalsList kvs globals = foldr insertGlobals globals kvs
+insertGlobalsVals :: [(Var, Val)] -> Globals -> Globals
+insertGlobalsVals kvs globals = foldr insertGlobalsVal globals kvs
 
 -- | `Globals` to key value pairs.
-globalsToList :: Globals -> [(Name, Value)]
+globalsToList :: Globals -> [(Name, Val)]
 globalsToList (Globals gmap) = M.toList gmap
 
 -- | Empty `PathCons`.
@@ -304,25 +304,25 @@
 insertPathCons cons (PathCons conss) = PathCons (cons : conss)
 
 -- | Insert a list of `Constraint`s into a `PathCons`.
-insertPathConsList :: [Constraint] -> PathCons -> PathCons
-insertPathConsList conss pathcons = foldr insertPathCons pathcons conss
+insertPathConss :: [Constraint] -> PathCons -> PathCons
+insertPathConss conss pathcons = foldr insertPathCons pathcons conss
 
 -- | `PathCons` to list of `Constraint`s.
-pathconsToList :: PathCons -> [Constraint]
-pathconsToList (PathCons conss) = conss
+pathConsToList :: PathCons -> [Constraint]
+pathConsToList (PathCons conss) = conss
 
 -- Complex functions that involve multiple data structures.
 
--- | `Value` lookup from the `Locals` first, then `Globals`.
-lookupValue :: Var -> Locals -> Globals -> Maybe Value
-lookupValue var locals globals = case lookupLocals var locals of
+-- | `Val` lookup from the `Locals` first, then `Globals`.
+lookupVal :: Var -> Locals -> Globals -> Maybe Val
+lookupVal var locals globals = case lookupLocals var locals of
     Just val -> Just val
     Nothing -> lookupGlobals var globals
 
--- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found.
+-- | `Heap` lookup. Returns the appropriate. `MemAddr` and `HeapObj` if found.
 vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)
 vlookupHeap var locals globals heap = do
-    val <- lookupValue var locals globals
+    val <- lookupVal var locals globals
     case val of
         LitVal _ -> Nothing
         MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)
@@ -335,6 +335,6 @@
         LitObj lit -> Just (litType lit)
         SymObj (Symbol svar _) -> Just (varType svar)
         ConObj dcon _ -> Just (dataConType dcon)
-        FunObj ps expr _ -> Just (foldr FunTy (exprType expr) (map varType ps))
+        FunObj ps ex _ -> Just (foldr FunTy (exprType ex) (map varType ps))
         Blackhole -> Just Bottom
 
diff --git a/src/SSTG/Core/Language/Naming.hs b/src/SSTG/Core/Language/Naming.hs
--- a/src/SSTG/Core/Language/Naming.hs
+++ b/src/SSTG/Core/Language/Naming.hs
@@ -4,11 +4,11 @@
     , varName
     , nameOccStr
     , nameInt
-    , freshString
+    , freshStr
     , freshName
     , freshSeededName
-    , freshNameList
-    , freshSeededNameList
+    , freshNames
+    , freshSeededNames
     ) where
 
 import SSTG.Core.Language.Syntax
@@ -38,15 +38,15 @@
 -- | `Name`s in a `BindRhs`.
 bindRhsNames :: BindRhs -> [Name]
 bindRhsNames (FunForm prms expr) = concatMap varNames prms ++ exprNames expr
-bindRhsNames (ConForm dcon args) = concatMap atomNames args ++ dataNames dcon
+bindRhsNames (ConForm dcon as) = dataConNames dcon ++ concatMap atomNames as
 
 -- | `Name`s in an `Expr`.
 exprNames :: Expr -> [Name]
 exprNames (Atom atom) = atomNames atom
 exprNames (Let binds expr) = exprNames expr ++ bindsNames binds
 exprNames (FunApp fun args) = varNames fun ++ concatMap atomNames args
-exprNames (PrimApp prim args) = pfunNames prim ++ concatMap atomNames args
-exprNames (ConApp dcon args) = dataNames dcon ++ concatMap atomNames args
+exprNames (PrimApp pfun args) = primFunNames pfun ++ concatMap atomNames args
+exprNames (ConApp dcon args) = dataConNames dcon ++ concatMap atomNames args
 exprNames (Case expr var alts) = exprNames expr ++ concatMap altNames alts
                                                 ++ varNames var
 
@@ -56,12 +56,12 @@
 atomNames (VarAtom var) = varNames var
 
 -- | `Name`s in a `PrimFun`.
-pfunNames :: PrimFun -> [Name]
-pfunNames (PrimFun name ty) = name : typeNames ty
+primFunNames :: PrimFun -> [Name]
+primFunNames (PrimFun name ty) = name : typeNames ty
 
 -- | `Name`s in a `DataCon`.
-dataNames :: DataCon -> [Name]
-dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)
+dataConNames :: DataCon -> [Name]
+dataConNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)
 
 -- | `Name`s in an `Alt`.
 altNames :: Alt -> [Name]
@@ -92,7 +92,7 @@
 tyConNames (FunTyCon name bndrs) = name : concatMap tyBinderNames bndrs
 tyConNames (PrimTyCon name bndrs) = name : concatMap tyBinderNames bndrs
 tyConNames (Promoted name bndrs dcon) = name : concatMap tyBinderNames bndrs
-                                            ++ dataNames dcon
+                                            ++ dataConNames dcon
 
 -- | `Name`s in a `Coercion`.
 coercionNames :: Coercion -> [Name]
@@ -117,9 +117,9 @@
 -- `String`s that we do not want our new `String` to conflict with. The sole
 -- purpose of the `Int` seed is to allow us tell us how much to multiply some
 -- prime number to "orbit" an index around a fixed list of acceptable `Char`s.
-freshString :: Int -> String -> S.Set String -> String
-freshString rand seed confs = if S.member seed confs
-    then freshString (rand + 1) (seed ++ [pick]) confs else seed
+freshStr :: Int -> String -> S.Set String -> String
+freshStr rand seed confs = if S.member seed confs
+    then freshStr (rand + 1) (seed ++ [pick]) confs else seed
   where
     pick = bank !! index
     index = raw_i `mod` (length bank)
@@ -147,25 +147,25 @@
 freshSeededName seed confs = Name occ' mdl ns unq'
   where
     Name occ mdl ns unq = seed
-    occ' = freshString 1 occ (S.fromList alls)
+    occ' = freshStr 1 occ (S.fromList alls)
     unq' = maxs + 1
     alls = map nameOccStr confs
     maxs = L.maximum (unq : map nameInt confs)
 
 -- | Generate a list of `Name`s, each corresponding to the appropriate element
 -- of the `NameSpace` list.
-freshNameList :: [NameSpace] -> [Name] -> [Name]
-freshNameList [] _ = []
-freshNameList (nspace:nss) confs = name' : freshNameList nss confs'
+freshNames :: [NameSpace] -> [Name] -> [Name]
+freshNames [] _ = []
+freshNames (nspace:ns) confs = name' : freshNames ns confs'
   where
     name' = freshName nspace confs
     confs' = name' : confs
 
 -- | List of seeded fresh `Name`s.
-freshSeededNameList :: [Name] -> [Name] -> [Name]
-freshSeededNameList [] _ = []
-freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs'
+freshSeededNames :: [Name] -> [Name] -> [Name]
+freshSeededNames [] _ = []
+freshSeededNames (name:ns) confs = name' : freshSeededNames ns confs'
   where
-    name' = freshSeededName n confs
+    name' = freshSeededName name confs
     confs' = name' : confs
 
diff --git a/src/SSTG/Core/Language/Syntax.hs b/src/SSTG/Core/Language/Syntax.hs
--- a/src/SSTG/Core/Language/Syntax.hs
+++ b/src/SSTG/Core/Language/Syntax.hs
@@ -4,8 +4,8 @@
     ) where
 
 -- | A `Program` is defined as a list of bindings. The @Name@ is an identifier
--- that determines a unique binder to the @var@. In practice, these are defined
--- to be `Name` and `Var` respectively.
+-- that determines a unique binder to the @var@. In practice, these are
+-- defined to be `Name` and `Var` respectively.
 newtype Program = Program [Binds] deriving (Show, Eq, Read)
 
 -- | Variables, data constructors, type variables, and type constructors.
diff --git a/src/SSTG/Core/Language/Typing.hs b/src/SSTG/Core/Language/Typing.hs
--- a/src/SSTG/Core/Language/Typing.hs
+++ b/src/SSTG/Core/Language/Typing.hs
@@ -47,6 +47,6 @@
 exprType (ConApp dc args) = foldl AppTy (dataConType dc) (map atomType args)
 exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args)
 exprType (Let _ expr) = exprType expr
-exprType (Case _ _ (a:_)) = altType a
+exprType (Case _ _ (alt:_)) = altType alt
 exprType _ = Bottom
 
diff --git a/src/SSTG/Core/Translation/Haskell.hs b/src/SSTG/Core/Translation/Haskell.hs
--- a/src/SSTG/Core/Translation/Haskell.hs
+++ b/src/SSTG/Core/Translation/Haskell.hs
@@ -2,8 +2,8 @@
 module SSTG.Core.Translation.Haskell
     ( CompileClosure
     , mkCompileClosure
-    , mkTargetBindsList
-    , mkIOString
+    , mkTargetBindss
+    , mkIOStr
     ) where
 
 import qualified SSTG.Core.Language as SL
@@ -31,15 +31,15 @@
 import qualified Data.Maybe as MB
 
 -- | Make IO String from Outputable.
-mkIOString :: (Outputable a) => a -> IO String
-mkIOString obj = runGhc (Just libdir) $ do
+mkIOStr :: (Outputable a) => a -> IO String
+mkIOStr obj = runGhc (Just libdir) $ do
     dflags <- getSessionDynFlags
     return (showPpr dflags obj)
 
 -- | Given the project directory and the source file path, compiles the
 -- `ModuleGraph` and translates it into a SSTG `Binds`s.
-mkTargetBindsList :: FilePath -> FilePath -> IO [SL.Binds]
-mkTargetBindsList proj src = do
+mkTargetBindss :: FilePath -> FilePath -> IO [SL.Binds]
+mkTargetBindss proj src = do
     (sums_gutss, dflags, env) <- mkCompileClosure proj src
     let (sums, gutss) = (map fst sums_gutss, map snd sums_gutss)
     let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums
@@ -145,7 +145,7 @@
   (MachDouble rat) -> SL.MachDouble rat ((mkType . literalType) lit)
   (LitInteger i _) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)
   (MachNullAddr) -> SL.MachNullAddr ((mkType . literalType) lit)
-  (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit)
+  (MachLabel f m _) -> SL.MachLabel (unpackFS f) m (mkType $ literalType lit)
 
 -- | `DataCon`'s `Name`.
 mkDataName :: DataCon -> SL.Name
diff --git a/src/SSTG/Utils/Printing.hs b/src/SSTG/Utils/Printing.hs
--- a/src/SSTG/Utils/Printing.hs
+++ b/src/SSTG/Utils/Printing.hs
@@ -47,13 +47,13 @@
 pprStateStr :: State -> String
 pprStateStr state = injNewLine acc_strs
   where
-    status_str= (pprStatusStr . state_status) state
+    status_str = (pprStatusStr . state_status) state
     stack_str = (pprStackStr . state_stack) state
     heap_str = (pprHeapStr . state_heap) state
     globals_str = (pprGlobalsStr . state_globals) state
     expr_str = (pprCodeStr . state_code) state
     names_str = (pprNamesStr . state_names) state
-    pcons_str = (pprPathConsStr . state_paths) state
+    pcons_str = (pprPathConsStr . state_path) state
     acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>"
                , status_str
                , "----- [Stack] ---------------"
@@ -184,7 +184,7 @@
     header = "ConObj"
     addr_str = pprMemAddrStr addr
     dcon_str = pprDataConStr dcon
-    vals_str = injIntoList (map pprValueStr vals)
+    vals_str = injIntoList (map pprValStr vals)
     acc_str = sub (addr_str ++ ", " ++ injSpace [header, dcon_str, vals_str])
 pprMemHeapObjStr (addr, FunObj params expr locals) = acc_str
   where
@@ -213,7 +213,7 @@
   where
     glist = globalsToList globals
     name_strs = map (pprNameStr . fst) glist
-    val_strs = map (pprValueStr . snd) glist
+    val_strs = map (pprValStr . snd) glist
     zipd_strs = zip name_strs val_strs
     acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs
 
@@ -223,18 +223,18 @@
   where
     llist = localsToList locals
     name_strs = map (pprNameStr . fst) llist
-    val_strs = map (pprValueStr . snd) llist
+    val_strs = map (pprValStr . snd) llist
     zipd_strs = zip name_strs val_strs
     acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs
 
--- | Print `Value`.
-pprValueStr :: Value -> String
-pprValueStr (LitVal lit) = injSpace acc_strs
+-- | Print `Val`.
+pprValStr :: Val -> String
+pprValStr (LitVal lit) = injSpace acc_strs
   where
     header = "LitVal"
     lit_str = pprLitStr lit
     acc_strs = [header, lit_str]
-pprValueStr (MemVal addr) = injSpace acc_strs
+pprValStr (MemVal addr) = injSpace acc_strs
   where
     header = "MemVal"
     ptr_str = pprMemAddrStr addr
@@ -395,7 +395,7 @@
 pprCodeStr (Return val) = injSpace acc_strs
   where
     header = "Return"
-    val_str = pprValueStr val
+    val_str = pprValStr val
     acc_strs = [header, val_str]
 
 -- | Print a list of `Name`s.
@@ -406,7 +406,7 @@
 pprPathConsStr :: PathCons -> String
 pprPathConsStr pathcons = injNewLineSeps5 strs
   where
-    strs = map pprConstraintStr (pathconsToList pathcons)
+    strs = map pprConstraintStr (pathConsToList pathcons)
 
 -- | Print `PathCond`.
 pprConstraintStr :: Constraint -> String