-- 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 i d 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]
  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
  LC : what is this for ?
  type var I d - >    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

 Definitions used during refinement phase
 Object-Int pair
 dt-id     -> [ty-vars]
 itf-id    -> [ty-vars]
 handler Id -> # of arguments
 constructor Id -> # of arguments
 command Id -> # of arguments
 effect var Id                  effect vars of current context
 get rigid data types
 Helper functions 
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

type IPair = (Id,Int)
  data type i d is mapped to rigid data type ( RDT ) variables ( for polymorphic data types )
  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
  LC : what is this for ?
  type var I d - >    VType Raw      type 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 }

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 }


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