module SSTG.Core.Execution.Support
( SymbolicT(..)
, fmap
, pure
, (<*>)
, return
, (>>=)
, State(..)
, Symbol(..)
, Status(..)
, Stack
, Frame(..)
, MemAddr
, Val(..)
, Locals
, Heap
, HeapObj(..)
, Globals
, Code(..)
, PathCons
, Constraint(..)
, null_addr
, memAddrInt
, init_status
, incStatusSteps
, updateStatusId
, empty_stack
, popStack
, pushStack
, stackToList
, empty_locals
, lookupLocals
, insertLocalsVal
, insertLocalsVals
, localsToList
, empty_heap
, lookupHeap
, insertHeapObj
, insertHeapObjs
, insertHeapRedir
, allocHeapObj
, allocHeapObjs
, heapToList
, empty_globals
, lookupGlobals
, insertGlobalsVal
, insertGlobalsVals
, globalsToList
, empty_pathcons
, insertPathCons
, insertPathConss
, pathConsToList
, lookupVal
, vlookupHeap
, memAddrType
) where
import SSTG.Core.Language
import qualified Data.Map as M
newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) }
instance Functor (SymbolicT s) where
fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1))
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))
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))
data State = State { state_status :: !Status
, state_stack :: !Stack
, state_heap :: !Heap
, state_globals :: !Globals
, state_code :: !Code
, state_names :: ![Name]
, state_path :: !PathCons
} deriving (Show, Eq, Read)
data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)
data Status = Status { status_id :: !Int
, status_parent :: !Int
, status_steps :: !Int
} deriving (Show, Eq, Read)
newtype Stack = Stack [Frame] deriving (Show, Eq, Read)
data Frame = CaseFrame Var [Alt] Locals
| ApplyFrame [Atom] Locals
| UpdateFrame MemAddr
deriving (Show, Eq, Read)
newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord)
data Val = LitVal Lit
| MemVal MemAddr
deriving (Show, Eq, Read)
newtype Locals = Locals (M.Map Name Val) deriving (Show, Eq, Read)
data Heap = Heap (M.Map MemAddr (Either MemAddr HeapObj)) MemAddr
deriving (Show, Eq, Read)
data HeapObj = LitObj Lit
| SymObj Symbol
| ConObj DataCon [Val]
| FunObj [Var] Expr Locals
| Blackhole
deriving (Show, Eq, Read)
newtype Globals = Globals (M.Map Name Val) deriving (Show, Eq, Read)
data Code = Evaluate Expr Locals
| Return Val
deriving (Show, Eq, Read)
newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)
data Constraint = Constraint AltCon Expr Locals Bool deriving (Show, Eq, Read)
null_addr :: MemAddr
null_addr = MemAddr 0
memAddrInt :: MemAddr -> Int
memAddrInt (MemAddr int) = int
init_status :: Status
init_status = Status { status_id = 1
, status_parent = 0
, status_steps = 0 }
incStatusSteps :: Status -> Status
incStatusSteps status = status { status_steps = (status_steps status) + 1 }
updateStatusId :: Int -> Status -> Status
updateStatusId int status = status { status_id = int
, status_parent = status_id status }
empty_stack :: Stack
empty_stack = Stack []
popStack :: Stack -> Maybe (Frame, Stack)
popStack (Stack []) = Nothing
popStack (Stack (frame:fs)) = Just (frame, Stack fs)
pushStack :: Frame -> Stack -> Stack
pushStack frame (Stack frames) = Stack (frame : frames)
stackToList :: Stack -> [Frame]
stackToList (Stack frames) = frames
empty_locals :: Locals
empty_locals = Locals M.empty
lookupLocals :: Var -> Locals -> Maybe Val
lookupLocals var (Locals lmap) = M.lookup (varName var) lmap
insertLocalsVal :: (Var, Val) -> Locals -> Locals
insertLocalsVal (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)
insertLocalsVals :: [(Var, Val)] -> Locals -> Locals
insertLocalsVals kvs locals = foldr insertLocalsVal locals kvs
localsToList :: Locals -> [(Name, Val)]
localsToList (Locals lmap) = M.toList lmap
empty_heap :: Heap
empty_heap = Heap M.empty null_addr
lookupHeap :: MemAddr -> Heap -> Maybe HeapObj
lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of
Just (Left redir) -> lookupHeap redir (Heap hmap prev)
Just (Right hobj) -> Just hobj
Nothing -> Nothing
insertHeapObj :: (MemAddr, HeapObj) -> Heap -> Heap
insertHeapObj (k, v) (Heap hmap prev) = Heap (M.insert k (Right v) hmap) prev
insertHeapObjs :: [(MemAddr, HeapObj)] -> Heap -> Heap
insertHeapObjs kvs heap = foldr insertHeapObj heap kvs
insertHeapRedir :: (MemAddr, MemAddr) -> Heap -> Heap
insertHeapRedir (a, r) (Heap hmap prev) = Heap (M.insert a (Left r) hmap) prev
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)
allocHeapObjs :: [HeapObj] -> Heap -> (Heap, [MemAddr])
allocHeapObjs [] heap = (heap, [])
allocHeapObjs (hobj:hs) heap = (heapf, addr : as)
where
(heap', addr) = allocHeapObj hobj heap
(heapf, as) = allocHeapObjs hs heap'
heapToList :: Heap -> [(MemAddr, Either MemAddr HeapObj)]
heapToList (Heap hmap _) = M.toList hmap
empty_globals :: Globals
empty_globals = Globals M.empty
lookupGlobals :: Var -> Globals -> Maybe Val
lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap
insertGlobalsVal :: (Var, Val) -> Globals -> Globals
insertGlobalsVal (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)
insertGlobalsVals :: [(Var, Val)] -> Globals -> Globals
insertGlobalsVals kvs globals = foldr insertGlobalsVal globals kvs
globalsToList :: Globals -> [(Name, Val)]
globalsToList (Globals gmap) = M.toList gmap
empty_pathcons :: PathCons
empty_pathcons = PathCons []
insertPathCons :: Constraint -> PathCons -> PathCons
insertPathCons cons (PathCons conss) = PathCons (cons : conss)
insertPathConss :: [Constraint] -> PathCons -> PathCons
insertPathConss conss pathcons = foldr insertPathCons pathcons conss
pathConsToList :: PathCons -> [Constraint]
pathConsToList (PathCons conss) = conss
lookupVal :: Var -> Locals -> Globals -> Maybe Val
lookupVal var locals globals = case lookupLocals var locals of
Just val -> Just val
Nothing -> lookupGlobals var globals
vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)
vlookupHeap var locals globals heap = do
val <- lookupVal var locals globals
case val of
LitVal _ -> Nothing
MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)
memAddrType :: MemAddr -> Heap -> Maybe Type
memAddrType addr heap = do
hobj <- lookupHeap addr heap
case hobj of
LitObj lit -> Just (litType lit)
SymObj (Symbol svar _) -> Just (varType svar)
ConObj dcon _ -> Just (dataConType dcon)
FunObj ps ex _ -> Just (foldr FunTy (exprType ex) (map varType ps))
Blackhole -> Just Bottom