RefineSyntaxCommon.hs

-- Definitions used during refinement phase
module RefineSyntaxCommon where

import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Data.Functor.Identity

import Data.List
import qualified Data.Map.Strict as M
import qualified Data.Set as S

import Syntax

type Refine = ExceptT String (State RState)

type TVarMap = M.Map Id (VType Raw)
type EVarSet = S.Set Id

-- Object-Int pair
type IPair = (Id,Int)
-- data type id is mapped to rigid data type (RDT) variables (for polymorphic data types)
type DTMap = M.Map Id [(Id, Kind)]                      -- dt-id     -> [ty-vars]
type IFMap = M.Map Id [(Id, Kind)]                      -- itf-id    -> [ty-vars]
type IFAliasesMap = M.Map Id ([(Id, Kind)], ItfMap Raw) -- itf-al-id -> ([ty-vars], itf's -> itf-instant's)

data TopLevelCtxt = Interface | InterfaceAlias | Datatype | Handler
  deriving (Show, Eq)

data RState = MkRState { interfaces :: IFMap
                       , interfaceAliases :: IFAliasesMap
                       , datatypes :: DTMap
                       , handlers :: [IPair]              -- handler Id -> # of arguments
                       , ctrs :: [IPair]                  -- constructor Id -> # of arguments
                       , cmds :: [IPair]                  -- command Id -> # of arguments
                       , program :: Prog Refined          -- LC: what is this for?
                       , tmap :: TVarMap                  -- type var Id ->   VType Raw     type vars of current context
                       , evmap :: EVarSet                 -- effect var Id                  effect vars of current context
                       , tlctxt :: Maybe TopLevelCtxt }

getRState :: Refine RState
getRState = get

putRState :: RState -> Refine ()
putRState = put

putRItfs :: IFMap -> Refine ()
putRItfs xs = do s <- getRState
                 putRState $ s { interfaces = xs }

getRItfs :: Refine IFMap
getRItfs = do s <- getRState
              return $ interfaces s

putRItfAliases :: IFAliasesMap -> Refine ()
putRItfAliases xs = do s <- getRState
                       putRState $ s {interfaceAliases = xs }

getRItfAliases :: Refine (IFAliasesMap)
getRItfAliases = do s <- getRState
                    return $ interfaceAliases s

putRDTs :: DTMap -> Refine ()
putRDTs m = do s <- getRState
               putRState $ s { datatypes = m }

-- get rigid data types
getRDTs :: Refine DTMap
getRDTs = do s <- getRState
             return $ datatypes s

putRCtrs :: [IPair] -> Refine ()
putRCtrs xs = do s <- getRState
                 putRState $ s { ctrs = xs }

getRCtrs :: Refine [IPair]
getRCtrs = do s <- getRState
              return $ ctrs s

putRCmds :: [IPair] -> Refine ()
putRCmds xs = do s <- getRState
                 putRState $ s { cmds = xs }

getRCmds :: Refine [IPair]
getRCmds = do s <- getRState
              return $ cmds s

putRMHs :: [IPair] -> Refine ()
putRMHs xs = do s <- getRState
                putRState $ s { handlers = xs }

getRMHs :: Refine [IPair]
getRMHs = do s <- getRState
             return $ handlers s

putTMap :: TVarMap -> Refine ()
putTMap m = do s <- getRState
               putRState $ s { tmap = m }

getTMap :: Refine TVarMap
getTMap = do s <- getRState
             return $ tmap s

putEVSet :: EVarSet -> Refine ()
putEVSet m = do s <- getRState
                putRState $ s { evmap = m }

getEVSet :: Refine EVarSet
getEVSet = do s <- getRState
              return $ evmap s

getTopLevelCtxt :: Refine (Maybe TopLevelCtxt)
getTopLevelCtxt = do s <- getRState
                     return $ tlctxt s

putTopLevelCtxt :: TopLevelCtxt -> Refine ()
putTopLevelCtxt ctxt = do s <- getRState
                          putRState $ s { tlctxt = Just ctxt }

{- Helper functions -}

isHdrCtxt :: Maybe TopLevelCtxt -> Bool
isHdrCtxt (Just Handler) = True
isHdrCtxt _              = False