{-|
Module      : Idris.Package
Description : Functionality for working with Idris packages.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP #-}
module Idris.Package where

import System.Directory
import System.Directory (copyFile, createDirectoryIfMissing)
import System.Environment
import System.Exit
import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
                        hasExtension, takeDirectory, takeExtension,
                        takeFileName, (</>))
import System.IO
import System.Process

import Util.System

import Control.Monad
import Control.Monad.Trans.Except (runExceptT)
import Control.Monad.Trans.State.Strict (execStateT)
import Data.Either (partitionEithers)
import Data.List
import Data.List.Split (splitOn)

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error (ifail)
import Idris.IBC
import Idris.IdrisDoc
import Idris.Imports
import Idris.Main (idris, idrisMain)
import Idris.Options
import Idris.Output
import Idris.Parser (loadModule)

import Idris.Package.Common
import Idris.Package.Parser

import IRTS.System

-- To build a package:
-- * read the package description
-- * check all the library dependencies exist
-- * invoke the makefile if there is one
-- * invoke idris on each module, with idris_opts
-- * install everything into datadir/pname, if install flag is set

getPkgDesc :: FilePath -> IO PkgDesc
getPkgDesc = parseDesc

--  --------------------------------------------------------- [ Build Packages ]

-- | Run the package through the idris compiler.
buildPkg :: [Opt]            -- ^ Command line options
         -> Bool             -- ^ Provide Warnings
         -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
         -> IO ()
buildPkg copts warnonly (install, fp) = do
  pkgdesc <- parseDesc fp
  dir <- getCurrentDirectory
  let idx' = pkgIndex $ pkgname pkgdesc
      idx  = PkgIndex $ case opt getIBCSubDir copts of
        (ibcsubdir:_) -> ibcsubdir </> idx'
        []            -> idx'
  oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
  when (and oks) $ do
    m_ist <- inPkgDir pkgdesc $ do

      make (makefile pkgdesc)
      case (execout pkgdesc) of
        Nothing -> do
          case mergeOptions copts (idx : NoREPL : Verbose 1 : idris_opts pkgdesc) of
            Left emsg -> do
              putStrLn emsg
              exitWith (ExitFailure 1)
            Right opts -> do
              auditPackage (AuditIPkg `elem` opts) pkgdesc
              buildMods opts (modules pkgdesc)
        Just o -> do
          let exec = dir </> o
          case mergeOptions copts (idx : NoREPL : Verbose 1 : Output exec : idris_opts pkgdesc) of
            Left emsg -> do
              putStrLn emsg
              exitWith (ExitFailure 1)
            Right opts -> do
              auditPackage (AuditIPkg `elem` opts) pkgdesc
              buildMain opts (idris_main pkgdesc)
    case m_ist of
      Nothing  -> exitWith (ExitFailure 1)
      Just ist -> do
        -- Quit with error code if there was a problem
        case errSpan ist of
          Just _ -> exitWith (ExitFailure 1)
          _      -> return ()
        when install $ installPkg (opt getIBCSubDir copts) pkgdesc
  where
    buildMain opts (Just mod) = buildMods opts [mod]
    buildMain _ Nothing = do
      putStrLn "Can't build an executable: No main module given"
      exitWith (ExitFailure 1)

--  --------------------------------------------------------- [ Check Packages ]

-- | Type check packages only
--
-- This differs from build in that executables are not built, if the
-- package contains an executable.
checkPkg :: [Opt]     -- ^ Command line Options
         -> Bool      -- ^ Show Warnings
         -> Bool      -- ^ quit on failure
         -> FilePath  -- ^ Path to ipkg file.
         -> IO ()
checkPkg copts warnonly quit fpath = do
  pkgdesc <- parseDesc fpath
  oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
  when (and oks) $ do
    res <- inPkgDir pkgdesc $ do
      make (makefile pkgdesc)

      case mergeOptions copts (NoREPL : Verbose 1 : idris_opts pkgdesc) of
        Left emsg -> do
          putStrLn emsg
          exitWith (ExitFailure 1)
        Right opts -> do
          auditPackage (AuditIPkg `elem` opts) pkgdesc
          buildMods opts (modules pkgdesc)
    when quit $ case res of
                  Nothing -> exitWith (ExitFailure 1)
                  Just res' -> do
                    case errSpan res' of
                      Just _ -> exitWith (ExitFailure 1)
                      _      -> return ()

--  ------------------------------------------------------------------- [ REPL ]

-- | Check a package and start a REPL.
--
-- This function only works with packages that have a main module.
--
replPkg :: [Opt]    -- ^ Command line Options
        -> FilePath -- ^ Path to ipkg file.
        -> Idris ()
replPkg copts fp = do
    orig <- getIState
    runIO $ checkPkg copts False False fp
    pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!

    case mergeOptions copts (idris_opts pkgdesc) of
      Left emsg  -> ifail emsg
      Right opts -> do

        putIState orig
        dir <- runIO getCurrentDirectory
        runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
        runMain opts (idris_main pkgdesc)
        runIO $ setCurrentDirectory dir

  where
    toPath n = foldl1' (</>) $ splitOn "." n

    runMain opts (Just mod) = do
      let f = toPath (showCG mod)
      idrisMain ((Filename f) : opts)
    runMain _ Nothing =
      iputStrLn "Can't start REPL: no main module given"

--  --------------------------------------------------------------- [ Cleaning ]

-- | Clean Package build files
cleanPkg :: [Opt]    -- ^ Command line options.
         -> FilePath -- ^ Path to ipkg file.
         -> IO ()
cleanPkg copts fp = do
  pkgdesc <- parseDesc fp
  dir <- getCurrentDirectory
  inPkgDir pkgdesc $ do
    clean (makefile pkgdesc)
    mapM_ rmIBC (modules pkgdesc)
    rmIdx (pkgname pkgdesc)
    case execout pkgdesc of
      Nothing -> return ()
      Just s -> rmExe $ dir </> s

--  ------------------------------------------------------ [ Generate IdrisDoc ]


-- | Generate IdrisDoc for package
-- TODO: Handle case where module does not contain a matching namespace
--       E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
--
-- Issue number #1572 on the issue tracker
--       https://github.com/idris-lang/Idris-dev/issues/1572
documentPkg :: [Opt]           -- ^ Command line options.
            -> (Bool,FilePath) -- ^ (Should we install?, Path to ipkg file).
            -> IO ()
documentPkg copts (install,fp) = do
  pkgdesc        <- parseDesc fp
  cd             <- getCurrentDirectory
  let pkgDir      = cd </> takeDirectory fp
      outputDir   = cd </> unPkgName (pkgname pkgdesc) ++ "_doc"
      popts       = NoREPL : Verbose 1 : idris_opts pkgdesc
      mods        = modules pkgdesc
      fs          = map (foldl1' (</>) . splitOn "." . showCG) mods
  setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
  make (makefile pkgdesc)
  setCurrentDirectory pkgDir
  case mergeOptions copts popts of
    Left emsg -> do
      putStrLn emsg
      exitWith (ExitFailure 1)
    Right opts -> do
      let run l       = runExceptT . execStateT l
          load []     = return ()
          load (f:fs) = do loadModule f IBC_Building; load fs
          loader      = do
            idrisMain opts
            addImportDir (sourcedir pkgdesc)
            load fs
      idrisImplementation  <- run loader idrisInit
      setCurrentDirectory cd
      case idrisImplementation of
        Left  err -> do
          putStrLn $ pshow idrisInit err
          exitWith (ExitFailure 1)
        Right ist -> do
          iDocDir   <- getIdrisDocDir
          pkgDocDir <- makeAbsolute (iDocDir </> unPkgName (pkgname pkgdesc))
          let out_dir = if install then pkgDocDir else outputDir
          when install $ do
              putStrLn $ unwords ["Attempting to install IdrisDocs for", show $ pkgname pkgdesc, "in:", out_dir]

          docRes <- generateDocs ist mods out_dir
          case docRes of
            Right _  -> return ()
            Left msg -> do
              putStrLn msg
              exitWith (ExitFailure 1)

--  ------------------------------------------------------------------- [ Test ]

-- | Build a package with a sythesized main function that runs the tests
testPkg :: [Opt]     -- ^ Command line options.
        -> FilePath  -- ^ Path to ipkg file.
        -> IO ExitCode
testPkg copts fp = do
  pkgdesc <- parseDesc fp
  ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)
  if and ok
    then do
      (m_ist, exitCode) <- inPkgDir pkgdesc $ do
        make (makefile pkgdesc)
        -- Get a temporary file to save the tests' source in
        (tmpn, tmph) <- tempfile ".idr"
        hPutStrLn tmph $
            "module Test_______\n" ++
            concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc]
                ++ "namespace Main\n"
                ++ "  main : IO ()\n"
                ++ "  main = do "
                ++ concat [ show t ++ "\n            "
                          | t <- idris_tests pkgdesc]
        hClose tmph
        (tmpn', tmph') <- tempfile ""
        hClose tmph'
        let popts = (Filename tmpn : NoREPL : Verbose 1 : Output tmpn' : idris_opts pkgdesc)
        case mergeOptions copts popts of
          Left emsg -> do
            putStrLn emsg
            exitWith (ExitFailure 1)
          Right opts -> do
            m_ist    <- idris opts
            let texe = if isWindows then addExtension tmpn' ".exe" else tmpn'
            exitCode <- rawSystem texe []
            return (m_ist, exitCode)
      case m_ist of
        Nothing  -> exitWith (ExitFailure 1)
        Just ist -> do
          -- Quit with error code if problem building
          case errSpan ist of
            Just _ -> exitWith (ExitFailure 1)
            _      -> return exitCode
    else return (ExitFailure 1)

--  ----------------------------------------------------------- [ Installation ]

-- | Install package
installPkg :: [String]  -- ^ Alternate install location
           -> PkgDesc   -- ^ iPKG file.
           -> IO ()
installPkg altdests pkgdesc = inPkgDir pkgdesc $ do
  d <- getIdrisLibDir
  let destdir = case altdests of
                  []     -> d
                  (d':_) -> d'
  case (execout pkgdesc) of
    Nothing -> do
      mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc)
      installIdx destdir (pkgname pkgdesc)
    Just o -> return () -- do nothing, keep executable locally, for noe

  mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc)

-- ---------------------------------------------------------- [ Helper Methods ]
-- Methods for building, testing, installing, and removal of idris
-- packages.

auditPackage :: Bool -> PkgDesc -> IO ()
auditPackage False _    = return ()
auditPackage True  ipkg = do
    cwd <- getCurrentDirectory

    let ms = map (sourcedir ipkg </>) $ map (toPath . showCG) (modules ipkg)
    ms' <- mapM makeAbsolute ms

    ifiles <- getIdrisFiles cwd

    let ifiles' = map dropExtension ifiles

    not_listed <- mapM makeRelativeToCurrentDirectory (ifiles' \\ ms')

    putStrLn $ unlines $
         ["Warning: The following modules are not listed in your iPkg file:\n"]
      ++ map (\m -> unwords ["-", m]) not_listed
      ++ ["\nModules that are not listed, are not installed."]

  where
    toPath n = foldl1' (</>) $ splitOn "." n

    getIdrisFiles :: FilePath -> IO [FilePath]
    getIdrisFiles dir = do
      contents <- getDirectoryContents dir

      -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

      files <- forM contents (findRest dir)
      return $ filter (isIdrisFile) (concat files)

    isIdrisFile :: FilePath -> Bool
    isIdrisFile fp = takeExtension fp == ".idr" || takeExtension fp == ".lidr"

    findRest :: FilePath -> FilePath -> IO [FilePath]
    findRest dir fn = do
      path <- makeAbsolute (dir </> fn)
      isDir <- doesDirectoryExist path
      if isDir
        then getIdrisFiles path
        else return [path]

buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
buildMods opts ns = do let f = map (toPath . showCG) ns
                       idris (map Filename f ++ opts)
    where
      toPath n = foldl1' (</>) $ splitOn "." n

testLib :: Bool -> PkgName -> String -> IO Bool
testLib warn p f
    = do d <- getIdrisCRTSDir
         gcc <- getCC
         (tmpf, tmph) <- tempfile ""
         hClose tmph
         let libtest = d </> "libtest.c"
         e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf]
         case e of
            ExitSuccess -> return True
            _ -> do if warn
                       then do putStrLn $ "Not building " ++ show p ++
                                          " due to missing library " ++ f
                               return False
                       else fail $ "Missing library " ++ f

rmIBC :: Name -> IO ()
rmIBC m = rmFile $ toIBCFile m

rmIdx :: PkgName -> IO ()
rmIdx p = do let f = pkgIndex p
             ex <- doesFileExist f
             when ex $ rmFile f

rmExe :: String -> IO ()
rmExe p = do
            fn <- return $ if isWindows && not (hasExtension p)
                                then addExtension p ".exe" else p
            rmFile fn

toIBCFile (UN n) = str n ++ ".ibc"
toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))

installIBC :: String -> PkgName -> Name -> IO ()
installIBC dest p m = do
    let f = toIBCFile m
    let destdir = dest </> unPkgName p </> getDest m
    putStrLn $ "Installing " ++ f ++ " to " ++ destdir
    createDirectoryIfMissing True destdir
    copyFile f (destdir </> takeFileName f)
    return ()
  where
    getDest (UN n) = ""
    getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

installIdx :: String -> PkgName -> IO ()
installIdx dest p = do
  let f = pkgIndex p
  let destdir = dest </> unPkgName p
  putStrLn $ "Installing " ++ f ++ " to " ++ destdir
  createDirectoryIfMissing True destdir
  copyFile f (destdir </> takeFileName f)
  return ()

installObj :: String -> PkgName -> String -> IO ()
installObj dest p o = do
  let destdir = addTrailingPathSeparator (dest </> unPkgName p)
  putStrLn $ "Installing " ++ o ++ " to " ++ destdir
  createDirectoryIfMissing True destdir
  copyFile o (destdir </> takeFileName o)
  return ()

#ifdef mingw32_HOST_OS
mkDirCmd = "mkdir "
#else
mkDirCmd = "mkdir -p "
#endif

inPkgDir :: PkgDesc -> IO a -> IO a
inPkgDir pkgdesc action =
  do dir <- getCurrentDirectory
     when (sourcedir pkgdesc /= "") $
       do putStrLn $ "Entering directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
          setCurrentDirectory $ dir </> sourcedir pkgdesc
     res <- action
     when (sourcedir pkgdesc /= "") $
       do putStrLn $ "Leaving directory `" ++ ("." </> sourcedir pkgdesc) ++ "'"
          setCurrentDirectory dir
     return res

-- ------------------------------------------------------- [ Makefile Commands ]
-- | Invoke a Makefile's target with an enriched system environment
makeTarget :: Maybe String -> Maybe String -> IO ()
makeTarget _ Nothing = return ()
makeTarget mtgt (Just s) = do incFlags <- intercalate " " <$> getIncFlags
                              libFlags <- intercalate " " <$> getLibFlags
                              newEnv <- (++ [("IDRIS_INCLUDES", incFlags),
                                             ("IDRIS_LDFLAGS", libFlags)]) <$> getEnvironment
                              let cmdLine = case mtgt of
                                              Nothing -> "make -f " ++ s
                                              Just tgt -> "make -f " ++ s ++ " " ++ tgt
                              (_, _, _, r) <- createProcess (shell cmdLine) { env = Just newEnv }
                              waitForProcess r
                              return ()


-- | Invoke a Makefile's default target.
make :: Maybe String -> IO ()
make = makeTarget Nothing

-- | Invoke a Makefile's clean target.
clean :: Maybe String -> IO ()
clean = makeTarget (Just "clean")

-- | Merge an option list representing the command line options into
-- those specified for a package description.
--
-- This is not a complete union between the two options sets. First,
-- to prevent important package specified options from being
-- overwritten. Second, the semantics for this merge are not fully
-- defined.
--
-- A discussion for this is on the issue tracker:
--     https://github.com/idris-lang/Idris-dev/issues/1448
--
mergeOptions :: [Opt] -- ^ The command line options
             -> [Opt] -- ^ The package options
             -> Either String [Opt]
mergeOptions copts popts =
    case partitionEithers (map chkOpt (normaliseOpts copts)) of
      ([], copts') -> Right $ copts' ++ popts
      (es, _)      -> Left  $ genErrMsg es
  where
    normaliseOpts :: [Opt] -> [Opt]
    normaliseOpts = filter filtOpt

    filtOpt :: Opt -> Bool
    filtOpt (PkgBuild        _) = False
    filtOpt (PkgInstall      _) = False
    filtOpt (PkgClean        _) = False
    filtOpt (PkgCheck        _) = False
    filtOpt (PkgREPL         _) = False
    filtOpt (PkgDocBuild     _) = False
    filtOpt (PkgDocInstall   _) = False
    filtOpt (PkgTest         _) = False
    filtOpt _                   = True

    chkOpt :: Opt -> Either String Opt
    chkOpt o@(OLogging _)     = Right o
    chkOpt o@(OLogCats _)     = Right o
    chkOpt o@(DefaultTotal)   = Right o
    chkOpt o@(DefaultPartial) = Right o
    chkOpt o@(WarnPartial)    = Right o
    chkOpt o@(WarnReach)      = Right o
    chkOpt o@(IBCSubDir _)    = Right o
    chkOpt o@(ImportDir _ )   = Right o
    chkOpt o@(UseCodegen _)   = Right o
    chkOpt o@(Verbose _)      = Right o
    chkOpt o@(AuditIPkg)      = Right o
    chkOpt o@(DumpHighlights) = Right o
    chkOpt o                  = Left (unwords ["\t", show o, "\n"])

    genErrMsg :: [String] -> String
    genErrMsg es = unlines
        [ "Not all command line options can be used to override package options."
        , "\nThe only changeable options are:"
        , "\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"
        , "\t--ibcsubdir <path>, -i --idrispath <path>"
        , "\t--logging-categories <cats>"
        , "\t--highlight"
        , "\nThe options need removing are:"
        , unlines es
        ]

-- --------------------------------------------------------------------- [ EOF ]