packages feed

SSTG 0.1.0.1 → 0.1.0.2

raw patch · 11 files changed

+315/−272 lines, 11 files

Files

SSTG.cabal view
@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.0.1+version:             0.1.0.2 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme@@ -30,6 +30,7 @@                      , SSTG.Core.Execution.Stepper                      , SSTG.Utils                      , SSTG.Utils.PrettyPrint+  ghc-options:         -Wall -fmax-pmcheck-iterations=2000000   build-depends:       base >= 4.7 && < 5                      , ghc                      , ghc-paths
app/Main.hs view
@@ -2,8 +2,6 @@  import SSTG -import qualified Data.Map as M- import System.Environment  main :: IO ()@@ -18,16 +16,17 @@     -- Do the loading.     let load_result = loadStateEntry entry (Program binds)     putStrLn $ "binds: " ++ show (length binds)+    -- putStrLn "Bindings"+    -- mapM_ (putStrLn . pprBindingStr) binds+     case load_result of         LoadError str -> do             error str         LoadOkay state -> do-            -- putStrLn "Bindings"-            -- mapM_ (putStrLn . pprBindingStr) binds             putStrLn" **************** INIT ***************"-            putStrLn "Initial state:"-            putStrLn $ pprStateStr state-            let lds = execute1 100 state+            -- putStrLn "Initial state:"+            -- putStrLn $ pprStateStr state+            let lds = execute1 200 state             putStrLn "*************** BEGIN ***************"             putStrLn $ pprLivesDeadsStr lds         LoadGuess state cands -> do
src/SSTG/Core/Execution/Engine.hs view
@@ -11,8 +11,7 @@ import SSTG.Core.Execution.Namer import SSTG.Core.Execution.Stepper -import qualified Data.List as L-import qualified Data.Map  as M+import qualified Data.Map as M  -- | Load Result data LoadResult = LoadOkay  State@@ -59,7 +58,6 @@                          , state_links   = SymLinks M.empty }          -- Gather information on all variables.-        names    = allNames state0         state    = state0 { state_names = allNames state0 }  -- | Allocate Binding@@ -89,12 +87,6 @@         bnd_addrss = zip bnds addrss         name_vals  = concatMap bndAddrsToNameVals bnd_addrss --- | Force Get Address-forceLookupAddr :: Var -> Globals -> MemAddr-forceLookupAddr var globals = case lookupGlobals var globals of-    Just (MemVal addr) -> addr-    otherwise          -> MemAddr (-1)- -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value forceLookupValue (LitAtom lit) _      _       = LitVal lit@@ -134,7 +126,7 @@  -- | Bind Filtering bindFilter :: String -> (Binding, Locals) -> Bool-bindFilter entry (bnd, loc) = lhsMatches entry bnd /= []+bindFilter entry (bnd, _) = lhsMatches entry bnd /= []  -- | Sub-Bindings String Match lhsMatches :: String -> Binding -> [(Var, BindRhs)]
src/SSTG/Core/Execution/Models.hs view
@@ -28,7 +28,7 @@ instance Monad (SymbolicT s) where     return a  = pure a     st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0-                                      (s2, a2) = (run (fs a1)) s2 in (s2, a2))+                                      (s2, a2) = (run (fs a1)) s1 in (s2, a2))  -- | State data State = State { state_status  :: Status@@ -91,7 +91,8 @@ type PathCons = [PathCond]  -- | Path Condition-data PathCond = PathCond Alt Expr Locals Bool deriving (Show, Eq, Read)+data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool+              deriving (Show, Eq, Read)  -- | Symbolic Link Table newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read)@@ -142,9 +143,9 @@ -- | Allocate Heap List allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) allocHeapList []           heap = (heap, [])-allocHeapList (hobj:hobjs) heap = (res_heap, addr : as)-  where (heap', addr)  = allocHeap hobj heap-        (res_heap, as) = allocHeapList hobjs heap'+allocHeapList (hobj:hobjs) heap = (heapf, addr : as)+  where (heap', addr) = allocHeap hobj heap+        (heapf, as)   = allocHeapList hobjs heap'  -- | Insert Heap insertHeap :: MemAddr -> HeapObj -> Heap -> Heap@@ -180,17 +181,12 @@     Nothing  -> lookupGlobals var globals     mb_value -> mb_value --- | Look Up Value by Atom-alookupValue :: Atom -> Locals -> Globals -> Maybe Value-alookupValue (LitAtom lit) _      _       = Just (LitVal lit)-alookupValue (VarAtom var) locals globals = lookupValue var locals globals- -- | Lookup Heap by Variable vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) vlookupHeap var locals globals heap = do     val <- lookupValue var locals globals     case val of-        LitVal lit  -> Nothing+        LitVal _    -> Nothing         MemVal addr -> lookupHeap addr heap >>= \hobj -> return (addr, hobj)  -- | MemAddr Type@@ -198,9 +194,9 @@ memAddrType addr heap = do     hobj <- lookupHeap addr heap     return $ case hobj of-        Blackhole            -> Bottom-        LitObj lit           -> litType lit-        SymObj (Symbol svar) -> varType svar-        ConObj dcon _        -> dataConType dcon-        FunObj params expr _ -> FunTy (map varType params ++ [exprType expr])+        Blackhole          -> Bottom+        LitObj lit         -> litType lit+        SymObj (Symbol sv) -> varType sv+        ConObj dcon _      -> dataConType dcon+        FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) 
src/SSTG/Core/Execution/Namer.hs view
@@ -11,11 +11,9 @@ import SSTG.Core.Syntax import SSTG.Core.Execution.Models -import qualified Data.Char   as C-import qualified Data.IntMap as IM-import qualified Data.List   as L-import qualified Data.Map    as M-import qualified Data.Set    as S+import qualified Data.List as L+import qualified Data.Map  as M+import qualified Data.Set  as S  -- | All Names in State allNames :: State -> [Name]@@ -56,12 +54,12 @@  -- | Heap Object Names heapObjNames :: HeapObj -> [Name]-heapObjNames Blackhole       = []-heapObjNames (LitObj _)      = []-heapObjNames (SymObj sym)    = symbolNames sym-heapObjNames (ConObj dcon _) = dataNames dcon-heapObjNames (FunObj prms expr locals) =-    concatMap varNames prms ++ exprNames expr ++ localsNames locals+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  -- | Symbol Names symbolNames :: Symbol -> [Name]@@ -97,8 +95,8 @@ exprNames (PrimApp prim args)  = pfunNames prim ++ concatMap atomNames args exprNames (ConApp dcon args)   = dataNames dcon ++ concatMap atomNames args exprNames (Let binds expr)     = bindingNames binds ++ exprNames expr-exprNames (Case expr var alts) = varNames var ++ exprNames expr ++-                                 concatMap altNames alts+exprNames (Case expr var alts) = varNames var ++ exprNames expr+                                              ++ concatMap altNames alts -- | Type Names typeNames :: Type -> [Name] typeNames (TyVarTy n ty)    = n : typeNames ty@@ -108,8 +106,7 @@ typeNames (TyConApp tc ty)  = tyConNames tc ++ concatMap typeNames ty typeNames (CoercionTy coer) = coercionNames coer typeNames (LitTy _)         = []-typeNames (FunTy tys)       = concatMap typeNames tys-typeNames (TyClosure ty ts) = concatMap typeNames (ty : ts)+typeNames (FunTy t1 t2)     = typeNames t1 ++ typeNames t2 typeNames (Bottom)          = []  -- | Prim Fun Names@@ -122,7 +119,7 @@  -- | Data Constructor Names dataNames :: DataCon -> [Name]-dataNames (DataCon id ty tys) = conTagName id : concatMap typeNames (ty : tys)+dataNames (DataCon tg ty tys) = conTagName tg : concatMap typeNames (ty : tys)  -- | Type Binder Names tyBinderNames :: TyBinder -> [Name]@@ -131,13 +128,13 @@  -- | Type Constructor Names tyConNames :: TyCon -> [Name]-tyConNames (FunTyCon n)     = [n]-tyConNames (AlgTyCon n r)   = n : algTyRhsNames r-tyConNames (SynonymTyCon n) = [n]-tyConNames (FamilyTyCon n)  = [n]-tyConNames (PrimTyCon n)    = [n]-tyConNames (TcTyCon n)      = [n]-tyConNames (PromotedDataCon n dcon) = n : dataNames dcon+tyConNames (FunTyCon n)      = [n]+tyConNames (AlgTyCon n r)    = n : algTyRhsNames r+tyConNames (SynonymTyCon n)  = [n]+tyConNames (FamilyTyCon n)   = [n]+tyConNames (PrimTyCon n)     = [n]+tyConNames (TcTyCon n)       = [n]+tyConNames (Promoted n dcon) = n : dataNames dcon  -- | Coercion Names coercionNames :: Coercion -> [Name]@@ -152,9 +149,9 @@  -- | Binding Names bindingNames :: Binding -> [Name]-bindingNames (Binding _ bnds) = lhs ++ rhs-  where lhs = concatMap (varNames . fst) bnds-        rhs = concatMap (bindRhsNames . snd) bnds+bindingNames (Binding _ bnd) = lhs ++ rhs+  where lhs = concatMap (varNames . fst) bnd+        rhs = concatMap (bindRhsNames . snd) bnd  -- | Path Constraint Names pconsNames :: PathCons -> [Name]@@ -163,12 +160,13 @@  -- | Path Condition Names pcondNames :: PathCond -> [Name]-pcondNames (PathCond alt expr locals _) = altNames alt ++ exprNames expr-                                                       ++ localsNames locals+pcondNames (PathCond (_, vars) expr locals _) = map varName vars +++                                                exprNames expr   +++                                                localsNames locals  -- | Symbolic Link Names linksNames :: SymLinks -> [Name]-linksNames (SymLinks links) = []  -- map (\(a, b) -> [a, b]) kvs+linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) kvs   where kvs = M.toList links  -- | Fresh String from Int Rand Seed@@ -192,8 +190,8 @@  -- | Seeded Fresh Name from Conflict List freshSeededName :: Name -> [Name] -> Name-freshSeededName seed confs = Name occ' mod ns unq'-  where Name occ mod ns unq = seed+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
src/SSTG/Core/Execution/Rules.hs view
@@ -9,13 +9,12 @@ import SSTG.Core.Execution.Models import SSTG.Core.Execution.Namer -import qualified Data.Map   as M- -- | Rules data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt           | RulePrimApp           | RuleConApp-          | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym | RuleFunAppUnInt+          | RuleFunAppExact | RuleFunAppUnder  | RuleFunAppSym+                            | RuleFunAppConPtr | RuleFunAppUnInt           | RuleLet           | RuleCaseLit | RuleCaseConPtr | RuleCaseAnyLit | RuleCaseAnyConPtr                         | RuleCaseSym@@ -43,14 +42,15 @@ isHeapValueForm _                  = False  -- | Is Value Form---   Either a lit or points to a heap value (not LitObj!)+--   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. isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool 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+isExprValueForm _                    _      _       _    = False  -- | Is State Value? isStateValueForm :: State -> Bool@@ -76,39 +76,86 @@ unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) unevenZip as     []     = ([], Left as) unevenZip []     bs     = ([], Right bs)-unevenZip (a:as) (b:bs) = ((a, b) : acc, rem)-  where (acc, rem) = unevenZip as bs+unevenZip (a:as) (b:bs) = ((a, b) : acc, excess)+  where (acc, excess) = unevenZip as bs --- | Inject Type Closure-injTyClosure :: Type -> [Atom] -> Type-injTyClosure ty args = TyClosure ty (map atomType args)+-- | Lift Action Wrap Type+data LiftAct a = LiftAct  a Locals Globals Heap [Name] --- | Bind Rhs to Heap Object-rhsToObj :: BindRhs -> Locals -> Globals -> Maybe HeapObj-rhsToObj (FunForm prms expr) locals _       = Just (FunObj prms expr locals)-rhsToObj (ConForm dcon args) locals globals = do-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    return (ConObj dcon arg_vals)+-- | Lift Uninterpreted Variable+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)) heap+        globals' = insertGlobals var (MemVal addr) globals+        confs'   = sname : confs+        pass_out = LiftAct addr locals globals' heap' confs' --- | Lift Let Binding-liftBinding :: Binding -> Locals -> Globals -> Heap -> Maybe (Heap, Locals)-liftBinding (Binding NonRec bnd) locals globals heap = do-    hobjs <- mapM (\r -> rhsToObj r locals globals) (map snd bnd)-    let (heap', addrs) = allocHeapList hobjs heap-    return (heap', locals)-liftBinding (Binding Rec bnd) (Locals lmap) globals heap = do-    let names    = map (varName . fst) bnd-    let hfakes   = map (const Blackhole) bnd-    -- Allocate dummy BlackholeS-    let (heap', addrs) = allocHeapList hfakes heap-    let mem_vals = map (\a -> MemVal a) addrs-    -- Use the allocated BlackholeS to construct the locals closure.-    let lmap'    = M.fromList (zip names mem_vals)-    let locals'  = Locals (M.union lmap' lmap)-    hobjs <- mapM (\r -> rhsToObj r locals' globals) (map snd bnd)-    let injects  = zip addrs hobjs-    return (insertHeapList injects heap', locals')+-- | Lift Atom+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') +-- | Lift Atom List+liftAtomList :: LiftAct [Atom] -> LiftAct [Value]+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+        LiftAct val locals' globals' heap' confs' = liftAtom pass_in+        pass_rest = LiftAct as locals' globals' heap' confs'+        LiftAct vs  localsf globalsf heapf confsf = liftAtomList pass_rest+        pass_out  = LiftAct (val : vs) localsf globalsf heapf confsf++-- | Lift Bind Rhs+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+liftBindRhs (LiftAct (ConForm dcon args) locals globals heap confs) = pass_out+  where pass_in  = LiftAct args locals globals heap confs+        LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+        pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs'++-- | Lift Bind Rhs List+liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj]+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+        LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in+        pass_rest = LiftAct rs locals' globals' heap' confs'+        LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest+        pass_out  = LiftAct (hobj : hos) localsf globalsf heapf confsf++-- | Lift Binding+liftBinding :: LiftAct Binding -> LiftAct ()+liftBinding (LiftAct (Binding NonRec bnd) locals globals heap confs) = pass_out+  where pass_in  = LiftAct (map snd bnd) locals globals heap confs+        LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in+        (heapf, addrs) = allocHeapList hobjs heap'+        mem_vals = map MemVal addrs+        localsf  = insertLocalsList (zip (map fst bnd) mem_vals) locals'+        pass_out = LiftAct () localsf globals' heapf confs'+liftBinding (LiftAct (Binding 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+        pass_in  = LiftAct (map snd bnd) locals' globals heap' confs+        LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in+        heapf    = insertHeapList (zip addrs hobjs) heap''+        pass_out = LiftAct () localsf globals' heapf confs'+ -- | Default Alts defaultAlts :: [Alt] -> [Alt] defaultAlts alts = [a | a @ (Alt Default _ _) <- alts]@@ -130,28 +177,30 @@ negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs  -- | Lift Sym Alt-liftSymAlt :: Var -> MemAddr -> Var -> Locals -> Heap -> [Name] -> Alt ->-              (Expr, Locals, Heap, PathCons, [Name])-liftSymAlt mvar addr cvar locals heap confs (Alt ac params expr) =-    (expr, locals', heap', pcons, confs')-  where pre_names = freshSeededNameList (map varName params) confs-        sym_vars  = map (\(p, n) -> Var n (varType p)) (zip params pre_names)-        sym_objs  = map (\v -> SymObj (Symbol v)) sym_vars-        (heap', addrs) = allocHeapList sym_objs heap-        mem_vals  = map (\a -> MemVal a) addrs-        llist     = (cvar, MemVal addr) : zip params mem_vals-        locals'   = insertLocalsList llist locals-        mxpr      = Atom (VarAtom mvar)-        pcons     = [PathCond (Alt ac params expr) mxpr locals' True]-        confs'    = pre_names ++ confs+liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, PathCons)+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 (SymObj . Symbol) svars+        (heap', addrs) = allocHeapList hobjs heap+        mem_vals = map MemVal addrs+        llist    = (cvar, MemVal addr) : zip params mem_vals+        locals'  = insertLocalsList llist locals+        mxpr     = Atom (VarAtom mvar)+        pcons    = [PathCond (ac, params) mxpr locals' True]+        confs'   = snames ++ confs+        pass_out = LiftAct (expr, pcons) locals' globals heap' confs'  -- | Alt Closure to State-altClosureToState :: State -> (Expr, Locals, Heap, PathCons, [Name]) -> State-altClosureToState state (expr, locals, heap, pcons, confs) = state'-  where state' = state { state_heap  = heap-                       , state_code  = Evaluate expr locals-                       , state_names = confs ++ state_names state-                       , state_paths = pcons ++ state_paths state }+liftedAltToState :: State -> LiftAct (Expr, PathCons) -> State+liftedAltToState state (LiftAct args locals globals heap confs) = state'+  where (expr, pcons) = args+        state' = state { state_heap    = heap+                       , state_globals = globals+                       , state_code    = Evaluate expr locals+                       , state_names   = confs+                       , state_paths   = pcons ++ state_paths state }  -- | Reduce reduce :: State -> Maybe (Rule, [State])@@ -159,8 +208,7 @@                      , state_heap    = heap                      , state_globals = globals                      , state_code    = code-                     , state_names   = confs-                     , state_paths   = paths }+                     , state_names   = confs }    -- Stack Independent Rules @@ -186,63 +234,73 @@   -- Rule Atom Uninterpreted   | Evaluate (Atom (VarAtom uvar)) locals <- code   , Nothing <- vlookupHeap uvar locals globals heap = do-    let sname    = freshSeededName (varName uvar) confs-    let svar     = Var sname (varType uvar)-    let sym      = Symbol svar-    let (heap', addr) = allocHeap (SymObj sym) heap-    let globals' = insertGlobals uvar (MemVal addr) globals+    let pass_in = LiftAct uvar locals globals heap confs+    let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in     return ( RuleAtomUnInt            , [state { state_heap    = heap'                     , state_globals = globals'-                    , state_code    = Evaluate (Atom (VarAtom uvar)) locals-                    , state_names   = sname : confs }])+                    , state_code    = Evaluate (Atom (VarAtom uvar)) locals'+                    , state_names   = confs' }])    -- Prim Function App   | Evaluate (PrimApp pfun args) locals <- code = do-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    let eval = SymLitEval pfun (map valueToLit arg_vals)+    let pass_in = LiftAct args locals globals heap confs+    let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+    let eval    = SymLitEval pfun (map valueToLit vals)     return ( RulePrimApp-           , [state { state_code = Evaluate (Atom (LitAtom eval)) locals }])+           , [state { state_heap    = heap'+                    , state_globals = globals'+                    , state_code    = Evaluate (Atom (LitAtom eval)) locals'+                    , state_names   = confs' }])    -- | Rule Con App   | Evaluate (ConApp dcon args) locals <- code = do-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    let (heap', addr) = allocHeap (ConObj dcon arg_vals) heap+    let pass_in = LiftAct args locals globals heap confs+    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+    let (heapf, addr) = allocHeap (ConObj dcon vals) heap'     return ( RuleConApp-           , [state { state_heap = heap'-                    , state_code = Return (MemVal addr) }])+           , [state { state_heap    = heapf+                    , state_globals = globals'+                    , 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   , FunObj params expr fun_locs <- hobj   , length params == length args = do-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+    let pass_in   = LiftAct args locals globals heap confs+    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+    let fun_locs' = insertLocalsList (zip params vals) fun_locs     return ( RuleFunAppExact-           , [state { state_code = Evaluate expr fun_locs' }])+           , [state { state_heap    = heap'+                    , state_globals = globals'+                    , 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   , FunObj params expr fun_locs <- hobj-  , (_, Left ex_prms)           <- unevenZip params args = do-    -- Set up existing closure first.-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+  , (_, Left ex_ps)             <- unevenZip params args = do+    let pass_in   = LiftAct args locals globals heap confs+    let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+    let fun_locs' = insertLocalsList (zip params vals) fun_locs     -- New Fun Object.-    let pfobj     = FunObj ex_prms expr fun_locs'-    let (heap', pfaddr) = allocHeap pfobj heap+    let pobj      = FunObj ex_ps expr fun_locs'+    let (heapf, paddr) = allocHeap pobj heap'     return ( RuleFunAppUnder-           , [state { state_heap = heap'-                    , state_code = Return (MemVal pfaddr) }])+           , [state { state_heap    = heapf+                    , state_globals = globals'+                    , 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   , SymObj (Symbol svar) <- hobj = do     let sname = freshSeededName (varName svar) confs-    let svar' = Var sname (injTyClosure (varType svar) args)+    let svar' = Var sname (foldl AppTy (varType svar) (map atomType args))     let sym   = Symbol svar'     let (heap', addr) = allocHeap (SymObj sym) heap     return ( RuleFunAppSym@@ -250,26 +308,33 @@                     , state_code  = Return (MemVal addr)                     , state_names = sname : confs }]) +  -- Rule Fun App ConObj+  | Evaluate (FunApp cvar []) locals <- code+  , Just (addr, hobj) <- vlookupHeap cvar locals globals heap+  , ConObj _ _        <- hobj = do+    return ( RuleFunAppConPtr+           , [state { state_code = Return (MemVal addr) }])+   -- Rule Fun App Uninterpreted   | Evaluate (FunApp ufun args) locals <- code   , Nothing  <- vlookupHeap ufun locals globals heap = do-    let sname    = freshSeededName (varName ufun) confs-    let svar     = Var sname (varType ufun)-    let sym      = Symbol svar-    let (heap', addr) = allocHeap (SymObj sym) heap-    let globals' = insertGlobals ufun (MemVal addr) globals+    let pass_in = LiftAct ufun locals globals heap confs+    let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in     return ( RuleFunAppUnInt-           , [state { state_heap    = heap'-                    , state_globals = globals'-                    , state_code    = Evaluate (FunApp ufun args) locals-                    , state_names   = sname : confs }])+           , [ state { state_heap    = heap'+                     , state_globals = globals'+                     , state_code    = Evaluate (FunApp ufun args) locals'+                     , state_names   = confs' }])    -- Rule Let   | Evaluate (Let bnd expr) locals <- code = do-    (heap', locals') <- liftBinding bnd locals globals heap+    let pass_in = LiftAct bnd locals globals heap confs+    let LiftAct _ locals' globals' heap' confs' = liftBinding pass_in     return ( RuleLet-           , [state { state_heap = heap'-                    , state_code = Evaluate expr locals' }])+           , [state { state_heap    = heap'+                    , state_globals = globals'+                    , state_code    = Evaluate expr locals'+                    , state_names   = confs' }])    -- Rule Case Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code@@ -318,16 +383,20 @@   , SymObj _              <- hobj   , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)   , length (acon_alts ++ def_alts) > 0 = do-    -- Remember to account for cvar.-    let acon_clss = map (liftSymAlt mvar addr cvar locals heap confs) acon_alts-    let def_clss  = map (liftSymAlt mvar addr cvar locals heap confs) def_alts+    let acon_ins   = map (\a -> LiftAct (mvar, addr, cvar, a)+                                        locals globals heap confs) acon_alts+    let acon_lifts = map liftSymAlt acon_ins+    let def_ins    = map (\a -> LiftAct (mvar, addr, cvar, a)+                                        locals globals heap confs) def_alts+    let def_lifts  = map liftSymAlt def_ins     -- Make AltCon states first.-    let acon_sts  = map (altClosureToState state) acon_clss-    -- Make Default states next.-    let all_pcons = concatMap (\(_, _, _, pc, _) -> pc) acon_clss-    let neg_pcons = negatePathCons all_pcons-    let def_clss' = map (\(e, l, h, p, c) -> (e, l, h, neg_pcons, c)) def_clss-    let def_sts   = map (altClosureToState state) def_clss'+    let acon_sts   = map (liftedAltToState state) acon_lifts+    -- Make DEFAULT states next.+    let all_pcons  = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts+    let negs       = negatePathCons all_pcons+    let def_lifts' = map (\(LiftAct (e, _) l g h c) ->+                           (LiftAct (e, negs) l g h c)) def_lifts+    let def_sts    = map (liftedAltToState state) def_lifts'     return (RuleCaseSym, acon_sts ++ def_sts)    -- Stack Dependent Rules@@ -404,12 +473,16 @@   , Evaluate (FunApp fun args) locals <- code   , Just (_, hobj)              <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj-  , (_, Right ex_args)          <- unevenZip params args = do-    arg_vals <- mapM (\a -> alookupValue a locals globals) args-    let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+  , (_, Right ex_as)            <- unevenZip params args = do+    let pass_in   = LiftAct args locals globals heap confs+    let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+    let fun_locs' = insertLocalsList (zip params vals) fun_locs     return ( RuleApplyCFunAppOver-           , [state { state_stack = Stack (ApplyFrame ex_args locals : frames)-                    , state_code  = Evaluate expr fun_locs' }])+           , [state { state_stack   = Stack (ApplyFrame ex_as locals' : frames)+                    , state_heap    = heap'+                    , state_globals = globals'+                    , state_code    = Evaluate expr fun_locs'+                    , state_names   = confs' }])    -- Rule Apply Frame Delete ReturnPtr Function   | Stack (ApplyFrame args frm_locs : rest) <- stack
src/SSTG/Core/Execution/Stepper.hs view
@@ -5,12 +5,9 @@     , runBoundedDFS     ) where -import SSTG.Core.Syntax import SSTG.Core.Execution.Models import SSTG.Core.Execution.Rules -import qualified Data.Map as M- type LiveState = ([Rule], State)  type DeadState = ([Rule], State)@@ -38,5 +35,6 @@         start     = SymbolicT { run = (\lives -> (lives, [])) }         execution = foldl (\acc s -> s <*> acc) start passes +runBoundedDFS :: a runBoundedDFS = undefined 
src/SSTG/Core/Syntax/Language.hs view
@@ -105,8 +105,7 @@                  | TyConApp   (GenTyCon bnd)    [GenType bnd]                  | CoercionTy (GenCoercion bnd)                  | LitTy      TyLit-                 | FunTy      [GenType bnd]-                 | TyClosure  (GenType bnd)     [GenType bnd]+                 | FunTy      (GenType bnd)     (GenType bnd)                  | Bottom                  deriving (Show, Eq, Read) @@ -125,13 +124,13 @@                      deriving (Show, Eq, Read)  -- | TyCon-data GenTyCon bnd = FunTyCon        bnd-                  | AlgTyCon        bnd (GenAlgTyRhs bnd)-                  | SynonymTyCon    bnd-                  | FamilyTyCon     bnd-                  | PrimTyCon       bnd-                  | PromotedDataCon bnd (GenDataCon bnd)-                  | TcTyCon         bnd+data GenTyCon bnd = FunTyCon     bnd+                  | AlgTyCon     bnd (GenAlgTyRhs bnd)+                  | SynonymTyCon bnd+                  | FamilyTyCon  bnd+                  | PrimTyCon    bnd+                  | Promoted     bnd (GenDataCon bnd)+                  | TcTyCon      bnd                   deriving (Show, Eq, Read)  -- | Algebraic Type Constructor RHS
src/SSTG/Core/Syntax/Typer.hs view
@@ -16,10 +16,11 @@ litType (MachFloat _ ty)     = ty litType (MachDouble _ ty)    = ty litType (MachNullAddr ty)    = ty+litType (MachLabel _ _ ty)   = ty litType (BlankAddr)          = Bottom-litType (AddrLit addr)       = Bottom+litType (AddrLit _)          = Bottom litType (SymLit var)         = varType var-litType (SymLitEval pf args) = TyClosure (primFunType pf) (map litType args)+litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args)  atomType :: Atom -> Type atomType (VarAtom var) = varType var@@ -36,9 +37,9 @@  exprType :: Expr -> Type exprType (Atom atom)       = atomType atom-exprType (PrimApp pf args) = TyClosure (primFunType pf) (map atomType args)+exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args) exprType (ConApp dcon _)   = dataConType dcon-exprType (FunApp fun args) = TyClosure (varType fun) (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
src/SSTG/Core/Translation/Haskell.hs view
@@ -1,43 +1,33 @@ -- | Haskell Translation --   Extracts SSTG from Haskell source. module SSTG.Core.Translation.Haskell-    ( mkTargetBindings+    ( mkCompileClosure+    , mkTargetBindings     , mkIOStr     ) where  import qualified SSTG.Core.Syntax.Language as SL -import BasicTypes import Coercion import CorePrep import CoreSyn import CoreToStg-import CostCentre import DataCon import FastString-import ForeignCall import GHC import GHC.Paths-import GhcMonad import HscTypes import Literal-import Module import Name import Outputable import Pair import PrimOp-import SrcLoc import StgSyn import TyCon import TyCoRep-import Type-import UniqSet import Unique import Var as V -import System.IO--import qualified Data.IntMap as IM import qualified Data.Maybe  as MB  -- | Make IO String from Outputable@@ -56,14 +46,13 @@     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 z1 = zip3 mod_lcs m_bndss m_tcss-    preps <- sequence $ map (\((m, l), b, t) -> corePrepPgm env m l b t) z1--    let z2 = zip (map fst mod_lcs) preps-    stg_bndss <- sequence $ map (\(m, p) -> coreToStg dflags m p) z2--    let sl_bnds = map mkBinding (concat stg_bndss)+    -- 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+    -- Create the bindings.+    let sl_bnds = map mkBinding (concat s_bndss)     return sl_bnds  -- | Make Compilation Closure@@ -76,19 +65,18 @@ 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--    mod_graph <- getModuleGraph-    pmods <- (sequence . map parseModule) mod_graph-    tmods <- (sequence . map typecheckModule) pmods-    dmods <- (sequence . map desugarModule) tmods-    let mod_gutss = map coreModule dmods--    let zipd = (zip mod_graph mod_gutss, dflags, env)+    _          <- 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  -- | Make SSTG Expr@@ -111,11 +99,11 @@  -- | Make SSTG Name mkName :: Name -> SL.Name-mkName name = SL.Name occ mod ns unq+mkName name = SL.Name occ mdl ns unq   where occ = (occNameString . nameOccName) name         ns  = (mkNameSpace . occNameSpace . nameOccName) name         unq = (getKey . nameUnique) name-        mod = case nameModule_maybe name of+        mdl = case nameModule_maybe name of             Nothing -> Nothing             Just md -> Just ((moduleNameString . moduleName) md) @@ -136,8 +124,8 @@ -- | Make SSTG Binding mkBinding :: StgBinding -> SL.Binding mkBinding (StgNonRec bnd rhs) = SL.Binding SL.NonRec [(mkVar bnd, mkRhs rhs)]-mkBinding (StgRec bnds) = SL.Binding SL.Rec-                                     (map (\(b, r) -> (mkVar b, mkRhs r)) bnds)+mkBinding (StgRec bnd) = SL.Binding SL.Rec+                                    (map (\(b, r) -> (mkVar b, mkRhs r)) bnd)  -- | Make SSTG Rhs mkRhs :: StgRhs -> SL.BindRhs@@ -148,7 +136,7 @@ -- | Make SSTG Lit mkLit :: Literal -> SL.Lit mkLit lit = case lit of-  (MachChar char)   -> SL.MachChar char ((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)@@ -161,15 +149,15 @@   (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit)  -- | Make SSTG Data Constructor ID-mkDataId :: DataCon -> SL.ConTag-mkDataId datacon = SL.ConTag name tag+mkDataTag :: DataCon -> SL.ConTag+mkDataTag datacon = SL.ConTag name tag   where name = (mkName . dataConName) datacon         tag  = dataConTag datacon  -- | Make SSTG Data Constructor mkData :: DataCon -> SL.DataCon mkData datacon = SL.DataCon dcid ty args-  where dcid = mkDataId datacon+  where dcid = mkDataTag datacon         ty   = (mkType . dataConRepType) datacon         args = map mkType (dataConOrigArgTys datacon) @@ -177,11 +165,11 @@ 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 otherwise = error "mkPrimOp: got StgPrimCallOp or StgFCallOp"+        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@@ -191,7 +179,7 @@ mkAltCon :: AltCon -> SL.AltCon mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc) mkAltCon (LitAlt lit) = SL.LitAlt  (mkLit lit)-mkAltCon DEFAULT      = SL.Default+mkAltCon (DEFAULT)    = SL.Default  -- | Make SSTG Type mkType :: Type -> SL.Type@@ -203,42 +191,37 @@ mkType (CastTy ty cor)  = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor) --- | Make SSTG Kind-mkKind :: Kind -> SL.Type-mkKind = mkType- -- | Make SSTG Type Constructor mkTyCon :: TyCon -> SL.TyCon-mkTyCon tc | isFunTyCon     tc = SL.FunTyCon     name-           | isAlgTyCon     tc = SL.AlgTyCon     name algrhs-           | isFamilyTyCon  tc = SL.FamilyTyCon  name-           | isPrimTyCon    tc = SL.PrimTyCon    name-           | isTcTyCon      tc = SL.TcTyCon      name+mkTyCon tc | isFunTyCon         tc = SL.FunTyCon     name+           | isAlgTyCon         tc = SL.AlgTyCon     name algrhs+           | isFamilyTyCon      tc = SL.FamilyTyCon  name+           | isPrimTyCon        tc = SL.PrimTyCon    name+           | isTcTyCon          tc = SL.TcTyCon      name            | isTypeSynonymTyCon tc = SL.SynonymTyCon name-           | isPromotedDataCon tc  = SL.PromotedDataCon name dcon+           | isPromotedDataCon  tc = SL.Promoted     name dcon            | otherwise = error "mkTyCon: unrecognized TyCon"   where name   = (mkName . tyConName) tc-        kind   = (mkKind . tyConKind) tc         algrhs = (mkAlgTyConRhs . algTyConRhs) tc         dcon   = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc  -- | Make SSTG Algebraic Type Constructor RHS mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b-mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon  (map mkDataId dcs)-mkAlgTyConRhs (TupleTyCon {data_con = dc})  = SL.TupleTyCon (mkDataId dc)-mkAlgTyConRhs (NewTyCon {data_con = dc})    = SL.NewTyCon   (mkDataId dc)+mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon  (map mkDataTag dcs)+mkAlgTyConRhs (TupleTyCon {data_con = dc})  = SL.TupleTyCon (mkDataTag dc)+mkAlgTyConRhs (NewTyCon {data_con = dc})    = SL.NewTyCon   (mkDataTag dc)  -- | make SSTG Type Binder mkTyBndr :: TyBinder -> SL.TyBinder mkTyBndr (Anon ty)   = SL.AnonTyBndr  (mkType ty)-mkTyBndr (Named v f) = SL.NamedTyBndr (mkName (V.varName v))+mkTyBndr (Named v _) = SL.NamedTyBndr (mkName (V.varName v))                                       (mkType (varType v))  -- | Make SSTG Type Literal mkTyLit :: TyLit -> SL.TyLit-mkTyLit (NumTyLit int) = SL.NumTyLit (fromInteger int)-mkTyLit (StrTyLit fs)  = SL.StrTyLit (unpackFS fs)+mkTyLit (NumTyLit i)  = SL.NumTyLit (fromInteger i)+mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs)  -- | Make SSTG Coercion mkCoercion :: Coercion -> SL.Coercion
src/SSTG/Utils/PrettyPrint.hs view
@@ -58,7 +58,7 @@                       , "----- [Expression] ----------"                       , expr_str                       , "----- [All Names] -------"-                      , "" -- names_str+                      , fst ("", names_str)  -- names_str                       , "----- [Path Constraint] -----"                       , pcons_str                       , "----- [Symbolic Links] ------"@@ -126,7 +126,7 @@ pprFrameStr (UpdateFrame addr) = injNewLine acc_strs   where header   = "UpdateFrame"         addr_str = pprMemAddrStr addr-        acc_strs = [addr_str]+        acc_strs = [header, addr_str]  pprHeapObjStr :: HeapObj -> String pprHeapObjStr Blackhole = "Blackhole!!!"@@ -156,7 +156,9 @@         addr_strs = map (pprMemAddrStr . fst) kvs         hobj_strs = map (pprHeapObjStr . snd) kvs         zipd_strs = zip addr_strs hobj_strs-        acc_strs  = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs+        addr_str  = pprMemAddrStr addr+        kvs_strs  = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs+        acc_strs  = addr_str : kvs_strs  pprGlobalsStr :: Globals -> String pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs)@@ -202,15 +204,15 @@         acc_strs = [header, lit_str]  pprConTagStr :: ConTag -> String-pprConTagStr (ConTag name int) = pprNameStr name+pprConTagStr (ConTag name _) = pprNameStr name  pprDataConStr :: DataCon -> String-pprDataConStr (DataCon id ty tys) = injSpace acc_strs+pprDataConStr (DataCon tag ty tys) = injSpace acc_strs   where header   = "DataCon"-        id_str   = (sub . pprConTagStr) id+        tag_str  = (sub . pprConTagStr) tag         ty_str   = (sub . pprTypeStr) ty         tys_str  = injIntoList (map pprTypeStr tys)-        acc_strs = [header, id_str, ty_str, tys_str]+        acc_strs = [header, tag_str, ty_str, tys_str]  pprPrimFunStr :: PrimFun -> String pprPrimFunStr (PrimFun name ty) = injSpace acc_strs@@ -219,21 +221,21 @@         type_str = (sub . pprTypeStr) ty         acc_strs = [header, name_str, type_str] -pprAltCon :: AltCon -> String-pprAltCon (DataAlt dcon) = injSpace acc_strs+pprAltConStr :: AltCon -> String+pprAltConStr (DataAlt dcon) = injSpace acc_strs   where header   = "DataAlt"         dcon_str = (sub . pprDataConStr) dcon         acc_strs = [header, dcon_str]-pprAltCon (LitAlt lit) = injSpace acc_strs+pprAltConStr (LitAlt lit) = injSpace acc_strs   where header   = "LitAlt"         lit_str  = (sub . pprLitStr) lit         acc_strs = [header, lit_str]-pprAltCon Default = "Default"+pprAltConStr Default = "Default"  pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs   where header   = "Alt"-        acon_str = (sub . pprAltCon) acon+        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]@@ -260,9 +262,9 @@         acc_strs = [var_str, lamf_str]  pprBindingStr :: Binding -> String-pprBindingStr (Binding rec bnds) = injSpace acc_strs-  where header   = case rec of { Rec -> "Rec-Bind"; NonRec -> "NonRec-Bind" }-        bnds_str = injIntoList (map bindStr bnds)+pprBindingStr (Binding rec bnd) = injSpace acc_strs+  where header   = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }+        bnds_str = injIntoList (map bindStr bnd)         acc_strs = [header, bnds_str]  pprExprStr :: Expr -> String@@ -298,7 +300,7 @@         acc_strs = [header, bnd_str, expr_str]  pprTypeStr :: Type -> String-pprTypeStr ty = "__Type__"+pprTypeStr ty = fst ("__Type__", ty)  -- | State Code String pprCodeStr :: Code -> String@@ -323,12 +325,13 @@  -- | Path Condition String pprPCondStr :: PathCond -> String-pprPCondStr (PathCond alt expr locals hold) = injIntoList acc_strs-  where alt_str  = pprAltStr alt+pprPCondStr (PathCond (acon, params) expr locals hold) = injIntoList acc_strs+  where acon_str = pprAltConStr acon+        prms_str = injIntoList (map pprVarStr params)         expr_str = pprExprStr expr         locs_str = pprLocalsStr locals         hold_str = case hold of { True -> "Positive"; False -> "Negative" }-        acc_strs = [alt_str, expr_str, locs_str, hold_str]+        acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]  -- | Symbolic Links String pprLinksStr :: SymLinks -> String