-- |
-- Module      :  Cryptol.ModuleSystem.Env
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.Env where

#ifndef RELOCATABLE
import Paths_cryptol (getDataDir)
#endif

import Cryptol.Eval (EvalEnv)
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)
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 Cryptol.Utils.PP (PP(..),text,parens,NameDisp)

import Data.ByteString(ByteString)
import Control.Monad (guard,mplus)
import qualified Control.Exception as X
import Data.Function (on)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Semigroup
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
import System.Environment(getExecutablePath)
import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
import qualified Data.List as List

import GHC.Generics (Generic)
import Control.DeepSeq

import Prelude ()
import Prelude.Compat

import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP(pp)

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

-- | This is the current state of the interpreter.
data ModuleEnv = ModuleEnv
  { meLoadedModules :: LoadedModules
    -- ^ Information about all loaded modules.  See 'LoadedModule'.
    -- Contains information such as the file where the module was loaded
    -- from, as well as the module's interface, used for type checking.

  , meNameSeeds     :: T.NameSeeds
    -- ^ A source of new names for the type checker.

  , meSolverConfig  :: T.SolverConfig
    -- ^ Configuration settings for the SMT solver used for type-checking.

  , meEvalEnv       :: EvalEnv
    -- ^ The evaluation environment.  Contains the values for all loaded
    -- modules, both public and private.

  , meCoreLint      :: CoreLint
    -- ^ Should we run the linter to ensure sanity.

  , meMonoBinds     :: !Bool
    -- ^ Are we assuming that local bindings are monomorphic.
    -- XXX: We should probably remove this flag, and set it to 'True'.



  , meFocusedModule :: Maybe ModName
    -- ^ The "current" module.  Used to decide how to print names, for example.

  , meSearchPath    :: [FilePath]
    -- ^ Where we look for things.

  , meDynEnv        :: DynamicEnv
    -- ^ This contains additional definitions that were made at the command
    -- line, and so they don't reside in any module.

  , meSupply        :: !Supply
    -- ^ Name source for the renamer

  } deriving Generic

instance NFData ModuleEnv where
  rnf x = meLoadedModules x `seq` meEvalEnv x `seq` meDynEnv x `seq` ()

-- | Should we run the linter?
data CoreLint = NoCoreLint        -- ^ Don't run core lint
              | CoreLint          -- ^ Run core lint
  deriving (Generic, NFData)

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
  -- looking up this directory can fail if no HOME is set, as in some
  -- CI settings
  let handle :: X.IOException -> IO String
      handle _e = return ""
  userDir <- X.catch (getAppUserDataDirectory "cryptol") handle
  let searchPath = [ 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
                   ]

  return ModuleEnv
    { meLoadedModules = mempty
    , meNameSeeds     = T.nameSeeds
    , meEvalEnv       = mempty
    , meFocusedModule = Nothing
      -- we search these in order, taking the first match
    , meSearchPath    = searchPath
    , meDynEnv        = mempty
    , meMonoBinds     = True
    , meSolverConfig  = T.SolverConfig
                          { T.solverPath = "z3"
                          , T.solverArgs = [ "-smt2", "-in" ]
                          , T.solverVerbose = 0
                          , T.solverPreludePath = searchPath
                          }
    , meCoreLint      = NoCoreLint
    , meSupply        = emptySupply
    }

-- | 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.
-- Note that this includes parameterized modules.
loadedModules :: ModuleEnv -> [T.Module]
loadedModules = map lmModule . getLoadedModules . meLoadedModules

-- | Get a list of all the loaded non-parameterized modules.
-- These are the modules that can be used for evaluation, proving etc.
loadedNonParamModules :: ModuleEnv -> [T.Module]
loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules

-- | Are any parameterized modules loaded?
hasParamModules :: ModuleEnv -> Bool
hasParamModules = not . null . lmLoadedParamModules . meLoadedModules

allDeclGroups :: ModuleEnv -> [T.DeclGroup]
allDeclGroups = concatMap T.mDecls . loadedNonParamModules

-- | Contains enough information to browse what's in scope,
-- or type check new expressions.
data ModContext = ModContext
  { mctxParams          :: IfaceParams
  , mctxDecls           :: IfaceDecls
  , mctxNames           :: R.NamingEnv
  , mctxNameDisp        :: NameDisp
  , mctxTypeProvenace   :: Map Name DeclProvenance
  , mctxValueProvenance :: Map Name DeclProvenance
  }

-- | Specifies how a declared name came to be in scope.
data DeclProvenance =
    NameIsImportedFrom ModName
  | NameIsLocalPublic
  | NameIsLocalPrivate
  | NameIsParameter
  | NameIsDynamicDecl
    deriving (Eq,Ord)


-- | Given the state of the environment, compute information about what's
-- in scope on the REPL.  This includes what's in the focused module, plus any
-- additional definitions from the REPL (e.g., let bound names, and @it@).
focusedEnv :: ModuleEnv -> ModContext
focusedEnv me =
  ModContext
    { mctxParams   = parameters
    , mctxDecls    = mconcat (dynDecls : localDecls : importedDecls)
    , mctxNames    = namingEnv
    , mctxNameDisp = R.toNameDisp namingEnv
    , mctxTypeProvenace = fst provenance
    , mctxValueProvenance = snd provenance
    }

  where
  (importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)
  localDecls    = publicDecls `mappend` privateDecls
  localNames    = R.unqualifiedEnv localDecls `mappend`
                                                R.modParamsNamingEnv parameters
  dynDecls      = deIfaceDecls (meDynEnv me)
  dynNames      = deNames (meDynEnv me)

  namingEnv     = dynNames   `R.shadowing`
                   localNames `R.shadowing`
                   mconcat importedNames

  provenance    = shadowProvs
                $ declsProv NameIsDynamicDecl dynDecls
                : declsProv NameIsLocalPublic publicDecls
                : declsProv NameIsLocalPrivate privateDecls
                : paramProv parameters
                : importedProvs

  (imports, parameters, publicDecls, privateDecls) =
    case meFocusedModule me of
      Nothing -> (mempty, noIfaceParams, mempty, mempty)
      Just fm ->
        case lookupModule fm me of
          Just lm ->
            let Iface { .. } = lmInterface lm
            in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate)
          Nothing -> panic "focusedEnv" ["Focused module is not loaded."]

  loadImport imp =
    case lookupModule (iModule imp) me of
      Just lm ->
        let decls = ifPublic (lmInterface lm)
        in ( R.interpImport imp decls
           , decls
           , declsProv (NameIsImportedFrom (iModule imp)) decls
           )
      Nothing -> panic "focusedEnv"
                   [ "Missing imported module: " ++ show (pp (iModule imp)) ]


  -- earlier ones shadow
  shadowProvs ps = let (tss,vss) = unzip ps
                   in (Map.unions tss, Map.unions vss)

  paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)
    where doMap mp = const NameIsParameter <$> mp

  declsProv prov IfaceDecls { .. } =
    ( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
    , doMap ifDecls
    )
    where doMap mp = const prov <$> mp


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

-- | The location of a module
data ModulePath = InFile FilePath
                | InMem String ByteString -- ^ Label, content
    deriving (Show, Generic, NFData)

-- | In-memory things are compared by label.
instance Eq ModulePath where
  p1 == p2 =
    case (p1,p2) of
      (InFile x, InFile y) -> x == y
      (InMem a _, InMem b _) -> a == b
      _ -> False

instance PP ModulePath where
  ppPrec _ e =
    case e of
      InFile p  -> text p
      InMem l _ -> parens (text l)



-- | The name of the content---either the file path, or the provided label.
modulePathLabel :: ModulePath -> String
modulePathLabel p =
  case p of
    InFile path -> path
    InMem lab _ -> lab



data LoadedModules = LoadedModules
  { lmLoadedModules      :: [LoadedModule]
    -- ^ Invariants:
    -- 1) All the dependencies of any module `m` must precede `m` in the list.
    -- 2) Does not contain any parameterized modules.

  , lmLoadedParamModules :: [LoadedModule]
    -- ^ Loaded parameterized modules.

  } deriving (Show, Generic, NFData)

getLoadedModules :: LoadedModules -> [LoadedModule]
getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x

instance Semigroup LoadedModules where
  l <> r = LoadedModules
    { lmLoadedModules = List.unionBy ((==) `on` lmName)
                                      (lmLoadedModules l) (lmLoadedModules r)
    , lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r }

instance Monoid LoadedModules where
  mempty = LoadedModules { lmLoadedModules = []
                         , lmLoadedParamModules = []
                         }
  mappend l r = l <> r

data LoadedModule = LoadedModule
  { lmName              :: ModName
    -- ^ The name of this module.  Should match what's in 'lmModule'

  , lmFilePath          :: ModulePath
    -- ^ The file path used to load this module (may not be canonical)

  , lmModuleId          :: String
    -- ^ An identifier used to identify the source of the bytes for the module.
    -- For files we just use the cononical path, for in memory things we
    -- use their label.

  , lmInterface         :: Iface
    -- ^ The module's interface. This is for convenient.  At the moment
    -- we have the whole module in 'lmModule', so this could be computer.

  , lmModule            :: T.Module
    -- ^ The actual type-checked module

  , lmFingerprint       :: Fingerprint
  } deriving (Show, Generic, NFData)

-- | Has this module been loaded already.
isLoaded :: ModName -> LoadedModules -> Bool
isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)

-- | Is this a loaded parameterized module.
isLoadedParamMod :: ModName -> LoadedModules -> Bool
isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln)

-- | Try to find a previously loaded module
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
  where
  search how = List.find ((mn ==) . lmName) (how (meLoadedModules me))


-- | Add a freshly loaded module.  If it was previously loaded, then
-- the new version is ignored.
addLoadedModule ::
  ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules
addLoadedModule path ident fp tm lm
  | isLoaded (T.mName tm) lm  = lm
  | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
                                                lmLoadedParamModules lm }
  | otherwise                = lm { lmLoadedModules =
                                          lmLoadedModules lm ++ [loaded] }
  where
  loaded = LoadedModule
    { lmName            = T.mName tm
    , lmFilePath        = path
    , lmModuleId        = ident
    , lmInterface       = genIface tm
    , lmModule          = tm
    , lmFingerprint     = fp
    }

-- | Remove a previously loaded module.
-- Note that this removes exactly the modules specified by the predicate.
-- One should be carfule to preserve the invariant on 'LoadedModules'.
removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
removeLoadedModule rm lm =
  LoadedModules
    { lmLoadedModules = filter (not . rm) (lmLoadedModules lm)
    , lmLoadedParamModules = filter (not . rm) (lmLoadedParamModules lm)
    }

-- 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
  } deriving Generic

instance Semigroup DynamicEnv where
  de1 <> de2 = DEnv
    { deNames = deNames de1 <> deNames de2
    , deDecls = deDecls de1 <> deDecls de2
    , deEnv   = deEnv   de1 <> deEnv   de2
    }

instance Monoid DynamicEnv where
  mempty = DEnv
    { deNames = mempty
    , deDecls = mempty
    , deEnv   = mempty
    }
  mappend de1 de2 = de1 <> 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
            , ifAbstractTypes = Map.empty
            , ifDecls    = Map.singleton (ifDeclName ifd) ifd
            }
          | decl <- concatMap T.groupDecls dgs
          , let ifd = mkIfaceDecl decl
          ]