RefineSyntaxSubstitItfAliases.hs

-- Recursively substitute an interface alias occurrence by its definition
module RefineSyntaxSubstitItfAliases (substitItfAls) 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 BwdFwd
import Syntax
import RefineSyntaxCommon
import RefineSyntaxConcretiseEps
import Debug

-- Given an occurrence of interface instantiation x t_1 ... t_n:
-- 1) Implicit [£] are made explicit
-- 2) Determine whether it is an interface alias and if so, recursiv. substitute
substitItfAls :: (Id, [TyArg Raw]) -> Refine (ItfMap Raw)
substitItfAls = substitItfAls' [] where
  substitItfAls' :: [Id] -> (Id, [TyArg Raw]) -> Refine (ItfMap Raw)
  substitItfAls' visited (x, ts) = do
    itfAls <- getRItfAliases
    if x `notElem` visited then
      case M.lookup x itfAls of
        Nothing -> return $ ItfMap (M.singleton x (BEmp :< ts)) (Raw Generated) --TODO: LC: put meaningful annot here
        Just (ps, ItfMap m _) ->
--            1) interface x p_1 ... p_n     = [itf_i p_i1 ... p_ik, ...]
--         or 2) interface x p_1 ... p_n [£] = [itf_i p_i1 ... p_ik, ...]
--               and [£] has been explicitly added before
--                                if 2), set t_{n+1} := [£]
          do evset <- getEVSet
             ctx <- getTopLevelCtxt
             let ts' = if "£" `S.member` evset || isHdrCtxt ctx
                       then concretiseEpsArg ps ts (Raw Implicit)
                       else ts
             checkArgs x (length ps) (length ts') (Raw Generated) -- TODO: LC: Fix annotation
             let subst = zip ps ts'
             -- replace   x ts
             --      by   [x_1 ts_1', ..., x_n ts_n']
             --           where ts_i' has been acted upon by subst
             m' <- mapM (mapM (mapM (substitInTyArg subst))) m
             -- recursively replace itf als in   x_1, ..., x_n
             --                       yielding   [[x_11 x_11_ts, ...], ...]
             ms <- mapM (\(x', insts) -> (mapM (\inst -> substitItfAls' (x:visited) (x', inst)) insts)) (M.toList m')
             let ms' = map (foldl plusItfMap (emptyItfMap (Raw Generated))) ms
             let m'' = foldl plusItfMap (emptyItfMap (Raw Generated)) ms'
             return m''
    else throwError $ errorRefItfAlCycle x

type Subst = [((Id, Kind), TyArg Raw)]

substLookupVT :: Subst -> Id -> Maybe (VType Raw)
substLookupVT subst x = case find (\((x', k), y) -> x' == x && k == VT) subst of
  Just (_, VArg ty a) -> Just ty
  _                    -> Nothing

substLookupET :: Subst -> Id -> Maybe (Ab Raw)
substLookupET subst x = case find (\((x', k), y) -> x' == x && k == ET) subst of
  Just (_, EArg ab a) -> Just ab
  _                    -> Nothing

substitInTyArgs :: Subst -> (Id, [TyArg Raw]) -> Refine (Id, [TyArg Raw])
substitInTyArgs subst (x, ts) = do ts' <- mapM (substitInTyArg subst) ts
                                   return (x, ts')
-- Replace (x, VT/ET) by ty-arg
substitInTyArg :: Subst -> TyArg Raw -> Refine (TyArg Raw)
substitInTyArg subst (VArg ty a) = VArg <$> substitInVType subst ty <*> pure a
substitInTyArg subst (EArg ab a) = EArg <$> substitInAb subst ab <*> pure a

substitInVType :: Subst -> VType Raw -> Refine (VType Raw)
substitInVType subst (DTTy x ts a) = do
  dtm <- getRDTs
  tmap <- getTMap
  ctx <- getTopLevelCtxt
  case (not (M.member x dtm) && -- Check if id really is type variable
        null ts &&
        (isHdrCtxt ctx ||
         M.member x tmap), substLookupVT subst x) of -- if so, then substitute
    (True, Just y) -> return y     -- TODO: LC: Right annotation assigned?
    _              -> do ts' <- mapM (substitInTyArg subst) ts
                         return $ DTTy x ts' a
substitInVType subst (SCTy ty a) = do cty <- substitInCType subst ty
                                      return $ SCTy cty a
substitInVType subst (TVar x a) =
  case substLookupVT subst x of
    Just y -> return y   -- TODO: LC: Right annotation assigned?
    _      -> return $ TVar x a
substitInVType subst ty = return ty  -- MkStringTy, MkIntTy, MkCharTy

substitInCType :: Subst -> CType Raw -> Refine (CType Raw)
substitInCType subst (CType ports peg a) = do ports' <- mapM (substitInPort subst) ports
                                              peg' <- substitInPeg subst peg
                                              return $ CType ports' peg' a

substitInPort :: Subst -> Port Raw -> Refine (Port Raw)
substitInPort subst (Port adjs ty a) = do adjs' <- mapM (substitInAdj subst) adjs
                                          ty' <- substitInVType subst ty
                                          return $ Port adjs' ty' a

substitInPeg :: Subst -> Peg Raw -> Refine (Peg Raw)
substitInPeg subst (Peg ab ty a) = do ab' <- substitInAb subst ab
                                      ty' <- substitInVType subst ty
                                      return $ Peg ab' ty' a

substitInAb :: Subst -> Ab Raw -> Refine (Ab Raw)
substitInAb subst = return

substitInAdj :: Subst -> Adjustment Raw -> Refine (Adjustment Raw)
substitInAdj subst (ConsAdj x ts a) = do
  ts' <- mapM (substitInTyArg subst) ts
  return $ ConsAdj x ts' a

substitInItfMap :: Subst -> ItfMap Raw -> Refine (ItfMap Raw)
substitInItfMap subst (ItfMap m a) = ItfMap <$> mapM (mapM (mapM (substitInTyArg subst))) m <*> pure a