{-|
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 :: PortNumber
defaultPort = Integer -> PortNumber
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
4294

loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs :: [String] -> Maybe Int -> Idris [String]
loadInputs [String]
inputs Maybe Int
toline -- furthest line to read in input source files
  = Idris [String] -> (Err -> Idris [String]) -> Idris [String]
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
       (do ist <- Idris IState
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 -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getOutput [Opt]
opts of
                               [] -> Bool -> Bool
not (Opt
NoREPL Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)
                               [String]
_ -> Bool
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 (\(String
i,[ImportInfo]
m) -> (String
i, (ImportInfo -> String) -> [ImportInfo] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ImportInfo -> String
import_path [ImportInfo]
m)) importlists))

           let ninputs = [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [String]
inputs
           ifiles <- mapWhileOK (\(Int
num, String
input) ->
                do IState -> Idris ()
putIState IState
ist
                   Int -> String -> Idris ()
logParser Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show String
"loadInputs (num, input)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, String) -> String
forall a. Show a => a -> String
show (Int
num, String
input)
                   modTree <- [String]
-> [(String, [ImportInfo])] -> String -> Idris [ModuleTree]
buildTree
                                   (((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> String
forall a b. (a, b) -> b
snd (Int -> [(Int, String)] -> [(Int, String)]
forall a. Int -> [a] -> [a]
take (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [(Int, String)]
ninputs))
                                   [(String, [ImportInfo])]
importlists
                                   String
input
                   let ifiles = [ModuleTree] -> [IFileType]
getModuleFiles [ModuleTree]
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 = IState -> Ctxt TIData
idris_tyinfodata IState
inew
           -- If it worked, load the whole thing from all the ibcs together
           case errSpan inew of
              Maybe FC
Nothing ->
                do IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist { idris_tyinfodata = tidata }
                   Int -> String -> Idris ()
logParser Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"loadInputs ifiles" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, [IFileType])] -> String
forall a. Show a => a -> String
show [(String, [IFileType])]
ifiles

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

                   ibcfiles <- (String -> Idris IFileType)
-> [String] -> StateT IState (ExceptT Err IO) [IFileType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM String -> Idris IFileType
fileToIFileType [String]
inputs
                   logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles

                   tryLoad True (IBC_REPL True) ibcfiles
              Maybe FC
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           exports <- findExports

           case opt getOutput opts of
               [] -> [Name] -> StateT IState (ExceptT Err IO) [Name]
performUsageAnalysis ([ExportIFace] -> [Name]
getExpNames [ExportIFace]
exports) -- interactive
               [String]
_  -> [Name] -> StateT IState (ExceptT Err IO) [Name]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []  -- batch, will be checked by the compiler

           return (map fst ifiles))
        (\Err
e -> do i <- Idris IState
getIState
                  case e of
                    At FC
f Err
e' -> do FC -> Idris ()
setErrSpan FC
f
                                  FC -> OutputDoc -> Idris ()
iWarn FC
f (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
i Err
e'
                    Err
ProgramLineComment -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- fail elsewhere
                    Err
_ -> do FC -> Idris ()
setErrSpan FC
emptyFC -- FIXME! Propagate it
                                               -- Issue #1576 on the issue tracker.
                                               -- https://github.com/idris-lang/Idris-dev/issues/1576
                            FC -> OutputDoc -> Idris ()
iWarn FC
emptyFC (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
i Err
e
                  return [])
   where -- load all files, stop if any fail
         tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
         tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
keepstate IBCPhase
phase [] = Idris ()
warnTotality Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         tryLoad Bool
keepstate IBCPhase
phase (IFileType
f : [IFileType]
fs)
                 = do ist <- Idris IState
getIState
                      logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++
                        show (keepstate, phase, f : fs)
                      let maxline
                            = case Maybe Int
toline of
                                Maybe Int
Nothing -> Maybe Int
forall a. Maybe a
Nothing
                                Just Int
l -> case IFileType
f of
                                            IDR String
fn -> if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
fmatch String
fn) [String]
inputs
                                                         then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
                                                         else Maybe Int
forall a. Maybe a
Nothing
                                            LIDR String
fn -> if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
fmatch String
fn) [String]
inputs
                                                          then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
                                                          else Maybe Int
forall a. Maybe a
Nothing
                                            IFileType
_ -> Maybe Int
forall a. Maybe a
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 = IState -> Ctxt TIData
idris_tyinfodata IState
inew
                      let patdefs = IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
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 :: IFileType -> Bool
ibc (IBC String
_ IFileType
_) = Bool
True
         ibc IFileType
_ = Bool
False

         fmatch :: String -> String -> Bool
fmatch (Char
'.':Char
'/':String
xs) String
ys = String -> String -> Bool
fmatch String
xs String
ys
         fmatch String
xs (Char
'.':Char
'/':String
ys) = String -> String -> Bool
fmatch String
xs String
ys
         fmatch String
xs String
ys = String
xs String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
ys

         -- Like mapM, but give up when there's an error
         mapWhileOK :: (t -> StateT IState (ExceptT Err IO) a)
-> [t] -> StateT IState (ExceptT Err IO) [a]
mapWhileOK t -> StateT IState (ExceptT Err IO) a
f [] = [a] -> StateT IState (ExceptT Err IO) [a]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
         mapWhileOK t -> StateT IState (ExceptT Err IO) a
f (t
x : [t]
xs) = do x' <- t -> StateT IState (ExceptT Err IO) a
f t
x
                                    ok <- noErrors
                                    if ok then do xs' <- mapWhileOK f xs
                                                  return (x' : xs')
                                          else return [x']

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

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