    {-# LANGUAGE CPP #-}

    {-| The scope monad with operations.
    -}

    module Agda.Syntax.Scope.Monad where

    import Prelude hiding (mapM)
    import Control.Applicative
    import Control.Monad hiding (mapM)
    import Control.Monad.Writer hiding (mapM)
    import Data.Map (Map)
    import Data.Traversable
    import Data.List
    import qualified Data.Map as Map

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Fixity
    import Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Concrete as C
    import Agda.Syntax.Scope.Base

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Options

    import Agda.Utils.Tuple
    import Agda.Utils.Fresh
    import Agda.Utils.Size
    import Agda.Utils.List

    #include "../../undefined.h"
    import Agda.Utils.Impossible

    -- * The scope checking monad

    -- | To simplify interaction between scope checking and type checking (in
    --   particular when chasing imports), we use the same monad.
    type ScopeM = TCM

    -- * Errors

    notInScope :: C.QName -> ScopeM a
    notInScope x = typeError $ NotInScope [x]

    -- * General operations

    getCurrentModule :: ScopeM A.ModuleName
    getCurrentModule = setRange noRange . scopeCurrent <$> getScope

    setCurrentModule :: A.ModuleName -> ScopeM ()
    setCurrentModule m = modifyScopeInfo $ \s -> s { scopeCurrent = m }

    withCurrentModule :: A.ModuleName -> ScopeM a -> ScopeM a
    withCurrentModule new action = do
      old <- getCurrentModule
      setCurrentModule new
      x   <- action
      setCurrentModule old
      return x

    getNamedScope :: A.ModuleName -> ScopeM Scope
    getNamedScope m = do
      scope <- getScope
      case Map.lookup m (scopeModules scope) of
        Just s  -> return s
        Nothing -> do
          reportSLn "" 0 $ "ERROR: In scope\n" ++ show scope ++ "\nNO SUCH SCOPE " ++ show m
          __IMPOSSIBLE__

    getCurrentScope :: ScopeM Scope
    getCurrentScope = getNamedScope =<< getCurrentModule

    -- | Create a new module with an empty scope
    createModule :: A.ModuleName -> ScopeM ()
    createModule m = do
      s <- getCurrentScope
      let parents = scopeName s : scopeParents s
      modifyScopes $ Map.insert m emptyScope { scopeName = m, scopeParents = parents }

    -- | Apply a function to the scope info.
    modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()
    modifyScopeInfo f = do
      scope <- getScope
      setScope $ f scope

    -- | Apply a function to the scope map.
    modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
    modifyScopes f = modifyScopeInfo $ \s -> s { scopeModules = f $ scopeModules s }

    -- | Apply a function to the given scope.
    modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
    modifyNamedScope m f = modifyScopes $ Map.mapWithKey f'
      where
        f' m' s | m' == m   = f s
                | otherwise = s

    -- | Apply a function to the current scope.
    modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope f = do
      m <- getCurrentModule
      modifyNamedScope m f

    -- | Apply a monadic function to the top scope.
    modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()
    modifyNamedScopeM m f = do
      s  <- getNamedScope m
      s' <- f s
      modifyNamedScope m (const s')

    modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()
    modifyCurrentScopeM f = do
      m <- getCurrentModule
      modifyNamedScopeM m f

    -- | Apply a function to the public or private name space.
    modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
    modifyCurrentNameSpace acc f = modifyCurrentScope action
      where
        action s = s { scopePublic   = pub $ scopePublic  s
                     , scopePrivate  = pri $ scopePrivate s
                     , scopeImported = imp $ scopeImported s
                     }
        (pub, pri, imp) = case acc of
          PublicNS   -> (f, id, id)
          PrivateNS  -> (id, f, id)
          ImportedNS -> (id, id, f)

    -- | Set context precedence
    setContextPrecedence :: Precedence -> ScopeM ()
    setContextPrecedence p = modifyScopeInfo $ \s -> s { scopePrecedence = p }

    getContextPrecedence :: ScopeM Precedence
    getContextPrecedence = scopePrecedence <$> getScope

    withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a
    withContextPrecedence p m = do
      p' <- getContextPrecedence
      setContextPrecedence p
      x <- m
      setContextPrecedence p'
      return x

    getLocalVars :: ScopeM LocalVars
    getLocalVars = scopeLocals <$> getScope

    setLocalVars :: LocalVars -> ScopeM ()
    setLocalVars vars = modifyScope $ \s -> s { scopeLocals = vars }

    -- | Run a computation without changing the local variables.
    withLocalVars :: ScopeM a -> ScopeM a
    withLocalVars m = do
      vars <- getLocalVars
      x    <- m
      setLocalVars vars
      return x

    -- * Names

    -- | Create a fresh abstract name from a concrete name.
    freshAbstractName :: Fixity -> C.Name -> ScopeM A.Name
    freshAbstractName fx x = do
      i <- fresh
      return $ A.Name i x (getRange x) fx

    -- | @freshAbstractName_ = freshAbstractName defaultFixity@
    freshAbstractName_ :: C.Name -> ScopeM A.Name
    freshAbstractName_ = freshAbstractName defaultFixity

    -- | Create a fresh abstract qualified name.
    freshAbstractQName :: Fixity -> C.Name -> ScopeM A.QName
    freshAbstractQName fx x = do
      y <- freshAbstractName fx x
      m <- getCurrentModule
      return $ A.qualify m y

    -- * Resolving names

    data ResolvedName = VarName A.Name
                      | DefinedName AbstractName
                      | ConstructorName [AbstractName]
                      | UnknownName
      deriving (Show)

    -- | Look up the abstract name referred to by a given concrete name.
    resolveName :: C.QName -> ScopeM ResolvedName
    resolveName x = do
      scope <- getScope
      let vars = map (C.QName -*- id) $ scopeLocals scope
      case lookup x vars of
        Just y  -> return $ VarName $ y { nameConcrete = unqualify x }
        Nothing -> case scopeLookup x scope of
          [] -> return UnknownName
          ds | all ((==ConName) . anameKind) ds ->
            return $ ConstructorName
                   $ map (\d -> updateConcreteName d $ unqualify x) ds
          [d] -> return $ DefinedName $ updateConcreteName d (unqualify x)
          ds  -> typeError $ AmbiguousName x (map anameName ds)
      where
      updateConcreteName :: AbstractName -> C.Name -> AbstractName
      updateConcreteName d@(AbsName { anameName = an@(A.QName { qnameName = qn }) }) x =
        d { anameName = an { qnameName = qn { nameConcrete = x } } }

    -- | Look up a module in the scope.
    resolveModule :: C.QName -> ScopeM AbstractModule
    resolveModule x = do
      ms <- scopeLookup x <$> getScope
      case ms of
        [AbsModule m] -> return $ AbsModule (m `withRangesOfQ` x)
        []            -> typeError $ NoSuchModule x
        ms            -> typeError $ AmbiguousModule x (map amodName ms)

    -- | Get the fixity of a name. The name is assumed to be in scope.
    getFixity :: C.QName -> ScopeM Fixity
    getFixity x = do
      r <- resolveName x
      case r of
        VarName y          -> return $ nameFixity y
        DefinedName d      -> return $ nameFixity $ qnameName $ anameName d
        ConstructorName ds
          | null fs        -> __IMPOSSIBLE__
          | allEqual fs    -> return $ head fs
          | otherwise      -> return defaultFixity
          where
            fs = map (nameFixity . qnameName . anameName) ds
        UnknownName        -> __IMPOSSIBLE__

    -- * Binding names

    -- | Bind a variable. The abstract name is supplied as the second argument.
    bindVariable :: C.Name -> A.Name -> ScopeM ()
    bindVariable x y = do
      scope <- getScope
      setScope scope { scopeLocals = (x, y) : scopeLocals scope }

    -- | Bind a defined name. Must not shadow anything.
    bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
    bindName acc kind x y = do
      r  <- resolveName (C.QName x)
      ys <- case r of
        DefinedName d      -> typeError $ ClashingDefinition (C.QName x) $ anameName d
        VarName z          -> typeError $ ClashingDefinition (C.QName x) $ A.qualify (mnameFromList []) z
        ConstructorName [] -> __IMPOSSIBLE__
        ConstructorName ds
          | kind == ConName && all ((==ConName) . anameKind) ds -> return [ AbsName y kind ]
          | otherwise -> typeError $ ClashingDefinition (C.QName x) $ anameName (head ds) -- TODO: head
        UnknownName        -> return [AbsName y kind]
      modifyCurrentScope $ addNamesToScope (localNameSpace acc) x ys

    -- | Bind a module name.
    bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
    bindModule acc x m = modifyCurrentScope $
      addModuleToScope (localNameSpace acc) x (AbsModule m)

    -- | Bind a qualified module name. Adds it to the imports field of the scope.
    bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
    bindQModule acc q m = modifyCurrentScope $ \s ->
      s { scopeImports = Map.insert q m (scopeImports s) }

    -- * Module manipulation operations

    -- | Clear the scope of any no names.
    stripNoNames :: ScopeM ()
    stripNoNames = modifyScopes $ Map.map strip
      where
        strip     = mapScope (\_ -> stripN) (\_ -> stripN)
        stripN m  = Map.filterWithKey (const . notNoName) m
        notNoName = not . isNoName

    -- | @renamedCanonicalNames old new s@ returns a renaming replacing all
    --   (abstract) names @old.m.x@ with @new.m.x@. Any other names are left
    --   untouched.
    renamedCanonicalNames :: ModuleName -> ModuleName -> Scope ->
                           ScopeM (Map A.QName A.QName, Map A.ModuleName A.ModuleName)
    renamedCanonicalNames old new s = (,) <$> renamedNames names <*> renamedMods mods
      where
        ns    = allThingsInScope s
        names = nsNames ns
        mods  = nsModules ns

        renamedNames ds = Map.fromList <$> zip xs <$> mapM renName xs
          where
            xs = filter (`isInModule` old) $ map anameName $ concat $ Map.elems ds

        renamedMods ms = Map.fromList <$> zip xs <$> mapM renMod xs
          where
            xs = filter (`isSubModuleOf` old) $ map amodName $ concat $ Map.elems ms

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renName :: A.QName -> ScopeM A.QName
        renName y = do
          i <- fresh
          return . qualifyQ new . dequalify
                 $ y { qnameName = (qnameName y) { nameId = i } }
          where
            dequalify = A.qnameFromList . drop (size old) . A.qnameToList

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renMod :: A.ModuleName -> ScopeM A.ModuleName
        renMod = return . qualifyM new . dequalify
          where
            dequalify = A.mnameFromList . drop (size old) . A.mnameToList

    type Ren a = Map a a
    type Out = [Either (Ren A.ModuleName) (Ren A.QName)]
    type WSM = WriterT Out ScopeM

    -- | Create a new scope with the given name from an old scope. Renames
    --   public names in the old scope to match the new name and returns the
    --   renamings.
    copyScope :: A.ModuleName -> Scope -> ScopeM (Scope, Ren A.ModuleName, Ren A.QName)
    copyScope new s = do
      s0 <- getNamedScope new
      (s', rho) <- runWriterT $ mapScopeM copyD copyM s
      let s'' = s' { scopeName    = scopeName s0
                   , scopeParents = scopeParents s0
                   }
      return (s'', modRenaming rho, defRenaming rho)
      where
        new' = killRange new
        old  = scopeName s
        modRenaming rho = Map.unions [ m | Left m  <- rho ]
        defRenaming rho = Map.unions [ m | Right m <- rho ]

        copyM :: NameSpaceId -> ModulesInScope -> WSM ModulesInScope
        copyM ImportedNS ms = return ms
        copyM PrivateNS  _  = return Map.empty
        copyM PublicNS   ms = traverse (mapM $ onMod renMod) ms

        copyD :: NameSpaceId -> NamesInScope -> WSM NamesInScope
        copyD ImportedNS ds = return ds
        copyD PrivateNS  _  = return Map.empty
        copyD PublicNS   ds = traverse (mapM $ onName renName) ds

        onMod f m = do
          x <- f $ amodName m
          return m { amodName = x }

        onName f d = do
          x <- f $ anameName d
          return d { anameName = x }

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renName :: A.QName -> WSM A.QName
        renName x = do
          i <- lift fresh
          let y = qualifyQ new' . dequalify
                $ x { qnameName = (qnameName x) { nameId = i } }
          tell [Right $ Map.singleton x y]
          return y
          where
            dequalify = A.qnameFromList . drop (size old) . A.qnameToList

        -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
        renMod :: A.ModuleName -> WSM A.ModuleName
        renMod x = do

          -- Create the name of the new module
          let y = qualifyM new' $ dequalify x
          tell [Left $ Map.singleton x y]

          -- We need to copy the contents of included modules recursively
          (s, renM, renD) <- lift $ do
            createModule y
            s0 <- getNamedScope x
            withCurrentModule y $ copyScope y s0
          lift $ modifyNamedScope y (const s)
          tell [Left renM, Right renD]
          return y
          where
            dequalify = A.mnameFromList . drop (size old) . A.mnameToList

    -- | Apply an importdirective and check that all the names mentioned actually
    --   exist.
    applyImportDirectiveM :: C.QName -> ImportDirective -> Scope -> ScopeM Scope
    applyImportDirectiveM m dir scope = do
      xs <- filterM doesntExist names
      reportSLn "scope.import.apply" 20 $ "non existing names: " ++ show xs
      case xs of
        []  -> return $ applyImportDirective dir scope
        _   -> typeError $ ModuleDoesntExport m xs
      where
        names :: [ImportedName]
        names = map renFrom (renaming dir) ++ case usingOrHiding dir of
          Using  xs -> xs
          Hiding xs -> xs

        doesntExist (ImportedName x) =
          case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractName) of
            Just _  -> return False
            Nothing -> return True
        doesntExist (ImportedModule x) =
          case Map.lookup x (allNamesInScope scope :: ThingsInScope AbstractModule) of
            Just _  -> return False
            Nothing -> return True

    -- | Open a module.
    openModule_ :: C.QName -> ImportDirective -> ScopeM ()
    openModule_ cm dir = do
      current <- getCurrentModule
      m <- amodName <$> resolveModule cm
      let ns = namespace current m
      s <- setScopeAccess ns <$>
            (applyImportDirectiveM cm dir . restrictPrivate =<< getNamedScope m)
      checkForClashes (scopeNameSpace ns s)
      modifyCurrentScope (`mergeScope` s)
      where
        namespace m0 m1
          | not (publicOpen dir)  = PrivateNS
          | m1 `isSubModuleOf` m0 = PublicNS
          | otherwise             = ImportedNS

        -- Only checks for clashes that would lead to the same
        -- name being exported twice from the module.
        checkForClashes new
          | not (publicOpen dir) = return ()
          | otherwise = do

            old <- allThingsInScope . restrictPrivate <$> (getNamedScope =<< getCurrentModule)

            let defClashes = Map.toList $ Map.intersectionWith (,) (nsNames new) (nsNames old)
                modClashes = Map.toList $ Map.intersectionWith (,) (nsModules new) (nsModules old)

                realClash (_, ([x],[y])) = x /= y
                realClash _              = True

                defClash (_, (qs0, qs1)) =
                  any ((/= ConName) . anameKind) (qs0 ++ qs1)

                (f & g) x = f x && g x

            case filter (realClash & defClash) defClashes of
              (x, (_, q:_)):_ -> typeError $ ClashingDefinition (C.QName x) (anameName q)
              _               -> return ()
            case filter realClash modClashes of
              (_, (m0:_, m1:_)):_ -> typeError $ ClashingModule (amodName m0) (amodName m1)
              _                   -> return ()