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

module Cryptol.ModuleSystem.Base where

import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Env (lookupModule, LoadedModule(..))
import qualified Cryptol.Eval                 as E
import qualified Cryptol.Eval.Value           as E
import qualified Cryptol.ModuleSystem.Renamer as R
import qualified Cryptol.Parser               as P
import qualified Cryptol.Parser.Unlit         as P
import Cryptol.Parser.AST as P
import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))
import Cryptol.Parser.NoInclude (removeIncludesModule)
import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
import qualified Cryptol.TypeCheck     as T
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Depends as T
import Cryptol.Utils.PP (pretty)

import Cryptol.Prelude (writePreludeContents)

import Cryptol.Transform.MonoValues

import Control.DeepSeq
import qualified Control.Exception as X
import Control.Monad (unless)
import Data.Function (on)
import Data.List (nubBy)
import Data.Maybe (mapMaybe,fromMaybe)
import Data.Monoid ((<>))
import System.Directory (doesFileExist)
import System.FilePath ( addExtension
                       , isAbsolute
                       , joinPath
                       , (</>)
                       , takeDirectory
                       , takeFileName
                       )
import qualified System.IO.Error as IOE
import qualified Data.Map as Map

#if __GLASGOW_HASKELL__ < 710
import Data.Foldable (foldMap)
#endif

-- Renaming --------------------------------------------------------------------

rename :: R.Rename a => R.NamingEnv -> a -> ModuleM a
rename env a = do
  renamerWarnings ws
  case res of
    Right r   -> return r
    Left errs -> renamerErrors errs
  where
  (res,ws) = R.runRenamer env (R.rename a)

-- | Rename a module in the context of its imported modules.
renameModule :: P.Module -> ModuleM P.Module
renameModule m = do
  iface <- importIfaces (map thing (P.mImports m))

  let menv    = R.namingEnv m
      (es,ws) = R.checkNamingEnv menv

  renamerWarnings ws
  unless (null es) (renamerErrors es)

  -- explicitly shadow the imported environment with the local environment
  rename (menv `R.shadowing` R.namingEnv iface) m

-- | Rename an expression in the context of the focused module.
renameExpr :: P.Expr -> ModuleM P.Expr
renameExpr e = do
  env <- getFocusedEnv
  denv <- getDynEnv
  rename (deNames denv `R.shadowing` R.namingEnv env) e

-- | Rename declarations in the context of the focused module.
renameDecls :: (R.Rename d, T.FromDecl d) => [d] -> ModuleM [d]
renameDecls ds = do
  env <- getFocusedEnv
  denv <- getDynEnv
  rename (deNames denv `R.shadowing` R.namingEnv env) ds

-- NoPat -----------------------------------------------------------------------

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
noPat a = do
  let (a',errs) = removePatterns a
  unless (null errs) (noPatErrors errs)
  return a'


-- Parsing ---------------------------------------------------------------------

parseModule :: FilePath -> ModuleM P.Module
parseModule path = do

  e <- io $ X.try $ do
    bytes <- readFile path
    return $!! bytes
  bytes <- case (e :: Either X.IOException String) of
    Right bytes -> return bytes
    Left exn | IOE.isDoesNotExistError exn -> cantFindFile path
             | otherwise                   -> otherIOError path exn

  let cfg = P.defaultConfig
              { P.cfgSource  = path
              , P.cfgPreProc = P.guessPreProc path
              }
  case P.parseModule cfg bytes of
    Right pm -> return pm
    Left err -> moduleParseError path err


-- Modules ---------------------------------------------------------------------

-- | Load a module by its path.
loadModuleByPath :: FilePath -> ModuleM T.Module
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
  let fileName = takeFileName path
  -- path' is the resolved, absolute path
  path' <- findFile fileName
  pm <- parseModule path'
  let n = thing (P.mName pm)

  -- Check whether this module name has already been loaded from a different file
  env <- getModuleEnv
  case lookupModule n env of
    Nothing -> loadingModule n (loadModule path' pm)
    Just lm
      | path' == loaded -> return (lmModule lm)
      | otherwise       -> duplicateModuleName n path' loaded
      where loaded = lmFilePath lm


-- | Load the module specified by an import.
loadImport :: Located P.Import -> ModuleM ()
loadImport li = do

  let i = thing li
      n = P.iModule i

  alreadyLoaded <- isLoaded n
  unless alreadyLoaded $
    do path <- findModule n
       pm   <- parseModule path
       loadingImport li $ do

         -- make sure that this module is the one we expect
         unless (n == thing (P.mName pm)) (moduleNameMismatch n (mName pm))

         _ <- loadModule path pm
         return ()

-- | Load dependencies, typecheck, and add to the eval environment.
loadModule :: FilePath -> P.Module -> ModuleM T.Module
loadModule path pm = do

  let pm' = addPrelude pm
  loadDeps pm'

  -- XXX make it possible to configure output
  io (putStrLn ("Loading module " ++ pretty (P.thing (P.mName pm'))))

  tcm <- checkModule pm'

  -- extend the eval env
  modifyEvalEnv (E.moduleEnv tcm)

  loadedModule path tcm

  return tcm


-- | Rewrite an import declaration to be of the form:
--
-- > import foo as foo [ [hiding] (a,b,c) ]
fullyQualified :: P.Import -> P.Import
fullyQualified i = i { iAs = Just (iModule i) }

-- | Process the interface specified by an import.
importIface :: P.Import -> ModuleM Iface
importIface i = interpImport i `fmap` getIface (T.iModule i)

-- | Load a series of interfaces, merging their public interfaces.
importIfaces :: [P.Import] -> ModuleM IfaceDecls
importIfaces is = foldMap ifPublic `fmap` mapM importIface is

moduleFile :: ModName -> String -> FilePath
moduleFile (ModName ns) = addExtension (joinPath ns)

-- | Discover a module.
findModule :: ModName -> ModuleM FilePath
findModule n = do
  paths <- getSearchPath
  loop (possibleFiles paths)
  where
  loop paths = case paths of

    path:rest -> do
      b <- io (doesFileExist path)
      if b then return path else loop rest

    [] -> handleNotFound

  handleNotFound =
    case n of
      m | m == preludeName -> writePreludeContents
      _ -> moduleNotFound n =<< getSearchPath

  -- generate all possible search paths
  possibleFiles paths = do
    path <- paths
    ext  <- P.knownExts
    return (path </> moduleFile n ext)

-- | Discover a file. This is distinct from 'findModule' in that we
-- assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath
findFile path | isAbsolute path = do
  -- No search path checking for absolute paths
  b <- io (doesFileExist path)
  if b then return path else cantFindFile path
findFile path = do
  paths <- getSearchPath
  loop (possibleFiles paths)
  where
  loop paths = case paths of
    path':rest -> do
      b <- io (doesFileExist path')
      if b then return path' else loop rest
    [] -> cantFindFile path
  possibleFiles paths = map (</> path) paths

preludeName :: P.ModName
preludeName  = P.ModName ["Cryptol"]

-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: P.Module -> P.Module
addPrelude m
  | preludeName == P.thing (P.mName m) = m
  | preludeName `elem` importedMods    = m
  | otherwise                          = m { mImports = importPrelude : mImports m }
  where
  importedMods  = map (P.iModule . P.thing) (P.mImports m)
  importPrelude = P.Located
    { P.srcRange = emptyRange
    , P.thing    = P.Import
      { iModule    = preludeName
      , iAs        = Nothing
      , iSpec      = Nothing
      }
    }

-- | Load the dependencies of a module into the environment.
loadDeps :: Module -> ModuleM ()
loadDeps m
  | null needed = return ()
  | otherwise   = mapM_ load needed
  where
  needed  = nubBy ((==) `on` P.iModule . thing) (P.mImports m)
  load mn = loadImport mn


-- Type Checking ---------------------------------------------------------------

-- | Typecheck a single expression.
checkExpr :: P.Expr -> ModuleM (T.Expr,T.Schema)
checkExpr e = do
  npe <- noPat e
  denv <- getDynEnv
  re  <- renameExpr npe
  env <- getQualifiedEnv
  let env' = env <> deIfaceDecls denv
  typecheck T.tcExpr re env'

-- | Typecheck a group of declarations.
checkDecls :: (HasLoc d, R.Rename d, T.FromDecl d) => [d] -> ModuleM [T.DeclGroup]
checkDecls ds = do
  -- nopat must already be run
  rds <- renameDecls ds
  denv <- getDynEnv
  env <- getQualifiedEnv
  let env' = env <> deIfaceDecls denv
  typecheck T.tcDecls rds env'

-- | Typecheck a module.
checkModule :: P.Module -> ModuleM T.Module
checkModule m = do
  -- remove includes first
  e   <- io (removeIncludesModule m)
  nim <- case e of
           Right nim  -> return nim
           Left ierrs -> noIncludeErrors ierrs

  -- remove pattern bindings
  npm <- noPat nim

  -- rename everything
  scm <- renameModule npm

  -- typecheck
  tcm <- typecheck T.tcModule scm =<< importIfacesTc (map thing (P.mImports scm))

  return (Cryptol.Transform.MonoValues.rewModule tcm)


type TCAction i o = i -> T.InferInput -> IO (T.InferOutput o)

typecheck :: HasLoc i => TCAction i o -> i -> IfaceDecls -> ModuleM o
typecheck action i env = do

  let range = fromMaybe emptyRange (getLoc i)
  input <- genInferInput range env
  out   <- io (action i input)

  case out of

    T.InferOK warns seeds o ->
      do setNameSeeds seeds
         typeCheckWarnings warns
         return o

    T.InferFailed warns errs ->
      do typeCheckWarnings warns
         typeCheckingFailed errs

-- | Process a list of imports, producing an aggregate interface suitable for use
-- when typechecking.
importIfacesTc :: [P.Import] -> ModuleM IfaceDecls
importIfacesTc is =
  mergePublic `fmap` mapM (importIface . fullyQualified) is
  where
  mergePublic = foldMap ifPublic

-- | Generate input for the typechecker.
genInferInput :: Range -> IfaceDecls -> ModuleM T.InferInput
genInferInput r env = do
  seeds <- getNameSeeds
  monoBinds <- getMonoBinds

  -- TODO: include the environment needed by the module
  return T.InferInput
    { T.inpRange     = r
    , T.inpVars      = Map.map ifDeclSig (filterEnv ifDecls)
    , T.inpTSyns     =                    filterEnv ifTySyns
    , T.inpNewtypes  =                    filterEnv ifNewtypes
    , T.inpNameSeeds = seeds
    , T.inpMonoBinds = monoBinds
    }
  where
  -- at this point, the names used in the aggregate interface should be
  -- unique
  keepOne :: (QName,[a]) -> Maybe (QName,a)
  keepOne (qn,syns) = case syns of
    [syn] -> Just (qn,syn)
    _     -> Nothing

  -- keep symbols without duplicates.  the renamer would have caught
  -- duplication already, so this is safe.
  filterEnv p = Map.fromList (mapMaybe keepOne (Map.toList (p env)))


-- Evaluation ------------------------------------------------------------------

evalExpr :: T.Expr -> ModuleM E.Value
evalExpr e = do
  env <- getEvalEnv
  denv <- getDynEnv
  return (E.evalExpr (env <> deEnv denv) e)

evalDecls :: [T.DeclGroup] -> ModuleM ()
evalDecls dgs = do
  env <- getEvalEnv
  denv <- getDynEnv
  let env' = env <> deEnv denv
      denv' = denv { deDecls = deDecls denv ++ dgs
                   , deEnv = E.evalDecls dgs env'
                   }
  setDynEnv denv'