{-# 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 4294
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs inputs :: [FilePath]
inputs toline :: Maybe Int
toline
= Idris [FilePath] -> (Err -> Idris [FilePath]) -> Idris [FilePath]
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do IState
ist <- Idris IState
getIState
[Opt]
opts <- Idris [Opt]
getCmdLine
let loadCode :: Bool
loadCode = case (Opt -> Maybe FilePath) -> [Opt] -> [FilePath]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe FilePath
getOutput [Opt]
opts of
[] -> Bool -> Bool
not (Opt
NoREPL Opt -> [Opt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)
_ -> Bool
True
Int -> FilePath -> Idris ()
logParser 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show "loadInputs loadCode" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Bool -> FilePath
forall a. Show a => a -> FilePath
show Bool
loadCode
[(FilePath, [ImportInfo])]
importlists <- [(FilePath, [ImportInfo])]
-> [FilePath] -> Idris [(FilePath, [ImportInfo])]
getImports [] [FilePath]
inputs
Int -> FilePath -> Idris ()
logParser 1 ([(FilePath, [FilePath])] -> FilePath
forall a. Show a => a -> FilePath
show (((FilePath, [ImportInfo]) -> (FilePath, [FilePath]))
-> [(FilePath, [ImportInfo])] -> [(FilePath, [FilePath])]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: FilePath
i,m :: [ImportInfo]
m) -> (FilePath
i, (ImportInfo -> FilePath) -> [ImportInfo] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ImportInfo -> FilePath
import_path [ImportInfo]
m)) [(FilePath, [ImportInfo])]
importlists))
let ninputs :: [(Int, FilePath)]
ninputs = [Int] -> [FilePath] -> [(Int, FilePath)]
forall a b. [a] -> [b] -> [(a, b)]
zip [1..] [FilePath]
inputs
[(FilePath, [IFileType])]
ifiles <- ((Int, FilePath)
-> StateT IState (ExceptT Err IO) (FilePath, [IFileType]))
-> [(Int, FilePath)]
-> StateT IState (ExceptT Err IO) [(FilePath, [IFileType])]
forall t a.
(t -> StateT IState (ExceptT Err IO) a)
-> [t] -> StateT IState (ExceptT Err IO) [a]
mapWhileOK (\(num :: Int
num, input :: FilePath
input) ->
do IState -> Idris ()
putIState IState
ist
Int -> FilePath -> Idris ()
logParser 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show "loadInputs (num, input)" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Int, FilePath) -> FilePath
forall a. Show a => a -> FilePath
show (Int
num, FilePath
input)
[ModuleTree]
modTree <- [FilePath]
-> [(FilePath, [ImportInfo])] -> FilePath -> Idris [ModuleTree]
buildTree
(((Int, FilePath) -> FilePath) -> [(Int, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Int, FilePath) -> FilePath
forall a b. (a, b) -> b
snd (Int -> [(Int, FilePath)] -> [(Int, FilePath)]
forall a. Int -> [a] -> [a]
take (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [(Int, FilePath)]
ninputs))
[(FilePath, [ImportInfo])]
importlists
FilePath
input
let ifiles :: [IFileType]
ifiles = [ModuleTree] -> [IFileType]
getModuleFiles [ModuleTree]
modTree
Int -> FilePath -> Idris ()
logParser 2 ("MODULE TREE : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [ModuleTree] -> FilePath
forall a. Show a => a -> FilePath
show [ModuleTree]
modTree)
Int -> FilePath -> Idris ()
logParser 2 ("RELOAD: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [IFileType] -> FilePath
forall a. Show a => a -> FilePath
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 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)
(FilePath, [IFileType])
-> StateT IState (ExceptT Err IO) (FilePath, [IFileType])
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
input, [IFileType]
ifiles))
[(Int, FilePath)]
ninputs
IState
inew <- Idris IState
getIState
let tidata :: Ctxt TIData
tidata = IState -> Ctxt TIData
idris_tyinfodata IState
inew
case IState -> Maybe FC
errSpan IState
inew of
Nothing ->
do IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
ist { idris_tyinfodata :: Ctxt TIData
idris_tyinfodata = Ctxt TIData
tidata }
Int -> FilePath -> Idris ()
logParser 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "loadInputs ifiles" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [(FilePath, [IFileType])] -> FilePath
forall a. Show a => a -> FilePath
show [(FilePath, [IFileType])]
ifiles
let fileToIFileType :: FilePath -> Idris IFileType
fileToIFileType :: FilePath -> Idris IFileType
fileToIFileType file :: FilePath
file = do
FilePath
ibcsd <- IState -> Idris FilePath
valIBCSubDir IState
ist
[FilePath]
ids <- FilePath -> Idris [FilePath]
rankedImportDirs FilePath
file
[FilePath] -> FilePath -> FilePath -> Idris IFileType
findImport [FilePath]
ids FilePath
ibcsd FilePath
file
[IFileType]
ibcfiles <- (FilePath -> Idris IFileType)
-> [FilePath] -> StateT IState (ExceptT Err IO) [IFileType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FilePath -> Idris IFileType
fileToIFileType [FilePath]
inputs
Int -> FilePath -> Idris ()
logParser 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show "loadInputs ibcfiles" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [IFileType] -> FilePath
forall a. Show a => a -> FilePath
show [IFileType]
ibcfiles
Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad Bool
True (Bool -> IBCPhase
IBC_REPL Bool
True) [IFileType]
ibcfiles
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[ExportIFace]
exports <- Idris [ExportIFace]
findExports
case (Opt -> Maybe FilePath) -> [Opt] -> [FilePath]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe FilePath
getOutput [Opt]
opts of
[] -> [Name] -> Idris [Name]
performUsageAnalysis ([ExportIFace] -> [Name]
getExpNames [ExportIFace]
exports)
_ -> [Name] -> Idris [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return []
[FilePath] -> Idris [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return (((FilePath, [IFileType]) -> FilePath)
-> [(FilePath, [IFileType])] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, [IFileType]) -> FilePath
forall a b. (a, b) -> a
fst [(FilePath, [IFileType])]
ifiles))
(\e :: Err
e -> do IState
i <- Idris IState
getIState
case Err
e of
At f :: FC
f e' :: 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'
ProgramLineComment -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> do FC -> Idris ()
setErrSpan FC
emptyFC
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
[FilePath] -> Idris [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
where
tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
tryLoad keepstate :: Bool
keepstate phase :: IBCPhase
phase [] = Idris ()
warnTotality Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
tryLoad keepstate :: Bool
keepstate phase :: IBCPhase
phase (f :: IFileType
f : fs :: [IFileType]
fs)
= do IState
ist <- Idris IState
getIState
Int -> FilePath -> Idris ()
logParser 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "tryLoad (keepstate, phase, f : fs)" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
(Bool, IBCPhase, [IFileType]) -> FilePath
forall a. Show a => a -> FilePath
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
Nothing -> Maybe Int
forall a. Maybe a
Nothing
Just l :: Int
l -> case IFileType
f of
IDR fn :: FilePath
fn -> if (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
fmatch FilePath
fn) [FilePath]
inputs
then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
else Maybe Int
forall a. Maybe a
Nothing
LIDR fn :: FilePath
fn -> if (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
fmatch FilePath
fn) [FilePath]
inputs
then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
else Maybe Int
forall a. Maybe a
Nothing
_ -> 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
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
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 :: 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 _ _) = Bool
True
ibc _ = Bool
False
fmatch :: FilePath -> FilePath -> Bool
fmatch ('.':'/':xs :: FilePath
xs) ys :: FilePath
ys = FilePath -> FilePath -> Bool
fmatch FilePath
xs FilePath
ys
fmatch xs :: FilePath
xs ('.':'/':ys :: FilePath
ys) = FilePath -> FilePath -> Bool
fmatch FilePath
xs FilePath
ys
fmatch xs :: FilePath
xs ys :: FilePath
ys = FilePath
xs FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
ys
mapWhileOK :: (t -> StateT IState (ExceptT Err IO) a)
-> [t] -> StateT IState (ExceptT Err IO) [a]
mapWhileOK f :: t -> StateT IState (ExceptT Err IO) a
f [] = [a] -> StateT IState (ExceptT Err IO) [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
mapWhileOK f :: t -> StateT IState (ExceptT Err IO) a
f (x :: t
x : xs :: [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 (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 (m :: * -> *) a. Monad m => a -> m a
return [a
x']
banner :: FilePath
banner = " ____ __ _ \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" / _/___/ /____(_)____ \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" / // __ / ___/ / ___/ Version " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
getIdrisVersion FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" /___/\\__,_/_/ /_/____/ Type :? for help \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"Idris is free software with ABSOLUTELY NO WARRANTY. \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"For details type :warranty."
warranty :: FilePath
warranty = "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"