{-|
Module      : Idris.ModeCommon
Description : Common utilities used by all modes.
License     : BSD3
Maintainer  : The Idris Community.
-}

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-binds #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Idris.ModeCommon (banner, defaultPort, loadInputs, warranty) where

import Idris.AbsSyntax
import Idris.Chaser
import Idris.Core.TT
import Idris.Delaborate
import Idris.Erasure
import Idris.Error
import Idris.IBC
import Idris.Imports
import Idris.Info
import Idris.Options
import Idris.Output
import Idris.Parser hiding (indent)
import IRTS.Exports

import Prelude hiding (id, (.), (<$>))

import Control.Category
import Control.DeepSeq
import Control.Monad
import Network.Socket (PortNumber)

defaultPort :: PortNumber
defaultPort = fromIntegral 4294

loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs inputs toline -- furthest line to read in input source files
  = idrisCatch
       (do ist <- getIState
           -- if we're in --check and not outputting anything, don't bother
           -- loading, as it gets really slow if there's lots of modules in
           -- a package (instead, reload all at the end to check for
           -- consistency only)
           opts <- getCmdLine

           let loadCode = case opt getOutput opts of
                               [] -> not (NoREPL `elem` opts)
                               _ -> True

           logParser 3 $ show "loadInputs loadCode" ++ show loadCode

           -- For each ifile list, check it and build ibcs in the same clean IState
           -- so that they don't interfere with each other when checking

           importlists <- getImports [] inputs

           logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))

           let ninputs = zip [1..] inputs
           ifiles <- mapWhileOK (\(num, input) ->
                do putIState ist
                   logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)
                   modTree <- buildTree
                                   (map snd (take (num-1) ninputs))
                                   importlists
                                   input
                   let ifiles = getModuleFiles modTree
                   logParser 2 ("MODULE TREE : " ++ show modTree)
                   logParser 2 ("RELOAD: " ++ show ifiles)
                   when (not (all ibc ifiles) || loadCode) $
                        tryLoad False IBC_Building (filter (not . ibc) ifiles)
                   -- return the files that need rechecking
                   return (input, ifiles))
                      ninputs
           inew <- getIState
           let tidata = idris_tyinfodata inew
           -- If it worked, load the whole thing from all the ibcs together
           case errSpan inew of
              Nothing ->
                do putIState $!! ist { idris_tyinfodata = tidata }
                   logParser 3 $ "loadInputs ifiles" ++ show ifiles

                   let fileToIFileType :: FilePath -> Idris IFileType
                       fileToIFileType file = do
                         ibcsd <- valIBCSubDir ist
                         ids <- rankedImportDirs file
                         findImport ids ibcsd file

                   ibcfiles <- mapM fileToIFileType inputs
                   logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles

                   tryLoad True (IBC_REPL True) ibcfiles
              _ -> return ()
           exports <- findExports

           case opt getOutput opts of
               [] -> performUsageAnalysis (getExpNames exports) -- interactive
               _  -> return []  -- batch, will be checked by the compiler

           return (map fst ifiles))
        (\e -> do i <- getIState
                  case e of
                    At f e' -> do setErrSpan f
                                  iWarn f $ pprintErr i e'
                    ProgramLineComment -> return () -- fail elsewhere
                    _ -> do setErrSpan emptyFC -- FIXME! Propagate it
                                               -- Issue #1576 on the issue tracker.
                                               -- https://github.com/idris-lang/Idris-dev/issues/1576
                            iWarn emptyFC $ pprintErr i e
                  return [])
   where -- load all files, stop if any fail
         tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
         tryLoad keepstate phase [] = warnTotality >> return ()
         tryLoad keepstate phase (f : fs)
                 = do ist <- getIState
                      logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++
                        show (keepstate, phase, f : fs)
                      let maxline
                            = case toline of
                                Nothing -> Nothing
                                Just l -> case f of
                                            IDR fn -> if any (fmatch fn) inputs
                                                         then Just l
                                                         else Nothing
                                            LIDR fn -> if any (fmatch fn) inputs
                                                          then Just l
                                                          else Nothing
                                            _ -> Nothing
                      loadFromIFile True phase f maxline
                      inew <- getIState
                      -- FIXME: Save these in IBC to avoid this hack! Need to
                      -- preserve it all from source inputs
                      --
                      -- Issue #1577 on the issue tracker.
                      --     https://github.com/idris-lang/Idris-dev/issues/1577
                      let tidata = idris_tyinfodata inew
                      let patdefs = idris_patdefs inew
                      ok <- noErrors
                      if ok then
                            -- The $!! here prevents a space leak on reloading.
                            -- This isn't a solution - but it's a temporary stopgap.
                            -- See issue #2386
                            do when (not keepstate) $ putIState $!! ist
                               ist <- getIState
                               putIState $!! ist { idris_tyinfodata = tidata,
                                                   idris_patdefs = patdefs }
                               tryLoad keepstate phase fs
                          else warnTotality

         ibc (IBC _ _) = True
         ibc _ = False

         fmatch ('.':'/':xs) ys = fmatch xs ys
         fmatch xs ('.':'/':ys) = fmatch xs ys
         fmatch xs ys = xs == ys

         -- Like mapM, but give up when there's an error
         mapWhileOK f [] = return []
         mapWhileOK f (x : xs) = do x' <- f x
                                    ok <- noErrors
                                    if ok then do xs' <- mapWhileOK f xs
                                                  return (x' : xs')
                                          else return [x']

banner = "     ____    __     _                                          \n" ++
         "    /  _/___/ /____(_)____                                     \n" ++
         "    / // __  / ___/ / ___/     Version " ++ getIdrisVersion ++ "\n" ++
         "  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      \n" ++
         " /___/\\__,_/_/  /_/____/       Type :? for help               \n" ++
         "\n" ++
         "Idris is free software with ABSOLUTELY NO WARRANTY.            \n" ++
         "For details type :warranty."

warranty = "\n"                                                                          ++
           "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY  \n" ++
           "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE     \n" ++
           "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR    \n" ++
           "\t PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE   \n" ++
           "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR   \n" ++
           "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF  \n" ++
           "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       \n" ++
           "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
           "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE  \n" ++
           "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
           "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"