-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}

module Cryptol.ModuleSystem.Env where

#ifndef RELOCATABLE
import Paths_cryptol (getDataDir)
#endif

import Cryptol.Eval (EvalEnv)
import Cryptol.ModuleSystem.Interface
import qualified Cryptol.ModuleSystem.NamingEnv as R
import Cryptol.Parser.AST
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.TypeCheck.AST as T

import Control.Monad (guard)
import Data.Foldable (fold)
import Data.Function (on)
import qualified Data.Map as Map
import Data.Monoid ((<>))
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
import System.Environment(getExecutablePath)
import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
import qualified Data.List as List

#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..))
#endif

-- Module Environment ----------------------------------------------------------

data ModuleEnv = ModuleEnv
  { meLoadedModules :: LoadedModules
  , meNameSeeds     :: T.NameSeeds
  , meEvalEnv       :: EvalEnv
  , meFocusedModule :: Maybe ModName
  , meSearchPath    :: [FilePath]
  , meDynEnv        :: DynamicEnv
  , meMonoBinds     :: !Bool
  }

resetModuleEnv :: ModuleEnv -> ModuleEnv
resetModuleEnv env = env
  { meLoadedModules = mempty
  , meNameSeeds     = T.nameSeeds
  , meEvalEnv       = mempty
  , meFocusedModule = Nothing
  , meDynEnv        = mempty
  }

initialModuleEnv :: IO ModuleEnv
initialModuleEnv  = do
  curDir <- getCurrentDirectory
#ifndef RELOCATABLE
  dataDir <- getDataDir
#endif
  binDir <- takeDirectory `fmap` getExecutablePath
  let instDir = normalise . joinPath . init . splitPath $ binDir
  userDir <- getAppUserDataDirectory "cryptol"
  return ModuleEnv
    { meLoadedModules = mempty
    , meNameSeeds     = T.nameSeeds
    , meEvalEnv       = mempty
    , meFocusedModule = Nothing
      -- we search these in order, taking the first match
    , meSearchPath    = [ curDir
                          -- something like $HOME/.cryptol
                        , userDir
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
                          -- ../cryptol on win32
                        , instDir </> "cryptol"
#else
                          -- ../share/cryptol on others
                        , instDir </> "share" </> "cryptol"
#endif

#ifndef RELOCATABLE
                          -- Cabal-defined data directory. Since this
                          -- is usually a global location like
                          -- /usr/local, search this one last in case
                          -- someone has multiple Cryptols
                        , dataDir
#endif
                        ]
    , meDynEnv        = mempty
    , meMonoBinds     = True
    }

-- | Try to focus a loaded module in the module environment.
focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
focusModule n me = do
  guard (isLoaded n (meLoadedModules me))
  return me { meFocusedModule = Just n }

-- | Get a list of all the loaded modules. Each module in the
-- resulting list depends only on other modules that precede it.
loadedModules :: ModuleEnv -> [T.Module]
loadedModules = map lmModule . getLoadedModules . meLoadedModules

-- | Produce an ifaceDecls that represents the focused environment of the module
-- system.
--
-- This could really do with some better error handling, just returning mempty
-- when one of the imports fails isn't really desirable.
focusedEnv :: ModuleEnv -> IfaceDecls
focusedEnv me = fold $ do
  (iface,imports) <- loadModuleEnv interpImport me
  let local = unqualified (ifPublic iface `mappend` ifPrivate iface)
  return (local `shadowing` imports)

-- | Produce an ifaceDecls that represents the internal environment of the
-- module, used for typechecking.
qualifiedEnv :: ModuleEnv -> IfaceDecls
qualifiedEnv me = fold $ do
  (iface,imports) <- loadModuleEnv (\ _ iface -> iface) me
  return (mconcat [ ifPublic iface, ifPrivate iface, imports ])

loadModuleEnv :: (Import -> Iface -> Iface) -> ModuleEnv
              -> Maybe (Iface,IfaceDecls)
loadModuleEnv processIface me = do
  fm      <- meFocusedModule me
  lm      <- lookupModule fm me
  imports <- mapM loadImport (T.mImports (lmModule lm))
  return (lmInterface lm, mconcat imports)
  where
  loadImport i = do
    lm <- lookupModule (iModule i) me
    return (ifPublic (processIface i (lmInterface lm)))


-- Loaded Modules --------------------------------------------------------------

newtype LoadedModules = LoadedModules
  { getLoadedModules :: [LoadedModule]
  } deriving (Show)
-- ^ Invariant: All the dependencies of any module `m` must precede `m` in the list.

instance Monoid LoadedModules where
  mempty        = LoadedModules []
  mappend l r   = LoadedModules
                $ List.unionBy ((==) `on` lmName) (getLoadedModules l) (getLoadedModules r)

data LoadedModule = LoadedModule
  { lmName      :: ModName
  , lmFilePath  :: FilePath
  , lmInterface :: Iface
  , lmModule    :: T.Module
  } deriving (Show)

isLoaded :: ModName -> LoadedModules -> Bool
isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)

lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule mn env = List.find ((mn ==) . lmName) (getLoadedModules (meLoadedModules env))

addLoadedModule :: FilePath -> T.Module -> LoadedModules -> LoadedModules
addLoadedModule path tm lm
  | isLoaded (T.mName tm) lm = lm
  | otherwise                = LoadedModules (getLoadedModules lm ++ [loaded])
  where
  loaded = LoadedModule
    { lmName      = T.mName tm
    , lmFilePath  = path
    , lmInterface = genIface tm
    , lmModule    = tm
    }

removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
removeLoadedModule path (LoadedModules ms) = LoadedModules (remove ms)
  where

  remove (lm:rest)
    | lmFilePath lm == path = rest
    | otherwise             = lm : remove rest

  remove [] = []

-- Dynamic Environments --------------------------------------------------------

-- | Extra information we need to carry around to dynamically extend
-- an environment outside the context of a single module. Particularly
-- useful when dealing with interactive declarations as in @:let@ or
-- @it@.

data DynamicEnv = DEnv
  { deNames :: R.NamingEnv
  , deDecls :: [T.DeclGroup]
  , deEnv   :: EvalEnv
  }

instance Monoid DynamicEnv where
  mempty = DEnv
    { deNames = mempty
    , deDecls = mempty
    , deEnv   = mempty
    }
  mappend de1 de2 = DEnv
    { deNames = deNames de1 <> deNames de2
    , deDecls = deDecls de1 <> deDecls de2
    , deEnv   = deEnv   de1 <> deEnv   de2
    }

-- | Build 'IfaceDecls' that correspond to all of the bindings in the
-- dynamic environment.
--
-- XXX: if we ever add type synonyms or newtypes at the REPL, revisit
-- this.
deIfaceDecls :: DynamicEnv -> IfaceDecls
deIfaceDecls DEnv { deDecls = dgs } =
  mconcat [ IfaceDecls
            { ifTySyns   = Map.empty
            , ifNewtypes = Map.empty
            , ifDecls    = Map.singleton (ifDeclName ifd) [ifd]
            }
          | decl <- concatMap T.groupDecls dgs
          , let ifd = mkIfaceDecl decl
          ]