SSTG 0.1.0.6 → 0.1.0.7

raw patch · 14 files changed

+322/−289 lines, 14 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +39/−6
• SSTG.cabal +3/−3
• src/SSTG/Core/Execution.hs +2/−2
• src/SSTG/Core/Execution/Engine.hs +1/−1
• src/SSTG/Core/Execution/Models.hs +0/−213
• src/SSTG/Core/Execution/Naming.hs +5/−5
• src/SSTG/Core/Execution/Rules.hs +1/−1
• src/SSTG/Core/Execution/Stepping.hs +1/−1
• src/SSTG/Core/Execution/Support.hs +213/−0
• src/SSTG/Core/Syntax.hs +2/−2
• src/SSTG/Core/Syntax/Language.hs +1/−1
• src/SSTG/Core/Syntax/Typecheck.hs +0/−53
• src/SSTG/Core/Syntax/Typing.hs +53/−0
• src/SSTG/Utils/FileIO.hs +1/−1

@@ -10,7 +10,7 @@ ## Dependencies * `ghc >= 8.0.1` -## Install+## Installation with Cabal `cabal install SSTG`  ## As an API@@ -27,7 +27,7 @@ This can be extracted from Haskell source by performing a call to the function:  ```-mkTargetBindings :: FilePath -> FilePath -> IO [SSTG.Binding]+mkTargetBindings :: FilePath -> FilePath -> IO [Binding] mkTargetBinding proj src = ... ``` @@ -45,15 +45,48 @@ proj = path/to/stuff src  = path/to/stuff/folder-one/source.hs ```-The extracted `[SSTG.Binding]`, like almost everything in SSTG, is endowed with `Show, Equal, Read`. However, it is advised to use the pretty-print functions defined in `SSTG.Utils.Printing`. For instance:+The extracted `[Binding]`, like almost everything in SSTG, is endowed with `Show, Equal, Read`. However, it is advised to use the pretty-print functions defined in `SSTG.Utils.Printing`. For instance: ```-pprBindingStr :: SSTG.Binding -> String+pprBindingStr :: Binding -> String ``` -#### Defunctionalizatoin+#### Defunctionalization+HEY KIDS YA EVER WANNA REASON ABOUT HIGHER-ORDER FUNCTIONS BUT YOUR SMT SOLVER AIN'T SMAHT ENOUGH??? CHECK OUT THIS [COOL WIKIPEDIA ARTICLE RIGHT HERE!!!][defunctionalization] +[defunctionalization]: https://en.wikipedia.org/wiki/Defunctionalization+ #### Symbolic Execution+Symbolic execution is done by performin a series of graph reductions on a `State` until we reach some value form, or our `step_count` tick runs out, creating a form of bounded execution exploration. +To load a `State`, two functions can be used:+```+data LoadResult = LoadOkay State | LoadGuess State [Binding] | LoadError String++newtype Program = Program [Binding]++loadState :: Program -> LoadResult++loadStateEntry :: String -> Program -> LoadResult+```+Next we have to fill out the flags for execution:+```+data StepType = BFS | BFSLogged | DFS | DFSLogged++data RunFlags = RunFlags { step_count :: Int+                         , step_type  :: StepType+                         , dump_dir   :: Maybe FilePath }+```+Here `step_count` is the number of steps we may take, the `step_type` is currently only implemented for `BFS` and `BFSLogged`, the latter of which keeps track of every step taken, while `BFS` only returns the very last state. Note that `BFSLogged` is currently unoptimized because it is easy to implement that way :)++Finally, to perform execution, the `execute` function is used:+```+execute :: RunFlags -> State -> [([LiveState], [DeadState])]+```+This yields a list of execution snapshots. The list is a singleton list if `BFS` or `DFS` is used, while multiple snapshots if the `BFSLogged` or `DFSLogged` is done. These can be then printed by using `pprLivesDeadsStr`:+```+pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String+```+ #### Constraint Solving To come. @@ -61,6 +94,6 @@ * Defunctionalization pre-processing * SMT integration -## Shortcommings+## Shortcomings * Uninterpreted function evaluations are abstracted as symbolic computations. This includes all functions defined in `Prelude` and those not defined in the scope of the target programs. * There might be bugs, who knows? :)

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.0.6+version:             0.1.0.7 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme@@ -21,13 +21,13 @@                      , SSTG.Core.Translation.Haskell                      , SSTG.Core.Syntax                      , SSTG.Core.Syntax.Language-                     , SSTG.Core.Syntax.Typecheck+                     , SSTG.Core.Syntax.Typing                      , SSTG.Core.Execution                      , SSTG.Core.Execution.Engine-                     , SSTG.Core.Execution.Models                      , SSTG.Core.Execution.Naming                      , SSTG.Core.Execution.Rules                      , SSTG.Core.Execution.Stepping+                     , SSTG.Core.Execution.Support                      , SSTG.Utils                      , SSTG.Utils.Printing                      , SSTG.Utils.FileIO

@@ -1,15 +1,15 @@ -- | Export Module for SSTG.Core.Execution module SSTG.Core.Execution     ( module SSTG.Core.Execution.Engine-    , module SSTG.Core.Execution.Models     , 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.Models import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping+import SSTG.Core.Execution.Support 

@@ -10,9 +10,9 @@     ) where  import SSTG.Core.Syntax-import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Stepping+import SSTG.Core.Execution.Support  import qualified Data.Map as M 

@@ -1,213 +0,0 @@--- | Symbolic STG Execution Models-module SSTG.Core.Execution.Models-    ( module SSTG.Core.Execution.Models-    ) where--import SSTG.Core.Syntax--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-                   , state_links   :: SymLinks-                   } 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 { 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-             | 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.-type PathCons = [PathCond]---- | Path conditions denote logical paths taken in program execution thus far.-data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool-              deriving (Show, Eq, Read)---- | Symbolic link tables helps keep track of what names went to what, what?-newtype SymLinks = SymLinks (M.Map Name Name) 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's unique `Int` key.-nameUnique :: Name -> Int-nameUnique (Name _ _ _ unq) = unq---- | Variable name.-varName :: Var -> Name-varName (Var name _) = name---- | `MemAddr`'s `Int` value.-memAddrInt :: MemAddr -> Int-memAddrInt (MemAddr int) = int---- | `Locals` lookup.-lookupLocals :: Var -> Locals -> Maybe Value-lookupLocals var (Locals lmap) = M.lookup (varName var) lmap---- | `Locals` insertion.-insertLocals :: Var -> Value -> Locals -> Locals-insertLocals var val (Locals lmap) = Locals lmap'-  where lmap' = M.insert (varName var) val lmap---- | List insertion into `Locals`.-insertLocalsList :: [(Var, Value)] -> Locals -> Locals-insertLocalsList []               locals = locals-insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'-  where locals' = insertLocals var val locals---- | `Heap` lookup.-lookupHeap :: MemAddr -> Heap -> Maybe HeapObj-lookupHeap addr (Heap hmap _) = M.lookup addr hmap---- | `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 ((memAddrInt 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 addr hobj (Heap hmap prev) = Heap hmap' prev-  where hmap' = M.insert addr hobj hmap---- | Insert a list of `HeapObj` at specified `MemAddr` locations.-insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap-insertHeapList []                 heap = heap-insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'-  where heap' = insertHeap addr hobj heap---- | `Globals` lookup.-lookupGlobals :: Var -> Globals -> Maybe Value-lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap---- | `Globals` insertion.-insertGlobals :: Var -> Value -> Globals -> Globals-insertGlobals var val (Globals gmap) = Globals gmap'-  where gmap' = M.insert (varName var) val 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 []               globals = globals-insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'-  where globals' = insertGlobals var val globals----   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-    mb_val  -> mb_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-    Just $ case hobj of-        Blackhole           -> Bottom-        LitObj lit          -> litType lit-        SymObj (Symbol s _) -> varType s-        ConObj dcon _       -> dataConType dcon-        FunObj prms expr _  -> foldr FunTy (exprType expr) (map varType prms)-

@@ -9,7 +9,7 @@     ) where  import SSTG.Core.Syntax-import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Support  import qualified Data.List as L import qualified Data.Map  as M@@ -49,8 +49,8 @@  -- | `Name`s in the `Heap`. heapNames :: Heap -> [Name]-heapNames (Heap heap _) = concatMap (heapObjNames . snd) kvs-  where kvs = M.toList heap+heapNames (Heap heap _) = concatMap (heapObjNames . snd) hlist+  where hlist = M.toList heap  -- | `Name`s in a `HeapObj`. heapObjNames :: HeapObj -> [Name]@@ -169,8 +169,8 @@  -- | `Name`s in a `SymLinks`. linksNames :: SymLinks -> [Name]-linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) kvs-  where kvs = M.toList links+linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) slist+  where slist = M.toList links  -- | 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

@@ -6,8 +6,8 @@     ) where  import SSTG.Core.Syntax-import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming+import SSTG.Core.Execution.Support  -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt

@@ -8,8 +8,8 @@     , runBoundedDFSLogged     ) where -import SSTG.Core.Execution.Models import SSTG.Core.Execution.Rules+import SSTG.Core.Execution.Support  -- | A `State` that is not in value form yet, capable of being evaluated. A -- list of `Rule`s is kept to denote reduction history.

@@ -0,0 +1,213 @@+-- | Symbolic STG Execution Support Architecture+module SSTG.Core.Execution.Support+    ( module SSTG.Core.Execution.Support+    ) where++import SSTG.Core.Syntax++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+                   , state_links   :: SymLinks+                   } 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 { 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+             | 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.+type PathCons = [PathCond]++-- | Path conditions denote logical paths taken in program execution thus far.+data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool+              deriving (Show, Eq, Read)++-- | Symbolic link tables helps keep track of what names went to what, what?+newtype SymLinks = SymLinks (M.Map Name Name) 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's unique `Int` key.+nameUnique :: Name -> Int+nameUnique (Name _ _ _ unq) = unq++-- | Variable name.+varName :: Var -> Name+varName (Var name _) = name++-- | `MemAddr`'s `Int` value.+memAddrInt :: MemAddr -> Int+memAddrInt (MemAddr int) = int++-- | `Locals` lookup.+lookupLocals :: Var -> Locals -> Maybe Value+lookupLocals var (Locals lmap) = M.lookup (varName var) lmap++-- | `Locals` insertion.+insertLocals :: Var -> Value -> Locals -> Locals+insertLocals var val (Locals lmap) = Locals lmap'+  where lmap' = M.insert (varName var) val lmap++-- | List insertion into `Locals`.+insertLocalsList :: [(Var, Value)] -> Locals -> Locals+insertLocalsList []               locals = locals+insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'+  where locals' = insertLocals var val locals++-- | `Heap` lookup.+lookupHeap :: MemAddr -> Heap -> Maybe HeapObj+lookupHeap addr (Heap hmap _) = M.lookup addr hmap++-- | `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 ((memAddrInt 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 addr hobj (Heap hmap prev) = Heap hmap' prev+  where hmap' = M.insert addr hobj hmap++-- | Insert a list of `HeapObj` at specified `MemAddr` locations.+insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap+insertHeapList []                 heap = heap+insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'+  where heap' = insertHeap addr hobj heap++-- | `Globals` lookup.+lookupGlobals :: Var -> Globals -> Maybe Value+lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap++-- | `Globals` insertion.+insertGlobals :: Var -> Value -> Globals -> Globals+insertGlobals var val (Globals gmap) = Globals gmap'+  where gmap' = M.insert (varName var) val 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 []               globals = globals+insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'+  where globals' = insertGlobals var val globals++--   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+    mb_val  -> mb_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+    Just $ case hobj of+        Blackhole           -> Bottom+        LitObj lit          -> litType lit+        SymObj (Symbol s _) -> varType s+        ConObj dcon _       -> dataConType dcon+        FunObj prms expr _  -> foldr FunTy (exprType expr) (map varType prms)+

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

@@ -22,7 +22,7 @@ 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 @bnd@ 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 [GenBinding bnd var]

@@ -1,53 +0,0 @@--- | Typing Module-module SSTG.Core.Syntax.Typecheck-    ( module SSTG.Core.Syntax.Typecheck-    ) where--import SSTG.Core.Syntax.Language---- | Variable type.-varType :: Var -> Type-varType (Var _ ty) = ty---- | 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 (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args)---- | Atom type.-atomType :: Atom -> Type-atomType (VarAtom var) = varType var-atomType (LitAtom lit) = litType lit---- | Primitive function type.-primFunType :: PrimFun -> Type-primFunType (PrimFun _ ty) = ty---- | Data constructor type denoted as a function.-dataConType :: DataCon -> Type-dataConType (DataCon _ ty tys) = foldr FunTy ty tys---- | Alt type-altType :: Alt -> Type-altType (Alt _ _ expr) = exprType expr---- | I wonder what this could possibly be?-exprType :: Expr -> Type-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-

@@ -0,0 +1,53 @@+-- | Typing Module+module SSTG.Core.Syntax.Typing+    ( module SSTG.Core.Syntax.Typing+    ) where++import SSTG.Core.Syntax.Language++-- | Variable type.+varType :: Var -> Type+varType (Var _ ty) = ty++-- | 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 (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args)++-- | Atom type.+atomType :: Atom -> Type+atomType (VarAtom var) = varType var+atomType (LitAtom lit) = litType lit++-- | Primitive function type.+primFunType :: PrimFun -> Type+primFunType (PrimFun _ ty) = ty++-- | Data constructor type denoted as a function.+dataConType :: DataCon -> Type+dataConType (DataCon _ ty tys) = foldr FunTy ty tys++-- | Alt type+altType :: Alt -> Type+altType (Alt _ _ expr) = exprType expr++-- | I wonder what this could possibly be?+exprType :: Expr -> Type+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+

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