module SSTG.Core.Execution.Models
( module SSTG.Core.Execution.Models
) where
import SSTG.Core.Syntax
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
, state_links :: SymLinks
} deriving (Show, Eq, Read)
data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)
data Status = 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
| 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)
type PathCons = [PathCond]
data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool
deriving (Show, Eq, Read)
newtype SymLinks = SymLinks (M.Map Name Name) 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
memAddrInt :: MemAddr -> Int
memAddrInt (MemAddr int) = int
lookupLocals :: Var -> Locals -> Maybe Value
lookupLocals var (Locals lmap) = M.lookup (varName var) lmap
insertLocals :: Var -> Value -> Locals -> Locals
insertLocals var val (Locals lmap) = Locals lmap'
where lmap' = M.insert (varName var) val lmap
insertLocalsList :: [(Var, Value)] -> Locals -> Locals
insertLocalsList [] locals = locals
insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'
where locals' = insertLocals var val locals
lookupHeap :: MemAddr -> Heap -> Maybe HeapObj
lookupHeap addr (Heap hmap _) = M.lookup addr hmap
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
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 addr hobj (Heap hmap prev) = Heap hmap' prev
where hmap' = M.insert addr hobj hmap
insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap
insertHeapList [] heap = heap
insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'
where heap' = insertHeap addr hobj heap
lookupGlobals :: Var -> Globals -> Maybe Value
lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap
insertGlobals :: Var -> Value -> Globals -> Globals
insertGlobals var val (Globals gmap) = Globals gmap'
where gmap' = M.insert (varName var) val gmap
insertGlobalsList :: [(Var, Value)] -> Globals -> Globals
insertGlobalsList [] globals = globals
insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'
where globals' = insertGlobals var val globals
lookupValue :: Var -> Locals -> Globals -> Maybe Value
lookupValue var locals globals = case lookupLocals var locals of
Nothing -> lookupGlobals var globals
mb_val -> mb_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
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)