{-# 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
= Idris [String] -> (Err -> Idris [String]) -> Idris [String]
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 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
[(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)
(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
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)
[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 []
[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 ()
Err
_ -> 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
[String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
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 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
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 = 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
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']
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"