module SSTG.Core.Language.Support
( SymbolicT(..)
, fmap
, pure
, (<*>)
, return
, (>>=)
, State(..)
, Symbol(..)
, Status(..)
, Stack
, Frame(..)
, MemAddr
, Value(..)
, Locals
, Heap
, HeapObj(..)
, Globals
, Code(..)
, PathCons
, Constraint(..)
, nameOccStr
, nameUnique
, varName
, null_addr
, addrInt
, init_status
, incStatusSteps
, updateStatusId
, empty_stack
, popStack
, pushStack
, stackToList
, empty_locals
, lookupLocals
, insertLocals
, insertLocalsList
, localsToList
, empty_heap
, lookupHeap
, allocHeap
, allocHeapList
, insertHeap
, insertHeapList
, heapToList
, empty_globals
, lookupGlobals
, insertGlobals
, insertGlobalsList
, globalsToList
, empty_pathcons
, insertPathCons
, insertPathConsList
, pathconsToList
, lookupValue
, vlookupHeap
, memAddrType
) where
import SSTG.Core.Language.Syntax
import SSTG.Core.Language.Typing
import qualified Data.Map as M
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_paths :: !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 Value = LitVal Lit
| MemVal MemAddr
deriving (Show, Eq, Read)
newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)
data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read)
data HeapObj = LitObj Lit
| SymObj Symbol
| ConObj DataCon [Value]
| FunObj [Var] Expr Locals
| AddrObj MemAddr
| Blackhole
deriving (Show, Eq, Read)
newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read)
data Code = Evaluate Expr Locals
| Return Value
deriving (Show, Eq, Read)
newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)
data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool
deriving (Show, Eq, Read)
nameOccStr :: Name -> String
nameOccStr (Name occ _ _ _) = occ
nameUnique :: Name -> Int
nameUnique (Name _ _ _ unq) = unq
varName :: Var -> Name
varName (Var name _) = name
null_addr :: MemAddr
null_addr = MemAddr 0
addrInt :: MemAddr -> Int
addrInt (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 new_id status = status { status_id = new_id
, status_parent = status_id status }
empty_stack :: Stack
empty_stack = Stack []
popStack :: Stack -> Maybe (Frame, Stack)
popStack (Stack []) = Nothing
popStack (Stack (frame:frames)) = Just (frame, Stack frames)
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 Value
lookupLocals var (Locals lmap) = M.lookup (varName var) lmap
insertLocals :: (Var, Value) -> Locals -> Locals
insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)
insertLocalsList :: [(Var, Value)] -> Locals -> Locals
insertLocalsList kvs locals = foldr insertLocals locals kvs
localsToList :: Locals -> [(Name, Value)]
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 (AddrObj redir) -> lookupHeap redir (Heap hmap prev)
mb_hobj -> mb_hobj
allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)
allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr)
where
addr = MemAddr ((addrInt prev) + 1)
hmap' = M.insert addr hobj hmap
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'
insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap
insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev
insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap
insertHeapList kvs heap = foldr insertHeap heap kvs
heapToList :: Heap -> [(MemAddr, HeapObj)]
heapToList (Heap hmap _) = M.toList hmap
empty_globals :: Globals
empty_globals = Globals M.empty
lookupGlobals :: Var -> Globals -> Maybe Value
lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap
insertGlobals :: (Var, Value) -> Globals -> Globals
insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)
insertGlobalsList :: [(Var, Value)] -> Globals -> Globals
insertGlobalsList kvs globals = foldr insertGlobals globals kvs
globalsToList :: Globals -> [(Name, Value)]
globalsToList (Globals gmap) = M.toList gmap
empty_pathcons :: PathCons
empty_pathcons = PathCons []
insertPathCons :: Constraint -> PathCons -> PathCons
insertPathCons cons (PathCons conss) = PathCons (cons : conss)
insertPathConsList :: [Constraint] -> PathCons -> PathCons
insertPathConsList conss pathcons = foldr insertPathCons pathcons conss
pathconsToList :: PathCons -> [Constraint]
pathconsToList (PathCons conss) = conss
lookupValue :: Var -> Locals -> Globals -> Maybe Value
lookupValue var locals globals = case lookupLocals var locals of
Nothing -> lookupGlobals var globals
Just val -> Just val
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)
memAddrType :: MemAddr -> Heap -> Maybe Type
memAddrType addr heap = do
hobj <- lookupHeap addr heap
case hobj of
AddrObj redir -> memAddrType redir heap
LitObj lit -> Just (litType lit)
SymObj (Symbol s _) -> Just (varType s)
ConObj dcon _ -> Just (dataconType dcon)
FunObj ps e _ -> Just (foldr FunTy (exprType e) (map varType ps))
Blackhole -> Just Bottom