SSTG 0.1.1.4 → 0.1.1.5

raw patch · 11 files changed

+206/−206 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +1/−1
• app/Main.hs +1/−1
• src/SSTG/Core/Execution/Engine.hs +31/−31
• src/SSTG/Core/Execution/Rules.hs +70/−70
• src/SSTG/Core/Execution/Stepping.hs +3/−3
• src/SSTG/Core/Execution/Support.hs +57/−57
• src/SSTG/Core/Language/Naming.hs +22/−22
• src/SSTG/Core/Language/Syntax.hs +2/−2
• src/SSTG/Core/Language/Typing.hs +1/−1
• src/SSTG/Core/Translation/Haskell.hs +7/−7
• src/SSTG/Utils/Printing.hs +11/−11

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.1.4+version:             0.1.1.5 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme

@@ -58,7 +58,7 @@     -- Get command line arguments.     (proj:src:tail_args) <- getArgs     -- Make bindings.-    bindss <- mkTargetBindsList proj src+    bindss <- mkTargetBindss proj src     -- Configure entry.     let entry = if length tail_args > 0 then tail_args !! 0 else "main"     -- Get the flags.

@@ -42,8 +42,8 @@     -- Globals and Heap are loaded together. They are still beta forms now.     heap0 = empty_heap     (glist, heap1, binds_addrss) = initGlobals bindss heap0-    globals0 = insertGlobalsList glist empty_globals-    (heap2, localss) = liftBindsList binds_addrss globals0 heap1+    globals0 = insertGlobalsVals glist empty_globals+    (heap2, localss) = liftBindsAddrss binds_addrss globals0 heap1     binds_locs = zip bindss localss     -- Code loading. Completes heap and globals with symbolic injection.     matches = entryMatches entry binds_locs@@ -57,7 +57,7 @@                    , state_globals = globals                    , state_code = code                    , state_names = []-                   , state_paths = empty_pathcons }+                   , state_path = empty_pathcons }      -- Gather information on all variables.     state = state0 { state_names = allNames (Program bindss) }@@ -67,35 +67,35 @@ allocBinds (Binds _ kvs) heap = (heap', addrs)   where     hfakes = map (const Blackhole) kvs-    (heap', addrs) = allocHeapList hfakes heap+    (heap', addrs) = allocHeapObjs hfakes heap  -- | Allocate List of `Binds`s-allocBindsList :: [Binds] -> Heap -> (Heap, [[MemAddr]])-allocBindsList [] heap = (heap, [])-allocBindsList (b:bs) heap = (heapf, addrs : as)+allocBindss :: [Binds] -> Heap -> (Heap, [[MemAddr]])+allocBindss [] heap = (heap, [])+allocBindss (bind:bs) heap = (heapf, addrs : as)   where-    (heap', addrs) = allocBinds b heap-    (heapf, as) = allocBindsList bs heap'+    (heap', addrs) = allocBinds bind heap+    (heapf, as) = allocBindss bs heap' --- | Binds Address to Name Values-bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Value)]+-- | Binds Address to Name Vals+bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Val)] bindsAddrsToVarVals (Binds _ kvs, addrs) = zip (map fst kvs) mem_vals   where     mem_vals = map (\a -> MemVal a) addrs  -- | Initialize Globals-initGlobals :: [Binds] -> Heap -> ([(Var, Value)], Heap, [(Binds, [MemAddr])])+initGlobals :: [Binds] -> Heap -> ([(Var, Val)], Heap, [(Binds, [MemAddr])]) initGlobals bindss heap = (var_vals, heap', binds_addrss)   where-    (heap', addrss) = allocBindsList bindss heap+    (heap', addrss) = allocBindss bindss heap     binds_addrss = zip bindss addrss     var_vals = concatMap bindsAddrsToVarVals binds_addrss  -- | Force Atom Lookup-forceLookupValue :: Atom -> Locals -> Globals -> Value-forceLookupValue (LitAtom lit) _ _ = LitVal lit-forceLookupValue (VarAtom var) locals globals =-    case lookupValue var locals globals of+forceLookupVal :: Atom -> Locals -> Globals -> Val+forceLookupVal (LitAtom lit) _ _ = LitVal lit+forceLookupVal (VarAtom var) locals globals =+    case lookupVal var locals globals of         Just val -> val         Nothing -> LitVal BlankAddr  -- An error, but I want to not crash. @@ -104,27 +104,27 @@ forceRhsObj (FunForm prms expr) locals _ = FunObj prms expr locals forceRhsObj (ConForm dcon args) locals globals = ConObj dcon arg_vals   where-    arg_vals = map (\a -> forceLookupValue a locals globals) args+    arg_vals = map (\a -> forceLookupVal a locals globals) args  -- | Lift `Binds`.-liftBinds :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)-liftBinds (Binds rec kvs, addrs) globals heap = (heap', locals)+liftBindsAddrs :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)+liftBindsAddrs (Binds rec kvs, addrs) globals heap = (heap', locals)   where     (vars, rhss) = unzip kvs     mem_vals = map (\a -> MemVal a) addrs     e_locs = empty_locals-    r_locs = insertLocalsList (zip vars mem_vals) e_locs+    r_locs = insertLocalsVals (zip vars mem_vals) e_locs     locals = case rec of { Rec -> r_locs; NonRec -> e_locs }     hobjs = map (\r -> forceRhsObj r locals globals) rhss-    heap' = insertHeapObjList (zip addrs hobjs) heap+    heap' = insertHeapObjs (zip addrs hobjs) heap  -- | Lift Binds List-liftBindsList :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])-liftBindsList [] _ heap = (heap, [])-liftBindsList (bm:bms) globals heap = (heapf, locals : ls)+liftBindsAddrss :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])+liftBindsAddrss [] _ heap = (heap, [])+liftBindsAddrss (bind_addr:bms) globals heap = (heapf, locals : ls)   where-    (heap', locals) = liftBinds bm globals heap-    (heapf, ls) = liftBindsList bms globals heap'+    (heap', locals) = liftBindsAddrs bind_addr globals heap+    (heapf, ls) = liftBindsAddrss bms globals heap'  -- | Return a sub-list of binds in which the entry candidate appears. entryMatches :: String -> [(Binds, Locals)] -> [(Binds, Locals)]@@ -144,18 +144,18 @@ loadCode ent (ConForm _ _) locals globals heap = (code, globals, heap)   where     code = Evaluate (Atom (VarAtom ent)) locals-loadCode ent (FunForm params expr) locals globals heap = (code, globals, heap')+loadCode ent (FunForm params expr) locals globals heap = (code,globals,heap')   where     actuals = traceArgs params expr locals globals heap     confs = map varName actuals-    names' = freshSeededNameList confs confs+    names' = freshSeededNames confs confs     adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals))     -- Throw the parameters on heap as symbolic objects     sym_objs = map (\p -> SymObj (Symbol p Nothing)) adjusted-    (heap', addrs) = allocHeapList sym_objs heap+    (heap', addrs) = allocHeapObjs sym_objs heap     -- make Atom representations for arguments and shove into locals.     mem_vals = map (\a -> MemVal a) addrs-    locals' = insertLocalsList (zip adjusted mem_vals) locals+    locals' = insertLocalsVals (zip adjusted mem_vals) locals     args = map (\p -> VarAtom p) adjusted     -- Set up code     code = Evaluate (FunApp ent args) locals'

@@ -2,7 +2,7 @@ module SSTG.Core.Execution.Rules     ( Rule(..)     , reduce-    , isStateValueForm+    , isStateValForm     ) where  import SSTG.Core.Language@@ -35,40 +35,40 @@  -- | Does not include `LitObj`. i.e. if something points to this, we have -- nothing to do in terms of reducitons.-isHeapValueForm :: HeapObj -> Bool-isHeapValueForm (SymObj _) = True-isHeapValueForm (ConObj _ _) = True-isHeapValueForm (FunObj (_:_) _ _) = True-isHeapValueForm _ = False+isHeapValForm :: HeapObj -> Bool+isHeapValForm (SymObj _) = True+isHeapValForm (ConObj _ _) = True+isHeapValForm (FunObj (_:_) _ _) = True+isHeapValForm _ = False  -- | Either a `Lit` or points to a `Heap` value (not LitObj!). If we find -- nothing in the `Heap`, then this means we can still upcast the var to a -- symbolic that we create additional mappings to in the `Globals`.-isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool-isExprValueForm (Atom (LitAtom _)) _ _ _ = True-isExprValueForm (Atom (VarAtom var)) locals globals heap =+isExprValForm :: Expr -> Locals -> Globals -> Heap -> Bool+isExprValForm (Atom (LitAtom _)) _ _ _ = True+isExprValForm (Atom (VarAtom var)) locals globals heap =     case vlookupHeap var locals globals heap of-        Just (_, hobj) -> isHeapValueForm hobj+        Just (_, hobj) -> isHeapValForm hobj         Nothing -> False-isExprValueForm _ _ _ _ = False+isExprValForm _ _ _ _ = False  -- | Is the `State` in a normal form that cannot be reduced further?-isStateValueForm :: State -> Bool-isStateValueForm state+isStateValForm :: State -> Bool+isStateValForm state   | Nothing <- popStack (state_stack state)   , Return (LitVal _) <- (state_code state) = True    | Nothing <- popStack (state_stack state)   , Return (MemVal addr) <- (state_code state)   , Just hobj <- lookupHeap addr (state_heap state)-  , isHeapValueForm hobj = True+  , isHeapValForm hobj = True    | otherwise = False --- | `Value` to `Lit`.-valueToLit :: Value -> Lit-valueToLit (LitVal lit) = lit-valueToLit (MemVal addr) = AddrLit (memAddrInt addr)+-- | `Val` to `Lit`.+valToLit :: Val -> Lit+valToLit (LitVal lit) = lit+valToLit (MemVal addr) = AddrLit (memAddrInt addr)  -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])@@ -87,36 +87,36 @@   where     sname = freshSeededName (varName var) confs     svar = Var sname (varType var)-    (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap-    globals' = insertGlobals (var, MemVal addr) globals+    (heap', addr) = allocHeapObj (SymObj (Symbol svar Nothing)) heap+    globals' = insertGlobalsVal (var, MemVal addr) globals     confs' = sname : confs     pass_out = LiftAct addr locals globals' heap' confs'  -- | Lift `Atom` if necessary (i.e. uinterpreted / out-of-scope).-liftAtom :: LiftAct Atom -> LiftAct Value+liftAtom :: LiftAct Atom -> LiftAct Val liftAtom (LiftAct atom locals globals heap confs) = pass_out   where     pass_out = LiftAct aval locals globals' heap' confs'     (aval, globals', heap', confs') = case atom of         LitAtom lit -> (LitVal lit, globals, heap, confs)-        VarAtom var -> case lookupValue var locals globals of+        VarAtom var -> case lookupVal var locals globals of             Just val -> (val, globals, heap, confs)             Nothing -> let pass_in = LiftAct var locals globals heap confs                            LiftAct addr _ g' h' c' = liftUnInt pass_in                        in (MemVal addr, g', h', c')  -- | Lift a list of `Atom`s.-liftAtomList :: LiftAct [Atom] -> LiftAct [Value]-liftAtomList (LiftAct [] locals globals heap confs) = pass_out+liftAtoms :: LiftAct [Atom] -> LiftAct [Val]+liftAtoms (LiftAct [] locals globals heap confs) = pass_out   where     pass_out = LiftAct [] locals globals heap confs-liftAtomList (LiftAct (atom:as) locals globals heap confs) = pass_out+liftAtoms (LiftAct (atom:as) locals globals heap confs) = pass_out   where     pass_in = LiftAct atom locals globals heap confs     pass_rest = LiftAct as locals' globals' heap' confs'     pass_out = LiftAct (val : vs) localsf globalsf heapf confsf     LiftAct val locals' globals' heap' confs' = liftAtom pass_in-    LiftAct vs localsf globalsf heapf confsf = liftAtomList pass_rest+    LiftAct vs localsf globalsf heapf confsf = liftAtoms pass_rest  -- | Lift `BindRhs`. liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj@@ -127,43 +127,43 @@   where     pass_in = LiftAct args locals globals heap confs     pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs'-    LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+    LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in  -- | Lift `BindRhs` list.-liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj]-liftBindRhsList (LiftAct [] locals globals heap confs) = pass_out+liftBindRhss :: LiftAct [BindRhs] -> LiftAct [HeapObj]+liftBindRhss (LiftAct [] locals globals heap confs) = pass_out   where     pass_out = LiftAct [] locals globals heap confs-liftBindRhsList (LiftAct (rhs:rs) locals globals heap confs) = pass_out+liftBindRhss (LiftAct (rhs:rs) locals globals heap confs) = pass_out   where     pass_in = LiftAct rhs locals globals heap confs     pass_rest = LiftAct rs locals' globals' heap' confs'     pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf     LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in-    LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest+    LiftAct hos localsf globalsf heapf confsf = liftBindRhss pass_rest  -- | Lift `Binds`. liftBinds :: LiftAct Binds -> LiftAct () liftBinds (LiftAct (Binds NonRec kvs) locals globals heap confs) = pass_out   where-    (heapf, addrs) = allocHeapList hobjs heap'+    (heapf, addrs) = allocHeapObjs hobjs heap'     mem_vals = map MemVal addrs-    localsf = insertLocalsList (zip (map fst kvs) mem_vals) locals'+    localsf = insertLocalsVals (zip (map fst kvs) mem_vals) locals'     pass_in = LiftAct (map snd kvs) locals globals heap confs     pass_out = LiftAct () localsf globals' heapf confs'-    LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in+    LiftAct hobjs locals' globals' heap' confs' = liftBindRhss pass_in liftBinds (LiftAct (Binds Rec kvs) locals globals heap confs) = pass_out   where     hfakes = map (const Blackhole) kvs     -- Allocate dummy BLACKHOLEs-    (heap', addrs) = allocHeapList hfakes heap+    (heap', addrs) = allocHeapObjs hfakes heap     mem_vals = map MemVal addrs     -- Use the reigstered loca BLACKHOLEs to construct the locals closure.-    locals' = insertLocalsList (zip (map fst kvs) mem_vals) locals-    heapf = insertHeapObjList (zip addrs hobjs) heap''+    locals' = insertLocalsVals (zip (map fst kvs) mem_vals) locals+    heapf = insertHeapObjs (zip addrs hobjs) heap''     pass_in = LiftAct (map snd kvs) locals' globals heap' confs     pass_out = LiftAct () localsf globals' heapf confs'-    LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in+    LiftAct hobjs localsf globals' heap'' confs' = liftBindRhss pass_in  -- | `Default` `Alt` branches in a `Case`. defaultAlts :: [Alt] -> [Alt]@@ -190,13 +190,13 @@ liftSymAlt (LiftAct args locals globals heap confs) = pass_out   where     (mvar, addr, cvar, Alt ac params expr) = args-    snames = freshSeededNameList (map varName params) confs+    snames = freshSeededNames (map varName params) confs     svars = map (\(p, n) -> Var n (varType p)) (zip params snames)     hobjs = map (\s -> SymObj (Symbol s Nothing)) svars-    (heap', addrs) = allocHeapList hobjs heap+    (heap', addrs) = allocHeapObjs hobjs heap     mem_vals = map MemVal addrs     kvs = (cvar, MemVal addr) : zip params mem_vals-    locals' = insertLocalsList kvs locals+    locals' = insertLocalsVals kvs locals     mexpr = Atom (VarAtom mvar)     conss = [Constraint (ac, params) mexpr locals' True]     confs' = snames ++ confs@@ -207,12 +207,12 @@ liftedAltToState state (LiftAct args locals globals heap confs) = state'   where     (expr, conss) = args-    pcons = state_paths state+    pcons = state_path state     state' = state { state_heap = heap                    , state_globals = globals                    , state_code = Evaluate expr locals                    , state_names = confs-                   , state_paths = insertPathConsList conss pcons }+                   , state_path = insertPathConss conss pcons }  -- | Reduce the state if it matches some type of reduction `Rule`. Return -- `Nothing` to denote that rule application has completely failed.@@ -240,7 +240,7 @@   -- Rule Atom Val Pointer   | Evaluate (Atom (VarAtom var)) locals <- code   , Just (addr, hobj) <- vlookupHeap var locals globals heap-  , isHeapValueForm hobj =+  , isHeapValForm hobj =     Just (RuleAtomValPtr          ,[state { state_code = Return (MemVal addr) }]) @@ -258,8 +258,8 @@   -- Prim Function App   | Evaluate (PrimApp pfun args) locals <- code =     let pass_in = LiftAct args locals globals heap confs-        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in-        eval = LitEval pfun (map valueToLit vals)+        LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in+        eval = LitEval pfun (map valToLit vals)     in Just (RulePrimApp             ,[state { state_heap = heap'                     , state_globals = globals'@@ -269,8 +269,8 @@   -- Rule Con App   | Evaluate (ConApp dcon args) locals <- code =     let pass_in = LiftAct args locals globals heap confs-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in-        (heapf, addr) = allocHeap (ConObj dcon vals) heap'+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in+        (heapf, addr) = allocHeapObj (ConObj dcon vals) heap'     in Just (RuleConApp             ,[state { state_heap = heapf                     , state_globals = globals'@@ -283,8 +283,8 @@   , FunObj params expr fun_locs <- hobj   , length params == length args =     let pass_in = LiftAct args locals globals heap confs-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in-        fun_locs' = insertLocalsList (zip params vals) fun_locs+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in+        fun_locs' = insertLocalsVals (zip params vals) fun_locs     in Just (RuleFunAppExact             ,[state { state_heap = heap'                     , state_globals = globals'@@ -297,11 +297,11 @@   , FunObj params expr fun_locs <- hobj   , (_, Left ex_params) <- unevenZip params args =     let pass_in = LiftAct args locals globals heap confs-        LiftAct vals _ globals' heap' confs' = liftAtomList pass_in-        fun_locs' = insertLocalsList (zip params vals) fun_locs+        LiftAct vals _ globals' heap' confs' = liftAtoms pass_in+        fun_locs' = insertLocalsVals (zip params vals) fun_locs         -- New Fun Object.         pobj = FunObj ex_params expr fun_locs'-        (heapf, paddr) = allocHeap pobj heap'+        (heapf, paddr) = allocHeapObj pobj heap'     in Just (RuleFunAppUnder             ,[state { state_heap = heapf                     , state_globals = globals'@@ -315,7 +315,7 @@     let sname = freshSeededName (varName svar) confs         svar' = Var sname (foldl AppTy (varType svar) (map atomType args))         sym = Symbol svar' (Just (FunApp sfun args, locals))-        (heap', addr) = allocHeap (SymObj sym) heap+        (heap', addr) = allocHeapObj (SymObj sym) heap     in Just (RuleFunAppSym             ,[state { state_heap = heap'                     , state_code = Return (MemVal addr)@@ -352,7 +352,7 @@   -- Rule Case Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code   , (Alt _ _ expr):_ <- matchLitAlts lit alts =-    let locals' = insertLocals (cvar, LitVal lit) locals+    let locals' = insertLocalsVal (cvar, LitVal lit) locals     in Just (RuleCaseLit             ,[state { state_code = Evaluate expr locals' }]) @@ -363,7 +363,7 @@   , (Alt _ params expr):_ <- matchDataAlts dcon alts   , length params == length vals =     let kvs = (cvar, MemVal addr) : zip params vals-        locals' = insertLocalsList kvs locals+        locals' = insertLocalsVals kvs locals     in Just (RuleCaseConPtr             ,[state { state_code = Evaluate expr locals' }]) @@ -371,7 +371,7 @@   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code   , [] <- matchLitAlts lit alts   , (Alt _ _ expr):_ <- defaultAlts alts =-    let locals' = insertLocals (cvar, LitVal lit) locals+    let locals' = insertLocalsVal (cvar, LitVal lit) locals     in Just (RuleCaseAnyLit             ,[state { state_code = Evaluate expr locals' }]) @@ -381,7 +381,7 @@   , ConObj dcon _ <- hobj   , [] <- matchDataAlts dcon alts   , (Alt _ _ expr):_ <- defaultAlts alts =-    let locals' = insertLocals (cvar, MemVal addr) locals+    let locals' = insertLocalsVal (cvar, MemVal addr) locals     in Just (RuleCaseAnyConPtr             ,[state { state_code = Evaluate expr locals' }]) @@ -403,7 +403,7 @@         all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts         negatives = map negateConstraint all_conss         def_lifts' = map (\(LiftAct (e, _) l g h c) ->-                                    (LiftAct (e, negatives) l g h c)) def_lifts+                           (LiftAct (e, negatives) l g h c)) def_lifts         def_sts = map (liftedAltToState state) def_lifts'     in Just (RuleCaseSym, acon_sts ++ def_sts) @@ -431,7 +431,7 @@   | Just (UpdateFrame frm_addr, stack') <- popStack stack   , Return (MemVal addr) <- code   , Just hobj <- lookupHeap addr heap-  , isHeapValueForm hobj =+  , isHeapValForm hobj =     Just (RuleUpdateDValPtr          ,[state { state_stack = stack'                  , state_heap = insertHeapRedir (frm_addr, addr) heap@@ -439,7 +439,7 @@    -- Rule Case Frame Create Case Non LitVal or MemVal   | Evaluate (Case mexpr cvar alts) locals <- code-  , not (isExprValueForm mexpr locals globals heap) =+  , not (isExprValForm mexpr locals globals heap) =     let frame = CaseFrame cvar alts locals     in Just (RuleCaseCCaseNonVal             ,[state { state_stack = pushStack frame stack@@ -453,15 +453,15 @@             ,[state { state_stack = stack'                     , state_code = Evaluate cexpr frm_locs }]) -  -- Rule Case Frame Delete Heap Value+  -- Rule Case Frame Delete Heap Val   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack   , Return (MemVal addr) <- code   , Just hobj <- lookupHeap addr heap-  , isHeapValueForm hobj =+  , isHeapValForm hobj =     let vname = freshSeededName (varName cvar) confs         vvar = Var vname (varType cvar)         cexpr = Case (Atom (VarAtom vvar)) cvar alts-        frm_locs' = insertLocals (vvar, MemVal addr) frm_locs+        frm_locs' = insertLocalsVal (vvar, MemVal addr) frm_locs     in Just (RuleCaseDValPtr             ,[state { state_stack = stack'                     , state_code = Evaluate cexpr frm_locs'@@ -482,8 +482,8 @@   , FunObj params expr fun_locs <- hobj   , (_, Right ex_args) <- unevenZip params args =     let pass_in = LiftAct args locals globals heap confs-        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in-        fun_locs' = insertLocalsList (zip params vals) fun_locs+        LiftAct vals locals' globals' heap' confs' = liftAtoms pass_in+        fun_locs' = insertLocalsVals (zip params vals) fun_locs         frame = ApplyFrame ex_args locals'     in Just (RuleApplyCFunAppOver             ,[state { state_stack = pushStack frame stack@@ -500,7 +500,7 @@   , Just ftype <- memAddrType addr heap =     let fname = freshName VarNSpace confs         fvar = Var fname ftype-        frm_locs' = insertLocals (fvar, MemVal addr) frm_locs+        frm_locs' = insertLocalsVal (fvar, MemVal addr) frm_locs     in Just (RuleApplyDReturnFun             ,[state { state_stack = stack'                     , state_code = Evaluate (FunApp fvar args) frm_locs'@@ -513,14 +513,14 @@   , SymObj (Symbol svar _) <- hobj =     let sname = freshSeededName (varName svar) confs         svar' = Var sname (varType svar)-        frm_locs' = insertLocals (svar', MemVal addr) frm_locs+        frm_locs' = insertLocalsVal (svar', MemVal addr) frm_locs     in Just (RuleApplyDReturnSym             ,[state { state_stack = stack'                     , state_code = Evaluate (FunApp svar' args) frm_locs'                     , state_names = sname : confs }]) -  -- State is Value Form-  | isStateValueForm state = Just (RuleIdentity, [state])+  -- State is Val Form+  | isStateValForm state = Just (RuleIdentity, [state])    -- Everything Broke!!!   | otherwise = Nothing

@@ -57,8 +57,8 @@ pass rule_states = (lives, \prev -> prev ++ deads)   where     stepped = concatMap step rule_states-    lives = filter (not . isStateValueForm . snd) stepped-    deads = filter (isStateValueForm . snd) stepped+    lives = filter (not . isStateValForm . snd) stepped+    deads = filter (isStateValForm . snd) stepped  -- | Run bounded breadth-first-search of the execution space with an `Int` to -- denote the maximum number of steps to take.@@ -70,7 +70,7 @@     execution = foldl (\acc s -> s <*> acc) start passes  -- | Run bounded breadth-first-search of the execution state with an `Int` to--- denote the maximum number of steps to take. We keep track of a list to track+-- denote the maximum number of steps to take. We keep a list to track -- a history of all the execution snapshots. As it stands, this is currently -- very NOT optimized. runBoundedBFSLogged :: Int -> State -> [([LiveState], [DeadState])]

@@ -13,7 +13,7 @@     , Stack     , Frame(..)     , MemAddr-    , Value(..)+    , Val(..)     , Locals     , Heap     , HeapObj(..)@@ -36,31 +36,31 @@      , empty_locals     , lookupLocals-    , insertLocals-    , insertLocalsList+    , insertLocalsVal+    , insertLocalsVals     , localsToList      , empty_heap     , lookupHeap     , insertHeapObj-    , insertHeapObjList+    , insertHeapObjs     , insertHeapRedir-    , allocHeap-    , allocHeapList+    , allocHeapObj+    , allocHeapObjs     , heapToList      , empty_globals     , lookupGlobals-    , insertGlobals-    , insertGlobalsList+    , insertGlobalsVal+    , insertGlobalsVals     , globalsToList      , empty_pathcons     , insertPathCons-    , insertPathConsList-    , pathconsToList+    , insertPathConss+    , pathConsToList -    , lookupValue+    , lookupVal     , vlookupHeap     , memAddrType     ) where@@ -100,12 +100,12 @@                    , state_globals :: !Globals                    , state_code :: !Code                    , state_names :: ![Name]-                   , state_paths :: !PathCons+                   , state_path :: !PathCons                    } deriving (Show, Eq, Read)  -- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the--- source from which the symbolic variable was generated. For instance, this is--- useful during symbolic function application.+-- source from which the symbolic variable was generated. For instance, this+-- is useful during symbolic function application. data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)  -- | State status.@@ -126,15 +126,15 @@ -- | Memory address for things on the `Heap`. newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) --- | A `Value` is something that we aim to reduce our current expression down+-- | A `Val` is something that we aim to reduce our current expression down -- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or -- `ConObj`, which are "returned" from expression evaluation in this form.-data Value = LitVal Lit-           | MemVal MemAddr-           deriving (Show, Eq, Read)+data Val = LitVal Lit+         | MemVal MemAddr+         deriving (Show, Eq, Read) --- | Locals binds a `Var`'s `Name` to its some `Value`.-newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)+-- | Locals binds a `Var`'s `Name` to its some `Val`.+newtype Locals = Locals (M.Map Name Val) deriving (Show, Eq, Read)  -- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address -- that was allocated. This allows us to consistently allocate fresh addresses@@ -145,7 +145,7 @@ -- | Heap objects. data HeapObj = LitObj Lit              | SymObj Symbol-             | ConObj DataCon [Value]+             | ConObj DataCon [Val]              | FunObj [Var] Expr Locals              | Blackhole              deriving (Show, Eq, Read)@@ -153,12 +153,12 @@ -- | Globals are statically loaded at the time when a `State` is loaded. -- However, because uninterpreted / out-of-scope variables are made symbolic -- at runtime, it can be modified during execution.-newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read)+newtype Globals = Globals (M.Map Name Val) deriving (Show, Eq, Read)  -- | Evaluation of the current expression. We are either evaluating, or ready--- to return with some `Value`.+-- to return with some `Val`. data Code = Evaluate Expr Locals-          | Return Value+          | Return Val           deriving (Show, Eq, Read)  -- | Path constraints are the conjunctive normal form of `Constraint`s.@@ -200,7 +200,7 @@ -- | `Stack` pop. popStack :: Stack -> Maybe (Frame, Stack) popStack (Stack []) = Nothing-popStack (Stack (frame:frames)) = Just (frame, Stack frames)+popStack (Stack (frame:fs)) = Just (frame, Stack fs)  -- | `Stack` push. pushStack :: Frame -> Stack -> Stack@@ -215,19 +215,19 @@ empty_locals = Locals M.empty  -- | `Locals` lookup.-lookupLocals :: Var -> Locals -> Maybe Value+lookupLocals :: Var -> Locals -> Maybe Val lookupLocals var (Locals lmap) = M.lookup (varName var) lmap  -- | `Locals` insertion.-insertLocals :: (Var, Value) -> Locals -> Locals-insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)+insertLocalsVal :: (Var, Val) -> Locals -> Locals+insertLocalsVal (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)  -- | List insertion into `Locals`.-insertLocalsList :: [(Var, Value)] -> Locals -> Locals-insertLocalsList kvs locals = foldr insertLocals locals kvs+insertLocalsVals :: [(Var, Val)] -> Locals -> Locals+insertLocalsVals kvs locals = foldr insertLocalsVal locals kvs  -- | `Locals` to key value pairs.-localsToList :: Locals -> [(Name, Value)]+localsToList :: Locals -> [(Name, Val)] localsToList (Locals lmap) = M.toList lmap  -- | Empty `Heap`.@@ -246,28 +246,28 @@ insertHeapObj (k, v) (Heap hmap prev) = Heap (M.insert k (Right v) hmap) prev  -- | Insert a list of `HeapObj` at specified `MemAddr` locations.-insertHeapObjList :: [(MemAddr, HeapObj)] -> Heap -> Heap-insertHeapObjList kvs heap = foldr insertHeapObj heap kvs+insertHeapObjs :: [(MemAddr, HeapObj)] -> Heap -> Heap+insertHeapObjs kvs heap = foldr insertHeapObj heap kvs  -- | Insert a redirection `MemAddr` into the `Heap`. insertHeapRedir :: (MemAddr, MemAddr) -> Heap -> Heap insertHeapRedir (a, r) (Heap hmap prev) = Heap (M.insert a (Left r) hmap) prev  -- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`.-allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)-allocHeap hobj (Heap hmap prev) = (heap', addr)+allocHeapObj :: HeapObj -> Heap -> (Heap, MemAddr)+allocHeapObj hobj (Heap hmap prev) = (heap', addr)   where     addr = MemAddr ((memAddrInt prev) + 1)     heap' = insertHeapObj (addr, hobj) (Heap hmap addr)  -- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the -- `MemAddr` at which they have been allocated at.-allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr])-allocHeapList [] heap = (heap, [])-allocHeapList (hobj:hobjs) heap = (heapf, addr : as)+allocHeapObjs :: [HeapObj] -> Heap -> (Heap, [MemAddr])+allocHeapObjs [] heap = (heap, [])+allocHeapObjs (hobj:hs) heap = (heapf, addr : as)   where-    (heap', addr) = allocHeap hobj heap-    (heapf, as) = allocHeapList hobjs heap'+    (heap', addr) = allocHeapObj hobj heap+    (heapf, as) = allocHeapObjs hs heap'  -- | `Heap` to key value pairs. heapToList :: Heap -> [(MemAddr, Either MemAddr HeapObj)]@@ -278,21 +278,21 @@ empty_globals = Globals M.empty  -- | `Globals` lookup.-lookupGlobals :: Var -> Globals -> Maybe Value+lookupGlobals :: Var -> Globals -> Maybe Val lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap  -- | `Globals` insertion.-insertGlobals :: (Var, Value) -> Globals -> Globals-insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)+insertGlobalsVal :: (Var, Val) -> Globals -> Globals+insertGlobalsVal (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap) --- | Insert a list of `Var` and `Value` pairs into `Globals`. This would+-- | Insert a list of `Var` and `Val` pairs into `Globals`. This would -- typically occur for new symbolic variables created from uninterpreted / -- out-of-scope variables during runtime.-insertGlobalsList :: [(Var, Value)] -> Globals -> Globals-insertGlobalsList kvs globals = foldr insertGlobals globals kvs+insertGlobalsVals :: [(Var, Val)] -> Globals -> Globals+insertGlobalsVals kvs globals = foldr insertGlobalsVal globals kvs  -- | `Globals` to key value pairs.-globalsToList :: Globals -> [(Name, Value)]+globalsToList :: Globals -> [(Name, Val)] globalsToList (Globals gmap) = M.toList gmap  -- | Empty `PathCons`.@@ -304,25 +304,25 @@ insertPathCons cons (PathCons conss) = PathCons (cons : conss)  -- | Insert a list of `Constraint`s into a `PathCons`.-insertPathConsList :: [Constraint] -> PathCons -> PathCons-insertPathConsList conss pathcons = foldr insertPathCons pathcons conss+insertPathConss :: [Constraint] -> PathCons -> PathCons+insertPathConss conss pathcons = foldr insertPathCons pathcons conss  -- | `PathCons` to list of `Constraint`s.-pathconsToList :: PathCons -> [Constraint]-pathconsToList (PathCons conss) = conss+pathConsToList :: PathCons -> [Constraint]+pathConsToList (PathCons conss) = conss  -- Complex functions that involve multiple data structures. --- | `Value` lookup from the `Locals` first, then `Globals`.-lookupValue :: Var -> Locals -> Globals -> Maybe Value-lookupValue var locals globals = case lookupLocals var locals of+-- | `Val` lookup from the `Locals` first, then `Globals`.+lookupVal :: Var -> Locals -> Globals -> Maybe Val+lookupVal var locals globals = case lookupLocals var locals of     Just val -> Just val     Nothing -> lookupGlobals var globals --- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found.+-- | `Heap` lookup. Returns the appropriate. `MemAddr` and `HeapObj` if found. vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) vlookupHeap var locals globals heap = do-    val <- lookupValue var locals globals+    val <- lookupVal var locals globals     case val of         LitVal _ -> Nothing         MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)@@ -335,6 +335,6 @@         LitObj lit -> Just (litType lit)         SymObj (Symbol svar _) -> Just (varType svar)         ConObj dcon _ -> Just (dataConType dcon)-        FunObj ps expr _ -> Just (foldr FunTy (exprType expr) (map varType ps))+        FunObj ps ex _ -> Just (foldr FunTy (exprType ex) (map varType ps))         Blackhole -> Just Bottom 

@@ -4,11 +4,11 @@     , varName     , nameOccStr     , nameInt-    , freshString+    , freshStr     , freshName     , freshSeededName-    , freshNameList-    , freshSeededNameList+    , freshNames+    , freshSeededNames     ) where  import SSTG.Core.Language.Syntax@@ -38,15 +38,15 @@ -- | `Name`s in a `BindRhs`. bindRhsNames :: BindRhs -> [Name] bindRhsNames (FunForm prms expr) = concatMap varNames prms ++ exprNames expr-bindRhsNames (ConForm dcon args) = concatMap atomNames args ++ dataNames dcon+bindRhsNames (ConForm dcon as) = dataConNames dcon ++ concatMap atomNames as  -- | `Name`s in an `Expr`. exprNames :: Expr -> [Name] exprNames (Atom atom) = atomNames atom exprNames (Let binds expr) = exprNames expr ++ bindsNames binds exprNames (FunApp fun args) = varNames fun ++ concatMap atomNames args-exprNames (PrimApp prim args) = pfunNames prim ++ concatMap atomNames args-exprNames (ConApp dcon args) = dataNames dcon ++ concatMap atomNames args+exprNames (PrimApp pfun args) = primFunNames pfun ++ concatMap atomNames args+exprNames (ConApp dcon args) = dataConNames dcon ++ concatMap atomNames args exprNames (Case expr var alts) = exprNames expr ++ concatMap altNames alts                                                 ++ varNames var @@ -56,12 +56,12 @@ atomNames (VarAtom var) = varNames var  -- | `Name`s in a `PrimFun`.-pfunNames :: PrimFun -> [Name]-pfunNames (PrimFun name ty) = name : typeNames ty+primFunNames :: PrimFun -> [Name]+primFunNames (PrimFun name ty) = name : typeNames ty  -- | `Name`s in a `DataCon`.-dataNames :: DataCon -> [Name]-dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)+dataConNames :: DataCon -> [Name]+dataConNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)  -- | `Name`s in an `Alt`. altNames :: Alt -> [Name]@@ -92,7 +92,7 @@ tyConNames (FunTyCon name bndrs) = name : concatMap tyBinderNames bndrs tyConNames (PrimTyCon name bndrs) = name : concatMap tyBinderNames bndrs tyConNames (Promoted name bndrs dcon) = name : concatMap tyBinderNames bndrs-                                            ++ dataNames dcon+                                            ++ dataConNames dcon  -- | `Name`s in a `Coercion`. coercionNames :: Coercion -> [Name]@@ -117,9 +117,9 @@ -- `String`s that we do not want our new `String` to conflict with. The sole -- purpose of the `Int` seed is to allow us tell us how much to multiply some -- prime number to "orbit" an index around a fixed list of acceptable `Char`s.-freshString :: Int -> String -> S.Set String -> String-freshString rand seed confs = if S.member seed confs-    then freshString (rand + 1) (seed ++ [pick]) confs else seed+freshStr :: Int -> String -> S.Set String -> String+freshStr rand seed confs = if S.member seed confs+    then freshStr (rand + 1) (seed ++ [pick]) confs else seed   where     pick = bank !! index     index = raw_i `mod` (length bank)@@ -147,25 +147,25 @@ freshSeededName seed confs = Name occ' mdl ns unq'   where     Name occ mdl ns unq = seed-    occ' = freshString 1 occ (S.fromList alls)+    occ' = freshStr 1 occ (S.fromList alls)     unq' = maxs + 1     alls = map nameOccStr confs     maxs = L.maximum (unq : map nameInt confs)  -- | Generate a list of `Name`s, each corresponding to the appropriate element -- of the `NameSpace` list.-freshNameList :: [NameSpace] -> [Name] -> [Name]-freshNameList [] _ = []-freshNameList (nspace:nss) confs = name' : freshNameList nss confs'+freshNames :: [NameSpace] -> [Name] -> [Name]+freshNames [] _ = []+freshNames (nspace:ns) confs = name' : freshNames ns confs'   where     name' = freshName nspace confs     confs' = name' : confs  -- | List of seeded fresh `Name`s.-freshSeededNameList :: [Name] -> [Name] -> [Name]-freshSeededNameList [] _ = []-freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs'+freshSeededNames :: [Name] -> [Name] -> [Name]+freshSeededNames [] _ = []+freshSeededNames (name:ns) confs = name' : freshSeededNames ns confs'   where-    name' = freshSeededName n confs+    name' = freshSeededName name confs     confs' = name' : confs 

@@ -4,8 +4,8 @@     ) where  -- | A `Program` is defined as a list of bindings. The @Name@ is an identifier--- that determines a unique binder to the @var@. In practice, these are defined--- to be `Name` and `Var` respectively.+-- that determines a unique binder to the @var@. In practice, these are+-- defined to be `Name` and `Var` respectively. newtype Program = Program [Binds] deriving (Show, Eq, Read)  -- | Variables, data constructors, type variables, and type constructors.

@@ -47,6 +47,6 @@ exprType (ConApp dc args) = foldl AppTy (dataConType dc) (map atomType args) exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) exprType (Let _ expr) = exprType expr-exprType (Case _ _ (a:_)) = altType a+exprType (Case _ _ (alt:_)) = altType alt exprType _ = Bottom 

@@ -2,8 +2,8 @@ module SSTG.Core.Translation.Haskell     ( CompileClosure     , mkCompileClosure-    , mkTargetBindsList-    , mkIOString+    , mkTargetBindss+    , mkIOStr     ) where  import qualified SSTG.Core.Language as SL@@ -31,15 +31,15 @@ import qualified Data.Maybe as MB  -- | Make IO String from Outputable.-mkIOString :: (Outputable a) => a -> IO String-mkIOString obj = runGhc (Just libdir) $ do+mkIOStr :: (Outputable a) => a -> IO String+mkIOStr obj = runGhc (Just libdir) $ do     dflags <- getSessionDynFlags     return (showPpr dflags obj)  -- | Given the project directory and the source file path, compiles the -- `ModuleGraph` and translates it into a SSTG `Binds`s.-mkTargetBindsList :: FilePath -> FilePath -> IO [SL.Binds]-mkTargetBindsList proj src = do+mkTargetBindss :: FilePath -> FilePath -> IO [SL.Binds]+mkTargetBindss proj src = do     (sums_gutss, dflags, env) <- mkCompileClosure proj src     let (sums, gutss) = (map fst sums_gutss, map snd sums_gutss)     let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums@@ -145,7 +145,7 @@   (MachDouble rat) -> SL.MachDouble rat ((mkType . literalType) lit)   (LitInteger i _) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)   (MachNullAddr) -> SL.MachNullAddr ((mkType . literalType) lit)-  (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit)+  (MachLabel f m _) -> SL.MachLabel (unpackFS f) m (mkType $ literalType lit)  -- | `DataCon`'s `Name`. mkDataName :: DataCon -> SL.Name

@@ -47,13 +47,13 @@ pprStateStr :: State -> String pprStateStr state = injNewLine acc_strs   where-    status_str= (pprStatusStr . state_status) state+    status_str = (pprStatusStr . state_status) state     stack_str = (pprStackStr . state_stack) state     heap_str = (pprHeapStr . state_heap) state     globals_str = (pprGlobalsStr . state_globals) state     expr_str = (pprCodeStr . state_code) state     names_str = (pprNamesStr . state_names) state-    pcons_str = (pprPathConsStr . state_paths) state+    pcons_str = (pprPathConsStr . state_path) state     acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>"                , status_str                , "----- [Stack] ---------------"@@ -184,7 +184,7 @@     header = "ConObj"     addr_str = pprMemAddrStr addr     dcon_str = pprDataConStr dcon-    vals_str = injIntoList (map pprValueStr vals)+    vals_str = injIntoList (map pprValStr vals)     acc_str = sub (addr_str ++ ", " ++ injSpace [header, dcon_str, vals_str]) pprMemHeapObjStr (addr, FunObj params expr locals) = acc_str   where@@ -213,7 +213,7 @@   where     glist = globalsToList globals     name_strs = map (pprNameStr . fst) glist-    val_strs = map (pprValueStr . snd) glist+    val_strs = map (pprValStr . snd) glist     zipd_strs = zip name_strs val_strs     acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs @@ -223,18 +223,18 @@   where     llist = localsToList locals     name_strs = map (pprNameStr . fst) llist-    val_strs = map (pprValueStr . snd) llist+    val_strs = map (pprValStr . snd) llist     zipd_strs = zip name_strs val_strs     acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs --- | Print `Value`.-pprValueStr :: Value -> String-pprValueStr (LitVal lit) = injSpace acc_strs+-- | Print `Val`.+pprValStr :: Val -> String+pprValStr (LitVal lit) = injSpace acc_strs   where     header = "LitVal"     lit_str = pprLitStr lit     acc_strs = [header, lit_str]-pprValueStr (MemVal addr) = injSpace acc_strs+pprValStr (MemVal addr) = injSpace acc_strs   where     header = "MemVal"     ptr_str = pprMemAddrStr addr@@ -395,7 +395,7 @@ pprCodeStr (Return val) = injSpace acc_strs   where     header = "Return"-    val_str = pprValueStr val+    val_str = pprValStr val     acc_strs = [header, val_str]  -- | Print a list of `Name`s.@@ -406,7 +406,7 @@ pprPathConsStr :: PathCons -> String pprPathConsStr pathcons = injNewLineSeps5 strs   where-    strs = map pprConstraintStr (pathconsToList pathcons)+    strs = map pprConstraintStr (pathConsToList pathcons)  -- | Print `PathCond`. pprConstraintStr :: Constraint -> String