{-|
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 = 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
  = forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
       (do IState
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)
           [Opt]
opts <- Idris [Opt]
getCmdLine

           let loadCode :: Bool
loadCode = case forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getOutput [Opt]
opts of
                               [] -> Bool -> Bool
not (Opt
NoREPL forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)
                               [String]
_ -> Bool
True

           Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
"loadInputs loadCode" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
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

           [(String, [ImportInfo])]
importlists <- [(String, [ImportInfo])]
-> [String] -> Idris [(String, [ImportInfo])]
getImports [] [String]
inputs

           Int -> String -> Idris ()
logParser Int
1 (forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map (\(String
i,[ImportInfo]
m) -> (String
i, forall a b. (a -> b) -> [a] -> [b]
map ImportInfo -> String
import_path [ImportInfo]
m)) [(String, [ImportInfo])]
importlists))

           let ninputs :: [(Int, String)]
ninputs = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [String]
inputs
           [(String, [IFileType])]
ifiles <- forall {t} {a}.
(t -> StateT IState (ExceptT Err IO) a)
-> [t] -> StateT IState (ExceptT Err IO) [a]
mapWhileOK (\(Int
num, String
input) ->
                do IState -> Idris ()
putIState IState
ist
                   Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show String
"loadInputs (num, input)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
num, String
input)
                   [ModuleTree]
modTree <- [String]
-> [(String, [ImportInfo])] -> String -> Idris [ModuleTree]
buildTree
                                   (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. Int -> [a] -> [a]
take (Int
numforall a. Num a => a -> a -> a
-Int
1) [(Int, String)]
ninputs))
                                   [(String, [ImportInfo])]
importlists
                                   String
input
                   let ifiles :: [IFileType]
ifiles = [ModuleTree] -> [IFileType]
getModuleFiles [ModuleTree]
modTree
                   Int -> String -> Idris ()
logParser Int
2 (String
"MODULE TREE : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [ModuleTree]
modTree)
                   Int -> String -> Idris ()
logParser Int
2 (String
"RELOAD: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [IFileType]
ifiles)
                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all IFileType -> Bool
ibc [IFileType]
ifiles) Bool -> Bool -> Bool
|| Bool
loadCode) forall a b. (a -> b) -> a -> b
$
                        Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
False IBCPhase
IBC_Building (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IFileType -> Bool
ibc) [IFileType]
ifiles)
                   -- return the files that need rechecking
                   forall (m :: * -> *) a. Monad m => a -> m a
return (String
input, [IFileType]
ifiles))
                      [(Int, String)]
ninputs
           IState
inew <- Idris IState
getIState
           let tidata :: Ctxt TIData
tidata = IState -> Ctxt TIData
idris_tyinfodata IState
inew
           -- If it worked, load the whole thing from all the ibcs together
           case IState -> Maybe FC
errSpan IState
inew of
              Maybe FC
Nothing ->
                do IState -> Idris ()
putIState forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist { idris_tyinfodata :: Ctxt TIData
idris_tyinfodata = Ctxt TIData
tidata }
                   Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ String
"loadInputs ifiles" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(String, [IFileType])]
ifiles

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

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

                   Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
True (Bool -> IBCPhase
IBC_REPL Bool
True) [IFileType]
ibcfiles
              Maybe FC
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
           [ExportIFace]
exports <- Idris [ExportIFace]
findExports

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

           forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, [IFileType])]
ifiles))
        (\Err
e -> do IState
i <- Idris IState
getIState
                  case Err
e of
                    At FC
f Err
e' -> do FC -> Idris ()
setErrSpan FC
f
                                  FC -> OutputDoc -> Idris ()
iWarn FC
f forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
i Err
e'
                    Err
ProgramLineComment -> 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 forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
i Err
e
                  forall (m :: * -> *) a. Monad m => a -> m a
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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return ()
         tryLoad Bool
keepstate IBCPhase
phase (IFileType
f : [IFileType]
fs)
                 = do IState
ist <- Idris IState
getIState
                      Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ String
"tryLoad (keepstate, phase, f : fs)" forall a. [a] -> [a] -> [a]
++
                        forall a. Show a => a -> String
show (Bool
keepstate, IBCPhase
phase, IFileType
f forall a. a -> [a] -> [a]
: [IFileType]
fs)
                      let maxline :: Maybe Int
maxline
                            = case Maybe Int
toline of
                                Maybe Int
Nothing -> forall a. Maybe a
Nothing
                                Just Int
l -> case IFileType
f of
                                            IDR String
fn -> if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
fmatch String
fn) [String]
inputs
                                                         then forall a. a -> Maybe a
Just Int
l
                                                         else forall a. Maybe a
Nothing
                                            LIDR String
fn -> if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
fmatch String
fn) [String]
inputs
                                                          then forall a. a -> Maybe a
Just Int
l
                                                          else forall a. Maybe a
Nothing
                                            IFileType
_ -> forall a. Maybe a
Nothing
                      Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
loadFromIFile Bool
True IBCPhase
phase IFileType
f Maybe Int
maxline
                      IState
inew <- Idris IState
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 :: Ctxt TIData
tidata = IState -> Ctxt TIData
idris_tyinfodata IState
inew
                      let patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
patdefs = IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
inew
                      Bool
ok <- Idris Bool
noErrors
                      if Bool
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 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
keepstate) forall a b. (a -> b) -> a -> b
$ IState -> Idris ()
putIState forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist
                               IState
ist <- Idris IState
getIState
                               IState -> Idris ()
putIState forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist { idris_tyinfodata :: Ctxt TIData
idris_tyinfodata = Ctxt TIData
tidata,
                                                   idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs = Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
patdefs }
                               Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
keepstate IBCPhase
phase [IFileType]
fs
                          else Idris ()
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 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
         mapWhileOK t -> StateT IState (ExceptT Err IO) a
f (t
x : [t]
xs) = do a
x' <- t -> StateT IState (ExceptT Err IO) a
f t
x
                                    Bool
ok <- Idris Bool
noErrors
                                    if Bool
ok then do [a]
xs' <- (t -> StateT IState (ExceptT Err IO) a)
-> [t] -> StateT IState (ExceptT Err IO) [a]
mapWhileOK t -> StateT IState (ExceptT Err IO) a
f [t]
xs
                                                  forall (m :: * -> *) a. Monad m => a -> m a
return (a
x' forall a. a -> [a] -> [a]
: [a]
xs')
                                          else forall (m :: * -> *) a. Monad m => a -> m a
return [a
x']

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

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