{-# LANGUAGE CPP, FlexibleContexts, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}
module Idris.REPL
( idemodeStart
, startServer
, runClient
, process
, replSettings
, repl
, proofs
) where
import Control.Category
import Control.Concurrent
import Control.Concurrent.Async (race)
import Control.DeepSeq
import qualified Control.Exception as X
import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Except (runExceptT)
import Control.Monad.Trans.State.Strict (evalStateT, get, put)
import qualified Data.Binary as Binary
import qualified Data.ByteString.Base64 as Base64
import qualified Data.ByteString.Lazy as Lazy
import qualified Data.ByteString.UTF8 as UTF8
import Data.Char
import Data.Either (partitionEithers)
import Data.List hiding (group)
import Data.List.Split (splitOn)
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Version
import Idris.AbsSyntax
import Idris.Apropos (apropos, aproposModules)
import Idris.ASTUtils
import Idris.Colours hiding (colourise)
import Idris.Completion
import Idris.Core.Constraints
import Idris.Core.Evaluate
import Idris.Core.Execute (execute)
import Idris.Core.TT
import Idris.Core.Unify
import Idris.Core.WHNF
import Idris.DataOpts
import Idris.Delaborate
import Idris.Docs
import Idris.Docstrings (overview, renderDocTerm, renderDocstring)
import Idris.Elab.Clause
import Idris.Elab.Term
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import Idris.ErrReverse
import Idris.Help
import Idris.IBC
import qualified Idris.IdeMode as IdeMode
import Idris.IdrisDoc
import Idris.Info
import Idris.Inliner
import Idris.Interactive
import Idris.ModeCommon
import Idris.Options
import Idris.Output
import Idris.Parser hiding (indent)
import Idris.Prover
import Idris.REPL.Browse (namesInNS, namespacesInNS)
import Idris.REPL.Commands
import Idris.REPL.Parser
import Idris.Termination
import Idris.TypeSearch (searchByType)
import Idris.WhoCalls
import IRTS.CodegenCommon
import IRTS.Compiler
import Network.Socket hiding (defaultPort)
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding (id, (.), (<$>), (<>))
#else
import Prelude hiding (id, (.), (<$>))
#endif
import System.Console.Haskeline as H
import System.Directory
import System.Environment
import System.Exit
import System.FilePath (addExtension, dropExtension, splitExtension,
takeDirectory, takeExtension, (<.>), (</>))
import System.FSNotify (watchDir, withManager)
import System.FSNotify.Devel (allEvents, doAllEvents)
import System.IO
import System.Process
import Util.DynamicLinker
import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)
import Util.Pretty hiding ((</>))
import Util.System
import Version_idris (gitHash)
repl :: IState
-> [FilePath]
-> FilePath
-> InputT Idris ()
repl :: IState -> [FilePath] -> FilePath -> InputT Idris ()
repl IState
orig [FilePath]
mods FilePath
efile
=
do let quiet :: Bool
quiet = IOption -> Bool
opt_quiet (IState -> IOption
idris_options IState
orig)
IState
i <- StateT IState (ExceptT Err IO) IState -> InputT Idris IState
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT IState (ExceptT Err IO) IState
getIState
let colour :: Bool
colour = IState -> Bool
idris_colourRepl IState
i
let theme :: ColourTheme
theme = IState -> ColourTheme
idris_colourTheme IState
i
let mvs :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
mvs = IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i
let prompt :: FilePath
prompt = if Bool
quiet
then FilePath
""
else Bool
-> ColourTheme
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> FilePath
forall a b. Show a => Bool -> ColourTheme -> [(a, b)] -> FilePath
showMVs Bool
colour ColourTheme
theme [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
mvs FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
let str :: FilePath
str = [FilePath] -> FilePath
mkPrompt [FilePath]
mods FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
">" in
(if Bool
colour Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isWindows
then ColourTheme -> FilePath -> FilePath
colourisePrompt ColourTheme
theme FilePath
str
else FilePath
str) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" "
Maybe FilePath
x <- InputT Idris (Maybe FilePath)
-> InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath)
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
H.handleInterrupt (InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath)
forall a. InputT Idris a -> InputT Idris a
ctrlC (Maybe FilePath -> InputT Idris (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath -> InputT Idris (Maybe FilePath))
-> Maybe FilePath -> InputT Idris (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"")) (InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
H.withInterrupt (InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath))
-> InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> InputT Idris (Maybe FilePath)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
FilePath -> InputT m (Maybe FilePath)
getInputLine FilePath
prompt)
case Maybe FilePath
x of
Maybe FilePath
Nothing -> do StateT IState (ExceptT Err IO) () -> InputT Idris ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) () -> InputT Idris ())
-> StateT IState (ExceptT Err IO) () -> InputT Idris ()
forall a b. (a -> b) -> a -> b
$ Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
quiet) (FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Bye bye")
() -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just FilePath
input ->
do Maybe [FilePath]
ms <- InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
H.handleInterrupt (InputT Idris (Maybe [FilePath]) -> InputT Idris (Maybe [FilePath])
forall a. InputT Idris a -> InputT Idris a
ctrlC (Maybe [FilePath] -> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
mods))) (InputT Idris (Maybe [FilePath]) -> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
H.withInterrupt (InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath]))
-> InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath]))
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath
-> IState
-> [FilePath]
-> FilePath
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
processInput FilePath
input IState
orig [FilePath]
mods FilePath
efile)
case Maybe [FilePath]
ms of
Just [FilePath]
mods -> let efile' :: FilePath
efile' = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
efile ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
mods)
in IState -> [FilePath] -> FilePath -> InputT Idris ()
repl IState
orig [FilePath]
mods FilePath
efile'
Maybe [FilePath]
Nothing -> () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where ctrlC :: InputT Idris a -> InputT Idris a
ctrlC :: InputT Idris a -> InputT Idris a
ctrlC InputT Idris a
act = do StateT IState (ExceptT Err IO) () -> InputT Idris ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) () -> InputT Idris ())
-> StateT IState (ExceptT Err IO) () -> InputT Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Interrupted"
InputT Idris a
act
showMVs :: Bool -> ColourTheme -> [(a, b)] -> FilePath
showMVs Bool
c ColourTheme
thm [] = FilePath
""
showMVs Bool
c ColourTheme
thm [(a, b)]
ms = FilePath
"Holes: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Integer -> Bool -> ColourTheme -> [a] -> FilePath
forall t a.
(Eq t, Num t, Show a) =>
t -> Bool -> ColourTheme -> [a] -> FilePath
show' Integer
4 Bool
c ColourTheme
thm (((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
ms) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n"
show' :: t -> Bool -> ColourTheme -> [a] -> FilePath
show' t
0 Bool
c ColourTheme
thm [a]
ms = let l :: Int
l = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ms in
FilePath
"... ( + " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
l
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" other"
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then FilePath
")" else FilePath
"s)"
show' t
n Bool
c ColourTheme
thm [a
m] = Bool -> ColourTheme -> a -> FilePath
forall a. Show a => Bool -> ColourTheme -> a -> FilePath
showM Bool
c ColourTheme
thm a
m
show' t
n Bool
c ColourTheme
thm (a
m : [a]
ms) = Bool -> ColourTheme -> a -> FilePath
forall a. Show a => Bool -> ColourTheme -> a -> FilePath
showM Bool
c ColourTheme
thm a
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
", " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
t -> Bool -> ColourTheme -> [a] -> FilePath
show' (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) Bool
c ColourTheme
thm [a]
ms
showM :: Bool -> ColourTheme -> a -> FilePath
showM Bool
c ColourTheme
thm a
n = if Bool
c then ColourTheme -> FilePath -> FilePath
colouriseFun ColourTheme
thm (a -> FilePath
forall a. Show a => a -> FilePath
show a
n)
else a -> FilePath
forall a. Show a => a -> FilePath
show a
n
startServer :: PortNumber -> IState -> [FilePath] -> Idris ()
startServer :: PortNumber
-> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
startServer PortNumber
port IState
orig [FilePath]
fn_in = do ThreadId
tid <- IO ThreadId -> Idris ThreadId
forall a. IO a -> Idris a
runIO (IO ThreadId -> Idris ThreadId) -> IO ThreadId -> Idris ThreadId
forall a b. (a -> b) -> a -> b
$ IO () -> IO ThreadId
forkIO (PortNumber -> IO ()
forall a. PortNumber -> IO a
serverLoop PortNumber
port)
() -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where serverLoop :: PortNumber -> IO a
serverLoop PortNumber
port = IO a -> IO a
forall a. IO a -> IO a
withSocketsDo (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$
do Socket
sock <- PortNumber -> IO Socket
listenOnLocalhost PortNumber
port
FilePath -> IState -> Socket -> IO a
forall b. FilePath -> IState -> Socket -> IO b
loop FilePath
fn IState
orig { idris_colourRepl :: Bool
idris_colourRepl = Bool
False } Socket
sock
fn :: FilePath
fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
fn_in)
loop :: FilePath -> IState -> Socket -> IO b
loop FilePath
fn IState
ist Socket
sock
= do (Socket
s, SockAddr
_) <- Socket -> IO (Socket, SockAddr)
accept Socket
sock
Handle
h <- Socket -> IOMode -> IO Handle
socketToHandle Socket
s IOMode
ReadWriteMode
Handle -> TextEncoding -> IO ()
hSetEncoding Handle
h TextEncoding
utf8
FilePath
cmd <- Handle -> IO FilePath
hGetLine Handle
h
let isth :: IState
isth = case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
_ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Handle -> OutputMode
RawOutput Handle
h}
IdeMode Integer
n Handle
_ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
n Handle
h}
(IState
ist', FilePath
fn) <- IState
-> IState
-> Handle
-> FilePath
-> FilePath
-> IO (IState, FilePath)
processNetCmd IState
orig IState
isth Handle
h FilePath
fn FilePath
cmd
Handle -> IO ()
hClose Handle
h
FilePath -> IState -> Socket -> IO b
loop FilePath
fn IState
ist' Socket
sock
processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
IO (IState, FilePath)
processNetCmd :: IState
-> IState
-> Handle
-> FilePath
-> FilePath
-> IO (IState, FilePath)
processNetCmd IState
orig IState
i Handle
h FilePath
fn FilePath
cmd
= do Either Err (IState, FilePath)
res <- case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i FilePath
"(net)" FilePath
cmd of
Left ParseError
err -> Either Err (IState, FilePath) -> IO (Either Err (IState, FilePath))
forall (m :: * -> *) a. Monad m => a -> m a
return (Err -> Either Err (IState, FilePath)
forall a b. a -> Either a b
Left (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
" invalid command"))
Right (Right Command
c) -> ExceptT Err IO (IState, FilePath)
-> IO (Either Err (IState, FilePath))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Err IO (IState, FilePath)
-> IO (Either Err (IState, FilePath)))
-> ExceptT Err IO (IState, FilePath)
-> IO (Either Err (IState, FilePath))
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) (IState, FilePath)
-> IState -> ExceptT Err IO (IState, FilePath)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn Command
c) IState
i
Right (Left FilePath
err) -> Either Err (IState, FilePath) -> IO (Either Err (IState, FilePath))
forall (m :: * -> *) a. Monad m => a -> m a
return (Err -> Either Err (IState, FilePath)
forall a b. a -> Either a b
Left (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
err))
case Either Err (IState, FilePath)
res of
Right (IState, FilePath)
x -> (IState, FilePath) -> IO (IState, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState, FilePath)
x
Left Err
err -> do Handle -> FilePath -> IO ()
hPutStrLn Handle
h (Err -> FilePath
forall a. Show a => a -> FilePath
show Err
err)
(IState, FilePath) -> IO (IState, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState
i, FilePath
fn)
where
processNet :: FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn Command
Reload = FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn (FilePath -> Maybe Int -> Command
Load FilePath
fn Maybe Int
forall a. Maybe a
Nothing)
processNet FilePath
fn (Load FilePath
f Maybe Int
toline) =
do IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options :: IOption
idris_options = IState -> IOption
idris_options IState
i
, idris_colourTheme :: ColourTheme
idris_colourTheme = IState -> ColourTheme
idris_colourTheme IState
i
, idris_colourRepl :: Bool
idris_colourRepl = Bool
False
}
Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
True
Handle -> StateT IState (ExceptT Err IO) ()
setOutH Handle
h
Bool -> StateT IState (ExceptT Err IO) ()
setQuiet Bool
True
Int -> StateT IState (ExceptT Err IO) ()
setVerbose Int
0
[FilePath]
mods <- [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
f] Maybe Int
toline
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
(IState, FilePath)
-> StateT IState (ExceptT Err IO) (IState, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState
ist, FilePath
f)
processNet FilePath
fn Command
c = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
c
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
(IState, FilePath)
-> StateT IState (ExceptT Err IO) (IState, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState
ist, FilePath
fn)
setOutH :: Handle -> Idris ()
setOutH :: Handle -> StateT IState (ExceptT Err IO) ()
setOutH Handle
h =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
_ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Handle -> OutputMode
RawOutput Handle
h}
IdeMode Integer
n Handle
_ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
n Handle
h}
runClient :: Maybe PortNumber -> String -> IO ()
runClient :: Maybe PortNumber -> FilePath -> IO ()
runClient Maybe PortNumber
port FilePath
str = IO () -> IO ()
forall a. IO a -> IO a
withSocketsDo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let port' :: PortNumber
port' = PortNumber -> Maybe PortNumber -> PortNumber
forall a. a -> Maybe a -> a
fromMaybe PortNumber
defaultPort Maybe PortNumber
port
Socket
s <- Family -> SocketType -> ProtocolNumber -> IO Socket
socket Family
AF_INET SocketType
Stream ProtocolNumber
defaultProtocol
Either SomeException ()
res <- IO () -> IO (Either SomeException ())
forall e a. Exception e => IO a -> IO (Either e a)
X.try (Socket -> SockAddr -> IO ()
connect Socket
s (PortNumber -> HostAddress -> SockAddr
SockAddrInet PortNumber
port' (HostAddress -> SockAddr) -> HostAddress -> SockAddr
forall a b. (a -> b) -> a -> b
$ (Word8, Word8, Word8, Word8) -> HostAddress
tupleToHostAddress (Word8
127,Word8
0,Word8
0,Word8
1)))
case Either SomeException ()
res of
Right () -> do
Handle
h <- Socket -> IOMode -> IO Handle
socketToHandle Socket
s IOMode
ReadWriteMode
Handle -> TextEncoding -> IO ()
hSetEncoding Handle
h TextEncoding
utf8
Handle -> FilePath -> IO ()
hPutStrLn Handle
h FilePath
str
FilePath
resp <- FilePath -> Handle -> IO FilePath
hGetResp FilePath
"" Handle
h
FilePath -> IO ()
putStr FilePath
resp
Handle -> IO ()
hClose Handle
h
Left SomeException
err -> do
SomeException -> IO ()
connectionError SomeException
err
ExitCode -> IO ()
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
where hGetResp :: FilePath -> Handle -> IO FilePath
hGetResp FilePath
acc Handle
h = do Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
if Bool
eof then FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
acc
else do FilePath
l <- Handle -> IO FilePath
hGetLine Handle
h
FilePath -> Handle -> IO FilePath
hGetResp (FilePath
acc FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n") Handle
h
connectionError :: X.SomeException -> IO ()
connectionError :: SomeException -> IO ()
connectionError SomeException
_ =
FilePath -> IO ()
putStrLn FilePath
"Unable to connect to a running Idris repl"
initIdemodeSocket :: IO Handle
initIdemodeSocket :: IO Handle
initIdemodeSocket = do
(Socket
sock, PortNumber
port) <- IO (Socket, PortNumber)
listenOnLocalhostAnyPort
FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ PortNumber -> FilePath
forall a. Show a => a -> FilePath
show PortNumber
port
(Socket
s, SockAddr
_) <- Socket -> IO (Socket, SockAddr)
accept Socket
sock
Handle
h <- Socket -> IOMode -> IO Handle
socketToHandle Socket
s IOMode
ReadWriteMode
Handle -> TextEncoding -> IO ()
hSetEncoding Handle
h TextEncoding
utf8
Handle -> IO Handle
forall (m :: * -> *) a. Monad m => a -> m a
return Handle
h
idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()
idemodeStart :: Bool -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemodeStart Bool
s IState
orig [FilePath]
mods
= do Handle
h <- IO Handle -> Idris Handle
forall a. IO a -> Idris a
runIO (IO Handle -> Idris Handle) -> IO Handle -> Idris Handle
forall a b. (a -> b) -> a -> b
$ if Bool
s then IO Handle
initIdemodeSocket else Handle -> IO Handle
forall (m :: * -> *) a. Monad m => a -> m a
return Handle
stdout
Bool -> Handle -> StateT IState (ExceptT Err IO) ()
setIdeMode Bool
True Handle
h
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Handle -> NewlineMode -> IO ()
hSetNewlineMode Handle
h (NewlineMode :: Newline -> Newline -> NewlineMode
NewlineMode { inputNL :: Newline
inputNL = Newline
CRLF, outputNL :: Newline
outputNL = Newline
LF })
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode Integer
n Handle
h ->
do IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Int -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"protocol-version" Int
IdeMode.ideModeEpoch Integer
n
case [FilePath]
mods of
FilePath
a:[FilePath]
_ -> Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> StateT IState (ExceptT Err IO) ()
runIdeModeCommand Handle
h Integer
n IState
i FilePath
"" [] (FilePath -> Maybe Int -> IdeModeCommand
IdeMode.LoadFile FilePath
a Maybe Int
forall a. Maybe a
Nothing)
[FilePath]
_ -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Handle -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemode Handle
h IState
orig [FilePath]
mods
idemode :: Handle -> IState -> [FilePath] -> Idris ()
idemode :: Handle -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemode Handle
h IState
orig [FilePath]
mods
= do StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do let inh :: Handle
inh = if Handle
h Handle -> Handle -> Bool
forall a. Eq a => a -> a -> Bool
== Handle
stdout then Handle
stdin else Handle
h
Either Err Int
len' <- IO (Either Err Int) -> Idris (Either Err Int)
forall a. IO a -> Idris a
runIO (IO (Either Err Int) -> Idris (Either Err Int))
-> IO (Either Err Int) -> Idris (Either Err Int)
forall a b. (a -> b) -> a -> b
$ Handle -> IO (Either Err Int)
IdeMode.getLen Handle
inh
Int
len <- case Either Err Int
len' of
Left Err
err -> Err -> StateT IState (ExceptT Err IO) Int
forall a. Err -> Idris a
ierror Err
err
Right Int
n -> Int -> StateT IState (ExceptT Err IO) Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
FilePath
l <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ Handle -> Int -> FilePath -> IO FilePath
IdeMode.getNChar Handle
inh Int
len FilePath
""
(SExp
sexp, Integer
id) <- case FilePath -> Either Err (SExp, Integer)
IdeMode.parseMessage FilePath
l of
Left Err
err -> Err -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall a. Err -> Idris a
ierror Err
err
Right (SExp
sexp, Integer
id) -> (SExp, Integer) -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (SExp
sexp, Integer
id)
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_outputmode :: OutputMode
idris_outputmode = (Integer -> Handle -> OutputMode
IdeMode Integer
id Handle
h) }
StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do let fn :: FilePath
fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
mods)
case SExp -> Maybe IdeModeCommand
IdeMode.sexpToCommand SExp
sexp of
Just IdeModeCommand
cmd -> Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> StateT IState (ExceptT Err IO) ()
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods IdeModeCommand
cmd
Maybe IdeModeCommand
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"did not understand" )
(\Err
e -> do FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e))
(\Err
e -> do FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e)
Handle -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemode Handle
h IState
orig [FilePath]
mods
runIdeModeCommand :: Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeMode.IdeModeCommand
-> Idris ()
runIdeModeCommand :: Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> StateT IState (ExceptT Err IO) ()
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Interpret FilePath
cmd) =
do Bool
c <- Idris Bool
colourise
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i FilePath
"(input)" FilePath
cmd of
Left ParseError
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> (ParseError -> FilePath)
-> ParseError
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (ParseError -> Doc) -> ParseError -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Doc -> Doc
fixColour Bool
False (Doc -> Doc) -> (ParseError -> Doc) -> ParseError -> Doc
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ParseError -> Doc
parseErrorDoc (ParseError -> StateT IState (ExceptT Err IO) ())
-> ParseError -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ ParseError
err
Right (Right (Prove Bool
mode Name
n')) ->
StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Name -> Command
Prove Bool
mode Name
n')
FilePath -> StateT IState (ExceptT Err IO) ()
isetPrompt ([FilePath] -> FilePath
mkPrompt [FilePath]
mods)
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode Integer
n Handle
h ->
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath -> (SExp, FilePath) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return"
(FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath
"")
Integer
n
OutputMode
_ -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
(\Err
e -> do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
FilePath -> StateT IState (ExceptT Err IO) ()
isetPrompt ([FilePath] -> FilePath
mkPrompt [FilePath]
mods)
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode Integer
n Handle
h ->
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath -> FilePath -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"abandon-proof" FilePath
"Abandoned" Integer
n
OutputMode
_ -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderError (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
e)
Right (Right Command
cmd) -> StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(FilePath -> Command -> StateT IState (ExceptT Err IO) ()
idemodeProcess FilePath
fn Command
cmd)
(\Err
e -> StateT IState (ExceptT Err IO) IState
getIState StateT IState (ExceptT Err IO) IState
-> (IState -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderError (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> (IState -> Doc OutputAnnotation)
-> IState
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Err -> Doc OutputAnnotation)
-> Err -> IState -> Doc OutputAnnotation
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> Err -> Doc OutputAnnotation
pprintErr Err
e)
Right (Left FilePath
err) -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.REPLCompletions FilePath
str) =
do (FilePath
unused, [Completion]
compls) <- CompletionFunc Idris
replCompletion (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
str, FilePath
"")
let good :: SExp
good = [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
([FilePath], FilePath) -> SExp
forall a. SExpable a => a -> SExp
IdeMode.toSExp ((Completion -> FilePath) -> [Completion] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Completion -> FilePath
replacement [Completion]
compls,
FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
unused)]
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> SExp -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" SExp
good Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.LoadFile FilePath
filename Maybe Int
toline) =
do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
StateT IState (ExceptT Err IO) ()
clearErr
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options :: IOption
idris_options = IState -> IOption
idris_options IState
i,
idris_outputmode :: OutputMode
idris_outputmode = (Integer -> Handle -> OutputMode
IdeMode Integer
id Handle
h) }
[FilePath]
mods <- [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
filename] Maybe Int
toline
FilePath -> StateT IState (ExceptT Err IO) ()
isetPrompt ([FilePath] -> FilePath
mkPrompt [FilePath]
mods)
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
case (IState -> Maybe FC
errSpan IState
i) of
Maybe FC
Nothing -> let msg :: SExp
msg = SExp -> (FC -> SExp) -> Maybe FC -> SExp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
[SExp] -> SExp
IdeMode.SexpList []])
(\FC
fc -> [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
FC -> SExp
forall a. SExpable a => a -> SExp
IdeMode.toSExp FC
fc])
(IState -> Maybe FC
idris_parsedSpan IState
i)
in IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> SExp -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" SExp
msg Integer
id
Just FC
x -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"didn't load " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
filename
Handle -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemode Handle
h IState
orig [FilePath]
mods
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.TypeOf FilePath
name) =
case FilePath -> Either FilePath Name
splitName FilePath
name of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
"(idemode)"
(PTerm -> Command
Check (FC -> [FC] -> Name -> PTerm
PRef (FilePath -> (Int, Int) -> (Int, Int) -> FC
FC FilePath
"(idemode)" (Int
0,Int
0) (Int
0,Int
0)) [] Name
n))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.DocsFor FilePath
name WhatDocs
w) =
case IState -> FilePath -> Either ParseError Const
parseConst IState
orig FilePath
name of
Right Const
c -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
"(idemode)" (Either Name Const -> HowMuchDocs -> Command
DocStr (Const -> Either Name Const
forall a b. b -> Either a b
Right Const
c) (WhatDocs -> HowMuchDocs
howMuch WhatDocs
w))
Left ParseError
_ ->
case FilePath -> Either FilePath Name
splitName FilePath
name of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
"(idemode)" (Either Name Const -> HowMuchDocs -> Command
DocStr (Name -> Either Name Const
forall a b. a -> Either a b
Left Name
n) (WhatDocs -> HowMuchDocs
howMuch WhatDocs
w))
where howMuch :: WhatDocs -> HowMuchDocs
howMuch WhatDocs
IdeMode.Overview = HowMuchDocs
OverviewDocs
howMuch WhatDocs
IdeMode.Full = HowMuchDocs
FullDocs
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.CaseSplit Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
CaseSplitAt Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddClause Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddClauseFrom Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddProofClause Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddProofClauseFrom Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddMissing Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddMissing Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeWithBlock Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeWith Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeCaseBlock Int
line FilePath
name) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeCase Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.ProofSearch Bool
r Int
line FilePath
name [FilePath]
hints Maybe Int
depth) =
FilePath
-> Bool
-> Bool
-> Int
-> Name
-> [Name]
-> Maybe Int
-> StateT IState (ExceptT Err IO) ()
doProofSearch FilePath
fn Bool
False Bool
r Int
line (FilePath -> Name
sUN FilePath
name) ((FilePath -> Name) -> [FilePath] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Name
sUN [FilePath]
hints) Maybe Int
depth
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeLemma Int
line FilePath
name) =
case FilePath -> Either FilePath Name
splitName FilePath
name of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeLemma Bool
False Int
line Name
n)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Apropos FilePath
a) =
FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PkgName] -> FilePath -> Command
Apropos [] FilePath
a)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeModeCommand
IdeMode.GetOpts) =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let opts :: IOption
opts = IState -> IOption
idris_options IState
ist
let impshow :: Bool
impshow = IOption -> Bool
opt_showimp IOption
opts
let errCtxt :: Bool
errCtxt = IOption -> Bool
opt_errContext IOption
opts
let options :: (SExp, [(SExp, Bool)])
options = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
[(FilePath -> SExp
IdeMode.SymbolAtom FilePath
"show-implicits", Bool
impshow),
(FilePath -> SExp
IdeMode.SymbolAtom FilePath
"error-context", Bool
errCtxt)])
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, [(SExp, Bool)]) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, [(SExp, Bool)])
options Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.SetOpt Opt
IdeMode.ShowImpl Bool
b) =
do Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
b
let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", Bool
b)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, Bool) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, Bool)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.SetOpt Opt
IdeMode.ErrContext Bool
b) =
do Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
b
let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", Bool
b)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, Bool) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, Bool)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Metavariables Int
cols) =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let mvs :: [(Name, Int)]
mvs = [(Name, Int)] -> [(Name, Int)]
forall a. [a] -> [a]
reverse ([(Name, Int)] -> [(Name, Int)]) -> [(Name, Int)] -> [(Name, Int)]
forall a b. (a -> b) -> a -> b
$ [ (Name
n, Int
i)
| (Name
n, (Maybe Name
_, Int
i, [Name]
_, Bool
_, Bool
_)) <- IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist
, Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
primDefs)
]
let splitMvs :: [(Name, ([(Name, Type, PTerm)], Type, PTerm))]
splitMvs = [ (Name
n, ([(Name, Type, PTerm)]
premises, Type
concl, PTerm
tm))
| (Name
n, Int
i, Type
ty) <- IState -> [(Name, Int)] -> [(Name, Int, Type)]
mvTys IState
ist [(Name, Int)]
mvs
, let ([(Name, Type, PTerm)]
premises, Type
concl, PTerm
tm) = IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi IState
ist Int
i Type
ty]
let mvOutput :: [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))]
mvOutput = ((FilePath,
([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))
-> (FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))
-> [(FilePath,
([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))]
-> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))]
forall a b. (a -> b) -> [a] -> [b]
map (\(FilePath
n, ([(FilePath, FilePath, SpanList OutputAnnotation)]
hs, (FilePath, SpanList OutputAnnotation)
c)) -> (FilePath
n, [(FilePath, FilePath, SpanList OutputAnnotation)]
hs, (FilePath, SpanList OutputAnnotation)
c)) ([(FilePath,
([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))]
-> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))])
-> [(FilePath,
([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))]
-> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))]
forall a b. (a -> b) -> a -> b
$
(Name -> FilePath)
-> (([(Name, Type, PTerm)], Type, PTerm)
-> ([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))
-> [(Name, ([(Name, Type, PTerm)], Type, PTerm))]
-> [(FilePath,
([(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation)))]
forall b a b b. (b -> a) -> (b -> b) -> [(b, b)] -> [(a, b)]
mapPair Name -> FilePath
forall a. Show a => a -> FilePath
show
(\([(Name, Type, PTerm)]
hs, Type
c, PTerm
pc) ->
let bnd :: [Name]
bnd = [ Name
n | (Name
n,Type
_,PTerm
_) <- [(Name, Type, PTerm)]
hs ] in
let bnds :: [[Name]]
bnds = [Name] -> [[Name]]
forall a. [a] -> [[a]]
inits [Name]
bnd in
((([Name], (Name, Type, PTerm))
-> (FilePath, FilePath, SpanList OutputAnnotation))
-> [([Name], (Name, Type, PTerm))]
-> [(FilePath, FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\([Name]
bnd, (Name, Type, PTerm)
h) -> IState
-> [Name]
-> (Name, Type, PTerm)
-> (FilePath, FilePath, SpanList OutputAnnotation)
processPremise IState
ist [Name]
bnd (Name, Type, PTerm)
h)
([[Name]]
-> [(Name, Type, PTerm)] -> [([Name], (Name, Type, PTerm))]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Name]]
bnds [(Name, Type, PTerm)]
hs),
IState
-> [Name] -> Type -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Type
c PTerm
pc))
[(Name, ([(Name, Type, PTerm)], Type, PTerm))]
splitMvs
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath
-> (SExp,
[(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))])
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
(FilePath, SpanList OutputAnnotation))]
mvOutput) Integer
id
where mapPair :: (b -> a) -> (b -> b) -> [(b, b)] -> [(a, b)]
mapPair b -> a
f b -> b
g [(b, b)]
xs = [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((b, b) -> a) -> [(b, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (b -> a
f (b -> a) -> ((b, b) -> b) -> (b, b) -> a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (b, b) -> b
forall a b. (a, b) -> a
fst) [(b, b)]
xs) (((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b -> b
g (b -> b) -> ((b, b) -> b) -> (b, b) -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (b, b) -> b
forall a b. (a, b) -> b
snd) [(b, b)]
xs)
splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi IState
ist Int
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
rest) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
let ([(Name, Type, PTerm)]
hs, Type
c, PTerm
_) = IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi IState
ist (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
rest in
((Name
n, Type
t, IState
-> [PArg]
-> [(Name, Type)]
-> Type
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Type
t Bool
False Bool
False Bool
True)(Name, Type, PTerm)
-> [(Name, Type, PTerm)] -> [(Name, Type, PTerm)]
forall a. a -> [a] -> [a]
:[(Name, Type, PTerm)]
hs,
Type
c, IState
-> [PArg]
-> [(Name, Type)]
-> Type
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Type
c Bool
False Bool
False Bool
True)
splitPi IState
ist Int
i Type
tm = ([], Type
tm, IState
-> [PArg]
-> [(Name, Type)]
-> Type
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Type
tm Bool
False Bool
False Bool
True)
mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
mvTys IState
ist [(Name, Int)]
mvs = [ (Name
n, Int
i, Type
ty)
| (Name
n, Int
i) <- [(Name, Int)]
mvs
, Type
ty <- Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (((Name, Type) -> Type) -> Maybe (Name, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Type
forall n. TT n -> TT n
vToP (Type -> Type) -> ((Name, Type) -> Type) -> (Name, Type) -> Type
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Type) -> Type
forall a b. (a, b) -> b
snd) (Name -> Context -> Maybe (Name, Type)
lookupTyNameExact Name
n (IState -> Context
tt_ctxt IState
ist)))
]
render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
render :: IState
-> [Name] -> Type -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Type
t PTerm
pt =
let prettyT :: Doc OutputAnnotation
prettyT = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist)
([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
bnd (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False))
[]
(IState -> [FixDecl]
idris_infixes IState
ist)
PTerm
pt
in
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
cols (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
bnd (Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
take ([Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
bnd) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False))) Type
t) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
Doc OutputAnnotation
prettyT
processPremise :: IState
-> [Name]
-> (Name, Type, PTerm)
-> (String,
String,
SpanList OutputAnnotation)
processPremise :: IState
-> [Name]
-> (Name, Type, PTerm)
-> (FilePath, FilePath, SpanList OutputAnnotation)
processPremise IState
ist [Name]
bnd (Name
n, Type
t, PTerm
pt) =
let (FilePath
out, SpanList OutputAnnotation
spans) = IState
-> [Name] -> Type -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Type
t PTerm
pt in
(Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n , FilePath
out, SpanList OutputAnnotation
spans)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.WhoCalls FilePath
n) =
case FilePath -> Either FilePath Name
splitName FilePath
n of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> do [(Name, [Name])]
calls <- Name -> Idris [(Name, [Name])]
whoCalls Name
n
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let msg :: (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
((Name, [Name])
-> ((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)]))
-> [(Name, [Name])]
-> [((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n,[Name]
ns) -> (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist Name
n, (Name -> (FilePath, SpanList OutputAnnotation))
-> [Name] -> [(FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist) [Name]
ns)) [(Name, [Name])]
calls)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
msg Integer
id
where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist = SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Name -> SimpleDoc OutputAnnotation)
-> Name
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
1000 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Name -> Doc OutputAnnotation)
-> Name
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.CallsWho FilePath
n) =
case FilePath -> Either FilePath Name
splitName FilePath
n of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> do [(Name, [Name])]
calls <- Name -> Idris [(Name, [Name])]
callsWho Name
n
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let msg :: (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
((Name, [Name])
-> ((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)]))
-> [(Name, [Name])]
-> [((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n,[Name]
ns) -> (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist Name
n, (Name -> (FilePath, SpanList OutputAnnotation))
-> [Name] -> [(FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist) [Name]
ns)) [(Name, [Name])]
calls)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp,
[((FilePath, SpanList OutputAnnotation),
[(FilePath, SpanList OutputAnnotation)])])
msg Integer
id
where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist = SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Name -> SimpleDoc OutputAnnotation)
-> Name
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
1000 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Name -> Doc OutputAnnotation)
-> Name
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.BrowseNS FilePath
ns) =
case FilePath -> FilePath -> [FilePath]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn FilePath
"." FilePath
ns of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"No namespace provided"
[FilePath]
ns -> do [FilePath]
underNSs <- ([[FilePath]] -> [FilePath])
-> StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath])
-> ([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([FilePath] -> FilePath)
-> ([FilePath] -> [FilePath]) -> [FilePath] -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse FilePath
".") (StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath])
-> StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> StateT IState (ExceptT Err IO) [[FilePath]]
namespacesInNS [FilePath]
ns
[Name]
names <- [FilePath] -> Idris [Name]
namesInNS [FilePath]
ns
if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
underNSs Bool -> Bool -> Bool
&& [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
names
then FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Invalid or empty namespace"
else do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
[(FilePath, SpanList OutputAnnotation)]
underNs <- (Name
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation))
-> [Name]
-> StateT
IState (ExceptT Err IO) [(FilePath, SpanList OutputAnnotation)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
pn [Name]
names
let msg :: (SExp, ([FilePath], [(FilePath, SpanList OutputAnnotation)]))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", ([FilePath]
underNSs, [(FilePath, SpanList OutputAnnotation)]
underNs))
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp, ([FilePath], [(FilePath, SpanList OutputAnnotation)]))
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, ([FilePath], [(FilePath, SpanList OutputAnnotation)]))
msg Integer
id
where pn :: Name
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
pn Name
n =
do Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
(FilePath, SpanList OutputAnnotation)
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
forall (m :: * -> *) a. Monad m => a -> m a
return ((FilePath, SpanList OutputAnnotation)
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation))
-> (FilePath, SpanList OutputAnnotation)
-> StateT
IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
1000 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$
Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
case Name -> Context -> Maybe Type
lookupTyExact Name
n Context
ctxt of
Just Type
t ->
Doc OutputAnnotation
forall a. Doc a
space Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (IState -> Name -> Type -> Doc OutputAnnotation
pprintDelabTy' IState
ist Name
n Type
t))
Maybe Type
Nothing ->
Doc OutputAnnotation
forall a. Doc a
empty
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermNormalise [(Name, Bool)]
bnd Type
tm) =
do Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let tm' :: Type
tm' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
tm
ptm :: Doc OutputAnnotation
ptm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Type
tm')
(PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist)
[(Name, Bool)]
bnd
[]
(IState -> [FixDecl]
idris_infixes IState
ist)
(IState -> Type -> PTerm
delab IState
ist Type
tm'))
msg :: (SExp, (FilePath, SpanList OutputAnnotation))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
ptm)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp, (FilePath, SpanList OutputAnnotation))
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermShowImplicits [(Name, Bool)]
bnd Type
tm) =
Handle
-> Integer
-> [(Name, Bool)]
-> Bool
-> Type
-> StateT IState (ExceptT Err IO) ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
True Type
tm
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermNoImplicits [(Name, Bool)]
bnd Type
tm) =
Handle
-> Integer
-> [(Name, Bool)]
-> Bool
-> Type
-> StateT IState (ExceptT Err IO) ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
False Type
tm
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermElab [(Name, Bool)]
bnd Type
tm) =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let ptm :: Doc OutputAnnotation
ptm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Type
tm)
([Name] -> Type -> Doc OutputAnnotation
pprintTT (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
bnd) Type
tm)
msg :: (SExp, (FilePath, SpanList OutputAnnotation))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
70 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
ptm)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp, (FilePath, SpanList OutputAnnotation))
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.PrintDef FilePath
name) =
case FilePath -> Either FilePath Name
splitName FilePath
name of
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
Right Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
"(idemode)" (Name -> Command
PrintDef Name
n)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.ErrString Err
e) =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let out :: FilePath -> FilePath
out = SimpleDoc OutputAnnotation -> FilePath -> FilePath
forall a. SimpleDoc a -> FilePath -> FilePath
displayS (SimpleDoc OutputAnnotation -> FilePath -> FilePath)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> FilePath
-> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
60 (Doc OutputAnnotation -> FilePath -> FilePath)
-> Doc OutputAnnotation -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
e
msg :: (SExp, SExp)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath -> SExp
IdeMode.StringAtom (FilePath -> SExp) -> FilePath -> SExp
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
out FilePath
"")
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, SExp) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, SExp)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.ErrPPrint Err
e) =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let (FilePath
out, SpanList OutputAnnotation
spans) =
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
e
msg :: (SExp, FilePath, SpanList OutputAnnotation)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath
out, SpanList OutputAnnotation
spans)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp, FilePath, SpanList OutputAnnotation)
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, FilePath, SpanList OutputAnnotation)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes IdeModeCommand
IdeMode.GetIdrisVersion =
let idrisVersion :: ([Int], [FilePath])
idrisVersion = (Version -> [Int]
versionBranch Version
getIdrisVersionNoGit,
if Bool -> Bool
not (FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
gitHash)
then [FilePath
gitHash]
else [])
msg :: (SExp, ([Int], [FilePath]))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", ([Int], [FilePath])
idrisVersion)
in IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, ([Int], [FilePath])) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, ([Int], [FilePath]))
msg Integer
id
ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits :: Handle
-> Integer
-> [(Name, Bool)]
-> Bool
-> Type
-> StateT IState (ExceptT Err IO) ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
impl Type
tm =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let expl :: Doc OutputAnnotation
expl = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Type
tm)
(PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm ((IState -> PPOption
ppOptionIst IState
ist) { ppopt_impl :: Bool
ppopt_impl = Bool
impl })
[(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist)
(IState -> Type -> PTerm
delab IState
ist Type
tm))
msg :: (SExp, (FilePath, SpanList OutputAnnotation))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
(OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation))
-> Doc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
expl)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SExp, (FilePath, SpanList OutputAnnotation))
-> Integer
-> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id
splitName :: String -> Either String Name
splitName :: FilePath -> Either FilePath Name
splitName FilePath
s | FilePath
"{{{{{" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
s =
FilePath -> Either FilePath Name
forall b. Binary b => FilePath -> Either FilePath b
decode (FilePath -> Either FilePath Name)
-> FilePath -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
drop Int
5 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
drop Int
5 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
s
where decode :: FilePath -> Either FilePath b
decode FilePath
x =
case ByteString -> Either FilePath ByteString
Base64.decode (FilePath -> ByteString
UTF8.fromString FilePath
x) of
Left FilePath
err -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left FilePath
err
Right ByteString
ok ->
case ByteString
-> Either
(ByteString, ByteOffset, FilePath) (ByteString, ByteOffset, b)
forall a.
Binary a =>
ByteString
-> Either
(ByteString, ByteOffset, FilePath) (ByteString, ByteOffset, a)
Binary.decodeOrFail (ByteString -> ByteString
Lazy.fromStrict ByteString
ok) of
Left (ByteString, ByteOffset, FilePath)
_ -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left FilePath
"Bad binary instance for Name"
Right (ByteString
_, ByteOffset
_, b
n) -> b -> Either FilePath b
forall a b. b -> Either a b
Right b
n
splitName FilePath
s = case [FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [FilePath]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn FilePath
"." FilePath
s of
[] -> FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left (FilePath
"Didn't understand name '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'")
[FilePath
n] -> Name -> Either FilePath Name
forall a b. b -> Either a b
Right (Name -> Either FilePath Name)
-> (FilePath -> Name) -> FilePath -> Either FilePath Name
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Name
sUN (FilePath -> Either FilePath Name)
-> FilePath -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
unparen FilePath
n
(FilePath
n:[FilePath]
ns) -> Name -> Either FilePath Name
forall a b. b -> Either a b
Right (Name -> Either FilePath Name) -> Name -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN (FilePath -> FilePath
unparen FilePath
n)) [FilePath]
ns
where unparen :: FilePath -> FilePath
unparen FilePath
"" = FilePath
""
unparen (Char
'(':Char
x:FilePath
xs) | FilePath -> Char
forall a. [a] -> a
last FilePath
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' = FilePath -> FilePath
forall a. [a] -> [a]
init (Char
xChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)
unparen FilePath
str = FilePath
str
idemodeProcess :: FilePath -> Command -> Idris ()
idemodeProcess :: FilePath -> Command -> StateT IState (ExceptT Err IO) ()
idemodeProcess FilePath
fn Command
ShowVersion = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
ShowVersion
idemodeProcess FilePath
fn Command
Warranty = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Warranty
idemodeProcess FilePath
fn Command
Help = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Help
idemodeProcess FilePath
fn (RunShellCommand FilePath
cmd) =
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
":! is not currently supported in IDE mode."
idemodeProcess FilePath
fn (ChangeDirectory FilePath
f) =
do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (FilePath -> Command
ChangeDirectory FilePath
f)
FilePath
dir <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ IO FilePath
getCurrentDirectory
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"changed directory to " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
dir
idemodeProcess FilePath
fn (ModImport FilePath
f) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (FilePath -> Command
ModImport FilePath
f)
idemodeProcess FilePath
fn (Eval PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Eval PTerm
t)
idemodeProcess FilePath
fn (NewDefn [PDecl]
decls) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PDecl] -> Command
NewDefn [PDecl]
decls)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
"defined"
idemodeProcess FilePath
fn (Undefine [Name]
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([Name] -> Command
Undefine [Name]
n)
idemodeProcess FilePath
fn (ExecVal PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
ExecVal PTerm
t)
idemodeProcess FilePath
fn (Check (PRef FC
x [FC]
hls Name
n)) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Check (FC -> [FC] -> Name -> PTerm
PRef FC
x [FC]
hls Name
n))
idemodeProcess FilePath
fn (Check PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Check PTerm
t)
idemodeProcess FilePath
fn (Core PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Core PTerm
t)
idemodeProcess FilePath
fn (DocStr Either Name Const
n HowMuchDocs
w) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Either Name Const -> HowMuchDocs -> Command
DocStr Either Name Const
n HowMuchDocs
w)
idemodeProcess FilePath
fn Command
Universes = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Universes
idemodeProcess FilePath
fn (Defn Name
n) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
Defn Name
n)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (TotCheck Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
TotCheck Name
n)
idemodeProcess FilePath
fn (DebugInfo Name
n) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
DebugInfo Name
n)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (Search [PkgName]
ps PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PkgName] -> PTerm -> Command
Search [PkgName]
ps PTerm
t)
idemodeProcess FilePath
fn (Spec PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Spec PTerm
t)
idemodeProcess FilePath
fn (ShowProof Name
n') = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
ShowProof Name
n')
idemodeProcess FilePath
fn (WHNF PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
WHNF PTerm
t)
idemodeProcess FilePath
fn (TestInline PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
TestInline PTerm
t)
idemodeProcess FilePath
fn (Execute PTerm
t) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Execute PTerm
t)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (Compile Codegen
codegen FilePath
f) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Codegen -> FilePath -> Command
Compile Codegen
codegen FilePath
f)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (LogLvl Int
i) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Int -> Command
LogLvl Int
i)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (Pattelab PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Pattelab PTerm
t)
idemodeProcess FilePath
fn (Missing Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
Missing Name
n)
idemodeProcess FilePath
fn (DynamicLink FilePath
l) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (FilePath -> Command
DynamicLink FilePath
l)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn Command
ListDynamic = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
ListDynamic
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn Command
Metavars = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Metavars
idemodeProcess FilePath
fn (SetOpt Opt
ErrContext) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ErrContext)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (UnsetOpt Opt
ErrContext) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ErrContext)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (SetOpt Opt
ShowImpl) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ShowImpl)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (UnsetOpt Opt
ShowImpl) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ShowImpl)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (SetOpt Opt
ShowOrigErr) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ShowOrigErr)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (UnsetOpt Opt
ShowOrigErr) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ShowOrigErr)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (SetOpt Opt
x) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
x)
idemodeProcess FilePath
fn (UnsetOpt Opt
x) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
x)
idemodeProcess FilePath
fn (CaseSplitAt Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
CaseSplitAt Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (AddProofClauseFrom Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddProofClauseFrom Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (AddClauseFrom Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddClauseFrom Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (AddMissing Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddMissing Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (MakeWith Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeWith Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (MakeCase Bool
False Int
pos Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeCase Bool
False Int
pos Name
str)
idemodeProcess FilePath
fn (DoProofSearch Bool
False Bool
r Int
pos Name
str [Name]
xs) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Bool -> Int -> Name -> [Name] -> Command
DoProofSearch Bool
False Bool
r Int
pos Name
str [Name]
xs)
idemodeProcess FilePath
fn (SetConsoleWidth ConsoleWidth
w) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (ConsoleWidth -> Command
SetConsoleWidth ConsoleWidth
w)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (SetPrinterDepth Maybe Int
d) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Maybe Int -> Command
SetPrinterDepth Maybe Int
d)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (Apropos [PkgName]
pkg FilePath
a) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PkgName] -> FilePath -> Command
Apropos [PkgName]
pkg FilePath
a)
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
""
idemodeProcess FilePath
fn (Browse [FilePath]
ns) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([FilePath] -> Command
Browse [FilePath]
ns)
idemodeProcess FilePath
fn (WhoCalls Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
WhoCalls Name
n)
idemodeProcess FilePath
fn (CallsWho Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
CallsWho Name
n)
idemodeProcess FilePath
fn (PrintDef Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
PrintDef Name
n)
idemodeProcess FilePath
fn (PPrint OutputFmt
fmt Int
n PTerm
tm) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (OutputFmt -> Int -> PTerm -> Command
PPrint OutputFmt
fmt Int
n PTerm
tm)
idemodeProcess FilePath
fn Command
_ = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"command not recognized or not supported"
mkPrompt :: [FilePath] -> FilePath
mkPrompt [] = FilePath
"Idris"
mkPrompt [FilePath
x] = FilePath
"*" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
dropExtension FilePath
x
mkPrompt (FilePath
x:[FilePath]
xs) = FilePath
"*" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
dropExtension FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
mkPrompt [FilePath]
xs
lit :: FilePath -> Bool
lit FilePath
f = case FilePath -> (FilePath, FilePath)
splitExtension FilePath
f of
(FilePath
_, FilePath
".lidr") -> Bool
True
(FilePath, FilePath)
_ -> Bool
False
reload :: IState -> [FilePath] -> Idris (Maybe [FilePath])
reload :: IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs = do
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options :: IOption
idris_options = IState -> IOption
idris_options IState
i
, idris_colourTheme :: ColourTheme
idris_colourTheme = IState -> ColourTheme
idris_colourTheme IState
i
, imported :: [FilePath]
imported = IState -> [FilePath]
imported IState
i
}
StateT IState (ExceptT Err IO) ()
clearErr
([FilePath] -> Maybe [FilePath])
-> Idris [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just (Idris [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath]))
-> Idris [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a b. (a -> b) -> a -> b
$ [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath]
inputs Maybe Int
forall a. Maybe a
Nothing
watch :: IState -> [FilePath] -> Idris (Maybe [FilePath])
watch :: IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs = do
Either FilePath FilePath
resp <- IO (Either FilePath FilePath) -> Idris (Either FilePath FilePath)
forall a. IO a -> Idris a
runIO (IO (Either FilePath FilePath) -> Idris (Either FilePath FilePath))
-> IO (Either FilePath FilePath)
-> Idris (Either FilePath FilePath)
forall a b. (a -> b) -> a -> b
$ do
let dirs :: [FilePath]
dirs = [FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a]
nub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
takeDirectory [FilePath]
inputs
Set FilePath
inputSet <- ([FilePath] -> Set FilePath) -> IO [FilePath] -> IO (Set FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
S.fromList (IO [FilePath] -> IO (Set FilePath))
-> IO [FilePath] -> IO (Set FilePath)
forall a b. (a -> b) -> a -> b
$ (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FilePath -> IO FilePath
canonicalizePath [FilePath]
inputs
MVar FilePath
signal <- IO (MVar FilePath)
forall a. IO (MVar a)
newEmptyMVar
(WatchManager -> IO (Either FilePath FilePath))
-> IO (Either FilePath FilePath)
forall a. (WatchManager -> IO a) -> IO a
withManager ((WatchManager -> IO (Either FilePath FilePath))
-> IO (Either FilePath FilePath))
-> (WatchManager -> IO (Either FilePath FilePath))
-> IO (Either FilePath FilePath)
forall a b. (a -> b) -> a -> b
$ \WatchManager
mgr -> do
[FilePath] -> (FilePath -> IO (IO ())) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [FilePath]
dirs ((FilePath -> IO (IO ())) -> IO ())
-> (FilePath -> IO (IO ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FilePath
dir ->
WatchManager -> FilePath -> ActionPredicate -> Action -> IO (IO ())
watchDir WatchManager
mgr FilePath
dir ((FilePath -> Bool) -> ActionPredicate
allEvents ((FilePath -> Bool) -> ActionPredicate)
-> (FilePath -> Bool) -> ActionPredicate
forall a b. (a -> b) -> a -> b
$ (FilePath -> Set FilePath -> Bool)
-> Set FilePath -> FilePath -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set FilePath
inputSet) ((FilePath -> IO ()) -> Action
forall (m :: * -> *).
Monad m =>
(FilePath -> m ()) -> Event -> m ()
doAllEvents ((FilePath -> IO ()) -> Action) -> (FilePath -> IO ()) -> Action
forall a b. (a -> b) -> a -> b
$ MVar FilePath -> FilePath -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar FilePath
signal)
IO FilePath -> IO FilePath -> IO (Either FilePath FilePath)
forall a b. IO a -> IO b -> IO (Either a b)
race IO FilePath
getLine (MVar FilePath -> IO FilePath
forall a. MVar a -> IO a
takeMVar MVar FilePath
signal)
case Either FilePath FilePath
resp of
Left FilePath
_ -> Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
Right FilePath
_ -> IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs
processInput :: String ->
IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])
processInput :: FilePath
-> IState
-> [FilePath]
-> FilePath
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
processInput FilePath
cmd IState
orig [FilePath]
inputs FilePath
efile
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let opts :: IOption
opts = IState -> IOption
idris_options IState
i
let quiet :: Bool
quiet = IOption -> Bool
opt_quiet IOption
opts
let fn :: FilePath
fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
inputs)
case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i FilePath
"(input)" FilePath
cmd of
Left ParseError
err -> [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs Maybe [FilePath]
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ParseError -> StateT IState (ExceptT Err IO) ()
forall w. Message w => w -> StateT IState (ExceptT Err IO) ()
emitWarning ParseError
err
Right (Right Command
Reload) ->
IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs
Right (Right Command
Watch) ->
if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
inputs then
do FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"No loaded files to watch."
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
else
do FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
efile
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Watching for .idr changes in " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
inputs FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
", press enter to cancel."
IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs
Right (Right (Load FilePath
f Maybe Int
toline)) ->
do IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options :: IOption
idris_options = IState -> IOption
idris_options IState
i
, idris_colourTheme :: ColourTheme
idris_colourTheme = IState -> ColourTheme
idris_colourTheme IState
i
}
StateT IState (ExceptT Err IO) ()
clearErr
[FilePath]
mod <- [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
f] Maybe Int
toline
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
mod)
Right (Right (ModImport FilePath
f)) ->
do StateT IState (ExceptT Err IO) ()
clearErr
Maybe FilePath
fmod <- FilePath -> IBCPhase -> Idris (Maybe FilePath)
loadModule FilePath
f (Bool -> IBCPhase
IBC_REPL Bool
True)
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just ([FilePath]
inputs [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
-> (FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:[]) Maybe FilePath
fmod))
Right (Right Command
Edit) -> do
FilePath -> IState -> StateT IState (ExceptT Err IO) ()
edit FilePath
efile IState
orig
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
Right (Right Command
Proofs) -> [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs Maybe [FilePath]
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IState -> StateT IState (ExceptT Err IO) ()
proofs IState
orig
Right (Right Command
Quit) -> Maybe [FilePath]
forall a. Maybe a
Nothing Maybe [FilePath]
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
quiet) (FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Bye bye")
Right (Right Command
cmd ) -> do StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
cmd)
(\Err
e -> do FilePath
msg <- Err -> Idris FilePath
showErr Err
e ; FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
msg)
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
Right (Left FilePath
err) -> do IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn FilePath
err
Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
resolveProof :: Name -> Idris Name
resolveProof :: Name -> Idris Name
resolveProof Name
n'
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
Context
ctxt <- Idris Context
getContext
Name
n <- case Name -> Context -> [Name]
lookupNames Name
n' Context
ctxt of
[Name
x] -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
[] -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
[Name]
ns -> Err -> Idris Name
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts [Name]
ns)
Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
removeProof :: Name -> Idris ()
removeProof :: Name -> StateT IState (ExceptT Err IO) ()
removeProof Name
n =
do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let proofs :: [(Name, (Bool, [FilePath]))]
proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
let ps :: [(Name, (Bool, [FilePath]))]
ps = ((Name, (Bool, [FilePath])) -> Bool)
-> [(Name, (Bool, [FilePath]))] -> [(Name, (Bool, [FilePath]))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n) (Name -> Bool)
-> ((Name, (Bool, [FilePath])) -> Name)
-> (Name, (Bool, [FilePath]))
-> Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, (Bool, [FilePath])) -> Name
forall a b. (a, b) -> a
fst) [(Name, (Bool, [FilePath]))]
proofs
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
i { proof_list :: [(Name, (Bool, [FilePath]))]
proof_list = [(Name, (Bool, [FilePath]))]
ps }
edit :: FilePath -> IState -> Idris ()
edit :: FilePath -> IState -> StateT IState (ExceptT Err IO) ()
edit FilePath
"" IState
orig = FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Nothing to edit"
edit FilePath
f IState
orig
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
[(FilePath, FilePath)]
env <- IO [(FilePath, FilePath)] -> Idris [(FilePath, FilePath)]
forall a. IO a -> Idris a
runIO IO [(FilePath, FilePath)]
getEnvironment
let editor :: FilePath
editor = [(FilePath, FilePath)] -> FilePath
getEditor [(FilePath, FilePath)]
env
let line :: FilePath
line = case IState -> Maybe FC
errSpan IState
i of
Just FC
l -> Char
'+' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Int -> FilePath
forall a. Show a => a -> FilePath
show ((Int, Int) -> Int
forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_start FC
l))
Maybe FC
Nothing -> FilePath
""
let cmdLine :: FilePath
cmdLine = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
" " [FilePath
editor, FilePath
line, FilePath -> FilePath
fixName FilePath
f]
IO ExitCode -> Idris ExitCode
forall a. IO a -> Idris a
runIO (IO ExitCode -> Idris ExitCode) -> IO ExitCode -> Idris ExitCode
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ExitCode
system FilePath
cmdLine
StateT IState (ExceptT Err IO) ()
clearErr
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options :: IOption
idris_options = IState -> IOption
idris_options IState
i
, idris_colourTheme :: ColourTheme
idris_colourTheme = IState -> ColourTheme
idris_colourTheme IState
i
}
[FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
f] Maybe Int
forall a. Maybe a
Nothing
StateT IState (ExceptT Err IO) ()
iucheck
() -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where getEditor :: [(FilePath, FilePath)] -> FilePath
getEditor [(FilePath, FilePath)]
env | Just FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"EDITOR" [(FilePath, FilePath)]
env = FilePath
ed
| Just FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"VISUAL" [(FilePath, FilePath)]
env = FilePath
ed
| Bool
otherwise = FilePath
"vi"
fixName :: FilePath -> FilePath
fixName FilePath
file | (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath
takeExtension FilePath
file) FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".lidr", FilePath
".idr"] = FilePath -> FilePath
quote FilePath
file
| Bool
otherwise = FilePath -> FilePath
quote (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath
addExtension FilePath
file FilePath
"idr"
where
quoteChar :: Char
quoteChar = if Bool
isWindows then Char
'"' else Char
'\''
quote :: FilePath -> FilePath
quote FilePath
s = [Char
quoteChar] FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Char
quoteChar]
proofs :: IState -> Idris ()
proofs :: IState -> StateT IState (ExceptT Err IO) ()
proofs IState
orig
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let ps :: [(Name, (Bool, [FilePath]))]
ps = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
case [(Name, (Bool, [FilePath]))]
ps of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"No proofs available"
[(Name, (Bool, [FilePath]))]
_ -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Proofs:\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ([Name] -> FilePath
forall a. Show a => a -> FilePath
show ([Name] -> FilePath) -> [Name] -> FilePath
forall a b. (a -> b) -> a -> b
$ ((Name, (Bool, [FilePath])) -> Name)
-> [(Name, (Bool, [FilePath]))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, [FilePath])) -> Name
forall a b. (a, b) -> a
fst [(Name, (Bool, [FilePath]))]
ps)
insertScript :: String -> [String] -> [String]
insertScript :: FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
prf [] = FilePath
"\n---------- Proofs ----------" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
"" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath
prf]
insertScript FilePath
prf (p :: FilePath
p@FilePath
"---------- Proofs ----------" : FilePath
"" : [FilePath]
xs)
= FilePath
p FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
"" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
prf FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
xs
insertScript FilePath
prf (FilePath
x : [FilePath]
xs) = FilePath
x FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
prf [FilePath]
xs
process :: FilePath -> Command -> Idris ()
process :: FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Help = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
displayHelp
process FilePath
fn Command
ShowVersion = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
getIdrisVersion
process FilePath
fn Command
Warranty = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
warranty
process FilePath
fn (RunShellCommand FilePath
cmd) = IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ExitCode
system FilePath
cmd IO ExitCode -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
process FilePath
fn (ChangeDirectory FilePath
f)
= do IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
setCurrentDirectory FilePath
f
() -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
process FilePath
fn (ModImport FilePath
f) = do Maybe FilePath
fmod <- FilePath -> IBCPhase -> Idris (Maybe FilePath)
loadModule FilePath
f (Bool -> IBCPhase
IBC_REPL Bool
True)
case Maybe FilePath
fmod of
Just FilePath
pr -> FilePath -> StateT IState (ExceptT Err IO) ()
isetPrompt FilePath
pr
Maybe FilePath
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Can't find import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
process FilePath
fn (Eval PTerm
t)
= StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> Idris a
withErrorReflection (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
do Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser Int
5 (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ PTerm -> FilePath
forall a. Show a => a -> FilePath
show PTerm
t
StateT IState (ExceptT Err IO) IState
getIState StateT IState (ExceptT Err IO) IState
-> (IState -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IState -> PTerm -> StateT IState (ExceptT Err IO) ())
-> PTerm -> IState -> StateT IState (ExceptT Err IO) ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> PTerm -> StateT IState (ExceptT Err IO) ()
warnDisamb PTerm
t
(Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Context
ctxt <- Idris Context
getContext
let tm' :: Type
tm' = Type -> Type
perhapsForce (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Context -> Env -> [Name] -> Type -> Type
normaliseBlocking Context
ctxt []
[FilePath -> Name
sUN FilePath
"foreign",
FilePath -> Name
sUN FilePath
"prim_read",
FilePath -> Name
sUN FilePath
"prim_write"]
Type
tm
let ty' :: Type
ty' = Type -> Type
perhapsForce (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty
(Context -> Context) -> StateT IState (ExceptT Err IO) ()
updateContext (Name -> Def -> Context -> Context
addCtxtDef (FilePath -> Name
sUN FilePath
"it") (Type -> Type -> Def
Function Type
ty' Type
tm'))
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser Int
3 (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Raw: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Type, Type) -> FilePath
forall a. Show a => a -> FilePath
show (Type
tm', Type
ty')
Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser Int
10 (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Debug: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Env -> Type -> FilePath
forall a.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> FilePath
showEnvDbg [] Type
tm'
let tmDoc :: Doc OutputAnnotation
tmDoc = IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist Type
tm'
tyDoc :: Doc OutputAnnotation
tyDoc = IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist (IState -> Type -> Type
errReverse IState
ist Type
ty')
Doc OutputAnnotation
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iPrintTermWithType Doc OutputAnnotation
tmDoc Doc OutputAnnotation
tyDoc
where perhapsForce :: Type -> Type
perhapsForce Type
tm | Int -> Type -> Bool
termSmallerThan Int
100 Type
tm = Type -> Type
forall a. NFData a => a -> a
force Type
tm
| Bool
otherwise = Type
tm
process FilePath
fn (NewDefn [PDecl]
decls) = do
Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser Int
3 (FilePath
"Defining names using these decls: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Doc OutputAnnotation -> FilePath
forall a. Show a => a -> FilePath
show (PPOption -> [PDecl] -> Doc OutputAnnotation
showDecls PPOption
verbosePPOption [PDecl]
decls))
([PDecl] -> StateT IState (ExceptT Err IO) ())
-> [[PDecl]] -> StateT IState (ExceptT Err IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [PDecl] -> StateT IState (ExceptT Err IO) ()
defineName [[PDecl]]
namedGroups where
namedGroups :: [[PDecl]]
namedGroups = (PDecl -> PDecl -> Bool) -> [PDecl] -> [[PDecl]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\PDecl
d1 PDecl
d2 -> PDecl -> Maybe Name
getName PDecl
d1 Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== PDecl -> Maybe Name
getName PDecl
d2) [PDecl]
decls
getName :: PDecl -> Maybe Name
getName :: PDecl -> Maybe Name
getName (PTy Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
opts Name
name FC
_ PTerm
ty) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
getName (PClauses FC
fc FnOpts
opts Name
name (PClause' PTerm
clause:[PClause' PTerm]
clauses)) = Name -> Maybe Name
forall a. a -> Maybe a
Just (PClause' PTerm -> Name
forall t. PClause' t -> Name
getClauseName PClause' PTerm
clause)
getName (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc DataOpts
opts PData' PTerm
dataDecl) = Name -> Maybe Name
forall a. a -> Maybe a
Just (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
dataDecl)
getName (PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc [(Name, PTerm)]
constraints Name
name FC
nfc [(Name, FC, PTerm)]
parms [(Name, Docstring (Either Err PTerm))]
parmdocs [(Name, FC)]
fds [PDecl]
decls Maybe (Name, FC)
_ Docstring (Either Err PTerm)
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
getName PDecl
_ = Maybe Name
forall a. Maybe a
Nothing
getClauseName :: PClause' t -> Name
getClauseName (PClause FC
fc Name
name t
whole [t]
with t
rhs [PDecl' t]
whereBlock) = Name
name
getClauseName (PWith FC
fc Name
name t
whole [t]
with t
rhs Maybe (Name, FC)
pn [PDecl' t]
whereBlock) = Name
name
defineName :: [PDecl] -> Idris ()
defineName :: [PDecl] -> StateT IState (ExceptT Err IO) ()
defineName (tyDecl :: PDecl
tyDecl@(PTy Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
opts Name
name FC
_ PTerm
ty) : [PDecl]
decls) = do
ElabWhat -> ElabInfo -> PDecl -> StateT IState (ExceptT Err IO) ()
elabDecl ElabWhat
EAll ElabInfo
info PDecl
tyDecl
ElabInfo
-> FC
-> FnOpts
-> Name
-> [PClause' PTerm]
-> StateT IState (ExceptT Err IO) ()
elabClauses ElabInfo
info FC
fc FnOpts
opts Name
name ((PDecl -> [PClause' PTerm]) -> [PDecl] -> [PClause' PTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [PClause' PTerm]
forall t. PDecl' t -> [PClause' t]
getClauses [PDecl]
decls)
Maybe Name -> StateT IState (ExceptT Err IO) ()
setReplDefined (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name)
defineName [PClauses FC
fc FnOpts
opts Name
_ [PClause' PTerm
clause]] = do
let pterm :: PTerm
pterm = PClause' PTerm -> PTerm
getRHS PClause' PTerm
clause
(Type
tm,Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal ElabInfo
info ElabMode
ERHS PTerm
pterm
Context
ctxt <- Idris Context
getContext
let tm' :: Type
tm' = Type -> Type
forall a. NFData a => a -> a
force (Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
tm)
let ty' :: Type
ty' = Type -> Type
forall a. NFData a => a -> a
force (Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty)
(Context -> Context) -> StateT IState (ExceptT Err IO) ()
updateContext (Name -> Def -> Context -> Context
addCtxtDef (PClause' PTerm -> Name
forall t. PClause' t -> Name
getClauseName PClause' PTerm
clause) (Type -> Type -> Def
Function Type
ty' Type
tm'))
Maybe Name -> StateT IState (ExceptT Err IO) ()
setReplDefined (Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ PClause' PTerm -> Name
forall t. PClause' t -> Name
getClauseName PClause' PTerm
clause)
defineName (PClauses{} : [PDecl]
_) = TC () -> StateT IState (ExceptT Err IO) ()
forall a. TC a -> Idris a
tclift (TC () -> StateT IState (ExceptT Err IO) ())
-> TC () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Only one function body is allowed without a type declaration.")
defineName (PFix FC
fc Fixity
fixity [FilePath]
strs : [PDecl]
defns) = do
Field IState [FixDecl]
-> ([FixDecl] -> [FixDecl]) -> StateT IState (ExceptT Err IO) ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [FixDecl]
idris_fixities ((FilePath -> FixDecl) -> [FilePath] -> [FixDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Fixity -> FilePath -> FixDecl
Fix Fixity
fixity) [FilePath]
strs [FixDecl] -> [FixDecl] -> [FixDecl]
forall a. [a] -> [a] -> [a]
++)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([PDecl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PDecl]
defns) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [PDecl] -> StateT IState (ExceptT Err IO) ()
defineName [PDecl]
defns
defineName (PSyntax FC
_ Syntax
syntax:[PDecl]
_) = do
IState
i <- StateT IState (ExceptT Err IO) IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
IState -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (IState -> Syntax -> IState
addReplSyntax IState
i Syntax
syntax)
defineName [PDecl]
decls = do
ElabInfo -> [PDecl] -> StateT IState (ExceptT Err IO) ()
elabDecls (FilePath -> ElabInfo
toplevelWith FilePath
fn) ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
forall t. PDecl' t -> PDecl' t
fixClauses [PDecl]
decls)
Maybe Name -> StateT IState (ExceptT Err IO) ()
setReplDefined (PDecl -> Maybe Name
getName ([PDecl] -> PDecl
forall a. [a] -> a
head [PDecl]
decls))
getClauses :: PDecl' t -> [PClause' t]
getClauses (PClauses FC
fc FnOpts
opts Name
name [PClause' t]
clauses) = [PClause' t]
clauses
getClauses PDecl' t
_ = []
getRHS :: PClause -> PTerm
getRHS :: PClause' PTerm -> PTerm
getRHS (PClause FC
fc Name
name PTerm
whole [PTerm]
with PTerm
rhs [PDecl]
whereBlock) = PTerm
rhs
getRHS (PWith FC
fc Name
name PTerm
whole [PTerm]
with PTerm
rhs Maybe (Name, FC)
pn [PDecl]
whereBlock) = PTerm
rhs
getRHS (PClauseR FC
fc [PTerm]
with PTerm
rhs [PDecl]
whereBlock) = PTerm
rhs
getRHS (PWithR FC
fc [PTerm]
with PTerm
rhs Maybe (Name, FC)
pn [PDecl]
whereBlock) = PTerm
rhs
setReplDefined :: Maybe Name -> Idris ()
setReplDefined :: Maybe Name -> StateT IState (ExceptT Err IO) ()
setReplDefined Maybe Name
Nothing = () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
setReplDefined (Just Name
n) = do
IState
oldState <- StateT IState (ExceptT Err IO) IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
Field IState [Name]
-> ([Name] -> [Name]) -> StateT IState (ExceptT Err IO) ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Name]
repl_definitions (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:)
fixClauses :: PDecl' t -> PDecl' t
fixClauses :: PDecl' t -> PDecl' t
fixClauses (PClauses FC
fc FnOpts
opts Name
_ css :: [PClause' t]
css@(PClause' t
clause:[PClause' t]
cs)) =
FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts (PClause' t -> Name
forall t. PClause' t -> Name
getClauseName PClause' t
clause) [PClause' t]
css
fixClauses (PImplementation Docstring (Either Err t)
doc [(Name, Docstring (Either Err t))]
argDocs SyntaxInfo
syn FC
fc [(Name, t)]
constraints [Name]
pnames Accessibility
acc FnOpts
opts Name
cls FC
nfc [t]
parms [(Name, t)]
pextra t
ty Maybe Name
implName [PDecl' t]
decls) =
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err t)
doc [(Name, Docstring (Either Err t))]
argDocs SyntaxInfo
syn FC
fc [(Name, t)]
constraints [Name]
pnames Accessibility
acc FnOpts
opts Name
cls FC
nfc [t]
parms [(Name, t)]
pextra t
ty Maybe Name
implName ((PDecl' t -> PDecl' t) -> [PDecl' t] -> [PDecl' t]
forall a b. (a -> b) -> [a] -> [b]
map PDecl' t -> PDecl' t
forall t. PDecl' t -> PDecl' t
fixClauses [PDecl' t]
decls)
fixClauses PDecl' t
decl = PDecl' t
decl
info :: ElabInfo
info = FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")
process FilePath
fn (Undefine [Name]
names) = [Name] -> StateT IState (ExceptT Err IO) ()
undefine [Name]
names
where
undefine :: [Name] -> Idris ()
undefine :: [Name] -> StateT IState (ExceptT Err IO) ()
undefine [] = do
[Name]
allDefined <- IState -> [Name]
idris_repl_defs (IState -> [Name])
-> StateT IState (ExceptT Err IO) IState -> Idris [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT IState (ExceptT Err IO) IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
[Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
allDefined []
undefine [Name]
names = [Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
names []
undefine' :: [Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [] [Name]
list = do Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [Name] -> Doc OutputAnnotation
printUndefinedNames [Name]
list
() -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
undefine' (Name
n:[Name]
names) [Name]
already = do
[Name]
allDefined <- IState -> [Name]
idris_repl_defs (IState -> [Name])
-> StateT IState (ExceptT Err IO) IState -> Idris [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT IState (ExceptT Err IO) IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
if Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
allDefined
then do [Name]
undefinedJustNow <- Name -> Idris [Name]
undefClosure Name
n
[Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
names ([Name]
undefinedJustNow [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
already)
else do TC Any -> Idris Any
forall a. TC a -> Idris a
tclift (TC Any -> Idris Any) -> TC Any -> Idris Any
forall a b. (a -> b) -> a -> b
$ Err -> TC Any
forall a. Err -> TC a
tfail (Err -> TC Any) -> Err -> TC Any
forall a b. (a -> b) -> a -> b
$ FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath
"Can't undefine " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" because it wasn't defined at the repl")
[Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
names [Name]
already
undefOne :: Name -> m ()
undefOne Name
n = do Field
IState
(Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> m ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Name
-> Field
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
(Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n Field
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
(Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Field
IState
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Field
IState
(Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Field
IState
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
known_terms) Maybe
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
forall a. Maybe a
Nothing
Field IState (Maybe InterfaceInfo) -> Maybe InterfaceInfo -> m ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Name -> Field (Ctxt InterfaceInfo) (Maybe InterfaceInfo)
forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n Field (Ctxt InterfaceInfo) (Maybe InterfaceInfo)
-> Field IState (Ctxt InterfaceInfo)
-> Field IState (Maybe InterfaceInfo)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Field IState (Ctxt InterfaceInfo)
known_interfaces) Maybe InterfaceInfo
forall a. Maybe a
Nothing
Field IState [Name] -> ([Name] -> [Name]) -> m ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Name]
repl_definitions (Name -> [Name] -> [Name]
forall a. Eq a => a -> [a] -> [a]
delete Name
n)
undefClosure :: Name -> Idris [Name]
undefClosure Name
n =
do [Name]
replDefs <- IState -> [Name]
idris_repl_defs (IState -> [Name])
-> StateT IState (ExceptT Err IO) IState -> Idris [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT IState (ExceptT Err IO) IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
[(Name, [Name])]
callGraph <- Name -> Idris [(Name, [Name])]
whoCalls Name
n
let users :: [Name]
users = case Name -> [(Name, [Name])] -> Maybe [Name]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, [Name])]
callGraph of
Just [Name]
ns -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub [Name]
ns
Maybe [Name]
Nothing -> FilePath -> [Name]
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath
"Tried to undefine nonexistent name" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n)
[Name]
undefinedJustNow <- [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Name]] -> [Name])
-> StateT IState (ExceptT Err IO) [[Name]] -> Idris [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Name -> Idris [Name])
-> [Name] -> StateT IState (ExceptT Err IO) [[Name]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> Idris [Name]
undefClosure [Name]
users
Name -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *). MonadState IState m => Name -> m ()
undefOne Name
n
[Name] -> Idris [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
undefinedJustNow))
process FilePath
fn (ExecVal PTerm
t)
= do Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
(Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
let ty' :: Type
ty' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty
Type
res <- Type -> Idris Type
execute Type
tm
let (Doc OutputAnnotation
resOut, Doc OutputAnnotation
tyOut) = (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Type -> PTerm
delab IState
ist Type
res),
IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Type -> PTerm
delab IState
ist Type
ty'))
Doc OutputAnnotation
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iPrintTermWithType Doc OutputAnnotation
resOut Doc OutputAnnotation
tyOut
process FilePath
fn (Check (PRef FC
_ [FC]
_ Name
n))
= do Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
case Name -> Context -> [Name]
lookupVisibleNames Name
n Context
ctxt of
ts :: [Name]
ts@(Name
t:[Name]
_) ->
case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
t (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
Just (Maybe Name
_, Int
i, [Name]
_, Bool
_, Bool
_) -> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
PPOption -> IState -> Name -> Int -> Doc OutputAnnotation
showMetavarInfo PPOption
ppo IState
ist Name
n Int
i
Maybe (Maybe Name, Int, [Name], Bool, Bool)
Nothing -> [(Name, Bool)]
-> Name
-> [(Name, Doc OutputAnnotation)]
-> StateT IState (ExceptT Err IO) ()
iPrintFunTypes [] Name
n ((Name -> (Name, Doc OutputAnnotation))
-> [Name] -> [(Name, Doc OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n)) [Name]
ts)
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"No such variable " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
where
lookupVisibleNames :: Name -> Context -> [Name]
lookupVisibleNames :: Name -> Context -> [Name]
lookupVisibleNames Name
n Context
ctxt = ((Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Name)
-> [(Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Name
forall a b. (a, b) -> a
fst ([(Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
-> [Name])
-> [(Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
-> [Name]
forall a b. (a -> b) -> a -> b
$ Name
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> [(Name,
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
visibleDefinitions Context
ctxt)
showMetavarInfo :: PPOption -> IState -> Name -> Int -> Doc OutputAnnotation
showMetavarInfo PPOption
ppo IState
ist Name
n Int
i
= case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
(Type
ty:[Type]
_) -> let ty' :: Type
ty' = Context -> Env -> Type -> Type
normaliseC (IState -> Context
tt_ctxt IState
ist) [] Type
ty in
PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist Int
i [] (IState -> Type -> PTerm
delab IState
ist (IState -> Type -> Type
errReverse IState
ist Type
ty'))
putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy :: PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist Int
0 [(Name, Bool)]
bnd PTerm
sc = PPOption
-> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
forall p.
p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal PPOption
ppo IState
ist [(Name, Bool)]
bnd PTerm
sc
putTy PPOption
ppo IState
ist Int
i [(Name, Bool)]
bnd (PPi Plicity
p Name
n FC
_ PTerm
t PTerm
sc)
= let current :: Doc OutputAnnotation
current = case Name
n of
MN Int
_ Text
_ -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
""
UN Text
nm | (Char
'_':Char
'_':FilePath
_) <- Text -> FilePath
str Text
nm -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
""
Name
_ -> RigCount -> Bool -> Doc OutputAnnotation
forall a. RigCount -> Bool -> Doc a
countOf (Plicity -> RigCount
pcount Plicity
p)
(LanguageExt
LinearTypes LanguageExt -> [LanguageExt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
ist) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
t)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
in
Doc OutputAnnotation
current Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) PTerm
sc
putTy PPOption
ppo IState
ist Int
_ [(Name, Bool)]
bnd PTerm
sc = PPOption
-> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
forall p.
p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal PPOption
ppo IState
ist ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) PTerm
sc
putGoal :: p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal p
ppo IState
ist [(Name, Bool)]
bnd PTerm
g
= FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"--------------------------------------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> FilePath -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
g)
countOf :: RigCount -> Bool -> Doc a
countOf RigCount
Rig0 Bool
True = FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"0"
countOf RigCount
Rig1 Bool
True = FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"1"
countOf RigCount
_ Bool
_ = FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
" "
tPretty :: [(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
t = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) PTerm
t
process FilePath
fn (Check PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let ty' :: Type
ty' = if IOption -> Bool
opt_evaltypes (IState -> IOption
idris_options IState
ist)
then Context -> Env -> Type -> Type
normaliseC Context
ctxt [] Type
ty
else Type
ty
case Type
tm of
TType UExp
_ ->
Doc OutputAnnotation
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iPrintTermWithType (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (FC -> PTerm
PType FC
emptyFC)) Doc OutputAnnotation
type1Doc
Type
_ -> Doc OutputAnnotation
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iPrintTermWithType (IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist Type
tm)
(IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist Type
ty')
process FilePath
fn (Core PTerm
t)
= case PTerm
t of
PRef FC
_ [FC]
_ Name
n ->
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
case Name -> Context -> [Def]
lookupDef Name
n (IState -> Context
tt_ctxt IState
ist) of
[CaseOp CaseInfo
_ Type
_ [(Type, Bool)]
_ [Either Type (Type, Type)]
_ [([Name], Type, Type)]
_ CaseDefs
_] -> Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
True Name
n Idris [Doc OutputAnnotation]
-> ([Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep
[Def]
_ -> PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm PTerm
t
PTerm
t -> PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm PTerm
t
where coreTerm :: PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm PTerm
t =
do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Doc OutputAnnotation
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iPrintTermWithType ([Name] -> Type -> Doc OutputAnnotation
pprintTT [] Type
tm) ([Name] -> Type -> Doc OutputAnnotation
pprintTT [] Type
ty)
process FilePath
fn (DocStr (Left Name
n) HowMuchDocs
w)
| UN Text
ty <- Name
n, Text
ty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
T.pack FilePath
"Type" = StateT IState (ExceptT Err IO) IState
getIState StateT IState (ExceptT Err IO) IState
-> (IState -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> (IState -> Doc OutputAnnotation)
-> IState
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Doc OutputAnnotation
pprintTypeDoc
| Bool
otherwise = do
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let docs :: [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
docs = Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. [a] -> [a] -> [a]
++
((Name, Docstring DocTerm)
-> (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)])))
-> [(Name, Docstring DocTerm)]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Docstring DocTerm
d)-> (Name
n, (Docstring DocTerm
d, [])))
(Name -> Ctxt (Docstring DocTerm) -> [(Name, Docstring DocTerm)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName (Name -> Name
modDocN Name
n) (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
ist))
case [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
docs of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"No documentation for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
[(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns -> do [Doc OutputAnnotation]
toShow <- ((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation))
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> Idris [Doc OutputAnnotation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IState
-> (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall b.
IState
-> (Name, b)
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
showDoc IState
ist) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
toShow)
where showDoc :: IState
-> (Name, b)
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
showDoc IState
ist (Name
n, b
d) = do Docs
doc <- Name -> HowMuchDocs -> Idris Docs
getDocs Name
n HowMuchDocs
w
Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation))
-> Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ IState -> Docs -> Doc OutputAnnotation
pprintDocs IState
ist Docs
doc
modDocN :: Name -> Name
modDocN (NS (UN Text
n) [Text]
ns) = Name -> [Text] -> Name
NS Name
modDocName (Text
nText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
ns)
modDocN (UN Text
n) = Name -> [Text] -> Name
NS Name
modDocName [Text
n]
modDocN Name
_ = Int -> FilePath -> Name
sMN Int
1 FilePath
"NotFoundForSure"
process FilePath
fn (DocStr (Right Const
c) HowMuchDocs
_)
= do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState -> Const -> FilePath -> Doc OutputAnnotation
pprintConstDocs IState
ist Const
c (Const -> FilePath
constDocs Const
c)
process FilePath
fn Command
Universes
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let cs :: Set ConstraintFC
cs = IState -> Set ConstraintFC
idris_constraints IState
i
let cslist :: [ConstraintFC]
cslist = Set ConstraintFC -> [ConstraintFC]
forall a. Set a -> [a]
S.toAscList Set ConstraintFC
cs
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> FilePath
showSep FilePath
"\n" ((ConstraintFC -> FilePath) -> [ConstraintFC] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ConstraintFC -> FilePath
forall a. Show a => a -> FilePath
show [ConstraintFC]
cslist)
let n :: Int
n = [ConstraintFC] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstraintFC]
cslist
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" constraints)"
case Set ConstraintFC -> TC ()
ucheck Set ConstraintFC
cs of
Error Err
e -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> FilePath
pshow IState
i Err
e
OK ()
_ -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
"Universes OK"
process FilePath
fn (Defn Name
n)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let head :: Doc a
head = FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"Compiled patterns:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<$>
FilePath -> Doc a
forall a. FilePath -> Doc a
text ([Def] -> FilePath
forall a. Show a => a -> FilePath
show (Name -> Context -> [Def]
lookupDef Name
n (IState -> Context
tt_ctxt IState
i)))
let defs :: Doc a
defs =
case Name
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
-> [([([(Name, Type)], Type, Type)], [PTerm])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
idris_patdefs IState
i) of
[] -> Doc a
forall a. Doc a
empty
[([([(Name, Type)], Type, Type)]
d, [PTerm]
_)] -> FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"Original definiton:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc a] -> Doc a
forall a. [Doc a] -> Doc a
vsep ((([(Name, Type)], Type, Type) -> Doc a)
-> [([(Name, Type)], Type, Type)] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ([(Name, Type)], Type, Type) -> Doc a
forall a a. IState -> (a, Type, Type) -> Doc a
printCase IState
i) [([(Name, Type)], Type, Type)]
d)
let tot :: Doc OutputAnnotation
tot =
case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
i) of
[Totality
t] -> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
i
[Totality]
_ -> Doc OutputAnnotation
forall a. Doc a
empty
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation
forall a. Doc a
head, Doc OutputAnnotation
forall a. Doc a
defs, Doc OutputAnnotation
tot]
where printCase :: IState -> (a, Type, Type) -> Doc a
printCase IState
i (a
_, Type
lhs, Type
rhs)
= let i' :: IState
i' = IState
i { idris_options :: IOption
idris_options = (IState -> IOption
idris_options IState
i) { opt_showimp :: Bool
opt_showimp = Bool
True } }
in FilePath -> Doc a
forall a. FilePath -> Doc a
text (IState -> PTerm -> FilePath
showTm IState
i' (IState -> Type -> PTerm
delab IState
i Type
lhs)) Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"=" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+>
FilePath -> Doc a
forall a. FilePath -> Doc a
text (IState -> PTerm -> FilePath
showTm IState
i' (IState -> Type -> PTerm
delab IState
i Type
rhs))
process FilePath
fn (TotCheck Name
n)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
case Name -> Context -> [(Name, Totality)]
lookupNameTotal Name
n (IState -> Context
tt_ctxt IState
i) of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Unknown operator " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
[(Name, Totality)]
ts -> do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Bool
c <- Idris Bool
colourise
let ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
let showN :: Name -> Doc OutputAnnotation
showN Name
n = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> FilePath -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> FilePath
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
ist) [] PPOption
ppo Bool
False Name
n
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([(Name, Totality)] -> Doc OutputAnnotation)
-> [(Name, Totality)]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([(Name, Totality)] -> [Doc OutputAnnotation])
-> [(Name, Totality)]
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
((Name, Totality) -> Doc OutputAnnotation)
-> [(Name, Totality)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Totality
t) -> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
hang Int
4 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Name -> Doc OutputAnnotation
showN Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
i) ([(Name, Totality)] -> StateT IState (ExceptT Err IO) ())
-> [(Name, Totality)] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
[(Name, Totality)]
ts
process FilePath
fn (DebugUnify PTerm
l PTerm
r)
= do (Type
ltm, Type
_) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
l
(Type
rtm, Type
_) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
r
Context
ctxt <- Idris Context
getContext
case Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, Type)], Fails)
unify Context
ctxt [] (Type
ltm, Maybe Provenance
forall a. Maybe a
Nothing) (Type
rtm, Maybe Provenance
forall a. Maybe a
Nothing) [] [] [] [] of
OK ([(Name, Type)], Fails)
ans -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (([(Name, Type)], Fails) -> FilePath
forall a. Show a => a -> FilePath
show ([(Name, Type)], Fails)
ans)
Error Err
e -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e)
process FilePath
fn (DebugInfo Name
n)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let oi :: [(Name, OptInfo)]
oi = Name -> Ctxt OptInfo -> [(Name, OptInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt OptInfo
idris_optimisation IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Name, OptInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, OptInfo)]
oi)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([(Name, OptInfo)] -> FilePath
forall a. Show a => a -> FilePath
show [(Name, OptInfo)]
oi)
let si :: [[Bool]]
si = Name -> Ctxt [Bool] -> [[Bool]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [Bool]
idris_statics IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([[Bool]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Bool]]
si)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([[Bool]] -> FilePath
forall a. Show a => a -> FilePath
show [[Bool]]
si)
let di :: [TypeInfo]
di = Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([TypeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeInfo]
di)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([TypeInfo] -> FilePath
forall a. Show a => a -> FilePath
show [TypeInfo]
di)
let imps :: [[PArg]]
imps = Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([[PArg]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[PArg]]
imps)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([[PArg]] -> FilePath
forall a. Show a => a -> FilePath
show [[PArg]]
imps)
let d :: [(Def, Accessibility)]
d = Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAcc Name
n Bool
False (IState -> Context
tt_ctxt IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Def, Accessibility)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Def, Accessibility)]
d)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Definition: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ((Def, Accessibility) -> FilePath
forall a. Show a => a -> FilePath
show ([(Def, Accessibility)] -> (Def, Accessibility)
forall a. [a] -> a
head [(Def, Accessibility)]
d))
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let cg' :: [(Name, CGInfo)]
cg' = Name -> Ctxt CGInfo -> [(Name, CGInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
i)
Totality
sc <- Name -> Idris Totality
checkSizeChange Name
n
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Size change: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Totality -> FilePath
forall a. Show a => a -> FilePath
show Totality
sc
let fn :: [(Name, FnInfo)]
fn = Name -> Ctxt FnInfo -> [(Name, FnInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt FnInfo
idris_fninfo IState
i)
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Name, CGInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, CGInfo)]
cg')) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ do FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Call graph:\n"
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([(Name, CGInfo)] -> FilePath
forall a. Show a => a -> FilePath
show [(Name, CGInfo)]
cg')
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([(Name, FnInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, FnInfo)]
fn)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn ([(Name, FnInfo)] -> FilePath
forall a. Show a => a -> FilePath
show [(Name, FnInfo)]
fn)
process FilePath
fn (Search [PkgName]
pkgs PTerm
t) = [PkgName] -> PTerm -> StateT IState (ExceptT Err IO) ()
searchByType [PkgName]
pkgs PTerm
t
process FilePath
fn (CaseSplitAt Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
caseSplitAt FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddClauseFrom Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddProofClauseFrom Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addProofClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddMissing Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeWith Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeWith FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeCase Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeCase FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeLemma Bool
updatefile Int
l Name
n)
= FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeLemma FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (DoProofSearch Bool
updatefile Bool
rec Int
l Name
n [Name]
hints)
= FilePath
-> Bool
-> Bool
-> Int
-> Name
-> [Name]
-> Maybe Int
-> StateT IState (ExceptT Err IO) ()
doProofSearch FilePath
fn Bool
updatefile Bool
rec Int
l Name
n [Name]
hints Maybe Int
forall a. Maybe a
Nothing
process FilePath
fn (Spec PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let tm' :: Type
tm' = Context -> Env -> Type -> Type
simplify Context
ctxt [] Type
tm
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (PTerm -> FilePath
forall a. Show a => a -> FilePath
show (IState -> Type -> PTerm
delab IState
ist Type
tm'))
process FilePath
fn (RmProof Name
n')
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
Name
n <- Name -> Idris Name
resolveProof Name
n'
let proofs :: [(Name, (Bool, [FilePath]))]
proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
case Name -> [(Name, (Bool, [FilePath]))] -> Maybe (Bool, [FilePath])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (Bool, [FilePath]))]
proofs of
Maybe (Bool, [FilePath])
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"No proof to remove"
Just (Bool, [FilePath])
_ -> do Name -> StateT IState (ExceptT Err IO) ()
removeProof Name
n
Name -> StateT IState (ExceptT Err IO) ()
insertMetavar Name
n
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Removed proof " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
where
insertMetavar :: Name -> Idris ()
insertMetavar :: Name -> StateT IState (ExceptT Err IO) ()
insertMetavar Name
n =
do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let ms :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ms = IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars = (Name
n, (Maybe Name
forall a. Maybe a
Nothing, Int
0, [], Bool
False, Bool
False)) (Name, (Maybe Name, Int, [Name], Bool, Bool))
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall a. a -> [a] -> [a]
: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ms }
process FilePath
fn' (AddProof Maybe Name
prf)
= do FilePath
fn <- do
let fn'' :: FilePath
fn'' = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') FilePath
fn'
Bool
ex <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist FilePath
fn''
let fnExt :: FilePath
fnExt = FilePath
fn'' FilePath -> FilePath -> FilePath
<.> FilePath
"idr"
Bool
exExt <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist FilePath
fnExt
if Bool
ex
then FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
fn''
else if Bool
exExt
then FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
fnExt
else FilePath -> Idris FilePath
forall a. FilePath -> Idris a
ifail (FilePath -> Idris FilePath) -> FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"Neither \""FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
fn''FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
"\" nor \""FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
fnExtFilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
"\" exist"
let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fn FilePath
fb
FilePath
prog <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSource FilePath
fb
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let proofs :: [(Name, (Bool, [FilePath]))]
proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
Name
n' <- case Maybe Name
prf of
Maybe Name
Nothing -> case [(Name, (Bool, [FilePath]))]
proofs of
[] -> FilePath -> Idris Name
forall a. FilePath -> Idris a
ifail FilePath
"No proof to add"
((Name
x, (Bool, [FilePath])
_) : [(Name, (Bool, [FilePath]))]
_) -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
Just Name
nm -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
nm
Name
n <- Name -> Idris Name
resolveProof Name
n'
case Name -> [(Name, (Bool, [FilePath]))] -> Maybe (Bool, [FilePath])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (Bool, [FilePath]))]
proofs of
Maybe (Bool, [FilePath])
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"No proof to add"
Just (Bool
mode, [FilePath]
prf) ->
do let script :: FilePath
script = if Bool
mode
then Bool -> Name -> [FilePath] -> FilePath
showRunElab (FilePath -> Bool
lit FilePath
fn) Name
n [FilePath]
prf
else Bool -> Name -> [FilePath] -> FilePath
showProof (FilePath -> Bool
lit FilePath
fn) Name
n [FilePath]
prf
let prog' :: [FilePath]
prog' = FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
script [FilePath]
ls
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fn ([FilePath] -> FilePath
unlines [FilePath]
prog')
Name -> StateT IState (ExceptT Err IO) ()
removeProof Name
n
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Added proof " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
where ls :: [FilePath]
ls = (FilePath -> [FilePath]
lines FilePath
prog)
process FilePath
fn (ShowProof Name
n')
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
Name
n <- Name -> Idris Name
resolveProof Name
n'
let proofs :: [(Name, (Bool, [FilePath]))]
proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
case Name -> [(Name, (Bool, [FilePath]))] -> Maybe (Bool, [FilePath])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (Bool, [FilePath]))]
proofs of
Maybe (Bool, [FilePath])
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"No proof to show"
Just (Bool
m, [FilePath]
p) -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ if Bool
m
then Bool -> Name -> [FilePath] -> FilePath
showRunElab Bool
False Name
n [FilePath]
p
else Bool -> Name -> [FilePath] -> FilePath
showProof Bool
False Name
n [FilePath]
p
process FilePath
fn (Prove Bool
mode Name
n')
= do Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let ns :: [Name]
ns = Name -> Context -> [Name]
lookupNames Name
n' Context
ctxt
let metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
metavars = (Name -> Maybe (Name, (Maybe Name, Int, [Name], Bool, Bool)))
-> [Name] -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\Name
n -> do (Maybe Name, Int, [Name], Bool, Bool)
c <- Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist); (Name, (Maybe Name, Int, [Name], Bool, Bool))
-> Maybe (Name, (Maybe Name, Int, [Name], Bool, Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, (Maybe Name, Int, [Name], Bool, Bool)
c)) [Name]
ns
Name
n <- case [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
metavars of
[] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Err) -> FilePath -> Err
forall a b. (a -> b) -> a -> b
$ FilePath
"Cannot find metavariable " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n')
[(Name
n, (Maybe Name
_,Int
_,[Name]
_,Bool
False,Bool
_))] -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
[(Name
_, (Maybe Name
_,Int
_,[Name]
_,Bool
_,Bool
False))] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Can't prove this hole as it depends on other holes")
[(Name
_, (Maybe Name
_,Int
_,[Name]
_,Bool
True,Bool
_))] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Declarations not solvable using prover")
[(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns -> Err -> Idris Name
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns))
ElabInfo
-> Bool -> Bool -> Name -> StateT IState (ExceptT Err IO) ()
prover (FilePath -> ElabInfo
toplevelWith FilePath
fn) Bool
mode (FilePath -> Bool
lit FilePath
fn) Name
n
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
(FC, Name) -> StateT IState (ExceptT Err IO) ()
totcheck (FilePath -> FC
fileFC FilePath
"(input)", Name
n)
((FC, Name) -> StateT IState (ExceptT Err IO) ())
-> [(FC, Name)] -> StateT IState (ExceptT Err IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (FC
f,Name
n) -> Name -> Totality -> StateT IState (ExceptT Err IO) ()
setTotality Name
n Totality
Unchecked) (IState -> [(FC, Name)]
idris_totcheck IState
i)
((FC, Name) -> Idris Totality)
-> [(FC, Name)] -> StateT IState (ExceptT Err IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris Totality
checkDeclTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
StateT IState (ExceptT Err IO) ()
warnTotality
process FilePath
fn (WHNF PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let tm' :: Type
tm' = Context -> Env -> Type -> Type
whnf Context
ctxt [] Type
tm
let tmArgs' :: Type
tmArgs' = Context -> Env -> Type -> Type
whnfArgs Context
ctxt [] Type
tm
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"WHNF: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (PTerm -> FilePath
forall a. Show a => a -> FilePath
show (IState -> Type -> PTerm
delab IState
ist Type
tm'))
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"WHNF args: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (PTerm -> FilePath
forall a. Show a => a -> FilePath
show (IState -> Type -> PTerm
delab IState
ist Type
tmArgs'))
process FilePath
fn (TestInline PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
Context
ctxt <- Idris Context
getContext
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let tm' :: Type
tm' = IState -> Type -> Type
inlineTerm IState
ist Type
tm
Bool
c <- Idris Bool
colourise
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (IState -> PTerm -> FilePath
showTm IState
ist (IState -> Type -> PTerm
delab IState
ist Type
tm'))
process FilePath
fn (Execute PTerm
tm)
= StateT IState (ExceptT Err IO) ()
-> (Err -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
(Type
m_in, Type
_) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS (FC -> PTerm -> PTerm
elabExec FC
fc PTerm
tm)
Type
m <- Type -> Idris Type
forall term. Optimisable term => term -> Idris term
applyOpts Type
m_in
(FilePath
tmpn, Handle
tmph) <- IO (FilePath, Handle) -> Idris (FilePath, Handle)
forall a. IO a -> Idris a
runIO (IO (FilePath, Handle) -> Idris (FilePath, Handle))
-> IO (FilePath, Handle) -> Idris (FilePath, Handle)
forall a b. (a -> b) -> a -> b
$ FilePath -> IO (FilePath, Handle)
tempfile FilePath
""
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Handle -> IO ()
hClose Handle
tmph
Codegen
t <- Idris Codegen
codegen
FilePath
progName <- FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Idris FilePath) -> FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ if Bool
isWindows then FilePath
tmpn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
".exe" else FilePath
tmpn
CodegenInfo
ir <- Codegen -> FilePath -> Maybe Type -> Idris CodegenInfo
compile Codegen
t FilePath
tmpn (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
m)
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Codegen -> FilePath -> CodegenInfo -> IO ()
generate Codegen
t ((FilePath, Bool) -> FilePath
forall a b. (a, b) -> a
fst ([(FilePath, Bool)] -> (FilePath, Bool)
forall a. [a] -> a
head (IState -> [(FilePath, Bool)]
idris_imported IState
ist))) CodegenInfo
ir
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput Handle
h ->
do ExitCode
res <- IO ExitCode -> Idris ExitCode
forall a. IO a -> Idris a
runIO (IO ExitCode -> Idris ExitCode) -> IO ExitCode -> Idris ExitCode
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> IO ExitCode
rawSystem FilePath
progName []
case ExitCode
res of
ExitCode
ExitSuccess -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ExitFailure Int
err ->
FilePath -> StateT IState (ExceptT Err IO) ()
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Compiled program " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
if Int
err Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
then FilePath
"was killed by signal " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Int -> FilePath
forall a. Show a => a -> FilePath
show (Int
0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
err)
else FilePath
"terminated with exit code " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Int -> FilePath
forall a. Show a => a -> FilePath
show Int
err
IdeMode Integer
n Handle
h -> IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> (FilePath -> IO ())
-> FilePath
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath -> FilePath -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"run-program" FilePath
tmpn Integer
n)
(\Err
e -> StateT IState (ExceptT Err IO) IState
getIState StateT IState (ExceptT Err IO) IState
-> (IState -> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderError (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> (IState -> Doc OutputAnnotation)
-> IState
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Err -> Doc OutputAnnotation)
-> Err -> IState -> Doc OutputAnnotation
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> Err -> Doc OutputAnnotation
pprintErr Err
e)
where fc :: FC
fc = FilePath -> FC
fileFC FilePath
"main"
process FilePath
fn (Compile Codegen
codegen FilePath
f)
| (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath
takeExtension FilePath
f) FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".idr", FilePath
".lidr", FilePath
".idc"] =
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Invalid filename for compiler output \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
"\""
| Bool
otherwise = do [Opt]
opts <- Idris [Opt]
getCmdLine
let iface :: Bool
iface = Opt
Interface Opt -> [Opt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
let mainname :: Name
mainname = Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN FilePath
"main") [FilePath
"Main"]
Maybe Type
m <- if Bool
iface then Maybe Type -> StateT IState (ExceptT Err IO) (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing else
do (Type
m', Type
_) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"compiler")) ElabMode
ERHS
(FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (FilePath -> Name
sUN FilePath
"run__IO"))
[PTerm -> PArg
forall t. t -> PArg' t
pexp (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
mainname])
Maybe Type -> StateT IState (ExceptT Err IO) (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
m')
CodegenInfo
ir <- Codegen -> FilePath -> Maybe Type -> Idris CodegenInfo
compile Codegen
codegen FilePath
f Maybe Type
m
IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let ir' :: CodegenInfo
ir' = CodegenInfo
ir {interfaces :: Bool
interfaces = Bool
iface}
IO () -> StateT IState (ExceptT Err IO) ()
forall a. IO a -> Idris a
runIO (IO () -> StateT IState (ExceptT Err IO) ())
-> IO () -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Codegen -> FilePath -> CodegenInfo -> IO ()
generate Codegen
codegen ((FilePath, Bool) -> FilePath
forall a b. (a, b) -> a
fst ([(FilePath, Bool)] -> (FilePath, Bool)
forall a. [a] -> a
head (IState -> [(FilePath, Bool)]
idris_imported IState
i))) CodegenInfo
ir'
where fc :: FC
fc = FilePath -> FC
fileFC FilePath
"main"
process FilePath
fn (LogLvl Int
i) = Int -> StateT IState (ExceptT Err IO) ()
setLogLevel Int
i
process FilePath
fn (LogCategory [LogCat]
cs) = [LogCat] -> StateT IState (ExceptT Err IO) ()
setLogCats [LogCat]
cs
process FilePath
fn (Pattelab PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ELHS PTerm
t
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Type -> FilePath
forall a. Show a => a -> FilePath
show Type
tm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n\n : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Type -> FilePath
forall a. Show a => a -> FilePath
show Type
ty
process FilePath
fn (Missing Name
n)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
PPOption
ppOpts <- (IState -> PPOption)
-> StateT IState (ExceptT Err IO) IState
-> StateT IState (ExceptT Err IO) PPOption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IState -> PPOption
ppOptionIst StateT IState (ExceptT Err IO) IState
getIState
case Name
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
-> [([([(Name, Type)], Type, Type)], [PTerm])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
idris_patdefs IState
i) of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Unknown name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
[([([(Name, Type)], Type, Type)]
_, [PTerm]
tms)] ->
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((PTerm -> Doc OutputAnnotation)
-> [PTerm] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppOpts
[]
[]
(IState -> [FixDecl]
idris_infixes IState
i))
[PTerm]
tms))
[([([(Name, Type)], Type, Type)], [PTerm])]
_ -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Ambiguous name"
process FilePath
fn (DynamicLink FilePath
l)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let importdirs :: [FilePath]
importdirs = IOption -> [FilePath]
opt_importdirs (IState -> IOption
idris_options IState
i)
lib :: FilePath
lib = FilePath -> FilePath
trim FilePath
l
Maybe DynamicLib
handle <- ExceptT Err IO (Maybe DynamicLib)
-> StateT IState (ExceptT Err IO) (Maybe DynamicLib)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT Err IO (Maybe DynamicLib)
-> StateT IState (ExceptT Err IO) (Maybe DynamicLib))
-> (IO (Maybe DynamicLib) -> ExceptT Err IO (Maybe DynamicLib))
-> IO (Maybe DynamicLib)
-> StateT IState (ExceptT Err IO) (Maybe DynamicLib)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IO (Maybe DynamicLib) -> ExceptT Err IO (Maybe DynamicLib)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe DynamicLib)
-> StateT IState (ExceptT Err IO) (Maybe DynamicLib))
-> IO (Maybe DynamicLib)
-> StateT IState (ExceptT Err IO) (Maybe DynamicLib)
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath -> IO (Maybe DynamicLib)
tryLoadLib [FilePath]
importdirs FilePath
lib
case Maybe DynamicLib
handle of
Maybe DynamicLib
Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Could not load dynamic lib \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\""
Just DynamicLib
x -> do let libs :: [DynamicLib]
libs = IState -> [DynamicLib]
idris_dynamic_libs IState
i
if DynamicLib
x DynamicLib -> [DynamicLib] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DynamicLib]
libs
then do Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser Int
1 (FilePath
"Tried to load duplicate library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ DynamicLib -> FilePath
lib_name DynamicLib
x)
() -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_dynamic_libs :: [DynamicLib]
idris_dynamic_libs = DynamicLib
xDynamicLib -> [DynamicLib] -> [DynamicLib]
forall a. a -> [a] -> [a]
:[DynamicLib]
libs }
where trim :: FilePath -> FilePath
trim = FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
process FilePath
fn Command
ListDynamic
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"Dynamic libraries:"
[DynamicLib] -> StateT IState (ExceptT Err IO) ()
showLibs ([DynamicLib] -> StateT IState (ExceptT Err IO) ())
-> [DynamicLib] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState -> [DynamicLib]
idris_dynamic_libs IState
i
where showLibs :: [DynamicLib] -> StateT IState (ExceptT Err IO) ()
showLibs [] = () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
showLibs ((Lib FilePath
name DL
_):[DynamicLib]
ls) = do FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name; [DynamicLib] -> StateT IState (ExceptT Err IO) ()
showLibs [DynamicLib]
ls
process FilePath
fn Command
Metavars
= do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let mvs :: [Name]
mvs = ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs
case [Name]
mvs of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"No global holes to solve"
[Name]
_ -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Global holes:\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
mvs
process FilePath
fn Command
NOP = () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
process FilePath
fn (SetOpt Opt
ErrContext) = Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
True
process FilePath
fn (UnsetOpt Opt
ErrContext) = Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
False
process FilePath
fn (SetOpt Opt
ShowImpl) = Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
True
process FilePath
fn (UnsetOpt Opt
ShowImpl) = Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
False
process FilePath
fn (SetOpt Opt
ShowOrigErr) = Bool -> StateT IState (ExceptT Err IO) ()
setShowOrigErr Bool
True
process FilePath
fn (UnsetOpt Opt
ShowOrigErr) = Bool -> StateT IState (ExceptT Err IO) ()
setShowOrigErr Bool
False
process FilePath
fn (SetOpt Opt
AutoSolve) = Bool -> StateT IState (ExceptT Err IO) ()
setAutoSolve Bool
True
process FilePath
fn (UnsetOpt Opt
AutoSolve) = Bool -> StateT IState (ExceptT Err IO) ()
setAutoSolve Bool
False
process FilePath
fn (SetOpt Opt
NoBanner) = Bool -> StateT IState (ExceptT Err IO) ()
setNoBanner Bool
True
process FilePath
fn (UnsetOpt Opt
NoBanner) = Bool -> StateT IState (ExceptT Err IO) ()
setNoBanner Bool
False
process FilePath
fn (SetOpt Opt
WarnReach) = Field IState [Opt]
-> ([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Opt]
opts_idrisCmdline (([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ())
-> ([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [Opt] -> [Opt]
forall a. Eq a => [a] -> [a]
nub ([Opt] -> [Opt]) -> ([Opt] -> [Opt]) -> [Opt] -> [Opt]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Opt
WarnReachOpt -> [Opt] -> [Opt]
forall a. a -> [a] -> [a]
:)
process FilePath
fn (UnsetOpt Opt
WarnReach) = Field IState [Opt]
-> ([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Opt]
opts_idrisCmdline (([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ())
-> ([Opt] -> [Opt]) -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ Opt -> [Opt] -> [Opt]
forall a. Eq a => a -> [a] -> [a]
delete Opt
WarnReach
process FilePath
fn (SetOpt Opt
EvalTypes) = Bool -> StateT IState (ExceptT Err IO) ()
setEvalTypes Bool
True
process FilePath
fn (UnsetOpt Opt
EvalTypes) = Bool -> StateT IState (ExceptT Err IO) ()
setEvalTypes Bool
False
process FilePath
fn (SetOpt Opt
DesugarNats) = Bool -> StateT IState (ExceptT Err IO) ()
setDesugarNats Bool
True
process FilePath
fn (UnsetOpt Opt
DesugarNats) = Bool -> StateT IState (ExceptT Err IO) ()
setDesugarNats Bool
False
process FilePath
fn (SetOpt Opt
_) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Not a valid option"
process FilePath
fn (UnsetOpt Opt
_) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Not a valid option"
process FilePath
fn (SetColour ColourType
ty IdrisColour
c) = ColourType -> IdrisColour -> StateT IState (ExceptT Err IO) ()
setColour ColourType
ty IdrisColour
c
process FilePath
fn Command
ColourOn
= do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
ist { idris_colourRepl :: Bool
idris_colourRepl = Bool
True }
process FilePath
fn Command
ColourOff
= do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
IState -> StateT IState (ExceptT Err IO) ()
putIState (IState -> StateT IState (ExceptT Err IO) ())
-> IState -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ IState
ist { idris_colourRepl :: Bool
idris_colourRepl = Bool
False }
process FilePath
fn Command
ListErrorHandlers =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ case IState -> [Name]
idris_errorhandlers IState
ist of
[] -> FilePath
"No registered error handlers"
[Name]
handlers -> FilePath
"Registered error handlers: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ([FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([FilePath] -> FilePath)
-> ([Name] -> [FilePath]) -> [Name] -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse FilePath
", " ([FilePath] -> [FilePath])
-> ([Name] -> [FilePath]) -> [Name] -> [FilePath]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show) [Name]
handlers
process FilePath
fn (SetConsoleWidth ConsoleWidth
w) = ConsoleWidth -> StateT IState (ExceptT Err IO) ()
setWidth ConsoleWidth
w
process FilePath
fn (SetPrinterDepth Maybe Int
d) = Maybe Int -> StateT IState (ExceptT Err IO) ()
setDepth Maybe Int
d
process FilePath
fn (Apropos [PkgName]
pkgs FilePath
a) =
do IState
orig <- StateT IState (ExceptT Err IO) IState
getIState
Bool
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([PkgName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PkgName]
pkgs)) (StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ())
-> StateT IState (ExceptT Err IO) ()
-> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Searching packages: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep FilePath
", " ((PkgName -> FilePath) -> [PkgName] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map PkgName -> FilePath
forall a. Show a => a -> FilePath
show [PkgName]
pkgs)
(PkgName -> StateT IState (ExceptT Err IO) ())
-> [PkgName] -> StateT IState (ExceptT Err IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PkgName -> StateT IState (ExceptT Err IO) ()
loadPkgIndex [PkgName]
pkgs
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
let mods :: [(FilePath, Docstring DocTerm)]
mods = IState -> Text -> [(FilePath, Docstring DocTerm)]
aproposModules IState
ist (FilePath -> Text
T.pack FilePath
a)
let names :: [Name]
names = IState -> Text -> [Name]
apropos IState
ist (FilePath -> Text
T.pack FilePath
a)
let aproposInfo :: [(Name, PTerm, Maybe (Docstring DocTerm))]
aproposInfo = [ (Name
n,
IState -> Name -> PTerm
delabTy IState
ist Name
n,
((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm)
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Docstring DocTerm -> Docstring DocTerm
forall a. Docstring a -> Docstring a
overview (Docstring DocTerm -> Docstring DocTerm)
-> ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm)
-> (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst) (Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist)))
| Name
n <- [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort [Name]
names, Name -> Bool
isUN Name
n ]
if (Bool -> Bool
not ([(FilePath, Docstring DocTerm)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FilePath, Docstring DocTerm)]
mods)) Bool -> Bool -> Bool
|| (Bool -> Bool
not ([(Name, PTerm, Maybe (Docstring DocTerm))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, PTerm, Maybe (Docstring DocTerm))]
aproposInfo))
then Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((FilePath, Docstring DocTerm) -> Doc OutputAnnotation)
-> [(FilePath, Docstring DocTerm)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\(FilePath
m, Docstring DocTerm
d) -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Module" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
m Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
IState -> Docstring DocTerm -> Doc OutputAnnotation
ppD IState
ist Docstring DocTerm
d Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line) [(FilePath, Docstring DocTerm)]
mods) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation)
-> [(Name, PTerm, Maybe (Docstring DocTerm))]
-> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState
-> (Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation
prettyDocumentedIst IState
ist) [(Name, PTerm, Maybe (Docstring DocTerm))]
aproposInfo)
else Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderError (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"No results found"
where isUN :: Name -> Bool
isUN (UN Text
_) = Bool
True
isUN (NS Name
n [Text]
_) = Name -> Bool
isUN Name
n
isUN Name
_ = Bool
False
ppD :: IState -> Docstring DocTerm -> Doc OutputAnnotation
ppD IState
ist = (DocTerm -> FilePath -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> FilePath -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Type -> Doc OutputAnnotation)
-> (Type -> Type) -> DocTerm -> FilePath -> Doc OutputAnnotation
renderDocTerm (IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Type -> Type
normaliseAll (IState -> Context
tt_ctxt IState
ist) []))
process FilePath
fn (WhoCalls Name
n) =
do [(Name, [Name])]
calls <- Name -> Idris [(Name, [Name])]
whoCalls Name
n
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ())
-> [Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
((Name, [Name]) -> Doc OutputAnnotation)
-> [(Name, [Name])] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, [Name]
ns) ->
FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Callers of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
1 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"*" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []) [Name]
ns)))
[(Name, [Name])]
calls
process FilePath
fn (CallsWho Name
n) =
do [(Name, [Name])]
calls <- Name -> Idris [(Name, [Name])]
callsWho Name
n
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ())
-> [Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
((Name, [Name]) -> Doc OutputAnnotation)
-> [(Name, [Name])] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, [Name]
ns) ->
Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"calls:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
1 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"*" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []) [Name]
ns)))
[(Name, [Name])]
calls
process FilePath
fn (Browse [FilePath]
ns) =
do [[FilePath]]
underNSs <- [FilePath] -> StateT IState (ExceptT Err IO) [[FilePath]]
namespacesInNS [FilePath]
ns
[Name]
names <- [FilePath] -> Idris [Name]
namesInNS [FilePath]
ns
if [[FilePath]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[FilePath]]
underNSs Bool -> Bool -> Bool
&& [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
names
then FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Invalid or empty namespace"
else do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$
FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Namespaces:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
2 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (([FilePath] -> Doc OutputAnnotation)
-> [[FilePath]] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> ([FilePath] -> FilePath) -> [FilePath] -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> [FilePath] -> FilePath
showSep FilePath
".") [[FilePath]]
underNSs)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Names:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
2 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
(Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n))
[Name]
names))
process FilePath
fn (MakeDoc FilePath
s) =
do IState
istate <- StateT IState (ExceptT Err IO) IState
getIState
let names :: [FilePath]
names = FilePath -> [FilePath]
words FilePath
s
parse :: FilePath -> Either FilePath Name
parse FilePath
n | Right Name
x <- Parser IState Name
-> IState -> FilePath -> FilePath -> Either ParseError Name
forall st res.
Parser st res
-> st -> FilePath -> FilePath -> Either ParseError res
runparser Parser IState Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name IState
istate FilePath
fn FilePath
n = Name -> Either FilePath Name
forall a b. b -> Either a b
Right Name
x
parse FilePath
n = FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left FilePath
n
([FilePath]
bad, [Name]
nss) = [Either FilePath Name] -> ([FilePath], [Name])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either FilePath Name] -> ([FilePath], [Name]))
-> [Either FilePath Name] -> ([FilePath], [Name])
forall a b. (a -> b) -> a -> b
$ (FilePath -> Either FilePath Name)
-> [FilePath] -> [Either FilePath Name]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Either FilePath Name
parse [FilePath]
names
FilePath
cd <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO IO FilePath
getCurrentDirectory
let outputDir :: FilePath
outputDir = FilePath
cd FilePath -> FilePath -> FilePath
</> FilePath
"doc"
Either FilePath ()
result <- if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
bad then IO (Either FilePath ()) -> Idris (Either FilePath ())
forall a. IO a -> Idris a
runIO (IO (Either FilePath ()) -> Idris (Either FilePath ()))
-> IO (Either FilePath ()) -> Idris (Either FilePath ())
forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> FilePath -> IO (Either FilePath ())
generateDocs IState
istate [Name]
nss FilePath
outputDir
else Either FilePath () -> Idris (Either FilePath ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either FilePath () -> Idris (Either FilePath ()))
-> (FilePath -> Either FilePath ())
-> FilePath
-> Idris (Either FilePath ())
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Either FilePath ()
forall a b. a -> Either a b
Left (FilePath -> Idris (Either FilePath ()))
-> FilePath -> Idris (Either FilePath ())
forall a b. (a -> b) -> a -> b
$ FilePath
"Illegal name: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. [a] -> a
head [FilePath]
bad
case Either FilePath ()
result of Right ()
_ -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn FilePath
"IdrisDoc generated"
Left FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
process FilePath
fn (PrintDef Name
n) =
do [Doc OutputAnnotation]
result <- Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
False Name
n
case [Doc OutputAnnotation]
result of
[] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Not found"
[Doc OutputAnnotation]
outs -> Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ())
-> [Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [Doc OutputAnnotation]
outs
process FilePath
fn (TransformInfo Name
n)
= do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
let ts :: [[(Type, Type)]]
ts = Name -> Ctxt [(Type, Type)] -> [[(Type, Type)]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [(Type, Type)]
idris_transforms IState
i)
let res :: [[Doc OutputAnnotation]]
res = ([(Type, Type)] -> [Doc OutputAnnotation])
-> [[(Type, Type)]] -> [[Doc OutputAnnotation]]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> [(Type, Type)] -> [Doc OutputAnnotation]
showTrans IState
i) [[(Type, Type)]]
ts
Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ()
iRenderResult (Doc OutputAnnotation -> StateT IState (ExceptT Err IO) ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> StateT IState (ExceptT Err IO) ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ())
-> [Doc OutputAnnotation] -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ [[Doc OutputAnnotation]] -> [Doc OutputAnnotation]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Doc OutputAnnotation]]
res
where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
showTrans :: IState -> [(Type, Type)] -> [Doc OutputAnnotation]
showTrans IState
i [] = []
showTrans IState
i ((Type
lhs, Type
rhs) : [(Type, Type)]
ts)
= let ppTm :: Type -> Doc OutputAnnotation
ppTm Type
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [] Type
tm) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
i) [] [] [] (PTerm -> Doc OutputAnnotation)
-> (Type -> PTerm) -> Type -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
IState -> Type -> PTerm
delab IState
i (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Type
tm
ts' :: [Doc OutputAnnotation]
ts' = IState -> [(Type, Type)] -> [Doc OutputAnnotation]
showTrans IState
i [(Type, Type)]
ts in
Type -> Doc OutputAnnotation
ppTm Type
lhs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
" ==> " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc OutputAnnotation
ppTm Type
rhs Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. a -> [a] -> [a]
: [Doc OutputAnnotation]
ts'
process FilePath
fn (PPrint OutputFmt
fmt Int
width (PRef FC
_ [FC]
_ Name
n))
= do [Doc OutputAnnotation]
outs <- Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
False Name
n
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> Idris FilePath -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OutputFmt -> Int -> Doc OutputAnnotation -> Idris FilePath
renderExternal OutputFmt
fmt Int
width ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
outs)
process FilePath
fn (PPrint OutputFmt
fmt Int
width PTerm
t)
= do (Type
tm, Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult (FilePath -> StateT IState (ExceptT Err IO) ())
-> Idris FilePath -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OutputFmt -> Int -> Doc OutputAnnotation -> Idris FilePath
renderExternal OutputFmt
fmt Int
width (IState -> Type -> Doc OutputAnnotation
pprintDelab IState
ist Type
tm)
process FilePath
fn Command
Quit = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':quit' is currently unsupported"
process FilePath
fn Command
Reload = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':reload' is currently unsupported"
process FilePath
fn Command
Watch = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':watch' is currently unsupported"
process FilePath
fn (Load FilePath
_ Maybe Int
_) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':load' is currently unsupported"
process FilePath
fn Command
Edit = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':edit' is currently unsupported"
process FilePath
fn Command
Proofs = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':proofs' is currently unsupported"
process FilePath
fn (Verbosity Int
_)
= FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
"Command ':verbosity' is currently unsupported"
showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal t :: Totality
t@(Partial (Other [Name]
ns)) IState
i
= FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"possibly not total due to:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> Doc OutputAnnotation
showTotalN IState
i) [Name]
ns)
showTotal t :: Totality
t@(Partial (Mutual [Name]
ns)) IState
i
= FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"possibly not total due to recursive path:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate Doc OutputAnnotation
forall a. Doc a
comma
((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n))
[Name]
ns))))
showTotal Totality
t IState
i = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (Totality -> FilePath
forall a. Show a => a -> FilePath
show Totality
t)
showTotalN :: IState -> Name -> Doc OutputAnnotation
showTotalN :: IState -> Name -> Doc OutputAnnotation
showTotalN IState
ist Name
n = case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
ist) of
[Totality
t] -> Name -> Doc OutputAnnotation
showN Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
", which is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
ist
[Totality]
_ -> Doc OutputAnnotation
forall a. Doc a
empty
where
ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
showN :: Name -> Doc OutputAnnotation
showN Name
n = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> FilePath -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> FilePath
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
ist) [] PPOption
ppo Bool
False Name
n
displayHelp :: FilePath
displayHelp = let vstr :: FilePath
vstr = Version -> FilePath
showVersion Version
getIdrisVersionNoGit in
FilePath
"\nIdris version " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"--------------" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map (\Char
x -> Char
'-') FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
(([FilePath], CmdArg, FilePath) -> FilePath)
-> [([FilePath], CmdArg, FilePath)] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([FilePath], CmdArg, FilePath) -> FilePath
forall a. Show a => ([FilePath], a, FilePath) -> FilePath
cmdInfo [([FilePath], CmdArg, FilePath)]
helphead FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
(([FilePath], CmdArg, FilePath) -> FilePath)
-> [([FilePath], CmdArg, FilePath)] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([FilePath], CmdArg, FilePath) -> FilePath
forall a. Show a => ([FilePath], a, FilePath) -> FilePath
cmdInfo [([FilePath], CmdArg, FilePath)]
help
where cmdInfo :: ([FilePath], a, FilePath) -> FilePath
cmdInfo ([FilePath]
cmds, a
args, FilePath
text) = FilePath
" " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col Int
16 Int
12 (FilePath -> [FilePath] -> FilePath
showSep FilePath
" " [FilePath]
cmds) (a -> FilePath
forall a. Show a => a -> FilePath
show a
args) FilePath
text
col :: Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col Int
c1 Int
c2 FilePath
l FilePath
m FilePath
r =
FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (Int
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
l) (Char -> FilePath
forall a. a -> [a]
repeat Char
' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (Int
c2 Int -> Int -> Int
forall a. Num a => a -> a -> a
- FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
m) (Char -> FilePath
forall a. a -> [a]
repeat Char
' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
r FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n"
pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
asCore Name
n =
do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
Context
ctxt <- Idris Context
getContext
let ambiguous :: Bool
ambiguous = [Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Name -> Context -> [Name]
lookupNames Name
n Context
ctxt) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
patdefs :: Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
patdefs = IState -> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
idris_patdefs IState
ist
tyinfo :: Ctxt TypeInfo
tyinfo = IState -> Ctxt TypeInfo
idris_datatypes IState
ist
if Bool
asCore
then [Doc OutputAnnotation] -> Idris [Doc OutputAnnotation]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Doc OutputAnnotation] -> Idris [Doc OutputAnnotation])
-> [Doc OutputAnnotation] -> Idris [Doc OutputAnnotation]
forall a b. (a -> b) -> a -> b
$ ((Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation)
-> [(Name, ([([(Name, Type)], Type, Type)], [PTerm]))]
-> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState
-> (Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation
ppCoreDef IState
ist) (Name
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
-> [(Name, ([([(Name, Type)], Type, Type)], [PTerm]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
patdefs)
else [Doc OutputAnnotation] -> Idris [Doc OutputAnnotation]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Doc OutputAnnotation] -> Idris [Doc OutputAnnotation])
-> [Doc OutputAnnotation] -> Idris [Doc OutputAnnotation]
forall a b. (a -> b) -> a -> b
$ ((Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation)
-> [(Name, ([([(Name, Type)], Type, Type)], [PTerm]))]
-> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation
ppDef Bool
ambiguous IState
ist) (Name
-> Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
-> [(Name, ([([(Name, Type)], Type, Type)], [PTerm]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n Ctxt ([([(Name, Type)], Type, Type)], [PTerm])
patdefs) [Doc OutputAnnotation]
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. [a] -> [a] -> [a]
++
((Name, TypeInfo) -> Doc OutputAnnotation)
-> [(Name, TypeInfo)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
ppTy Bool
ambiguous IState
ist) (Name -> Ctxt TypeInfo -> [(Name, TypeInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n Ctxt TypeInfo
tyinfo) [Doc OutputAnnotation]
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. [a] -> [a] -> [a]
++
(Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IState -> Name -> Doc OutputAnnotation
ppCon Bool
ambiguous IState
ist) ((Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Name -> Context -> Bool) -> Context -> Name -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Bool
isDConName Context
ctxt) (Name -> Context -> [Name]
lookupNames Name
n Context
ctxt))
where ppCoreDef :: IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
ppCoreDef :: IState
-> (Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation
ppCoreDef IState
ist (Name
n, ([([(Name, Type)], Type, Type)]
clauses, [PTerm]
missing)) =
case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[] -> FilePath -> Doc OutputAnnotation
forall a. HasCallStack => FilePath -> a
error FilePath
"Attempted pprintDef of TT of thing that doesn't exist"
(Type
ty:[Type]
_) -> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [] Type
ty) ([Name] -> Type -> Doc OutputAnnotation
pprintTT [] Type
ty)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((([(Name, Type)], Type, Type) -> Doc OutputAnnotation)
-> [([(Name, Type)], Type, Type)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\([(Name, Type)]
vars, Type
lhs, Type
rhs) -> [(Name, Type)] -> Type -> Type -> Doc OutputAnnotation
pprintTTClause [(Name, Type)]
vars Type
lhs Type
rhs) [([(Name, Type)], Type, Type)]
clauses)
ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
ppDef :: Bool
-> IState
-> (Name, ([([(Name, Type)], Type, Type)], [PTerm]))
-> Doc OutputAnnotation
ppDef Bool
amb IState
ist (Name
n, ([([(Name, Type)], Type, Type)]
clauses, [PTerm]
missing)) =
Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
IState -> [([(Name, Type)], Type, Type)] -> Doc OutputAnnotation
ppClauses IState
ist [([(Name, Type)], Type, Type)]
clauses Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> [PTerm] -> Doc OutputAnnotation
forall p a. p -> Doc a
ppMissing [PTerm]
missing
ppClauses :: IState -> [([(Name, Type)], Type, Type)] -> Doc OutputAnnotation
ppClauses IState
ist [] = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"No clauses."
ppClauses IState
ist [([(Name, Type)], Type, Type)]
cs = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((([(Name, Type)], Type, Type) -> Doc OutputAnnotation)
-> [([(Name, Type)], Type, Type)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Type)], Type, Type) -> Doc OutputAnnotation
pp [([(Name, Type)], Type, Type)]
cs)
where pp :: ([(Name, Type)], Type, Type) -> Doc OutputAnnotation
pp ([(Name, Type)]
varTys, Type
lhs, Type
rhs) =
let vars :: [Name]
vars = ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
varTys
ppTm :: Type -> Doc OutputAnnotation
ppTm Type
t = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Type
t) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist)
([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False))
[] (IState -> [FixDecl]
idris_infixes IState
ist) (PTerm -> Doc OutputAnnotation)
-> (Type -> PTerm) -> Type -> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
IState -> [(Name, Type)] -> Type -> PTerm
delabWithEnv IState
ist [(Name, Type)]
varTys (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
Type
t
in Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Type -> Doc OutputAnnotation
ppTm Type
lhs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
hang Int
2 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Type -> Doc OutputAnnotation
ppTm Type
rhs)
ppMissing :: p -> Doc a
ppMissing p
_ = Doc a
forall a. Doc a
empty
ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
ppTy Bool
amb IState
ist (Name
n, TI [Name]
constructors Bool
isCodata DataOpts
_ [Int]
_ [Name]
_ Bool
_)
= FilePath -> Doc OutputAnnotation
kwd FilePath
key Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
kwd FilePath
"where" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
2 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IState -> Name -> Doc OutputAnnotation
ppCon Bool
False IState
ist) [Name]
constructors))
where
key :: FilePath
key | Bool
isCodata = FilePath
"codata"
| Bool
otherwise = FilePath
"data"
kwd :: FilePath -> Doc OutputAnnotation
kwd = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate OutputAnnotation
AnnKeyword (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text
ppCon :: Bool -> IState -> Name -> Doc OutputAnnotation
ppCon Bool
amb IState
ist Name
n = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n)
helphead :: [([FilePath], CmdArg, FilePath)]
helphead =
[ ([FilePath
"Command"], CmdArg
SpecialHeaderArg, FilePath
"Purpose"),
([FilePath
""], CmdArg
NoArg, FilePath
"")
]
replSettings :: Maybe FilePath -> Settings Idris
replSettings :: Maybe FilePath -> Settings Idris
replSettings Maybe FilePath
hFile = CompletionFunc Idris -> Settings Idris -> Settings Idris
forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete CompletionFunc Idris
replCompletion (Settings Idris -> Settings Idris)
-> Settings Idris -> Settings Idris
forall a b. (a -> b) -> a -> b
$ Settings Idris
forall (m :: * -> *). MonadIO m => Settings m
defaultSettings {
historyFile :: Maybe FilePath
historyFile = Maybe FilePath
hFile
}