{-|
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 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 (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

           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 loadCode" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
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 ([(String, [String])] -> String
forall a. Show a => a -> String
show (((String, [ImportInfo]) -> (String, [String]))
-> [(String, [ImportInfo])] -> [(String, [String])]
forall a b. (a -> b) -> [a] -> [b]
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)) [(String, [ImportInfo])]
importlists))

           let ninputs :: [(Int, String)]
ninputs = [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [String]
inputs
           [(String, [IFileType])]
ifiles <- ((Int, String)
 -> StateT IState (ExceptT Err IO) (String, [IFileType]))
-> [(Int, String)]
-> StateT IState (ExceptT Err IO) [(String, [IFileType])]
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 (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)
                   [ModuleTree]
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 :: [IFileType]
ifiles = [ModuleTree] -> [IFileType]
getModuleFiles [ModuleTree]
modTree
                   Int -> String -> Idris ()
logParser Int
2 (String
"MODULE TREE : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ModuleTree] -> String
forall a. Show a => a -> String
show [ModuleTree]
modTree)
                   Int -> String -> Idris ()
logParser Int
2 (String
"RELOAD: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [IFileType] -> String
forall a. Show a => a -> String
show [IFileType]
ifiles)
                   Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ((IFileType -> Bool) -> [IFileType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all IFileType -> Bool
ibc [IFileType]
ifiles) Bool -> Bool -> Bool
|| Bool
loadCode) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
                        Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
False IBCPhase
IBC_Building ((IFileType -> Bool) -> [IFileType] -> [IFileType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (IFileType -> Bool) -> IFileType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
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
                   (String, [IFileType])
-> StateT IState (ExceptT Err IO) (String, [IFileType])
forall a. a -> StateT IState (ExceptT Err IO) a
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 (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
                         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 <- (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
                   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 ibcfiles" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [IFileType] -> String
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
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           [ExportIFace]
exports <- Idris [ExportIFace]
findExports

           case (Opt -> Maybe String) -> [Opt] -> [String]
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]
_  -> [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

           [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (((String, [IFileType]) -> String)
-> [(String, [IFileType])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, [IFileType]) -> String
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 (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
                  [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
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 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 IState
ist <- Idris IState
getIState
                      Int -> String -> Idris ()
logParser Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"tryLoad (keepstate, phase, f : fs)" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        (Bool, IBCPhase, [IFileType]) -> String
forall a. Show a => a -> String
show (Bool
keepstate, IBCPhase
phase, IFileType
f IFileType -> [IFileType] -> [IFileType]
forall a. a -> [a] -> [a]
: [IFileType]
fs)
                      let maxline :: Maybe Int
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
                      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 Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
keepstate) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist
                               IState
ist <- Idris IState
getIState
                               IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist { idris_tyinfodata = tidata,
                                                   idris_patdefs = 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 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 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
                                                  [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 (a
x' a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs')
                                          else [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 [a
x']

 = 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"