SSTG 0.1.1.2 → 0.1.1.3

raw patch · 20 files changed

+1325/−1237 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +9/−5
• src/SSTG/Core.hs +4/−0
• src/SSTG/Core/Execution.hs +0/−4
• src/SSTG/Core/Execution/Engine.hs +89/−81
• src/SSTG/Core/Execution/Naming.hs +0/−209
• src/SSTG/Core/Execution/Rules.hs +209/−200
• src/SSTG/Core/Execution/Stepping.hs +20/−16
• src/SSTG/Core/Execution/Support.hs +0/−348
• src/SSTG/Core/Language.hs +5/−1
• src/SSTG/Core/Language/Naming.hs +217/−0
• src/SSTG/Core/Language/Support.hs +351/−0
• src/SSTG/Core/Language/Syntax.hs +63/−86
• src/SSTG/Core/Language/Typing.hs +17/−17
• src/SSTG/Core/Preprocessing.hs +7/−0
• src/SSTG/Core/Preprocessing/Defunctionalization.hs +8/−0
• src/SSTG/Core/SMT.hs +7/−0
• src/SSTG/Core/SMT/Syntax.hs +7/−0
• src/SSTG/Core/Translation/Haskell.hs +93/−92
• src/SSTG/Utils/FileIO.hs +1/−2
• src/SSTG/Utils/Printing.hs +218/−176

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.1.2+version:             0.1.1.3 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme@@ -17,17 +17,21 @@   hs-source-dirs:      src   exposed-modules:     SSTG                      , SSTG.Core-                     , SSTG.Core.Translation-                     , SSTG.Core.Translation.Haskell                      , SSTG.Core.Language+                     , SSTG.Core.Language.Naming+                     , SSTG.Core.Language.Support                      , SSTG.Core.Language.Syntax                      , SSTG.Core.Language.Typing+                     , SSTG.Core.Preprocessing+                     , SSTG.Core.Preprocessing.Defunctionalization+                     , SSTG.Core.SMT+                     , SSTG.Core.SMT.Syntax+                     , SSTG.Core.Translation+                     , SSTG.Core.Translation.Haskell                      , SSTG.Core.Execution                      , SSTG.Core.Execution.Engine-                     , SSTG.Core.Execution.Naming                      , SSTG.Core.Execution.Rules                      , SSTG.Core.Execution.Stepping-                     , SSTG.Core.Execution.Support                      , SSTG.Utils                      , SSTG.Utils.Printing                      , SSTG.Utils.FileIO

@@ -2,10 +2,14 @@ module SSTG.Core     ( module SSTG.Core.Execution     , module SSTG.Core.Language+    , module SSTG.Core.Preprocessing+    , module SSTG.Core.SMT     , module SSTG.Core.Translation     ) where  import SSTG.Core.Execution import SSTG.Core.Language+import SSTG.Core.Preprocessing+import SSTG.Core.SMT import SSTG.Core.Translation 

@@ -1,15 +1,11 @@ -- | Export Module for SSTG.Core.Execution module SSTG.Core.Execution     ( module SSTG.Core.Execution.Engine-    , module SSTG.Core.Execution.Naming     , module SSTG.Core.Execution.Rules     , module SSTG.Core.Execution.Stepping-    , module SSTG.Core.Execution.Support     ) where  import SSTG.Core.Execution.Engine-import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping-import SSTG.Core.Execution.Support 

@@ -10,12 +10,10 @@     ) where  import SSTG.Core.Language-import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Stepping-import SSTG.Core.Execution.Support  -- | Load Result-data LoadResult = LoadOkay  State+data LoadResult = LoadOkay State                 | LoadGuess State [Bind]                 | LoadError String                 deriving (Show, Eq, Read)@@ -24,100 +22,107 @@ -- experimental results. loadState :: Program -> LoadResult loadState prog = loadStateEntry main_occ_name prog-  where main_occ_name = "main"  -- Based on a few experimental programs.+  where+    main_occ_name = "main"  -- Based on a few experimental programs.  -- | Load from a specified entry point. loadStateEntry :: String -> Program -> LoadResult loadStateEntry entry (Program bnds) = if length matches == 0     then LoadError ("No entry candidates found for: [" ++ entry ++ "]")     else if length others == 0-        then LoadOkay  state+        then LoadOkay state         else LoadGuess state (map fst others)-  where -- Status or something.-        status   = Status { status_id = 1-                          , status_parent_id = 0-                          , status_steps = 0 }-        -- Stack initialized to empty.-        stack    = empty_stack-        -- Globals and Heap are loaded together. They are still beta forms now.-        heap0    = empty_heap-        (glist, heap1, bnd_addrss) = initGlobals bnds heap0-        globals0 = insertGlobalsList glist empty_globals-        (heap2, localss) = liftBinds bnd_addrss globals0 heap1-        bnd_locs = zip bnds localss-        -- Code loading. Completes heap and globals with symbolic injection.-        matches  = entryMatches entry bnd_locs-        ((tgt_bnd, tgt_loc):others) = matches-        ((tgt_var, tgt_rhs):_)      = lhsMatches entry tgt_bnd-        (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2-        -- Ready to fill the state.-        state0   = State { state_status  = status-                         , state_stack   = stack-                         , state_heap    = heap-                         , state_globals = globals-                         , state_code    = code-                         , state_names   = []-                         , state_paths   = empty_pathcons }+  where+    -- Status or something.+    status = init_status+    -- Stack initialized to empty.+    stack = empty_stack+    -- Globals and Heap are loaded together. They are still beta forms now.+    heap0 = empty_heap+    (glist, heap1, bnd_addrss) = initGlobals bnds heap0+    globals0 = insertGlobalsList glist empty_globals+    (heap2, localss) = liftBinds bnd_addrss globals0 heap1+    bnd_locs = zip bnds localss+    -- Code loading. Completes heap and globals with symbolic injection.+    matches = entryMatches entry bnd_locs+    ((tgt_bnd, tgt_loc):others) = matches+    ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_bnd+    (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2+    -- Ready to fill the state.+    state0 = State { state_status = status+                   , state_stack = stack+                   , state_heap = heap+                   , state_globals = globals+                   , state_code = code+                   , state_names = []+                   , state_paths = empty_pathcons } -        -- Gather information on all variables.-        state    = state0 { state_names = allNames state0 }+    -- Gather information on all variables.+    state = state0 { state_names = allNames state0 }  -- | Allocate Bind allocBind :: Bind -> Heap -> (Heap, [MemAddr]) allocBind (Bind _ pairs) heap = (heap', addrs)-  where hfakes = map (const Blackhole) pairs-        (heap', addrs) = allocHeapList hfakes heap+  where+    hfakes = map (const Blackhole) pairs+    (heap', addrs) = allocHeapList hfakes heap  -- | Allocate List of `Bind`s allocBindList :: [Bind] -> Heap -> (Heap, [[MemAddr]])-allocBindList []     heap = (heap, [])+allocBindList [] heap = (heap, []) allocBindList (b:bs) heap = (heapf, addrs : as)-  where (heap', addrs) = allocBind b heap-        (heapf, as)    = allocBindList bs heap'+  where+    (heap', addrs) = allocBind b heap+    (heapf, as) = allocBindList bs heap'  -- | Bind Address to Name Values bndAddrsToVarVals :: (Bind, [MemAddr]) -> [(Var, Value)] bndAddrsToVarVals (Bind _ rhss, addrs) = zip (map fst rhss) mem_vals-  where mem_vals = map (\a -> MemVal a) addrs+  where+    mem_vals = map (\a -> MemVal a) addrs  -- | Initialize Globals initGlobals :: [Bind] -> Heap -> ([(Var, Value)], Heap, [(Bind, [MemAddr])]) initGlobals bnds heap = (var_vals, heap', bnd_addrss)-  where (heap', addrss) = allocBindList bnds heap-        bnd_addrss = zip bnds addrss-        var_vals   = concatMap bndAddrsToVarVals bnd_addrss+  where+    (heap', addrss) = allocBindList bnds heap+    bnd_addrss = zip bnds addrss+    var_vals = concatMap bndAddrsToVarVals bnd_addrss  -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value-forceLookupValue (LitAtom lit) _      _       = LitVal lit+forceLookupValue (LitAtom lit) _ _ = LitVal lit forceLookupValue (VarAtom var) locals globals =     case lookupValue var locals globals of-        Nothing  -> LitVal BlankAddr  -- An error, but I want to not crash.+        Nothing -> LitVal BlankAddr  -- An error, but I want to not crash.         Just val -> val  -- | Full Rhs Object forceRhsObj :: BindRhs -> Locals -> Globals -> HeapObj-forceRhsObj (FunForm prms expr) locals _       = FunObj prms expr locals+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+  where+    arg_vals = map (\a -> forceLookupValue a locals globals) args  -- | Lift `Bind`. liftBind :: (Bind, [MemAddr]) -> Globals -> Heap -> (Heap, Locals) liftBind (Bind rec pairs, addrs) globals heap = (heap', locals)-  where (vars, rhss) = unzip pairs-        mem_vals = map (\a -> MemVal a) addrs-        e_locs   = empty_locals-        r_locs   = insertLocalsList (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'    = insertHeapList (zip addrs hobjs) heap+  where+    (vars, rhss) = unzip pairs+    mem_vals = map (\a -> MemVal a) addrs+    e_locs = empty_locals+    r_locs = insertLocalsList (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' = insertHeapList (zip addrs hobjs) heap  -- | Lift Bind List liftBinds :: [(Bind, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])-liftBinds []       _       heap = (heap, [])+liftBinds [] _ heap = (heap, []) liftBinds (bm:bms) globals heap = (heapf, locals : ls)-  where (heap', locals) = liftBind bm globals heap-        (heapf, ls)     = liftBinds bms globals heap'+  where+    (heap', locals) = liftBind bm globals heap+    (heapf, ls) = liftBinds bms globals heap'  -- | Return a sub-list of binds in which the entry candidate appears. entryMatches :: String -> [(Bind, Locals)] -> [(Bind, Locals)]@@ -134,28 +139,30 @@  -- | Load Code loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap -> (Code,Globals,Heap)-loadCode ent (ConForm _ _)         locals globals heap = (code, globals, heap)-  where code = Evaluate (Atom (VarAtom ent)) locals+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')-  where actuals  = traceArgs params expr locals globals heap-        confs    = map varName actuals-        names'   = freshSeededNameList 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-        -- make Atom representations for arguments and shove into locals.-        mem_vals = map (\a -> MemVal a) addrs-        locals'  = insertLocalsList (zip adjusted mem_vals) locals-        args     = map (\p -> VarAtom p) adjusted-        -- Set up code-        code     = Evaluate (FunApp ent args) locals'+  where+    actuals = traceArgs params expr locals globals heap+    confs = map varName actuals+    names' = freshSeededNameList 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+    -- make Atom representations for arguments and shove into locals.+    mem_vals = map (\a -> MemVal a) addrs+    locals' = insertLocalsList (zip adjusted mem_vals) locals+    args = map (\p -> VarAtom p) adjusted+    -- Set up code+    code = Evaluate (FunApp ent args) locals'  -- | We need to do stupid tracing if it's THUNK'D by default >:( traceArgs :: [Var] -> Expr -> Locals -> Globals -> Heap -> [Var] traceArgs base expr locals globals heap-  | FunApp var []     <- expr-  , Just (_, hobj)    <- vlookupHeap var locals globals heap+  | FunApp var [] <- expr+  , Just (_, hobj) <- vlookupHeap var locals globals heap   , FunObj params _ _ <- hobj   , length params > 0   , length base == 0 = params@@ -164,8 +171,8 @@  -- | Run flags. data RunFlags = RunFlags { flag_step_count :: Int-                         , flag_step_type  :: StepType-                         , flag_dump_dir   :: Maybe FilePath+                         , flag_step_type :: StepType+                         , flag_dump_dir :: Maybe FilePath                          } deriving (Show, Eq, Read)  -- | Step execution type.@@ -174,15 +181,16 @@ -- | Perform execution on a `State` given the run flags. execute :: RunFlags -> State -> [([LiveState], [DeadState])] execute flags state = step (flag_step_count flags) state-  where step :: Int -> State -> [([LiveState], [DeadState])]-        step = case flag_step_type flags of-                   BFS       -> \k s -> [runBoundedBFS k s]-                   BFSLogged -> runBoundedBFSLogged-                   DFS       -> \k s -> [runBoundedDFS k s]-                   DFSLogged -> runBoundedDFSLogged+  where+    step :: Int -> State -> [([LiveState], [DeadState])]+    step = case flag_step_type flags of+               BFS -> \k s -> [runBoundedBFS k s]+               BFSLogged -> runBoundedBFSLogged+               DFS -> \k s -> [runBoundedDFS k s]+               DFSLogged -> runBoundedDFSLogged  -- | Simple `BFS` based execution on a state. execute1 :: Int -> State -> ([LiveState], [DeadState])-execute1 n state | n < 1     = ([([], state)], [])+execute1 n state | n < 1 = ([([], state)], [])                  | otherwise = runBoundedBFS n state 

@@ -1,209 +0,0 @@--- | Naming Module-module SSTG.Core.Execution.Naming-    ( allNames-    , freshString-    , freshName-    , freshSeededName-    , freshNameList-    , freshSeededNameList-    ) where--import SSTG.Core.Language-import SSTG.Core.Execution.Support--import qualified Data.List as L-import qualified Data.Set  as S---- | All `Name`s in a `State`.-allNames :: State -> [Name]-allNames state = L.nub acc_ns-  where stack_ns = stackNames   (state_stack   state)-        heap_ns  = heapNames    (state_heap    state)-        glbls_ns = globalsNames (state_globals state)-        expr_ns  = codeNames    (state_code    state)-        pcons_ns = pconsNames   (state_paths   state)-        acc_ns   = stack_ns ++ heap_ns ++ glbls_ns ++ expr_ns ++ pcons_ns---- | `Name`s in a `Stack`.-stackNames :: Stack -> [Name]-stackNames stack = concatMap frameNames (stackToList stack)---- | `Name`s in a `Frame`.-frameNames :: Frame -> [Name]-frameNames (UpdateFrame _)         = []-frameNames (ApplyFrame as ls)      = localsNames ls ++ concatMap atomNames as-frameNames (CaseFrame var alts ls) = localsNames ls ++ concatMap altNames alts-                                                    ++ varNames var---- | `Name`s in an `Alt`.-altNames :: Alt -> [Name]-altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr---- | `Name`s in the `Locals`-localsNames :: Locals -> [Name]-localsNames locals = map fst (localsToList locals)---- | `Name`s in the `Heap`.-heapNames :: Heap -> [Name]-heapNames heap = concatMap (heapObjNames . snd) (heapToList heap)---- | `Name`s in a `HeapObj`.-heapObjNames :: HeapObj -> [Name]-heapObjNames (AddrObj _)           = []-heapObjNames (Blackhole)           = []-heapObjNames (LitObj _)            = []-heapObjNames (SymObj sym)          = symbolNames sym-heapObjNames (ConObj dcon _)       = dataNames dcon-heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs-                                                    ++ concatMap varNames ps---- | `Name`s in a `Symbol`.-symbolNames :: Symbol -> [Name]-symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_ns-  where scls_ns = case mb_scls of-                      Nothing     -> []-                      Just (e, l) -> exprNames e ++ localsNames l---- | `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---- | `Name`s in a `Var`.-varNames :: Var -> [Name]-varNames (Var n t) = n : typeNames t---- | `Name`s in an `Atom`.-atomNames :: Atom -> [Name]-atomNames (LitAtom _)   = []-atomNames (VarAtom var) = varNames var---- | `Name`s in `Globals`.-globalsNames :: Globals -> [Name]-globalsNames globals = map fst (globalsToList globals)---- | `Name`s in the current evaluation `Code`.-codeNames :: Code -> [Name]-codeNames (Return _)             = []-codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals---- | `Name`s in an `Expr`.-exprNames :: Expr -> [Name]-exprNames (Atom atom)          = atomNames atom-exprNames (Let bnd expr)       = exprNames expr ++ bindNames bnd-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 (Case expr var alts) = exprNames expr ++ concatMap altNames  alts-                                                ++ varNames var--- | `Name`s in a `Type`.-typeNames :: Type -> [Name]-typeNames (TyVarTy n ty)    = n : typeNames ty-typeNames (CoercionTy coer) = coercionNames coer-typeNames (AppTy t1 t2)     = typeNames  t1 ++ typeNames t2-typeNames (CastTy ty coer)  = typeNames  ty ++ coercionNames coer-typeNames (ForAllTy bnd ty) = typeNames  ty ++ tyBinderNames bnd-typeNames (FunTy t1 t2)     = typeNames  t1 ++ typeNames t2-typeNames (TyConApp tc ty)  = tyConNames tc ++ concatMap typeNames ty-typeNames (LitTy _)         = []-typeNames (Bottom)          = []---- | `Name`s in a `PrimFun`.-pfunNames :: PrimFun -> [Name]-pfunNames (PrimFun n ty) = n : typeNames ty---- | `Name`s in a `DataCon`.-dataNames :: DataCon -> [Name]-dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys)---- | `Name`s in a `TyBinder`.-tyBinderNames :: TyBinder -> [Name]-tyBinderNames (AnonTyBndr)    = []-tyBinderNames (NamedTyBndr n) = [n]---- | `Name`s in a `TyCon`.-tyConNames :: TyCon -> [Name]-tyConNames (FamilyTyCon n ns)  = n : ns-tyConNames (SynonymTyCon n ns) = n : ns-tyConNames (AlgTyCon n ns r)   = n : ns ++ algTyRhsNames r-tyConNames (FunTyCon n bs)     = n : concatMap tyBinderNames bs-tyConNames (PrimTyCon n bs)    = n : concatMap tyBinderNames bs-tyConNames (Promoted n bs dc)  = n : concatMap tyBinderNames bs ++ dataNames dc---- | `Name`s in a `Coercion`.-coercionNames :: Coercion -> [Name]-coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2---- | `Name`s in a `AlgTyRhs`.-algTyRhsNames :: AlgTyRhs -> [Name]-algTyRhsNames (AbstractTyCon _) = []-algTyRhsNames (DataTyCon ns)    = ns-algTyRhsNames (TupleTyCon n)    = [n]-algTyRhsNames (NewTyCon n)      = [n]---- | `Name`s in a `Bind`.-bindNames :: Bind -> [Name]-bindNames (Bind _ bnd) = lhs ++ rhs-  where lhs = concatMap (varNames . fst) bnd-        rhs = concatMap (bindRhsNames . snd) bnd---- | `Name`s in a `PathCons`.-pconsNames :: PathCons -> [Name]-pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons)---- | `Name`s in a `PathCons`.-constraintNames :: Constraint -> [Name]-constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs-                                                            ++ map varName vs---- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of--- `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-  where pick  = bank !! index-        index = raw_i `mod` (length bank)-        raw_i = (abs rand) * prime-        prime = 151  -- The original? :)-        bank  = lower ++ upper ++ nums-        lower = "abcdefghijlkmnopqrstuvwxyz"-        upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"-        nums  = "1234567890"---- | Fresh `Name` given a list of `Name`s that acts as conflicts. The fresh--- `Name`s generated in this manner are prefixed with @"fs?"@, which is not a--- valid identifier in Haskell, but okay in SSTG. we also specify the--- `NameSpace` under which the `Name` will be generated. This will generally--- be `VarNSpace` in actual usage.-freshName :: NameSpace -> [Name] -> Name-freshName nspace confs = freshSeededName seed confs-  where seed = Name "fs?" Nothing nspace 0---- | A fresh `Name` generated from a seed `Name`, which will act as the prefix--- of the new `Name`. We ues the same `NameSpace` as the seed `Name` when--- generating this way.-freshSeededName :: Name -> [Name] -> Name-freshSeededName seed confs = Name occ' mdl ns unq'-  where Name occ mdl ns unq = seed-        occ' = freshString 1 occ (S.fromList alls)-        unq' = maxs + 1-        alls = map nameOccStr confs-        maxs = L.maximum (unq : map nameUnique 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'-  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'-  where name'  = freshSeededName n confs-        confs' = name' : confs-

@@ -6,14 +6,12 @@     ) where  import SSTG.Core.Language-import SSTG.Core.Execution.Naming-import SSTG.Core.Execution.Support  -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt           | RulePrimApp           | RuleConApp-          | RuleFunAppExact | RuleFunAppUnder  | RuleFunAppSym+          | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym                             | RuleFunAppConPtr | RuleFunAppUnInt           | RuleLet           | RuleCaseLit | RuleCaseConPtr | RuleCaseAnyLit | RuleCaseAnyConPtr@@ -25,59 +23,58 @@           | RuleCaseCCaseNonVal           | RuleCaseDLit | RuleCaseDValPtr -          | RuleApplyCFunThunk  | RuleApplyCFunAppOver+          | RuleApplyCFunThunk | RuleApplyCFunAppOver           | RuleApplyDReturnFun | RuleApplyDReturnSym            | RuleIdentity           deriving (Show, Eq, Read, Ord) ---  Stack Independent Rules+-- Stack Independent Rules  -- | 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 (SymObj _) = True+isHeapValueForm (ConObj _ _) = True isHeapValueForm (FunObj (_:_) _ _) = True-isHeapValueForm _                  = False+isHeapValueForm _ = 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 (LitAtom _)) _ _ _ = True isExprValueForm (Atom (VarAtom var)) locals globals heap =     case vlookupHeap var locals globals heap of         Just (_, hobj) -> isHeapValueForm hobj-        Nothing        -> False-isExprValueForm _                    _      _       _    = False+        Nothing -> False+isExprValueForm _ _ _ _ = False  -- | Is the `State` in a normal form that cannot be reduced further? isStateValueForm :: State -> Bool-isStateValueForm State { state_stack = stack-                       , state_heap  = heap-                       , state_code  = code }-  | Nothing           <- popStack stack-  , Return (LitVal _) <- code = True+isStateValueForm state+  | Nothing <- popStack (state_stack state)+  , Return (LitVal _) <- (state_code state) = True -  | Nothing              <- popStack stack-  , Return (MemVal addr) <- code-  , Just hobj            <- lookupHeap addr heap+  | Nothing <- popStack (state_stack state)+  , Return (MemVal addr) <- (state_code state)+  , Just hobj <- lookupHeap addr (state_heap state)   , isHeapValueForm hobj = True    | otherwise = False  -- | `Value` to `Lit`. valueToLit :: Value -> Lit-valueToLit (LitVal lit)  = lit+valueToLit (LitVal lit) = lit valueToLit (MemVal addr) = AddrLit (addrInt addr)  -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])-unevenZip as     []     = ([], Left as)-unevenZip []     bs     = ([], Right bs)+unevenZip as [] = ([], Left as)+unevenZip [] bs = ([], Right bs) unevenZip (a:as) (b:bs) = ((a, b) : acc, excess)-  where (acc, excess) = unevenZip as bs+  where+    (acc, excess) = unevenZip as bs  -- | Lift action wrapper type. data LiftAct a = LiftAct a Locals Globals Heap [Name]@@ -85,76 +82,86 @@ -- | Lift uninterpreted `Var`s into `Globals`. liftUnInt :: LiftAct Var -> LiftAct MemAddr liftUnInt (LiftAct var locals globals heap confs) = pass_out-  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-        confs'   = sname : confs-        pass_out = LiftAct addr locals globals' heap' confs'+  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+    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 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-                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')+  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+            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-  where pass_out  = LiftAct []   locals  globals  heap  confs+liftAtomList (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-  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+  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  -- | Lift `BindRhs`. liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj liftBindRhs (LiftAct (FunForm prms expr) locals globals heap confs) = pass_out-  where pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs+  where+    pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs liftBindRhs (LiftAct (ConForm dcon args) locals globals heap confs) = pass_out-  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+  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  -- | Lift `BindRhs` list. liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj]-liftBindRhsList (LiftAct []       locals globals heap confs) = pass_out-  where pass_out  = LiftAct []  locals  globals  heap  confs+liftBindRhsList (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-  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+  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  -- | Lift `Bind`. liftBind :: LiftAct Bind -> LiftAct () liftBind (LiftAct (Bind NonRec bnd) locals globals heap confs) = pass_out-  where (heapf, addrs) = allocHeapList hobjs heap'-        mem_vals = map MemVal addrs-        localsf  = insertLocalsList (zip (map fst bnd) mem_vals) locals'-        pass_in  = LiftAct (map snd bnd) locals globals heap confs-        pass_out = LiftAct () localsf globals' heapf confs'-        LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in-liftBind (LiftAct (Bind Rec bnd)    locals globals heap confs) = pass_out-  where hfakes   = map (const Blackhole) bnd-        -- Allocate dummy BLACKHOLEs-        (heap', addrs) = allocHeapList hfakes heap-        mem_vals = map MemVal addrs-        -- Use the reigstered loca BLACKHOLEs to construct the locals closure.-        locals'  = insertLocalsList (zip (map fst bnd) mem_vals) locals-        heapf    = insertHeapList (zip addrs hobjs) heap''-        pass_in  = LiftAct (map snd bnd) locals' globals heap' confs-        pass_out = LiftAct () localsf globals' heapf confs'-        LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in+  where+    (heapf, addrs) = allocHeapList hobjs heap'+    mem_vals = map MemVal addrs+    localsf = insertLocalsList (zip (map fst bnd) mem_vals) locals'+    pass_in = LiftAct (map snd bnd) locals globals heap confs+    pass_out = LiftAct () localsf globals' heapf confs'+    LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in+liftBind (LiftAct (Bind Rec bnd) locals globals heap confs) = pass_out+  where+    hfakes = map (const Blackhole) bnd+    -- Allocate dummy BLACKHOLEs+    (heap', addrs) = allocHeapList hfakes heap+    mem_vals = map MemVal addrs+    -- Use the reigstered loca BLACKHOLEs to construct the locals closure.+    locals' = insertLocalsList (zip (map fst bnd) mem_vals) locals+    heapf = insertHeapList (zip addrs hobjs) heap''+    pass_in = LiftAct (map snd bnd) locals' globals heap' confs+    pass_out = LiftAct () localsf globals' heapf confs'+    LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in  -- | `Default` `Alt` branches in a `Case`. defaultAlts :: [Alt] -> [Alt]@@ -179,59 +186,61 @@ -- | Lift `Alt`s during branching caused by symbolics. liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, [Constraint]) liftSymAlt (LiftAct args locals globals heap confs) = pass_out-  where (mvar, addr, cvar, Alt ac params expr) = args-        snames   = freshSeededNameList (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-        mem_vals = map MemVal addrs-        kvs      = (cvar, MemVal addr) : zip params mem_vals-        locals'  = insertLocalsList kvs locals-        mxpr     = Atom (VarAtom mvar)-        conss    = [Constraint (ac, params) mxpr locals' True]-        confs'   = snames ++ confs-        pass_out = LiftAct (expr, conss) locals' globals heap' confs'+  where+    (mvar, addr, cvar, Alt ac params expr) = args+    snames = freshSeededNameList (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+    mem_vals = map MemVal addrs+    kvs = (cvar, MemVal addr) : zip params mem_vals+    locals' = insertLocalsList kvs locals+    mxpr = Atom (VarAtom mvar)+    conss = [Constraint (ac, params) mxpr locals' True]+    confs' = snames ++ confs+    pass_out = LiftAct (expr, conss) locals' globals heap' confs'  -- | `Alt` closure to `State`. liftedAltToState :: State -> LiftAct (Expr, [Constraint]) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state'-  where (expr, conss) = args-        pathcons = state_paths state-        state'   = state { state_heap    = heap-                         , state_globals = globals-                         , state_code    = Evaluate expr locals-                         , state_names   = confs-                         , state_paths   = insertPathConsList conss pathcons }+  where+    (expr, conss) = args+    pcons = state_paths state+    state' = state { state_heap = heap+                   , state_globals = globals+                   , state_code = Evaluate expr locals+                   , state_names = confs+                   , state_paths = insertPathConsList conss pcons }  -- | Reduce the state if it matches some type of reduction `Rule`. Return -- `Nothing` to denote that rule application has completely failed. reduce :: State -> Maybe (Rule, [State])-reduce state @ State { state_stack   = stack-                     , state_heap    = heap+reduce state @ State { state_stack = stack+                     , state_heap = heap                      , state_globals = globals-                     , state_code    = code-                     , state_names   = confs }+                     , state_code = code+                     , state_names = confs } -  -- Stack Independent Rules+-- Stack Independent Rules    -- Atom Lit   | Evaluate (Atom (LitAtom lit)) _ <- code =-       Just (RuleAtomLit-            ,[state { state_code = Return (LitVal lit) }])+    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 =-       Just (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 =-       Just (RuleAtomValPtr-            ,[state { state_code = Return (MemVal addr) }])+    Just (RuleAtomValPtr+         ,[state { state_code = Return (MemVal addr) }])    -- Rule Atom Uninterpreted   | Evaluate (Atom (VarAtom uvar)) locals <- code@@ -239,21 +248,21 @@     let pass_in = LiftAct uvar locals globals heap confs         LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in     in Just (RuleAtomUnInt-            ,[state { state_heap    = heap'+            ,[state { state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate (Atom (VarAtom uvar)) locals'-                    , state_names   = confs' }])+                    , state_code = Evaluate (Atom (VarAtom uvar)) locals'+                    , state_names = confs' }])    -- 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    = SymLitEval pfun (map valueToLit vals)+        eval = SymLitEval pfun (map valueToLit vals)     in Just (RulePrimApp-            ,[state { state_heap    = heap'+            ,[state { state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate (Atom (LitAtom eval)) locals'-                    , state_names   = confs' }])+                    , state_code = Evaluate (Atom (LitAtom eval)) locals'+                    , state_names = confs' }])    -- Rule Con App   | Evaluate (ConApp dcon args) locals <- code =@@ -261,61 +270,61 @@         LiftAct vals _ globals' heap' confs' = liftAtomList pass_in         (heapf, addr) = allocHeap (ConObj dcon vals) heap'     in Just (RuleConApp-            ,[state { state_heap    = heapf+            ,[state { state_heap = heapf                     , state_globals = globals'-                    , state_code    = Return (MemVal addr)-                    , state_names   = confs' }])+                    , state_code = Return (MemVal addr)+                    , state_names = confs' }])    -- Rule Fun App Exact   | Evaluate (FunApp fun args) locals <- code-  , Just (_, hobj)              <- vlookupHeap fun locals globals heap+  , Just (_, hobj) <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj   , length params == length args =-    let pass_in   = LiftAct args locals globals heap confs+    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     in Just (RuleFunAppExact-            ,[state { state_heap    = heap'+            ,[state { state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate expr fun_locs'-                    , state_names   = confs' }])+                    , state_code = Evaluate expr fun_locs'+                    , state_names = confs' }])    -- Rule Fun App Under   | Evaluate (FunApp fun args) locals <- code-  , Just (_, hobj)              <- vlookupHeap fun locals globals heap+  , Just (_, hobj) <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj-  , (_, Left ex_params)         <- unevenZip params args =-    let pass_in   = LiftAct args locals globals heap confs+  , (_, 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         -- New Fun Object.-        pobj      = FunObj ex_params expr fun_locs'+        pobj = FunObj ex_params expr fun_locs'         (heapf, paddr) = allocHeap pobj heap'     in Just (RuleFunAppUnder-            ,[state { state_heap    = heapf+            ,[state { state_heap = heapf                     , state_globals = globals'-                    , state_code    = Return (MemVal paddr)-                    , state_names   = confs' }])+                    , state_code = Return (MemVal paddr)+                    , state_names = confs' }])    -- Rule Fun App Symbolic   | Evaluate (FunApp sfun args) locals <- code-  , Just (_, hobj)         <- vlookupHeap sfun locals globals heap+  , Just (_, hobj) <- vlookupHeap sfun locals globals heap   , SymObj (Symbol svar _) <- hobj =     let sname = freshSeededName (varName svar) confs         svar' = Var sname (foldl AppTy (varType svar) (map atomType args))-        sym   = Symbol svar' (Just (FunApp sfun args, locals))+        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 { 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 =-       Just (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@@ -323,20 +332,20 @@     let pass_in = LiftAct ufun locals globals heap confs         LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in     in Just (RuleFunAppUnInt-            ,[state { state_heap    = heap'+            ,[state { state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate (FunApp ufun args) locals'-                    , state_names   = confs' }])+                    , state_code = Evaluate (FunApp ufun args) locals'+                    , state_names = confs' }])    -- Rule Let   | Evaluate (Let bnd expr) locals <- code =     let pass_in = LiftAct bnd locals globals heap confs         LiftAct _ locals' globals' heap' confs' = liftBind pass_in     in Just (RuleLet-            ,[state { state_heap    = heap'+            ,[state { state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate expr locals'-                    , state_names   = confs' }])+                    , state_code = Evaluate expr locals'+                    , state_names = confs' }])    -- Rule Case Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code@@ -347,18 +356,18 @@    -- 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+  , Just (addr, hobj) <- vlookupHeap mvar locals globals heap+  , ConObj dcon vals <- hobj   , (Alt _ params expr):_ <- matchDataAlts dcon alts   , length params == length vals =-    let kvs     = (cvar, MemVal addr) : zip params vals+    let kvs = (cvar, MemVal addr) : zip params vals         locals' = insertLocalsList kvs 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+  , [] <- matchLitAlts lit alts   , (Alt _ _ expr):_ <- defaultAlts alts =     let locals' = insertLocals (cvar, LitVal lit) locals     in Just (RuleCaseAnyLit@@ -367,64 +376,64 @@   -- 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 =+  , ConObj dcon _ <- hobj+  , [] <- matchDataAlts dcon alts+  , (Alt _ _ expr):_ <- defaultAlts alts =     let locals' = insertLocals (cvar, MemVal addr) 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+  , Just (addr, hobj) <- vlookupHeap mvar locals globals heap+  , SymObj _ <- hobj   , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)   , length (acon_alts ++ def_alts) > 0 =-    let acon_ins   = map (\a -> LiftAct (mvar, addr, cvar, a)-                                        locals globals heap confs) acon_alts+    let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a)+                                      locals globals heap confs) acon_alts         acon_lifts = map liftSymAlt acon_ins-        def_ins    = map (\a -> LiftAct (mvar, addr, cvar, a)-                                        locals globals heap confs) def_alts-        def_lifts  = map liftSymAlt def_ins+        def_ins = map (\a -> LiftAct (mvar, addr, cvar, a)+                                     locals globals heap confs) def_alts+        def_lifts = map liftSymAlt def_ins         -- Make AltCon states first.-        acon_sts   = map (liftedAltToState state) acon_lifts+        acon_sts = map (liftedAltToState state) acon_lifts         -- Make DEFAULT states next.-        all_conss  = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts-        negatives  = map negateConstraint all_conss+        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-        def_sts    = map (liftedAltToState state) def_lifts'+        def_sts = map (liftedAltToState state) def_lifts'     in Just (RuleCaseSym, acon_sts ++ def_sts) -  -- Stack Dependent Rules+-- Stack Dependent Rules    -- Rule Update Frame Create Thunk   | Evaluate (Atom (VarAtom var)) locals <- code-  , Just (addr, hobj)       <- vlookupHeap var locals globals heap-  , FunObj [] expr fun_locs <- hobj = -- Thunk form.+  , Just (addr, hobj) <- vlookupHeap var locals globals heap+  , FunObj [] expr fun_locs <- hobj =  -- Thunk form.     let frame = UpdateFrame addr     in Just (RuleUpdateCThunk             ,[state { state_stack = pushStack frame stack-                    , state_heap  = insertHeap (addr, Blackhole) heap-                    , state_code  = Evaluate expr fun_locs }])+                    , state_heap = insertHeap (addr, Blackhole) heap+                    , state_code = Evaluate expr fun_locs }])    -- Rule Update Frame Delete Lit   | Just (UpdateFrame frm_addr, stack') <- popStack stack-  , Return (LitVal lit)                 <- code =-       Just (RuleUpdateDLit-            ,[state { state_stack = stack'-                    , state_heap  = insertHeap (frm_addr, LitObj lit) heap-                    , state_code  = Return (LitVal lit) }])+  , Return (LitVal lit) <- code =+    Just (RuleUpdateDLit+         ,[state { state_stack = stack'+                 , state_heap = insertHeap (frm_addr, LitObj lit) heap+                 , state_code = Return (LitVal lit) }])    -- Rule Update Frame Delete Val Pointer   | Just (UpdateFrame frm_addr, stack') <- popStack stack-  , Return (MemVal addr)                <- code+  , Return (MemVal addr) <- code   , Just hobj <- lookupHeap addr heap   , isHeapValueForm hobj =-       Just (RuleUpdateDValPtr-            ,[state { state_stack = stack'-                    , state_heap  = insertHeap (frm_addr, AddrObj addr) heap-                    , state_code  = Return (MemVal addr) }])+    Just (RuleUpdateDValPtr+         ,[state { state_stack = stack'+                 , state_heap = insertHeap (frm_addr, AddrObj addr) heap+                 , state_code = Return (MemVal addr) }])    -- Rule Case Frame Create Case Non LitVal or MemVal   | Evaluate (Case mxpr cvar alts) locals <- code@@ -432,80 +441,80 @@     let frame = CaseFrame cvar alts locals     in Just (RuleCaseCCaseNonVal             ,[state { state_stack = pushStack frame stack-                    , state_code  = Evaluate mxpr locals }])+                    , state_code = Evaluate mxpr locals }])      -- Rule Case Frame Delete Lit   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack-  , Return (LitVal lit)                         <- code =+  , Return (LitVal lit) <- code =     let mxpr = Atom (LitAtom lit)     in Just (RuleCaseDLit             ,[state { state_stack = stack'-                    , state_code  = Evaluate (Case mxpr cvar alts) frm_locs }])+                    , state_code = Evaluate (Case mxpr cvar alts) frm_locs }])    -- Rule Case Frame Delete Heap Value   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack-  , Return (MemVal addr)                        <- code+  , Return (MemVal addr) <- code   , Just hobj <- lookupHeap addr heap   , isHeapValueForm hobj =-    let vname     = freshSeededName (varName cvar) confs-        vvar      = Var vname (varType cvar)-        mxpr      = Atom (VarAtom vvar)+    let vname = freshSeededName (varName cvar) confs+        vvar = Var vname (varType cvar)+        mxpr = Atom (VarAtom vvar)         frm_locs' = insertLocals (vvar, MemVal addr) frm_locs     in Just (RuleCaseDValPtr             ,[state { state_stack = stack'-                    , state_code  = Evaluate (Case mxpr cvar alts) frm_locs'+                    , state_code = Evaluate (Case mxpr cvar alts) frm_locs'                     , state_names = vname : confs }])    -- Rule Apply Frame Create Function Thunk   | Evaluate (FunApp fun args) locals <- code   , Just (_, hobj) <- vlookupHeap fun locals globals heap-  , FunObj [] _ _  <- hobj =+  , FunObj [] _ _ <- hobj =     let frame = ApplyFrame args locals     in Just (RuleApplyCFunThunk             ,[state { state_stack = pushStack frame stack-                    , state_code  = Evaluate (Atom (VarAtom fun)) locals }])+                    , state_code = Evaluate (Atom (VarAtom fun)) locals }])    -- Rule Apply Frame Create Function Over Application   | Evaluate (FunApp fun args) locals <- code-  , Just (_, hobj)              <- vlookupHeap fun locals globals heap+  , Just (_, hobj) <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj-  , (_, Right ex_args)          <- unevenZip params args =-    let pass_in   = LiftAct args locals globals heap confs+  , (_, 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-        frame     = ApplyFrame ex_args locals'+        frame = ApplyFrame ex_args locals'     in Just (RuleApplyCFunAppOver-            ,[state { state_stack   = pushStack frame stack-                    , state_heap    = heap'+            ,[state { state_stack = pushStack frame stack+                    , state_heap = heap'                     , state_globals = globals'-                    , state_code    = Evaluate expr fun_locs'-                    , state_names   = confs' }])+                    , state_code = Evaluate expr fun_locs'+                    , state_names = confs' }])    -- Rule Apply Frame Delete ReturnPtr Function   | Just (ApplyFrame args frm_locs, stack') <- popStack stack-  , Return (MemVal addr)                    <- code-  , Just hobj    <- lookupHeap addr heap+  , Return (MemVal addr) <- code+  , Just hobj <- lookupHeap addr heap   , FunObj _ _ _ <- hobj-  , Just ftype   <- memAddrType addr heap =-    let fname     = freshName VarNSpace confs-        fvar      = Var fname ftype+  , Just ftype <- memAddrType addr heap =+    let fname = freshName VarNSpace confs+        fvar = Var fname ftype         frm_locs' = insertLocals (fvar, MemVal addr) frm_locs     in Just (RuleApplyDReturnFun             ,[state { state_stack = stack'-                    , state_code  = Evaluate (FunApp fvar args) frm_locs'+                    , state_code = Evaluate (FunApp fvar args) frm_locs'                     , state_names = fname : confs }])    -- Rule Apply Frame Delete ReturnPtr Sym   | Just (ApplyFrame args frm_locs, stack') <- popStack stack-  , Return (MemVal addr)                    <- code-  , Just hobj              <- lookupHeap addr heap+  , Return (MemVal addr) <- code+  , Just hobj <- lookupHeap addr heap   , SymObj (Symbol svar _) <- hobj =-    let sname     = freshSeededName (varName svar) confs-        svar'     = Var sname (varType svar)+    let sname = freshSeededName (varName svar) confs+        svar' = Var sname (varType svar)         frm_locs' = insertLocals (svar', MemVal addr) frm_locs     in Just (RuleApplyDReturnSym             ,[state { state_stack = stack'-                    , state_code  = Evaluate (FunApp svar' args) frm_locs'+                    , state_code = Evaluate (FunApp svar' args) frm_locs'                     , state_names = sname : confs }])    -- State is Value Form

@@ -8,8 +8,8 @@     , runBoundedDFSLogged     ) where +import SSTG.Core.Language import SSTG.Core.Execution.Rules-import SSTG.Core.Execution.Support  import qualified Data.Char as C import qualified Data.List as L@@ -17,10 +17,11 @@ -- | Custom hash function. hash :: [Rule] -> Int hash rules = L.foldl' (\acc c -> (acc + p2 * C.ord c)`mod` p3) p1 str-  where str = concatMap show rules-        p1  = 5381-        p2  = 1009-        p3  = 433494437+  where+    str = concatMap show rules+    p1 = 5381+    p2 = 1009+    p3 = 433494437  -- | A `State` that is not in value form yet, capable of being evaluated. A -- list of `Rule`s is kept to denote reduction history.@@ -33,16 +34,17 @@ -- | Increment Status conditions, and shift the current / parent id as needed. incStatus :: Maybe Int -> State -> State incStatus mb_id state = state { state_status = status' }-  where status  = state_status state-        status' = case mb_id of-                      Nothing  -> incStatusSteps status-                      Just id' -> incStatusSteps (updateStatusId id' status)+  where+    status = state_status state+    status' = case mb_id of+                  Nothing -> incStatusSteps status+                  Just id' -> incStatusSteps (updateStatusId id' status)  -- | Given a list of `State` along with its list of past `Rule` reductions, -- apply STG reduction. If reduction yields `Nothing`, simply return itself. step :: ([Rule], State) -> [([Rule], State)] step (hist, start) = case reduce start of-    Nothing              -> [(hist, start)]+    Nothing -> [(hist, start)]     Just (rule, results) ->         let trace = hist ++ [rule]             mb_id = if length results > 1@@ -53,17 +55,19 @@ -- | This is what we use the `<*>` over. pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState]) pass rule_states = (lives, \prev -> prev ++ deads)-  where stepped = concatMap step rule_states-        lives   = filter (not . isStateValueForm . snd) stepped-        deads   = filter       (isStateValueForm . snd) stepped+  where+    stepped = concatMap step rule_states+    lives = filter (not . isStateValueForm . snd) stepped+    deads = filter (isStateValueForm . snd) stepped  -- | Run bounded breadth-first-search of the execution space with an `Int` to -- denote the maximum number of steps to take. runBoundedBFS :: Int -> State -> ([LiveState], [DeadState]) runBoundedBFS n state = (run execution) [([], state)]-  where passes    = take n (repeat (SymbolicT { run = pass }))-        start     = SymbolicT { run = (\lives -> (lives, [])) }-        execution = foldl (\acc s -> s <*> acc) start passes+  where+    passes = take n (repeat (SymbolicT { run = pass }))+    start = SymbolicT { run = (\lives -> (lives, [])) }+    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

@@ -1,348 +0,0 @@--- | Symbolic STG Execution Support Architecture-module SSTG.Core.Execution.Support-    ( SymbolicT(..)-    , fmap-    , pure-    , (<*>)-    , return-    , (>>=)--    , State(..)-    , Symbol(..)-    , Status(..)-    , Stack-    , Frame(..)-    , MemAddr-    , Value(..)-    , Locals-    , Heap-    , HeapObj(..)-    , Globals-    , Code(..)-    , PathCons-    , Constraint(..)--    , nameOccStr-    , nameUnique-    , varName-    , null_addr-    , addrInt--    , init_status-    , incStatusSteps-    , updateStatusId--    , empty_stack-    , popStack-    , pushStack-    , stackToList--    , empty_locals-    , lookupLocals-    , insertLocals-    , insertLocalsList-    , localsToList--    , empty_heap-    , lookupHeap-    , allocHeap-    , allocHeapList-    , insertHeap-    , insertHeapList-    , heapToList--    , empty_globals-    , lookupGlobals-    , insertGlobals-    , insertGlobalsList-    , globalsToList--    , empty_pathcons-    , insertPathCons-    , insertPathConsList-    , pathconsToList--    , lookupValue-    , vlookupHeap-    , memAddrType-    ) where--import SSTG.Core.Language--import qualified Data.Map as M---- | Symbolic Transformation represents transformations applied to some--- State`(s). This is useful in allowing us to transfer from different actions--- within the engine.-newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) }---- | Functor instance of Symbolic Transformation.-instance Functor (SymbolicT s) where-    fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1))---- | Applicative instance of Symbolic Transformation.-instance Applicative (SymbolicT s) where-    pure a    = SymbolicT (\s -> (s, a))--    sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0-                                      (s2, f2) = (run sf) s1 in (s2, f2 a1))---- | Monad instance of Symbolic Transformation.-instance Monad (SymbolicT s) where-    return a  = pure a--    st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0-                                      (s2, a2) = (run (fs a1)) s1 in (s2, a2))---- | `State` contains the information necessary to perform symbolic execution.--- Eval/Apply graph reduction semantics are used.-data State = State { state_status  :: Status-                   , state_stack   :: Stack-                   , state_heap    :: Heap-                   , state_globals :: Globals-                   , state_code    :: Code-                   , state_names   :: [Name]-                   , state_paths   :: 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.-data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)---- | State status.-data Status = Status { status_id        :: Int-                     , status_parent_id :: Int-                     , status_steps     :: Int-                     } deriving (Show, Eq, Read)---- | Execution stack used in graph reduction semnatics.-newtype Stack = Stack [Frame] deriving (Show, Eq, Read)---- | Frames of a stack.-data Frame = CaseFrame   Var [Alt] Locals-           | ApplyFrame  [Atom] Locals-           | UpdateFrame MemAddr-           deriving (Show, Eq, Read)---- | 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--- 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)---- | Locals binds a `Var`'s `Name` to its some `Value`.-newtype Locals = Locals (M.Map Name Value) 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--- on the `Heap`.-data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read)---- | Heap objects.-data HeapObj = LitObj  Lit-             | SymObj  Symbol-             | ConObj  DataCon [Value]-             | FunObj  [Var] Expr Locals-             | AddrObj MemAddr-             | Blackhole-             deriving (Show, Eq, Read)---- | 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)---- | Evaluation of the current expression. We are either evaluating, or ready--- to return with some `Value`.-data Code = Evaluate Expr Locals-          | Return   Value-          deriving (Show, Eq, Read)---- | Path constraints are the conjunctive normal form of `Constraint`s.-newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)---- | Constraints denote logical paths taken in program execution thus far.-data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool-                deriving (Show, Eq, Read)----   Simple functions that require only the immediate data structure.---- | A `Name`'s occurrence string.-nameOccStr :: Name -> String-nameOccStr (Name occ _ _ _) = occ---- | `Name` imique `Int`.-nameUnique :: Name -> Int-nameUnique (Name _ _ _ unq) = unq---- | Variable name.-varName :: Var -> Name-varName (Var name _) = name---- | Null `MemAddr`.-null_addr :: MemAddr-null_addr = MemAddr 0---- | `MemAddr`'s `Int` value.-addrInt :: MemAddr -> Int-addrInt (MemAddr int) = int---- | Initial `Status`.-init_status :: Status-init_status = Status { status_id        = 1-                     , status_parent_id = 0-                     , status_steps     = 0 }---- | Increment `Status` steps.-incStatusSteps :: Status -> Status-incStatusSteps status = status { status_steps = (status_steps status) + 1 }---- | Update the `Status` id.-updateStatusId :: Int -> Status -> Status-updateStatusId new_id status = status { status_id        = new_id-                                      , status_parent_id = status_id status }---- | Empty `Stack.-empty_stack :: Stack-empty_stack = Stack []---- | `Stack` pop.-popStack :: Stack -> Maybe (Frame, Stack)-popStack (Stack [])             = Nothing-popStack (Stack (frame:frames)) = Just (frame, Stack frames)---- | `Stack` push.-pushStack :: Frame -> Stack -> Stack-pushStack frame (Stack frames) = Stack (frame : frames)---- | `Stack` as list of `Frame`s.-stackToList :: Stack -> [Frame]-stackToList (Stack frames) = frames---- | Empty `Locals`.-empty_locals :: Locals-empty_locals = Locals M.empty---- | `Locals` lookup.-lookupLocals :: Var -> Locals -> Maybe Value-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)---- | List insertion into `Locals`.-insertLocalsList :: [(Var, Value)] -> Locals -> Locals-insertLocalsList kvs locals = foldr insertLocals locals kvs---- | `Locals` to key value pairs.-localsToList :: Locals -> [(Name, Value)]-localsToList (Locals lmap) = M.toList lmap---- | Empty `Heap`.-empty_heap :: Heap-empty_heap = Heap M.empty null_addr---- | `Heap` lookup.-lookupHeap :: MemAddr -> Heap -> Maybe HeapObj-lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of-    Just (AddrObj redir) -> lookupHeap redir (Heap hmap prev)-    mb_hobj              -> mb_hobj---- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`.-allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)-allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr)-  where addr  = MemAddr ((addrInt prev) + 1)-        hmap' = M.insert addr hobj hmap---- | 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)-  where (heap', addr) = allocHeap hobj heap-        (heapf, as)   = allocHeapList hobjs heap'---- | `Heap` direct insertion at a specific `MemAddr`.-insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap-insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev---- | Insert a list of `HeapObj` at specified `MemAddr` locations.-insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap-insertHeapList kvs heap = foldr insertHeap heap kvs---- | `Heap` to key value pairs.-heapToList :: Heap -> [(MemAddr, HeapObj)]-heapToList (Heap hmap _) = M.toList hmap---- | Empty `Globals`.-empty_globals :: Globals-empty_globals = Globals M.empty---- | `Globals` lookup.-lookupGlobals :: Var -> Globals -> Maybe Value-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)---- | Insert a list of `Var` and `Value` 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---- | `Globals` to key value pairs.-globalsToList :: Globals -> [(Name, Value)]-globalsToList (Globals gmap) = M.toList gmap---- | Empty `PathCons`.-empty_pathcons :: PathCons-empty_pathcons = PathCons []---- | `PathCons` insertion.-insertPathCons :: Constraint -> PathCons -> PathCons-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---- | `PathCons` to list of `Constraint`s.-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-    Nothing  -> lookupGlobals var globals-    Just val -> Just val---- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found.-vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)-vlookupHeap var locals globals heap = do-    val <- lookupValue var locals globals-    case val of-        LitVal _    -> Nothing-        MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)---- | Type of `HeapObj` held at `MemAddr`, if found.-memAddrType :: MemAddr -> Heap -> Maybe Type-memAddrType addr heap = do-    hobj <- lookupHeap addr heap-    case hobj of-        AddrObj redir       -> memAddrType redir heap-        LitObj lit          -> Just (litType lit)-        SymObj (Symbol s _) -> Just (varType s)-        ConObj dcon _       -> Just (dataconType dcon)-        FunObj ps e _       -> Just (foldr FunTy (exprType e) (map varType ps))-        Blackhole           -> Just Bottom-

@@ -1,9 +1,13 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Language-    ( module SSTG.Core.Language.Syntax+    ( module SSTG.Core.Language.Naming+    , module SSTG.Core.Language.Support+    , module SSTG.Core.Language.Syntax     , module SSTG.Core.Language.Typing     ) where +import SSTG.Core.Language.Naming+import SSTG.Core.Language.Support import SSTG.Core.Language.Syntax import SSTG.Core.Language.Typing 

@@ -0,0 +1,217 @@+-- | Naming Module+module SSTG.Core.Language.Naming+    ( allNames+    , freshString+    , freshName+    , freshSeededName+    , freshNameList+    , freshSeededNameList+    ) where++import SSTG.Core.Language.Support+import SSTG.Core.Language.Syntax++import qualified Data.List as L+import qualified Data.Set as S++-- | All `Name`s in a `State`.+allNames :: State -> [Name]+allNames state = L.nub acc_ns+  where+    stack_ns = stackNames (state_stack state)+    heap_ns = heapNames (state_heap state)+    glbls_ns = globalsNames (state_globals state)+    expr_ns = codeNames (state_code state)+    pcons_ns = pconsNames (state_paths state)+    acc_ns = stack_ns ++ heap_ns ++ glbls_ns ++ expr_ns ++ pcons_ns++-- | `Name`s in a `Stack`.+stackNames :: Stack -> [Name]+stackNames stack = concatMap frameNames (stackToList stack)++-- | `Name`s in a `Frame`.+frameNames :: Frame -> [Name]+frameNames (UpdateFrame _) = []+frameNames (ApplyFrame as ls) = localsNames ls ++ concatMap atomNames as+frameNames (CaseFrame var alts ls) = localsNames ls ++ concatMap altNames alts+                                                    ++ varNames var++-- | `Name`s in an `Alt`.+altNames :: Alt -> [Name]+altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr++-- | `Name`s in the `Locals`+localsNames :: Locals -> [Name]+localsNames locals = map fst (localsToList locals)++-- | `Name`s in the `Heap`.+heapNames :: Heap -> [Name]+heapNames heap = concatMap (heapObjNames . snd) (heapToList heap)++-- | `Name`s in a `HeapObj`.+heapObjNames :: HeapObj -> [Name]+heapObjNames (AddrObj _) = []+heapObjNames (Blackhole) = []+heapObjNames (LitObj _) = []+heapObjNames (SymObj sym) = symbolNames sym+heapObjNames (ConObj dcon _) = dataNames dcon+heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs+                                                    ++ concatMap varNames ps++-- | `Name`s in a `Symbol`.+symbolNames :: Symbol -> [Name]+symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_ns+  where+    scls_ns = case mb_scls of+                  Nothing -> []+                  Just (e, l) -> exprNames e ++ localsNames l++-- | `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++-- | `Name`s in a `Var`.+varNames :: Var -> [Name]+varNames (Var n t) = n : typeNames t++-- | `Name`s in an `Atom`.+atomNames :: Atom -> [Name]+atomNames (LitAtom _) = []+atomNames (VarAtom var) = varNames var++-- | `Name`s in `Globals`.+globalsNames :: Globals -> [Name]+globalsNames globals = map fst (globalsToList globals)++-- | `Name`s in the current evaluation `Code`.+codeNames :: Code -> [Name]+codeNames (Return _) = []+codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals++-- | `Name`s in an `Expr`.+exprNames :: Expr -> [Name]+exprNames (Atom atom) = atomNames atom+exprNames (Let bnd expr) = exprNames expr ++ bindNames bnd+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 (Case expr var alts) = exprNames expr ++ concatMap altNames alts+                                                ++ varNames var+-- | `Name`s in a `Type`.+typeNames :: Type -> [Name]+typeNames (TyVarTy n ty) = n : typeNames ty+typeNames (CoercionTy coer) = coercionNames coer+typeNames (AppTy t1 t2) = typeNames t1 ++ typeNames t2+typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer+typeNames (ForAllTy bnd ty) = typeNames ty ++ tyBinderNames bnd+typeNames (FunTy t1 t2) = typeNames t1 ++ typeNames t2+typeNames (TyConApp tc ty) = tyConNames tc ++ concatMap typeNames ty+typeNames (LitTy _) = []+typeNames (Bottom) = []++-- | `Name`s in a `PrimFun`.+pfunNames :: PrimFun -> [Name]+pfunNames (PrimFun n ty) = n : typeNames ty++-- | `Name`s in a `DataCon`.+dataNames :: DataCon -> [Name]+dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys)++-- | `Name`s in a `TyBinder`.+tyBinderNames :: TyBinder -> [Name]+tyBinderNames (AnonTyBndr) = []+tyBinderNames (NamedTyBndr n) = [n]++-- | `Name`s in a `TyCon`.+tyConNames :: TyCon -> [Name]+tyConNames (FamilyTyCon n ns) = n : ns+tyConNames (SynonymTyCon n ns) = n : ns+tyConNames (AlgTyCon n ns r) = n : ns ++ algTyRhsNames r+tyConNames (FunTyCon n bs) = n : concatMap tyBinderNames bs+tyConNames (PrimTyCon n bs) = n : concatMap tyBinderNames bs+tyConNames (Promoted n bs dc) = n : concatMap tyBinderNames bs ++ dataNames dc++-- | `Name`s in a `Coercion`.+coercionNames :: Coercion -> [Name]+coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2++-- | `Name`s in a `AlgTyRhs`.+algTyRhsNames :: AlgTyRhs -> [Name]+algTyRhsNames (AbstractTyCon _) = []+algTyRhsNames (DataTyCon ns) = ns+algTyRhsNames (TupleTyCon n) = [n]+algTyRhsNames (NewTyCon n) = [n]++-- | `Name`s in a `Bind`.+bindNames :: Bind -> [Name]+bindNames (Bind _ bnd) = lhs ++ rhs+  where+    lhs = concatMap (varNames . fst) bnd+    rhs = concatMap (bindRhsNames . snd) bnd++-- | `Name`s in a `PathCons`.+pconsNames :: PathCons -> [Name]+pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons)++-- | `Name`s in a `PathCons`.+constraintNames :: Constraint -> [Name]+constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs+                                                            ++ map varName vs++-- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of+-- `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+  where+    pick = bank !! index+    index = raw_i `mod` (length bank)+    raw_i = (abs rand) * prime+    prime = 151  -- The original? :)+    bank = lower ++ upper ++ nums+    lower = "abcdefghijlkmnopqrstuvwxyz"+    upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"+    nums = "1234567890"++-- | Fresh `Name` given a list of `Name`s that acts as conflicts. The fresh+-- `Name`s generated in this manner are prefixed with @"fs?"@, which is not a+-- valid identifier in Haskell, but okay in SSTG. we also specify the+-- `NameSpace` under which the `Name` will be generated. This will generally+-- be `VarNSpace` in actual usage.+freshName :: NameSpace -> [Name] -> Name+freshName nspace confs = freshSeededName seed confs+  where+    seed = Name "fs?" Nothing nspace 0++-- | A fresh `Name` generated from a seed `Name`, which will act as the prefix+-- of the new `Name`. We ues the same `NameSpace` as the seed `Name` when+-- generating this way.+freshSeededName :: Name -> [Name] -> Name+freshSeededName seed confs = Name occ' mdl ns unq'+  where+    Name occ mdl ns unq = seed+    occ' = freshString 1 occ (S.fromList alls)+    unq' = maxs + 1+    alls = map nameOccStr confs+    maxs = L.maximum (unq : map nameUnique 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'+  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'+  where+    name' = freshSeededName n confs+    confs' = name' : confs+

@@ -0,0 +1,351 @@+-- | Symbolic STG Execution Support Architecture+module SSTG.Core.Language.Support+    ( SymbolicT(..)+    , fmap+    , pure+    , (<*>)+    , return+    , (>>=)++    , State(..)+    , Symbol(..)+    , Status(..)+    , Stack+    , Frame(..)+    , MemAddr+    , Value(..)+    , Locals+    , Heap+    , HeapObj(..)+    , Globals+    , Code(..)+    , PathCons+    , Constraint(..)++    , nameOccStr+    , nameUnique+    , varName+    , null_addr+    , addrInt++    , init_status+    , incStatusSteps+    , updateStatusId++    , empty_stack+    , popStack+    , pushStack+    , stackToList++    , empty_locals+    , lookupLocals+    , insertLocals+    , insertLocalsList+    , localsToList++    , empty_heap+    , lookupHeap+    , allocHeap+    , allocHeapList+    , insertHeap+    , insertHeapList+    , heapToList++    , empty_globals+    , lookupGlobals+    , insertGlobals+    , insertGlobalsList+    , globalsToList++    , empty_pathcons+    , insertPathCons+    , insertPathConsList+    , pathconsToList++    , lookupValue+    , vlookupHeap+    , memAddrType+    ) where++import SSTG.Core.Language.Syntax+import SSTG.Core.Language.Typing++import qualified Data.Map as M++-- | Symbolic Transformation represents transformations applied to some+-- State`(s). This is useful in allowing us to transfer from different actions+-- within the engine.+newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) }++-- | Functor instance of Symbolic Transformation.+instance Functor (SymbolicT s) where+    fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1))++-- | Applicative instance of Symbolic Transformation.+instance Applicative (SymbolicT s) where+    pure a = SymbolicT (\s -> (s, a))++    sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0+                                      (s2, f2) = (run sf) s1 in (s2, f2 a1))++-- | Monad instance of Symbolic Transformation.+instance Monad (SymbolicT s) where+    return a = pure a++    st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0+                                      (s2, a2) = (run (fs a1)) s1 in (s2, a2))++-- | `State` contains the information necessary to perform symbolic execution.+-- Eval/Apply graph reduction semantics are used.+data State = State { state_status :: !Status+                   , state_stack :: !Stack+                   , state_heap :: !Heap+                   , state_globals :: !Globals+                   , state_code :: !Code+                   , state_names :: ![Name]+                   , state_paths :: !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.+data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)++-- | State status.+data Status = Status { status_id :: !Int+                     , status_parent :: !Int+                     , status_steps :: !Int+                     } deriving (Show, Eq, Read)++-- | Execution stack used in graph reduction semnatics.+newtype Stack = Stack [Frame] deriving (Show, Eq, Read)++-- | Frames of a stack.+data Frame = CaseFrame Var [Alt] Locals+           | ApplyFrame [Atom] Locals+           | UpdateFrame MemAddr+           deriving (Show, Eq, Read)++-- | 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+-- 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)++-- | Locals binds a `Var`'s `Name` to its some `Value`.+newtype Locals = Locals (M.Map Name Value) 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+-- on the `Heap`.+data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read)++-- | Heap objects.+data HeapObj = LitObj Lit+             | SymObj Symbol+             | ConObj DataCon [Value]+             | FunObj [Var] Expr Locals+             | AddrObj MemAddr+             | Blackhole+             deriving (Show, Eq, Read)++-- | 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)++-- | Evaluation of the current expression. We are either evaluating, or ready+-- to return with some `Value`.+data Code = Evaluate Expr Locals+          | Return Value+          deriving (Show, Eq, Read)++-- | Path constraints are the conjunctive normal form of `Constraint`s.+newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)++-- | Constraints denote logical paths taken in program execution thus far.+data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool+                deriving (Show, Eq, Read)++-- Simple functions that require only the immediate data structure.++-- | A `Name`'s occurrence string.+nameOccStr :: Name -> String+nameOccStr (Name occ _ _ _) = occ++-- | `Name` imique `Int`.+nameUnique :: Name -> Int+nameUnique (Name _ _ _ unq) = unq++-- | Variable name.+varName :: Var -> Name+varName (Var name _) = name++-- | Null `MemAddr`.+null_addr :: MemAddr+null_addr = MemAddr 0++-- | `MemAddr`'s `Int` value.+addrInt :: MemAddr -> Int+addrInt (MemAddr int) = int++-- | Initial `Status`.+init_status :: Status+init_status = Status { status_id = 1+                     , status_parent = 0+                     , status_steps = 0 }++-- | Increment `Status` steps.+incStatusSteps :: Status -> Status+incStatusSteps status = status { status_steps = (status_steps status) + 1 }++-- | Update the `Status` id.+updateStatusId :: Int -> Status -> Status+updateStatusId new_id status = status { status_id = new_id+                                      , status_parent = status_id status }++-- | Empty `Stack.+empty_stack :: Stack+empty_stack = Stack []++-- | `Stack` pop.+popStack :: Stack -> Maybe (Frame, Stack)+popStack (Stack []) = Nothing+popStack (Stack (frame:frames)) = Just (frame, Stack frames)++-- | `Stack` push.+pushStack :: Frame -> Stack -> Stack+pushStack frame (Stack frames) = Stack (frame : frames)++-- | `Stack` as list of `Frame`s.+stackToList :: Stack -> [Frame]+stackToList (Stack frames) = frames++-- | Empty `Locals`.+empty_locals :: Locals+empty_locals = Locals M.empty++-- | `Locals` lookup.+lookupLocals :: Var -> Locals -> Maybe Value+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)++-- | List insertion into `Locals`.+insertLocalsList :: [(Var, Value)] -> Locals -> Locals+insertLocalsList kvs locals = foldr insertLocals locals kvs++-- | `Locals` to key value pairs.+localsToList :: Locals -> [(Name, Value)]+localsToList (Locals lmap) = M.toList lmap++-- | Empty `Heap`.+empty_heap :: Heap+empty_heap = Heap M.empty null_addr++-- | `Heap` lookup.+lookupHeap :: MemAddr -> Heap -> Maybe HeapObj+lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of+    Just (AddrObj redir) -> lookupHeap redir (Heap hmap prev)+    mb_hobj -> mb_hobj++-- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`.+allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)+allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr)+  where+    addr = MemAddr ((addrInt prev) + 1)+    hmap' = M.insert addr hobj hmap++-- | 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)+  where+    (heap', addr) = allocHeap hobj heap+    (heapf, as) = allocHeapList hobjs heap'++-- | `Heap` direct insertion at a specific `MemAddr`.+insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap+insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev++-- | Insert a list of `HeapObj` at specified `MemAddr` locations.+insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap+insertHeapList kvs heap = foldr insertHeap heap kvs++-- | `Heap` to key value pairs.+heapToList :: Heap -> [(MemAddr, HeapObj)]+heapToList (Heap hmap _) = M.toList hmap++-- | Empty `Globals`.+empty_globals :: Globals+empty_globals = Globals M.empty++-- | `Globals` lookup.+lookupGlobals :: Var -> Globals -> Maybe Value+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)++-- | Insert a list of `Var` and `Value` 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++-- | `Globals` to key value pairs.+globalsToList :: Globals -> [(Name, Value)]+globalsToList (Globals gmap) = M.toList gmap++-- | Empty `PathCons`.+empty_pathcons :: PathCons+empty_pathcons = PathCons []++-- | `PathCons` insertion.+insertPathCons :: Constraint -> PathCons -> PathCons+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++-- | `PathCons` to list of `Constraint`s.+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+    Nothing -> lookupGlobals var globals+    Just val -> Just val++-- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found.+vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)+vlookupHeap var locals globals heap = do+    val <- lookupValue var locals globals+    case val of+        LitVal _ -> Nothing+        MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)++-- | Type of `HeapObj` held at `MemAddr`, if found.+memAddrType :: MemAddr -> Heap -> Maybe Type+memAddrType addr heap = do+    hobj <- lookupHeap addr heap+    case hobj of+        AddrObj redir -> memAddrType redir heap+        LitObj lit -> Just (litType lit)+        SymObj (Symbol s _) -> Just (varType s)+        ConObj dcon _ -> Just (dataconType dcon)+        FunObj ps e _ -> Just (foldr FunTy (exprType e) (map varType ps))+        Blackhole -> Just Bottom+

@@ -3,29 +3,10 @@     ( module SSTG.Core.Language.Syntax     ) where -type Program  = GenProgram  Name Var--type Lit      = GenLit      Name Var-type Atom     = GenAtom     Name Var-type PrimFun  = GenPrimFun  Name Var-type Expr     = GenExpr     Name Var-type Alt      = GenAlt      Name Var-type AltCon   = GenAltCon   Name Var-type Bind     = GenBind     Name Var-type BindRhs  = GenBindRhs  Name Var--type DataCon  = GenDataCon  Name-type Type     = GenType     Name-type TyBinder = GenTyBinder Name-type Coercion = GenCoercion Name-type TyCon    = GenTyCon    Name-type AlgTyRhs = GenAlgTyRhs Name---- | A `Program` is defined as a list of bindings. The @bnd@ is an identifier+-- | 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.-newtype GenProgram bnd var = Program [GenBind bnd var]-                           deriving (Show, Eq, Read)+newtype Program = Program [Bind] deriving (Show, Eq, Read)  -- | Variables, data constructors, type variables, and type constructors. data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace@@ -39,92 +20,89 @@           deriving (Show, Eq, Read, Ord)  -- | Variables consist of a `Name` and a `Type`.-data Var = Var Name (GenType Name) deriving (Show, Eq, Read)+data Var = Var Name Type deriving (Show, Eq, Read)  -- | Literals are largely augmented from the original GHC implementation, with -- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for -- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to -- represent symbolic literal evaluation, as literal manipulation functions -- are defined in the Haskell Prelude, and thus outside of scope for us.-data GenLit bnd var = MachChar     Char (GenType bnd)-                    | MachStr      String (GenType bnd)-                    | MachInt      Int (GenType bnd)-                    | MachWord     Int (GenType bnd)-                    | MachFloat    Rational (GenType bnd)-                    | MachDouble   Rational (GenType bnd)-                    | MachNullAddr (GenType bnd)-                    | MachLabel    String (Maybe Int) (GenType bnd)-                    | BlankAddr-                    | AddrLit      Int-                    | SymLit       var-                    | SymLitEval   (GenPrimFun bnd var) [GenLit bnd var]-                    deriving (Show, Eq, Read)+data Lit = MachChar Char Type+         | MachStr String Type+         | MachInt Int Type+         | MachWord Int Type+         | MachFloat Rational Type+         | MachDouble Rational Type+         | MachLabel String (Maybe Int) Type+         | MachNullAddr Type+         | BlankAddr+         | AddrLit Int+         | SymLit Var+         | SymLitEval PrimFun [Lit]+         deriving (Show, Eq, Read)  -- | Atomic objects. `VarAtom` may be used for variable lookups, while -- `LitAtom` is used to denote literals.-data GenAtom bnd var = LitAtom (GenLit bnd var)-                     | VarAtom var-                     deriving (Show, Eq, Read)+data Atom = LitAtom (Lit)+          | VarAtom Var+          deriving (Show, Eq, Read)  -- | Primitive functions.-data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read)+data PrimFun = PrimFun Name Type deriving (Show, Eq, Read)  -- | Expressions closely correspond to their representation in GHC.-data GenExpr bnd var = Atom    (GenAtom bnd var)-                     | PrimApp (GenPrimFun bnd var) [GenAtom bnd var]-                     | ConApp  (GenDataCon bnd) [GenAtom bnd var]-                     | FunApp  var [GenAtom bnd var]-                     | Let     (GenBind bnd var) (GenExpr bnd var)-                     | Case    (GenExpr bnd var) var [GenAlt bnd var]-                     deriving (Show, Eq, Read)+data Expr = Atom Atom+          | PrimApp PrimFun [Atom]+          | ConApp DataCon [Atom]+          | FunApp Var [Atom]+          | Let Bind Expr+          | Case Expr Var [Alt]+          deriving (Show, Eq, Read)  -- | Alternatives utilize an `AltCon`, a list of parameters of that match to -- the appropriate `DataAlt` as applicable, and an expression for the result.-data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)-                    deriving (Show, Eq, Read)+data Alt = Alt AltCon [Var] Expr deriving (Show, Eq, Read)  -- | Alt Constructor-data GenAltCon bnd var = DataAlt (GenDataCon bnd)-                       | LitAlt  (GenLit bnd var)-                       | Default-                       deriving (Show, Eq, Read)+data AltCon = DataAlt DataCon+            | LitAlt Lit+            | Default+            deriving (Show, Eq, Read)  -- | Bind-data GenBind bnd var = Bind RecForm [(var, GenBindRhs bnd var)]-                     deriving (Show, Eq, Read)+data Bind = Bind RecForm [(Var, BindRhs)] deriving (Show, Eq, Read)  -- | Recursive? data RecForm = Rec | NonRec deriving (Show, Eq, Read)  -- | `BindRhs` taken straight from STG can be either in constructor form, or -- function form. Empty parameter list denotes a thunk.-data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]-                        | FunForm [var] (GenExpr bnd var)-                        deriving (Show, Eq, Read)+data BindRhs = ConForm DataCon [Atom]+             | FunForm [Var] Expr+             deriving (Show, Eq, Read)  -- | Data Constructor consists of its tag, the type that corresponds to its -- ADT, and a list of paramters it takes.-data GenDataCon bnd = DataCon bnd (GenType bnd) [GenType bnd]-                    deriving (Show, Eq, Read)+data DataCon = DataCon Name Type [Type] deriving (Show, Eq, Read)  -- | Types are information that are useful to keep during symbolic execution -- in order to generate correct feeds into the SMT solver. Overapproxmation is -- currently performed, and is likely to be cut back in the future.-data GenType bnd = TyVarTy    bnd (GenType bnd)-                 | AppTy      (GenType bnd) (GenType bnd)-                 | ForAllTy   (GenTyBinder bnd) (GenType bnd)-                 | CastTy     (GenType bnd) (GenCoercion bnd)-                 | TyConApp   (GenTyCon bnd) [GenType bnd]-                 | CoercionTy (GenCoercion bnd)-                 | LitTy      TyLit-                 | FunTy      (GenType bnd) (GenType bnd)-                 | Bottom-                 deriving (Show, Eq, Read)+data Type = TyVarTy Name Type+          | AppTy Type Type+          | ForAllTy TyBinder Type+          | CastTy Type Coercion+          | TyConApp TyCon [Type]+          | CoercionTy Coercion+          | LitTy TyLit+          | FunTy Type Type+          | Bottom+          deriving (Show, Eq, Read)  -- | Type binder for `ForAllTy`.-data GenTyBinder bnd = NamedTyBndr bnd-                     | AnonTyBndr-                     deriving (Show, Eq, Read)+data TyBinder = NamedTyBndr Name+              | AnonTyBndr+              deriving (Show, Eq, Read)  -- | `Type` literal. data TyLit = NumTyLit Int@@ -132,22 +110,21 @@            deriving (Show, Eq, Read)  -- | Coercion. I have no idea what this does :)-data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)-                     deriving (Show, Eq, Read)+data Coercion = Coercion Type Type deriving (Show, Eq, Read)  -- | Type constructor.-data GenTyCon bnd = FunTyCon     bnd [GenTyBinder bnd]-                  | AlgTyCon     bnd [bnd] (GenAlgTyRhs bnd)-                  | SynonymTyCon bnd [bnd]-                  | FamilyTyCon  bnd [bnd]-                  | PrimTyCon    bnd [GenTyBinder bnd]-                  | Promoted     bnd [GenTyBinder bnd] (GenDataCon bnd)-                  deriving (Show, Eq, Read)+data TyCon = FunTyCon Name [TyBinder]+           | AlgTyCon Name [Name] AlgTyRhs+           | SynonymTyCon Name [Name]+           | FamilyTyCon Name [Name]+           | PrimTyCon Name [TyBinder]+           | Promoted Name [TyBinder] DataCon+           deriving (Show, Eq, Read)  -- | ADT RHS.-data GenAlgTyRhs bnd = AbstractTyCon Bool-                     | DataTyCon     [bnd]-                     | NewTyCon      bnd-                     | TupleTyCon    bnd-                     deriving (Show, Eq, Read)+data AlgTyRhs = AbstractTyCon Bool+              | DataTyCon [Name]+              | NewTyCon Name+              | TupleTyCon Name+              deriving (Show, Eq, Read) 

@@ -11,17 +11,17 @@  -- | Literal type. litType :: Lit -> Type-litType (MachChar _ ty)      = ty-litType (MachStr _ ty)       = ty-litType (MachInt _ ty)       = ty-litType (MachWord _ ty)      = ty-litType (MachFloat _ ty)     = ty-litType (MachDouble _ ty)    = ty-litType (MachNullAddr ty)    = ty-litType (MachLabel _ _ ty)   = ty-litType (BlankAddr)          = Bottom-litType (AddrLit _)          = Bottom-litType (SymLit var)         = varType var+litType (MachChar _ ty) = ty+litType (MachStr _ ty) = ty+litType (MachInt _ ty) = ty+litType (MachWord _ ty) = ty+litType (MachFloat _ ty) = ty+litType (MachDouble _ ty) = ty+litType (MachLabel _ _ ty) = ty+litType (MachNullAddr ty) = ty+litType (BlankAddr) = Bottom+litType (AddrLit _) = Bottom+litType (SymLit var) = varType var litType (SymLitEval pf args) = foldl AppTy (primfunType pf) (map litType args)  -- | Atom type.@@ -43,11 +43,11 @@  -- | I wonder what this could possibly be? exprType :: Expr -> Type-exprType (Atom atom)       = atomType atom+exprType (Atom atom) = atomType atom exprType (PrimApp pf args) = foldl AppTy (primfunType pf) (map atomType args)-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 _                 = Bottom+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 _ = Bottom 

@@ -0,0 +1,7 @@+-- | Export Module for SSTG.Core.Preprocessing+module SSTG.Core.Preprocessing+    ( module SSTG.Core.Preprocessing.Defunctionalization+    ) where++import SSTG.Core.Preprocessing.Defunctionalization+

@@ -0,0 +1,8 @@+-- | Defunctionalization+module SSTG.Core.Preprocessing.Defunctionalization+    ( defunctionalize+    ) where++defunctionalize :: a+defunctionalize = undefined+

@@ -0,0 +1,7 @@+-- | Export Module for SSTG.Core.SMT+module SSTG.Core.SMT+    ( module SSTG.Core.SMT.Syntax+    ) where++import SSTG.Core.SMT.Syntax+

@@ -0,0 +1,7 @@+-- | SMT2-Lib Syntax+module SSTG.Core.SMT.Syntax+    ( SMTExpr(..)+    ) where++data SMTExpr = SMTEXPR+

@@ -34,8 +34,7 @@ mkIOString :: (Outputable a) => a -> IO String mkIOString obj = runGhc (Just libdir) $ do     dflags <- getSessionDynFlags-    let ppr_str = showPpr dflags obj-    return ppr_str+    return (showPpr dflags obj)  -- | Given the project directory and the source file path, compiles the -- `ModuleGraph` and translates it into a SSTG `Bind`s.@@ -44,16 +43,15 @@     (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-    let m_bndss = map mg_binds gutss-    let m_tcss  = map mg_tcs gutss+    let mod_bindss = map mg_binds gutss+    let mod_tycss = map mg_tcs gutss     -- Zip in preparation for STG transformation.-    let z1      = zip3 mod_lcs m_bndss m_tcss-    preps   <- mapM (\((m, l), b, t) -> corePrepPgm env m l b t) z1-    let z2      = zip (map fst mod_lcs) preps-    s_bndss <- mapM (\(m, p) -> coreToStg dflags m p) z2+    let zipd1 = zip3 mod_lcs mod_bindss mod_tycss+    preps <- mapM (\((m, l), b, t) -> corePrepPgm env m l b t) zipd1+    let zipd2 = zip (map fst mod_lcs) preps+    stg_bindss <- mapM (\(m, p) -> coreToStg dflags m p) zipd2     -- Create the binds.-    let sl_bnds = map mkBind (concat s_bndss)-    return sl_bnds+    return (map mkBind (concat stg_bindss))  -- | Compilation closure type. type CompileClosure = ([(ModSummary, ModGuts)], DynFlags, HscEnv)@@ -66,32 +64,31 @@ mkCompileClosure proj src = runGhc (Just libdir) $ do     beta_flags <- getSessionDynFlags     let dflags = beta_flags { importPaths = [proj] }-    _          <- setSessionDynFlags dflags-    env        <- getSession-    target     <- guessTarget src Nothing-    _          <- setTargets [target]-    _          <- load LoadAllTargets+    _ <- setSessionDynFlags dflags+    env <- getSession+    target <- guessTarget src Nothing+    _ <- setTargets [target]+    _ <- load LoadAllTargets     -- Now that things are loaded, make the compilation closure.-    mod_graph  <- getModuleGraph-    pmods      <- mapM parseModule mod_graph-    tmods      <- mapM typecheckModule pmods-    dmods      <- mapM desugarModule tmods-    let m_gtss = map coreModule dmods-    let zipd   = (zip mod_graph m_gtss, dflags, env)-    return zipd+    mod_graph <- getModuleGraph+    pmods <- mapM parseModule mod_graph+    tmods <- mapM typecheckModule pmods+    dmods <- mapM desugarModule tmods+    let mod_gutss = map coreModule dmods+    return (zip mod_graph mod_gutss, dflags, env)  -- | Make SSTG `Expr`. mkExpr :: StgExpr -> SL.Expr-mkExpr (StgLit lit)         = SL.Atom (SL.LitAtom (mkLit lit))-mkExpr (StgApp occ args)    = SL.FunApp (mkVar occ) (map mkAtom args)-mkExpr (StgConApp dc args)  = SL.ConApp (mkData dc) (map mkAtom args)+mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit))+mkExpr (StgApp occ args) = SL.FunApp (mkVar occ) (map mkAtom args)+mkExpr (StgConApp dcon args) = SL.ConApp (mkData dcon) (map mkAtom args) mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkAtom args)-mkExpr (StgTick _ expr)     = mkExpr expr-mkExpr (StgLam _ _)         = error "mkExpr: StgLam detected"-mkExpr (StgLet bnd expr)    = SL.Let (mkBind bnd) (mkExpr expr)-mkExpr (StgLetNoEscape _ _ bnd expr)     = mkExpr (StgLet bnd expr)-mkExpr (StgCase mexpr _ _ bndr _ _ alts) = SL.Case (mkExpr mexpr) (mkVar bndr)-                                                   (map mkAlt alts)+mkExpr (StgTick _ expr)= mkExpr expr+mkExpr (StgLam _ _) = error "mkExpr: StgLam detected"+mkExpr (StgLet bind expr) = SL.Let (mkBind bind) (mkExpr expr)+mkExpr (StgLetNoEscape _ _ bind expr) = mkExpr (StgLet bind expr)+mkExpr (StgCase mxpr _ _ cvar _ _ alts) = SL.Case (mkExpr mxpr) (mkVar cvar)+                                                  (map mkAlt alts)  -- | Make SSTG `Atom`. mkAtom :: StgArg -> SL.Atom@@ -101,51 +98,52 @@ -- | Make SSTG `Name`. mkName :: Name -> SL.Name mkName name = SL.Name occ mdl ns unq-  where occ = (occNameString . nameOccName) name-        ns  = (mkNameSpace . occNameSpace . nameOccName) name-        unq = (getKey . nameUnique) name-        mdl = case nameModule_maybe name of-                  Nothing -> Nothing-                  Just md -> Just ((moduleNameString . moduleName) md)+  where+    occ = (occNameString . nameOccName) name+    ns = (mkNameSpace . occNameSpace . nameOccName) name+    unq = (getKey . nameUnique) name+    mdl = case nameModule_maybe name of+              Nothing -> Nothing+              Just md -> Just ((moduleNameString . moduleName) md)  -- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace-mkNameSpace ns | isVarNameSpace ns     = SL.VarNSpace-               | isTvNameSpace  ns     = SL.TvNSpace+mkNameSpace ns | isVarNameSpace ns = SL.VarNSpace+               | isTvNameSpace ns = SL.TvNSpace                | isDataConNameSpace ns = SL.DataNSpace-               | isTcClsNameSpace ns   = SL.TcClsNSpace-               | otherwise             = error "mkNameSpace: unrecognized"+               | isTcClsNameSpace ns = SL.TcClsNSpace+               | otherwise = error "mkNameSpace: unrecognized"  -- | Make SSTG Var mkVar :: Var -> SL.Var mkVar var = SL.Var vname vtype-  where vname = (mkName . V.varName) var-        vtype = (mkType . varType) var+  where+    vname = (mkName . V.varName) var+    vtype = (mkType . varType) var  -- | Make SSTG `Bind`. mkBind :: StgBinding -> SL.Bind-mkBind (StgNonRec bnd r) = SL.Bind SL.NonRec [(mkVar bnd, mkRhs r)]-mkBind (StgRec bnd)      = SL.Bind SL.Rec (map (\(b, r) ->-                                                 (mkVar b, mkRhs r)) bnd)+mkBind (StgNonRec bind r) = SL.Bind SL.NonRec [(mkVar bind, mkRhs r)]+mkBind (StgRec bind) = SL.Bind SL.Rec (map (\(b,r) -> (mkVar b, mkRhs r)) bind)  -- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs-mkRhs (StgRhsCon _ dc args)          = SL.ConForm (mkData dc) (map mkAtom args)+mkRhs (StgRhsCon _ dcon args) = SL.ConForm (mkData dcon) (map mkAtom args) mkRhs (StgRhsClosure _ _ _ _ _ ps e) = SL.FunForm (map mkVar ps) (mkExpr e)  -- | Make SSTG `Lit`. mkLit :: Literal -> SL.Lit mkLit lit = case lit of-  (MachChar chr)    -> SL.MachChar chr ((mkType . literalType) lit)-  (MachStr bstr)    -> SL.MachStr (show bstr)   ((mkType . literalType) lit)-  (MachInt i)       -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)-  (MachInt64 i)     -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)-  (MachWord i)      -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)-  (MachWord64 i)    -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)-  (MachFloat rat)   -> SL.MachFloat rat ((mkType . literalType) lit)-  (MachDouble rat)  -> SL.MachDouble rat ((mkType . literalType) lit)-  (LitInteger i _)  -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)-  (MachNullAddr)    -> SL.MachNullAddr ((mkType . literalType) lit)+  (MachChar chr) -> SL.MachChar chr ((mkType . literalType) lit)+  (MachStr bstr) -> SL.MachStr (show bstr) ((mkType . literalType) lit)+  (MachInt i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)+  (MachInt64 i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)+  (MachWord i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)+  (MachWord64 i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)+  (MachFloat rat) -> SL.MachFloat rat ((mkType . literalType) lit)+  (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)  -- | `DataCon`'s `Name`.@@ -155,19 +153,21 @@ -- | Make SSTG `DataCon`. mkData :: DataCon -> SL.DataCon mkData datacon = SL.DataCon name ty args-  where name = mkDataName datacon-        ty   = (mkType . dataConRepType) datacon-        args = map mkType (dataConOrigArgTys datacon)+  where+    name = mkDataName datacon+    ty = (mkType . dataConRepType) datacon+    args = map mkType (dataConOrigArgTys datacon)  -- | Make SSTG `PrimFun`. mkPrimOp :: StgOp -> SL.PrimFun mkPrimOp (StgPrimOp op) = SL.PrimFun (SL.Name occ Nothing ns unq) ty-  where occname = primOpOcc op-        occ     = occNameString occname-        ns      = (mkNameSpace . occNameSpace) occname-        unq     = primOpTag op-        ty      = (mkType . primOpType) op-mkPrimOp _              = error "mkPrimOp: got StgPrimCallOp or StgFCallOp"+  where+    occname = primOpOcc op+    occ = occNameString occname+    ns = (mkNameSpace . occNameSpace) occname+    unq = primOpTag op+    ty = (mkType . primOpType) op+mkPrimOp _ = error "mkPrimOp: got StgPrimCallOp or StgFCallOp"  -- | Make SSTG `Alt`. mkAlt :: StgAlt -> SL.Alt@@ -176,54 +176,55 @@ -- | Make SSTG `AltCon`. mkAltCon :: AltCon -> SL.AltCon mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc)-mkAltCon (LitAlt lit) = SL.LitAlt  (mkLit lit)-mkAltCon (DEFAULT)    = SL.Default+mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit)+mkAltCon (DEFAULT) = SL.Default  -- | Make SSTG `Type`. mkType :: Type -> SL.Type-mkType (AppTy t1 t2)    = SL.AppTy (mkType t1) (mkType t2)+mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v))+mkType (AppTy t1 t2) = SL.AppTy (mkType t1) (mkType t2) mkType (TyConApp tc ts) = SL.TyConApp (mkTyCon tc) (map mkType ts)-mkType (ForAllTy b ty)  = SL.ForAllTy (mkTyBinder b) (mkType ty)-mkType (LitTy tlit)     = SL.LitTy (mkTyLit tlit)-mkType (CastTy ty cor)  = SL.CastTy (mkType ty) (mkCoercion cor)+mkType (ForAllTy b ty) = SL.ForAllTy (mkTyBinder b) (mkType ty)+mkType (LitTy tlit) = SL.LitTy (mkTyLit tlit)+mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor)-mkType (TyVarTy v)      = SL.TyVarTy (mkName (V.varName v))-                                     (mkType (varType v))  -- | Make SSTG `TyCon`. mkTyCon :: TyCon -> SL.TyCon-mkTyCon tc | isFunTyCon         tc = SL.FunTyCon     name tcbndrs-           | isAlgTyCon         tc = SL.AlgTyCon     name tvnames algrhs-           | isFamilyTyCon      tc = SL.FamilyTyCon  name tvnames-           | isPrimTyCon        tc = SL.PrimTyCon    name tcbndrs+mkTyCon tc | isFunTyCon tc = SL.FunTyCon name tcbindrs+           | isAlgTyCon tc = SL.AlgTyCon name tvnames algrhs+           | isFamilyTyCon tc = SL.FamilyTyCon name tvnames+           | isPrimTyCon tc = SL.PrimTyCon name tcbindrs            | isTypeSynonymTyCon tc = SL.SynonymTyCon name tvnames-           | isPromotedDataCon  tc = SL.Promoted     name tcbndrs dcon-           | otherwise             = error "mkTyCon: unrecognized TyCon"-  where name    = (mkName . tyConName) tc-        algrhs  = (mkAlgTyConRhs . algTyConRhs) tc-        tcbndrs = map mkTyBinder (tyConBinders tc)-        tvnames = map (mkName. V.varName) (tyConTyVars tc)-        dcon    = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc+           | isPromotedDataCon tc = SL.Promoted name tcbindrs dcon+           | otherwise = error "mkTyCon: unrecognized TyCon"+  where+    name = (mkName . tyConName) tc+    algrhs = (mkAlgTyConRhs . algTyConRhs) tc+    tcbindrs = map mkTyBinder (tyConBinders tc)+    tvnames = map (mkName. V.varName) (tyConTyVars tc)+    dcon = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc  -- | Make SSTG `AlgTyRhs`. mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs-mkAlgTyConRhs (AbstractTyCon b)            = SL.AbstractTyCon b-mkAlgTyConRhs (DataTyCon {data_cons = ds}) = SL.DataTyCon  (map mkDataName ds)-mkAlgTyConRhs (TupleTyCon {data_con = d})  = SL.TupleTyCon (mkDataName d)-mkAlgTyConRhs (NewTyCon {data_con = d})    = SL.NewTyCon   (mkDataName d)+mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b+mkAlgTyConRhs (DataTyCon {data_cons = ds}) = SL.DataTyCon (map mkDataName ds)+mkAlgTyConRhs (TupleTyCon {data_con = d}) = SL.TupleTyCon (mkDataName d)+mkAlgTyConRhs (NewTyCon {data_con = d}) = SL.NewTyCon (mkDataName d)  -- | make SSTG `TyBinder`. mkTyBinder :: TyBinder -> SL.TyBinder-mkTyBinder (Anon _)    = SL.AnonTyBndr+mkTyBinder (Anon _) = SL.AnonTyBndr mkTyBinder (Named v _) = SL.NamedTyBndr (mkName (V.varName v))  -- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit-mkTyLit (NumTyLit i)  = SL.NumTyLit (fromInteger i)+mkTyLit (NumTyLit i) = SL.NumTyLit (fromInteger i) mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs)  -- | Make SSTG `Coercion`. mkCoercion :: Coercion -> SL.Coercion mkCoercion coer = SL.Coercion (mkType a) (mkType b)-  where (a, b) = (unPair . coercionKind) coer+  where+    (a, b) = (unPair . coercionKind) coer 

@@ -5,8 +5,7 @@     , writePrettyState     ) where -import SSTG.Core.Execution.Stepping-import SSTG.Core.Execution.Support+import SSTG.Core import SSTG.Utils.Printing  import Text.Read

@@ -12,26 +12,29 @@ -- | Print `LiveState` and `DeadState` that yield from execution snapshots. pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String pprLivesDeadsStr (lives, deads) = injNewLineSeps10 acc_strs-  where header   = "(Lives, Deads)"-        lv_str   = (injNewLineSeps5 . map pprLiveStr) lives-        dd_str   = (injNewLineSeps5 . map pprDeadStr) deads-        acc_strs = [header, lv_str, dd_str]+  where+    header = "(Lives, Deads)"+    lv_str = (injNewLineSeps5 . map pprLiveStr) lives+    dd_str = (injNewLineSeps5 . map pprDeadStr) deads+    acc_strs = [header, lv_str, dd_str]  -- | Print `LiveState`. pprLiveStr :: LiveState -> String pprLiveStr (rules, state) = injNewLine acc_strs-  where header   = "Live"-        rule_str = pprRulesStr rules-        st_str   = pprStateStr state-        acc_strs = [header, rule_str, st_str]+  where+    header = "Live"+    rule_str = pprRulesStr rules+    st_str = pprStateStr state+    acc_strs = [header, rule_str, st_str]  -- | Print `DeadState`. pprDeadStr :: LiveState -> String pprDeadStr (rules, state) = injNewLine acc_strs-  where header   = "Dead"-        rule_str = pprRulesStr rules-        st_str   = pprStateStr state-        acc_strs = [header, rule_str, st_str]+  where+    header = "Dead"+    rule_str = pprRulesStr rules+    st_str = pprStateStr state+    acc_strs = [header, rule_str, st_str]  -- | Print `Rule`. pprRuleStr :: Rule -> String@@ -42,29 +45,30 @@  -- | Print `State`. pprStateStr :: State -> String-pprStateStr state   = injNewLine acc_strs-  where 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-        acc_strs    = [ ">>>>> [State] >>>>>>>>>>>>>>>"-                      , status_str-                      , "----- [Stack] ---------------"-                      , stack_str-                      , "----- [Heap] ----------------"-                      , heap_str-                      , "----- [Globals] -------------"-                      , globals_str-                      , "----- [Expression] ----------"-                      , expr_str-                      , "----- [All Names] -------"-                      , fst ("", names_str)  -- names_str-                      , "----- [Path Constraint] -----"-                      , pcons_str-                      , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ]+pprStateStr state = injNewLine acc_strs+  where+    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+    acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>"+               , status_str+               , "----- [Stack] ---------------"+               , stack_str+               , "----- [Heap] ----------------"+               , heap_str+               , "----- [Globals] -------------"+               , globals_str+               , "----- [Expression] ----------"+               , expr_str+               , "----- [All Names] -------"+               , fst ("", names_str)  -- names_str+               , "----- [Path Constraint] -----"+               , pcons_str+               , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ]  -- | Inject `String` into parantheses. sub :: String -> String@@ -89,12 +93,14 @@ -- | Inject a list of `String`s with newline separators of dashes length 5. injNewLineSeps5 :: [String] -> String injNewLineSeps5 strs = L.intercalate seps strs-  where seps = "\n-----\n"+  where+    seps = "\n-----\n"  -- | Inject a list of `String`s wit hnewline separators of dashes length 10. injNewLineSeps10 :: [String] -> String injNewLineSeps10 strs = L.intercalate seps strs-  where seps = "\n----------\n"+  where+    seps = "\n----------\n"  -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String@@ -115,155 +121,177 @@ -- | Print `Stack`. pprStackStr :: Stack -> String pprStackStr stack = injNewLineSeps10 acc_strs-  where frame_strs = map pprFrameStr (stackToList stack)-        acc_strs   = "Stack" : frame_strs+  where+    frame_strs = map pprFrameStr (stackToList stack)+    acc_strs = "Stack" : frame_strs  -- | Print `Frame`. pprFrameStr :: Frame -> String pprFrameStr (CaseFrame var alts locals) = injNewLine acc_strs-  where header   = "CaseFrame"-        var_str  = pprVarStr var-        alts_str = pprAltsStr alts-        locs_str = pprLocalsStr locals-        acc_strs = [header, var_str, alts_str, locs_str]+  where+    header = "CaseFrame"+    var_str = pprVarStr var+    alts_str = pprAltsStr alts+    locs_str = pprLocalsStr locals+    acc_strs = [header, var_str, alts_str, locs_str] pprFrameStr (ApplyFrame args locals) = injNewLine acc_strs-  where header   = "ApplyFrame"-        args_str = injIntoList (map pprAtomStr args)-        locs_str = pprLocalsStr locals-        acc_strs = [header, args_str, locs_str]+  where+    header = "ApplyFrame"+    args_str = injIntoList (map pprAtomStr args)+    locs_str = pprLocalsStr locals+    acc_strs = [header, args_str, locs_str] pprFrameStr (UpdateFrame addr) = injNewLine acc_strs-  where header   = "UpdateFrame"-        addr_str = pprMemAddrStr addr-        acc_strs = [header, addr_str]+  where+    header = "UpdateFrame"+    addr_str = pprMemAddrStr addr+    acc_strs = [header, addr_str]  -- | Print the @Maybe (Expr, Locals)@. pprSymClosureStr :: Maybe (Expr, Locals) -> String-pprSymClosureStr (Nothing)             = "SymClosure ()"+pprSymClosureStr (Nothing) = "SymClosure ()" pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs-  where header   = "SymClosure"-        expr_str = pprExprStr expr-        locs_str = pprLocalsStr locals-        acc_strs = [header, injIntoList [expr_str, locs_str]]+  where+    header = "SymClosure"+    expr_str = pprExprStr expr+    locs_str = pprLocalsStr locals+    acc_strs = [header, injIntoList [expr_str, locs_str]]  -- | Print `HeapObj`. pprHeapObjStr :: HeapObj -> String pprHeapObjStr (Blackhole) = "Blackhole!!!" pprHeapObjStr (AddrObj addr) = pprMemAddrStr addr pprHeapObjStr (LitObj lit) = injSpace acc_strs-  where header   = "LitObj"-        lit_str  = pprLitStr lit-        acc_strs = [header, lit_str]+  where+    header = "LitObj"+    lit_str = pprLitStr lit+    acc_strs = [header, lit_str] pprHeapObjStr (SymObj (Symbol sym mb_scls)) = injSpace acc_strs-  where header   = "SymObj"-        var_str  = pprVarStr sym-        scls_str = (sub . pprSymClosureStr) mb_scls-        acc_strs = [header, var_str, scls_str]+  where+    header = "SymObj"+    var_str = pprVarStr sym+    scls_str = (sub . pprSymClosureStr) mb_scls+    acc_strs = [header, var_str, scls_str] pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs-  where header   = "ConObj"-        dcon_str = pprDataConStr dcon-        vals_str = injIntoList (map pprValueStr vals)-        acc_strs = [header, dcon_str, vals_str]+  where+    header = "ConObj"+    dcon_str = pprDataConStr dcon+    vals_str = injIntoList (map pprValueStr vals)+    acc_strs = [header, dcon_str, vals_str] pprHeapObjStr (FunObj params expr locals) = injSpace acc_strs-  where header   = "FunObj"-        prms_str = injIntoList (map pprVarStr params)-        expr_str = pprExprStr expr-        locs_str = pprLocalsStr locals-        acc_strs = [header, prms_str, expr_str, locs_str]+  where+    header = "FunObj"+    prms_str = injIntoList (map pprVarStr params)+    expr_str = pprExprStr expr+    locs_str = pprLocalsStr locals+    acc_strs = [header, prms_str, expr_str, locs_str]  -- | Print `Heap`. pprHeapStr :: Heap -> String pprHeapStr heap = injNewLine acc_strs-  where hlist     = heapToList heap-        addr_strs = map (pprMemAddrStr . fst) hlist-        hobj_strs = map (pprHeapObjStr . snd) hlist-        zipd_strs = zip addr_strs hobj_strs-        acc_strs  = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs+  where+    hlist = heapToList heap+    addr_strs = map (pprMemAddrStr . fst) hlist+    hobj_strs = map (pprHeapObjStr . snd) hlist+    zipd_strs = zip addr_strs hobj_strs+    acc_strs = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs  -- | Print `Globals`. pprGlobalsStr :: Globals -> String pprGlobalsStr globals = injNewLine acc_strs-  where glist     = globalsToList globals-        name_strs = map (pprNameStr . fst) glist-        val_strs  = map (pprValueStr . snd) glist-        zipd_strs = zip name_strs val_strs-        acc_strs  = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs+  where+    glist = globalsToList globals+    name_strs = map (pprNameStr . fst) glist+    val_strs = map (pprValueStr . snd) glist+    zipd_strs = zip name_strs val_strs+    acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs  -- | Print `Locals`. pprLocalsStr :: Locals -> String pprLocalsStr locals = injIntoList acc_strs-  where llist     = localsToList locals-        name_strs = map (pprNameStr . fst) llist-        val_strs  = map (pprValueStr . snd) llist-        zipd_strs = zip name_strs val_strs-        acc_strs  = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs+  where+    llist = localsToList locals+    name_strs = map (pprNameStr . fst) llist+    val_strs = map (pprValueStr . 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-  where header   = "LitVal"-        lit_str  = pprLitStr lit-        acc_strs = [header, lit_str]+  where+    header = "LitVal"+    lit_str = pprLitStr lit+    acc_strs = [header, lit_str] pprValueStr (MemVal addr) = injSpace acc_strs-  where header   = "MemVal"-        ptr_str  = pprMemAddrStr addr-        acc_strs = [header, ptr_str]+  where+    header = "MemVal"+    ptr_str = pprMemAddrStr addr+    acc_strs = [header, ptr_str]  -- | Print `Var`. pprVarStr :: Var -> String pprVarStr (Var name ty) = injSpace acc_strs-  where header   = "Var"-        name_str = (sub . pprNameStr) name-        type_str = (sub . pprTypeStr) ty-        acc_strs = [header, name_str, type_str]+  where+    header = "Var"+    name_str = (sub . pprNameStr) name+    type_str = (sub . pprTypeStr) ty+    acc_strs = [header, name_str, type_str]  -- | Print `Atom`. pprAtomStr :: Atom -> String pprAtomStr (VarAtom var) = injSpace acc_strs-  where header   = "VarAtom"-        var_str  = (sub . pprVarStr) var-        acc_strs = [header, var_str]+  where+    header = "VarAtom"+    var_str = (sub . pprVarStr) var+    acc_strs = [header, var_str] pprAtomStr (LitAtom lit) = injSpace acc_strs-  where header   = "LitAtom"-        lit_str  = (sub . pprLitStr) lit-        acc_strs = [header, lit_str]+  where+    header = "LitAtom"+    lit_str = (sub . pprLitStr) lit+    acc_strs = [header, lit_str]  -- | Print `DataCon`. pprDataConStr :: DataCon -> String pprDataConStr (DataCon name ty tys) = injSpace acc_strs-  where header   = "DataCon"-        tag_str  = (sub . pprNameStr) name-        ty_str   = (sub . pprTypeStr) ty-        tys_str  = injIntoList (map pprTypeStr tys)-        acc_strs = [header, tag_str, ty_str, tys_str]+  where+    header = "DataCon"+    tag_str = (sub . pprNameStr) name+    ty_str = (sub . pprTypeStr) ty+    tys_str = injIntoList (map pprTypeStr tys)+    acc_strs = [header, tag_str, ty_str, tys_str]  -- | Print `PrimFun`. pprPrimFunStr :: PrimFun -> String pprPrimFunStr (PrimFun name ty) = injSpace acc_strs-  where header   = "PrimFun"-        name_str = (sub . pprNameStr) name-        type_str = (sub . pprTypeStr) ty-        acc_strs = [header, name_str, type_str]+  where+    header = "PrimFun"+    name_str = (sub . pprNameStr) name+    type_str = (sub . pprTypeStr) ty+    acc_strs = [header, name_str, type_str]  -- | Print `AltCon`. pprAltConStr :: AltCon -> String pprAltConStr (DataAlt dcon) = injSpace acc_strs-  where header   = "DataAlt"-        dcon_str = (sub . pprDataConStr) dcon-        acc_strs = [header, dcon_str]+  where+    header = "DataAlt"+    dcon_str = (sub . pprDataConStr) dcon+    acc_strs = [header, dcon_str] pprAltConStr (LitAlt lit) = injSpace acc_strs-  where header   = "LitAlt"-        lit_str  = (sub . pprLitStr) lit-        acc_strs = [header, lit_str]+  where+    header = "LitAlt"+    lit_str = (sub . pprLitStr) lit+    acc_strs = [header, lit_str] pprAltConStr (Default) = "Default"  -- | Print `Alt`. pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs-  where header   = "Alt"-        acon_str = (sub . pprAltConStr) acon-        vars_str = injIntoList (map pprVarStr var)-        expr_str = (sub . pprExprStr) expr-        acc_strs = [header, acon_str, vars_str, expr_str]+  where+    header = "Alt"+    acon_str = (sub . pprAltConStr) acon+    vars_str = injIntoList (map pprVarStr var)+    expr_str = (sub . pprExprStr) expr+    acc_strs = [header, acon_str, vars_str, expr_str]  -- | Print a list of `Alt`s. pprAltsStr :: [Alt] -> String@@ -272,79 +300,91 @@ -- | Print `BindRhs`. pprBindRhsStr :: BindRhs -> String pprBindRhsStr (FunForm params expr) = injSpace acc_strs-  where header   = "FunForm"-        prms_str = injIntoList (map pprVarStr params)-        expr_str = (sub . pprExprStr) expr-        acc_strs = [header, prms_str, expr_str]+  where+    header = "FunForm"+    prms_str = injIntoList (map pprVarStr params)+    expr_str = (sub . pprExprStr) expr+    acc_strs = [header, prms_str, expr_str] pprBindRhsStr (ConForm dcon args) = injSpace acc_strs-  where header   = "ConForm"-        dcon_str = (sub . pprDataConStr) dcon-        args_str = injIntoList (map pprAtomStr args)-        acc_strs = [header, dcon_str, args_str]+  where+    header = "ConForm"+    dcon_str = (sub . pprDataConStr) dcon+    args_str = injIntoList (map pprAtomStr args)+    acc_strs = [header, dcon_str, args_str]  -- | Print @(Var, BindRhs)@. pprBindKVStr :: (Var, BindRhs) -> String pprBindKVStr (var, lamf) = (sub . injComma) acc_strs-  where var_str  = pprVarStr var-        lamf_str = pprBindRhsStr lamf-        acc_strs = [var_str, lamf_str]+  where+    var_str = pprVarStr var+    lamf_str = pprBindRhsStr lamf+    acc_strs = [var_str, lamf_str]  -- | Print `Bind`. pprBindStr :: Bind -> String pprBindStr (Bind rec bnd) = injSpace acc_strs-  where header   = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }-        bnds_str = injIntoList (map pprBindKVStr bnd)-        acc_strs = [header, bnds_str]+  where+    header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }+    bnds_str = injIntoList (map pprBindKVStr bnd)+    acc_strs = [header, bnds_str]  -- | Print `Expr`. pprExprStr :: Expr -> String pprExprStr (Atom atom) = injSpace acc_strs-  where header   = "Atom"-        atom_str = (sub . pprAtomStr) atom-        acc_strs = [header, atom_str]+  where+    header = "Atom"+    atom_str = (sub . pprAtomStr) atom+    acc_strs = [header, atom_str] pprExprStr (FunApp var args) = injSpace acc_strs-  where header   = "FunApp"-        var_str  = (sub . pprVarStr) var-        args_str = injIntoList (map pprAtomStr args)-        acc_strs = [header, var_str, args_str]+  where+    header = "FunApp"+    var_str = (sub . pprVarStr) var+    args_str = injIntoList (map pprAtomStr args)+    acc_strs = [header, var_str, args_str] pprExprStr (PrimApp pfun args) = injSpace acc_strs-  where header   = "PrimApp"-        pfun_str = (sub . pprPrimFunStr) pfun-        args_str = injIntoList (map pprAtomStr args)-        acc_strs = [header, pfun_str, args_str]+  where+    header = "PrimApp"+    pfun_str = (sub . pprPrimFunStr) pfun+    args_str = injIntoList (map pprAtomStr args)+    acc_strs = [header, pfun_str, args_str] pprExprStr (ConApp dcon args) = injSpace acc_strs-  where header   = "ConApp"-        dcon_str = (sub . pprDataConStr) dcon-        args_str = injIntoList (map pprAtomStr args)-        acc_strs = [header, dcon_str, args_str]+  where+    header = "ConApp"+    dcon_str = (sub . pprDataConStr) dcon+    args_str = injIntoList (map pprAtomStr args)+    acc_strs = [header, dcon_str, args_str] pprExprStr (Case expr var alts) = injSpace acc_strs-  where header   = "Case"-        expr_str = (sub . pprExprStr) expr-        var_str  = (sub . pprVarStr) var-        alts_str = pprAltsStr alts-        acc_strs = [header, expr_str, var_str, alts_str]+  where+    header = "Case"+    expr_str = (sub . pprExprStr) expr+    var_str = (sub . pprVarStr) var+    alts_str = pprAltsStr alts+    acc_strs = [header, expr_str, var_str, alts_str] pprExprStr (Let bnd expr) = injSpace acc_strs-  where header   = "Let"-        bnd_str  = (sub . pprBindStr) bnd-        expr_str = (sub . pprExprStr) expr-        acc_strs = [header, bnd_str, expr_str]+  where+    header = "Let"+    bnd_str = (sub . pprBindStr) bnd+    expr_str = (sub . pprExprStr) expr+    acc_strs = [header, bnd_str, expr_str]  -- | Print `Type`. NOTE: currently only prints @"__TyPE__"@ because there is -- a lot of `Type` information which makes analysis of dumps hard otherwise. pprTypeStr :: Type -> String-pprTypeStr ty = fst ("__Type__", ty)+pprTypeStr ty = snd ("__Type__", show ty)  -- | Print `Code`. pprCodeStr :: Code -> String pprCodeStr (Evaluate expr locals) = injSpace acc_strs-  where header   = "Evaluate"-        expr_str = (sub . pprExprStr) expr-        loc_str  = (sub . pprLocalsStr) locals-        acc_strs = [header, expr_str, loc_str]+  where+    header = "Evaluate"+    expr_str = (sub . pprExprStr) expr+    loc_str = (sub . pprLocalsStr) locals+    acc_strs = [header, expr_str, loc_str] pprCodeStr (Return val) = injSpace acc_strs-  where header   = "Return"-        val_str  = pprValueStr val-        acc_strs = [header, val_str]+  where+    header = "Return"+    val_str = pprValueStr val+    acc_strs = [header, val_str]  -- | Print a list of `Name`s. pprNamesStr :: [Name] -> String@@ -353,15 +393,17 @@ -- | Print `PathCons`. pprPathConsStr :: PathCons -> String pprPathConsStr pathcons = injNewLineSeps5 strs-  where strs = map pprConstraintStr (pathconsToList pathcons)+  where+    strs = map pprConstraintStr (pathconsToList pathcons)  -- | Print `PathCond`. pprConstraintStr :: Constraint -> String pprConstraintStr (Constraint (ac, ps) expr locals hold) = injIntoList acc_strs-  where acon_str = pprAltConStr ac-        prms_str = injIntoList (map pprVarStr ps)-        expr_str = pprExprStr expr-        locs_str = pprLocalsStr locals-        hold_str = case hold of { True -> "Positive"; False -> "Negative" }-        acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]+  where+    acon_str = pprAltConStr ac+    prms_str = injIntoList (map pprVarStr ps)+    expr_str = pprExprStr expr+    locs_str = pprLocalsStr locals+    hold_str = case hold of { True -> "Positive"; False -> "Negative" }+    acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]