{-# 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
= 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 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
[(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)
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
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)
[String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
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 ()
Err
_ -> do FC -> Idris ()
setErrSpan FC
emptyFC
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
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
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 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
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']
banner :: String
banner = 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"