{-|
Module      : Idris.REPL
Description : Entry Point for the Idris REPL and CLI.
License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE CPP, FlexibleContexts, PatternGuards #-}
-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# 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)

-- | Run the REPL
repl :: IState -- ^ The initial state
     -> [FilePath] -- ^ The loaded modules
     -> FilePath -- ^ The file to edit (with :e)
     -> InputT Idris ()
repl :: IState -> [FilePath] -> FilePath -> InputT Idris ()
repl orig :: IState
orig mods :: [FilePath]
mods efile :: FilePath
efile
   = -- H.catch
     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 ""
                        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]
++ ">" 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]
++ " "
        Maybe FilePath
x <- InputT Idris (Maybe FilePath)
-> (SomeException -> InputT Idris (Maybe FilePath))
-> InputT Idris (Maybe FilePath)
forall (m :: * -> *) e a.
(MonadException m, Exception e) =>
m a -> (e -> m a) -> m a
H.catch (InputT Idris (Maybe FilePath) -> InputT Idris (Maybe FilePath)
forall (m :: * -> *) a.
MonadException 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 :: * -> *).
MonadException m =>
FilePath -> InputT m (Maybe FilePath)
getInputLine FilePath
prompt)
                     (InputT Idris (Maybe FilePath)
-> SomeException -> InputT Idris (Maybe FilePath)
forall a. InputT Idris a -> SomeException -> 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 ""))
        case Maybe FilePath
x of
            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 "Bye bye")
                          () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just input :: FilePath
input -> -- H.catch
                do Maybe [FilePath]
ms <- InputT Idris (Maybe [FilePath])
-> (SomeException -> InputT Idris (Maybe [FilePath]))
-> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) e a.
(MonadException m, Exception e) =>
m a -> (e -> m a) -> m a
H.catch (InputT Idris (Maybe [FilePath]) -> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a.
MonadException 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)
                                 (InputT Idris (Maybe [FilePath])
-> SomeException -> InputT Idris (Maybe [FilePath])
forall a. InputT Idris a -> SomeException -> 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)))
                   case Maybe [FilePath]
ms of
                        Just mods :: [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'
                        Nothing -> () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--                             ctrlC)
--       ctrlC
   where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
         ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
ctrlC act :: InputT Idris a
act e :: SomeException
e = 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 (SomeException -> FilePath
forall a. Show a => a -> FilePath
show SomeException
e)
                          InputT Idris a
act -- repl orig mods

         showMVs :: Bool -> ColourTheme -> [(a, b)] -> FilePath
showMVs c :: Bool
c thm :: ColourTheme
thm [] = ""
         showMVs c :: Bool
c thm :: ColourTheme
thm ms :: [(a, b)]
ms = "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' 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]
++ "\n"

         show' :: t -> Bool -> ColourTheme -> [a] -> FilePath
show' 0 c :: Bool
c thm :: ColourTheme
thm ms :: [a]
ms = let l :: Int
l = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ms in
                          "... ( + " 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]
++ " other"
                             FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then ")" else "s)"
         show' n :: t
n c :: Bool
c thm :: ColourTheme
thm [m :: a
m] = Bool -> ColourTheme -> a -> FilePath
forall a. Show a => Bool -> ColourTheme -> a -> FilePath
showM Bool
c ColourTheme
thm a
m
         show' n :: t
n c :: Bool
c thm :: ColourTheme
thm (m :: a
m : ms :: [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
forall a. [a] -> [a] -> [a]
++
                                  t -> Bool -> ColourTheme -> [a] -> FilePath
show' (t
n t -> t -> t
forall a. Num a => a -> a -> a
- 1) Bool
c ColourTheme
thm [a]
ms

         showM :: Bool -> ColourTheme -> a -> FilePath
showM c :: Bool
c thm :: ColourTheme
thm n :: 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

-- | Run the REPL server
startServer :: PortNumber -> IState -> [FilePath] -> Idris ()
startServer :: PortNumber
-> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
startServer port :: PortNumber
port orig :: IState
orig fn_in :: [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 port :: 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] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
fn_in)

        loop :: FilePath -> IState -> Socket -> IO b
loop fn :: FilePath
fn ist :: IState
ist sock :: Socket
sock
            = do (s :: Socket
s, _) <- 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 _ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Handle -> OutputMode
RawOutput Handle
h}
                              IdeMode n :: Integer
n _ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
n Handle
h}
                 (ist' :: IState
ist', fn :: 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 orig :: IState
orig i :: IState
i h :: Handle
h fn :: FilePath
fn cmd :: FilePath
cmd
    = do Either Err (IState, FilePath)
res <- case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i "(net)" FilePath
cmd of
                  Left err :: 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 " invalid command"))
                  Right (Right c :: 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 err :: 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 x :: (IState, FilePath)
x -> (IState, FilePath) -> IO (IState, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState, FilePath)
x
              Left err :: 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 fn :: FilePath
fn 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 fn :: FilePath
fn (Load f :: FilePath
f toline :: Maybe Int
toline) =
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
        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 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 fn :: FilePath
fn c :: 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 h :: 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 _ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Handle -> OutputMode
RawOutput Handle
h}
           IdeMode n :: Integer
n _ -> IState
ist {idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
n Handle
h}

-- | Run a command on the server on localhost
runClient :: Maybe PortNumber -> String -> IO ()
runClient :: Maybe PortNumber -> FilePath -> IO ()
runClient port :: Maybe PortNumber
port str :: 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 (127,0,0,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 "" Handle
h
                  FilePath -> IO ()
putStr FilePath
resp
                  Handle -> IO ()
hClose Handle
h

                Left err :: SomeException
err -> do
                  SomeException -> IO ()
connectionError SomeException
err
                  ExitCode -> IO ()
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure 1)

    where hGetResp :: FilePath -> Handle -> IO FilePath
hGetResp acc :: FilePath
acc h :: 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]
++ "\n") Handle
h

          connectionError :: X.SomeException -> IO ()
          connectionError :: SomeException -> IO ()
connectionError _ =
            FilePath -> IO ()
putStrLn "Unable to connect to a running Idris repl"


initIdemodeSocket :: IO Handle
initIdemodeSocket :: IO Handle
initIdemodeSocket = do
  (sock :: Socket
sock, port :: 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
  (s :: Socket
s, _) <- 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

-- | Run the IdeMode
idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()
idemodeStart :: Bool -> IState -> [FilePath] -> StateT IState (ExceptT Err IO) ()
idemodeStart s :: Bool
s orig :: IState
orig mods :: [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
       IState
i <- StateT IState (ExceptT Err IO) IState
getIState
       case IState -> OutputMode
idris_outputmode IState
i of
         IdeMode n :: Integer
n h :: 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 "protocol-version" Int
IdeMode.ideModeEpoch Integer
n
              case [FilePath]
mods of
                a :: FilePath
a:_ -> Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> StateT IState (ExceptT Err IO) ()
runIdeModeCommand Handle
h Integer
n IState
i "" [] (FilePath -> Maybe Int -> IdeModeCommand
IdeMode.LoadFile FilePath
a Maybe Int
forall a. Maybe a
Nothing)
                _   -> () -> 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 h :: Handle
h orig :: IState
orig mods :: [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 -> Err -> Idris Int
forall a. Err -> Idris a
ierror Err
err
               Right n :: Int
n  -> Int -> Idris 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 ""
             (sexp :: SExp
sexp, id :: Integer
id) <- case FilePath -> Either Err (SExp, Integer)
IdeMode.parseMessage FilePath
l of
                             Left err :: Err
err -> Err -> Idris (SExp, Integer)
forall a. Err -> Idris a
ierror Err
err
                             Right (sexp :: SExp
sexp, id :: Integer
id) -> (SExp, Integer) -> Idris (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 -- to report correct id back!
               (do let fn :: FilePath
fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe "" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
mods)
                   case SExp -> Maybe IdeModeCommand
IdeMode.sexpToCommand SExp
sexp of
                     Just cmd :: 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
                     Nothing  -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "did not understand" )
               (\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))
         (\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

-- | Run IDEMode commands
runIdeModeCommand :: Handle -- ^^ The handle for communication
                   -> Integer -- ^^ The continuation ID for the client
                   -> IState -- ^^ The original IState
                   -> FilePath -- ^^ The current open file
                   -> [FilePath] -- ^^ The currently loaded modules
                   -> IdeMode.IdeModeCommand -- ^^ The command to process
                   -> Idris ()
runIdeModeCommand :: Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> StateT IState (ExceptT Err IO) ()
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.Interpret cmd :: 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 "(input)" FilePath
cmd of
       Left err :: 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 mode :: Bool
mode n' :: 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 n :: Integer
n h :: Handle
h -> -- signal completion of proof to ide
                   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 "return"
                       (FilePath -> SExp
IdeMode.SymbolAtom "ok", "")
                       Integer
n
                 _ -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           (\e :: 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 n :: Integer
n h :: 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 "abandon-proof" "Abandoned" Integer
n
                       _ -> () -> 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 cmd :: 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)
                        (\e :: 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 err :: FilePath
err) -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.REPLCompletions str :: FilePath
str) =
  do (unused :: FilePath
unused, compls :: [Completion]
compls) <- CompletionFunc Idris
replCompletion (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
str, "")
     let good :: SExp
good = [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom "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 "return" SExp
good Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.LoadFile filename :: FilePath
filename toline :: Maybe Int
toline) =
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
  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)
     -- Report either success or failure
     IState
i <- StateT IState (ExceptT Err IO) IState
getIState
     case (IState -> Maybe FC
errSpan IState
i) of
       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 "ok",
                                                      [SExp] -> SExp
IdeMode.SexpList []])
                                  (\fc :: FC
fc -> [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom "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 "return" SExp
msg Integer
id
       Just x :: 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
$ "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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.TypeOf name :: FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
    Right n :: Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process "(idemode)"
                 (PTerm -> Command
Check (FC -> [FC] -> Name -> PTerm
PRef (FilePath -> (Int, Int) -> (Int, Int) -> FC
FC "(idemode)" (0,0) (0,0)) [] Name
n))
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.DocsFor name :: FilePath
name w :: WhatDocs
w) =
  case IState -> FilePath -> Either ParseError Const
parseConst IState
orig FilePath
name of
    Right c :: Const
c -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process "(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 _ ->
     case FilePath -> Either FilePath Name
splitName FilePath
name of
       Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
       Right n :: Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process "(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 IdeMode.Overview = HowMuchDocs
OverviewDocs
        howMuch IdeMode.Full     = HowMuchDocs
FullDocs
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.CaseSplit line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.AddClause line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.AddProofClause line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.AddMissing line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.MakeWithBlock line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.MakeCaseBlock line :: Int
line name :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.ProofSearch r :: Bool
r line :: Int
line name :: FilePath
name hints :: [FilePath]
hints depth :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.MakeLemma line :: Int
line name :: FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
    Right n :: Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeLemma Bool
False Int
line Name
n)
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.Apropos a :: FilePath
a) =
  FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PkgName] -> FilePath -> Command
Apropos [] FilePath
a)
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [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 "ok",
                    [(FilePath -> SExp
IdeMode.SymbolAtom "show-implicits", Bool
impshow),
                     (FilePath -> SExp
IdeMode.SymbolAtom "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 "return" (SExp, [(SExp, Bool)])
options Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.SetOpt IdeMode.ShowImpl b :: Bool
b) =
  do Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
b
     let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom "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 "return" (SExp, Bool)
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.SetOpt IdeMode.ErrContext b :: Bool
b) =
  do Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
b
     let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom "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 "return" (SExp, Bool)
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.Metavariables cols :: 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)
                         | (n :: Name
n, (_, i :: Int
i, _, _, _)) <- 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)
                         ]
     -- splitMvs is a list of pairs of names and their split types
     let splitMvs :: [(Name, ([(Name, Type, PTerm)], Type, PTerm))]
splitMvs = [ (Name
n, ([(Name, Type, PTerm)]
premises, Type
concl, PTerm
tm))
                    | (n :: Name
n, i :: Int
i, ty :: Type
ty) <- IState -> [(Name, Int)] -> [(Name, Int, Type)]
mvTys IState
ist [(Name, Int)]
mvs
                    , let (premises :: [(Name, Type, PTerm)]
premises, concl :: Type
concl, tm :: PTerm
tm) = IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi IState
ist Int
i Type
ty]
     -- mvOutput is the pretty-printed version ready for conversion to SExpr
     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 (\(n :: FilePath
n, (hs :: [(FilePath, FilePath, SpanList OutputAnnotation)]
hs, c :: (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
                            (\(hs :: [(Name, Type, PTerm)]
hs, c :: Type
c, pc :: PTerm
pc) ->
                             let bnd :: [Name]
bnd = [ Name
n | (n :: Name
n,_,_) <- [(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 (\(bnd :: [Name]
bnd, h :: (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 "return" (FilePath -> SExp
IdeMode.SymbolAtom "ok", [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
  (FilePath, SpanList OutputAnnotation))]
mvOutput) Integer
id
  where mapPair :: (b -> a) -> (b -> b) -> [(b, b)] -> [(a, b)]
mapPair f :: b -> a
f g :: b -> b
g xs :: [(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)
        -- | Split a function type into a pair of premises, conclusion.
        -- Each maintains both the original and delaborated versions.
        splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
        splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi ist :: IState
ist i :: Int
i (Bind n :: Name
n (Pi _ _ t :: Type
t _) rest :: Type
rest) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 =
          let (hs :: [(Name, Type, PTerm)]
hs, c :: Type
c, _) = IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
splitPi IState
ist (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 ist :: IState
ist i :: Int
i tm :: Type
tm = ([], Type
tm, IState
-> [PArg]
-> [(Name, Type)]
-> Type
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Type
tm Bool
False Bool
False Bool
True)

        -- | Get the types of a list of metavariable names
        mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
        mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
mvTys ist :: IState
ist mvs :: [(Name, Int)]
mvs = [ (Name
n, Int
i, Type
ty)
                        | (n :: Name
n, i :: 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)))
                        ]

        -- | Show a type and its corresponding PTerm in a format suitable
        -- for the IDE - that is, pretty-printed and annotated.
        render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
        render :: IState
-> [Name] -> Type -> PTerm -> (FilePath, SpanList OutputAnnotation)
render ist :: IState
ist bnd :: [Name]
bnd t :: Type
t pt :: 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 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

        -- | Juggle the bits of a premise to prepare for output.
        processPremise :: IState
                       -> [Name] -- ^ the names to highlight as bound
                       -> (Name, Type, PTerm)
                       -> (String,
                           String,
                           SpanList OutputAnnotation)
        processPremise :: IState
-> [Name]
-> (Name, Type, PTerm)
-> (FilePath, FilePath, SpanList OutputAnnotation)
processPremise ist :: IState
ist bnd :: [Name]
bnd (n :: Name
n, t :: Type
t, pt :: PTerm
pt) =
          let (out :: FilePath
out, spans :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.WhoCalls n :: FilePath
n) =
  case FilePath -> Either FilePath Name
splitName FilePath
n of
       Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
       Right n :: 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 "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 (\ (n :: Name
n,ns :: [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 "return" (SExp,
 [((FilePath, SpanList OutputAnnotation),
   [(FilePath, SpanList OutputAnnotation)])])
msg Integer
id
  where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn ist :: 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 0.9 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.CallsWho n :: FilePath
n) =
  case FilePath -> Either FilePath Name
splitName FilePath
n of
       Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
       Right n :: 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 "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 (\ (n :: Name
n,ns :: [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 "return" (SExp,
 [((FilePath, SpanList OutputAnnotation),
   [(FilePath, SpanList OutputAnnotation)])])
msg Integer
id
  where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn ist :: 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 0.9 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.BrowseNS ns :: FilePath
ns) =
  case FilePath -> FilePath -> [FilePath]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn "." FilePath
ns of
    [] -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "No namespace provided"
    ns :: [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 ".") (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 "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 "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 "return" (SExp, ([FilePath], [(FilePath, SpanList OutputAnnotation)]))
msg Integer
id
  where pn :: Name
-> StateT
     IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
pn n :: 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 0.9 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 t :: 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 -> Type -> Doc OutputAnnotation
pprintDelab IState
ist Type
t))
                   Nothing ->
                     Doc OutputAnnotation
forall a. Doc a
empty

runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.TermNormalise bnd :: [(Name, Bool)]
bnd tm :: 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 "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 0.9 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 "return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.TermShowImplicits bnd :: [(Name, Bool)]
bnd tm :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.TermNoImplicits bnd :: [(Name, Bool)]
bnd tm :: 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 h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.TermElab bnd :: [(Name, Bool)]
bnd tm :: 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 "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 0.9 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 "return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn mods :: [FilePath]
mods (IdeMode.PrintDef name :: FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
    Right n :: Name
n -> FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process "(idemode)" (Name -> Command
PrintDef Name
n)
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.ErrString e :: 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 1.0 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 "ok", FilePath -> SExp
IdeMode.StringAtom (FilePath -> SExp) -> FilePath -> SExp
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
out "")
     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 "return" (SExp, SExp)
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes (IdeMode.ErrPPrint e :: Err
e) =
  do IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
     let (out :: FilePath
out, spans :: 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 0.9 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 "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 "return" (SExp, FilePath, SpanList OutputAnnotation)
msg Integer
id
runIdeModeCommand h :: Handle
h id :: Integer
id orig :: IState
orig fn :: FilePath
fn modes :: [FilePath]
modes 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 "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 "return" (SExp, ([Int], [FilePath]))
msg Integer
id


-- | Show a term for IDEMode with the specified implicitness
ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits :: Handle
-> Integer
-> [(Name, Bool)]
-> Bool
-> Type
-> StateT IState (ExceptT Err IO) ()
ideModeForceTermImplicits h :: Handle
h id :: Integer
id bnd :: [(Name, Bool)]
bnd impl :: Bool
impl tm :: 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 "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 0.9 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 "return" (SExp, (FilePath, SpanList OutputAnnotation))
msg Integer
id

splitName :: String -> Either String Name
splitName :: FilePath -> Either FilePath Name
splitName s :: FilePath
s | "{{{{{" 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 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 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 x :: FilePath
x =
          case ByteString -> Either FilePath ByteString
Base64.decode (FilePath -> ByteString
UTF8.fromString FilePath
x) of
            Left err :: FilePath
err -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left FilePath
err
            Right ok :: 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 _ -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left "Bad binary instance for Name"
                Right (_, _, n :: b
n) -> b -> Either FilePath b
forall a b. b -> Either a b
Right b
n

splitName s :: 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
s of
                [] -> FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left ("Didn't understand name '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'")
                [n :: 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
                (n :: FilePath
n:ns :: [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 "" = ""
        unparen ('(':x :: Char
x:xs :: FilePath
xs) | FilePath -> Char
forall a. [a] -> a
last FilePath
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')' = FilePath -> FilePath
forall a. [a] -> [a]
init (Char
xChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)
        unparen str :: FilePath
str = FilePath
str

idemodeProcess :: FilePath -> Command -> Idris ()
idemodeProcess :: FilePath -> Command -> StateT IState (ExceptT Err IO) ()
idemodeProcess fn :: FilePath
fn ShowVersion = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
ShowVersion
idemodeProcess fn :: FilePath
fn Warranty = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Warranty
idemodeProcess fn :: FilePath
fn Help = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Help
idemodeProcess fn :: FilePath
fn (RunShellCommand cmd :: FilePath
cmd) =
  FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError ":! is not currently supported in IDE mode."
idemodeProcess fn :: FilePath
fn (ChangeDirectory f :: 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
$ "changed directory to " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
dir
idemodeProcess fn :: FilePath
fn (ModImport f :: FilePath
f) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (FilePath -> Command
ModImport FilePath
f)
idemodeProcess fn :: FilePath
fn (Eval t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Eval PTerm
t)
idemodeProcess fn :: FilePath
fn (NewDefn decls :: [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 "defined"
idemodeProcess fn :: FilePath
fn (Undefine n :: [Name]
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([Name] -> Command
Undefine [Name]
n)
idemodeProcess fn :: FilePath
fn (ExecVal t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
ExecVal PTerm
t)
idemodeProcess fn :: FilePath
fn (Check (PRef x :: FC
x hls :: [FC]
hls n :: 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 fn :: FilePath
fn (Check t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Check PTerm
t)
idemodeProcess fn :: FilePath
fn (Core t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Core PTerm
t)
idemodeProcess fn :: FilePath
fn (DocStr n :: Either Name Const
n w :: 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 fn :: FilePath
fn Universes = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Universes
idemodeProcess fn :: FilePath
fn (Defn n :: 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 ""
idemodeProcess fn :: FilePath
fn (TotCheck n :: Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
TotCheck Name
n)
idemodeProcess fn :: FilePath
fn (DebugInfo n :: 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 ""
idemodeProcess fn :: FilePath
fn (Search ps :: [PkgName]
ps t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn ([PkgName] -> PTerm -> Command
Search [PkgName]
ps PTerm
t)
idemodeProcess fn :: FilePath
fn (Spec t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Spec PTerm
t)
-- RmProof and AddProof not supported!
idemodeProcess fn :: FilePath
fn (ShowProof n' :: Name
n') = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
ShowProof Name
n')
idemodeProcess fn :: FilePath
fn (WHNF t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
WHNF PTerm
t)
--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!
idemodeProcess fn :: FilePath
fn (TestInline t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
TestInline PTerm
t)

idemodeProcess fn :: FilePath
fn (Execute t :: 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 ""
idemodeProcess fn :: FilePath
fn (Compile codegen :: Codegen
codegen f :: 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 ""
idemodeProcess fn :: FilePath
fn (LogLvl i :: 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 ""
idemodeProcess fn :: FilePath
fn (Pattelab t :: PTerm
t) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (PTerm -> Command
Pattelab PTerm
t)
idemodeProcess fn :: FilePath
fn (Missing n :: Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
Missing Name
n)
idemodeProcess fn :: FilePath
fn (DynamicLink l :: 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 ""
idemodeProcess fn :: FilePath
fn ListDynamic = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
ListDynamic
                                   FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn Metavars = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn Command
Metavars
idemodeProcess fn :: FilePath
fn (SetOpt ErrContext) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ErrContext)
                                           FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (UnsetOpt ErrContext) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ErrContext)
                                             FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (SetOpt ShowImpl) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ShowImpl)
                                         FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (UnsetOpt ShowImpl) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ShowImpl)
                                           FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (SetOpt ShowOrigErr) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
ShowOrigErr)
                                            FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (UnsetOpt ShowOrigErr) = do FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
ShowOrigErr)
                                              FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult ""
idemodeProcess fn :: FilePath
fn (SetOpt x :: Opt
x) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
SetOpt Opt
x)
idemodeProcess fn :: FilePath
fn (UnsetOpt x :: Opt
x) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Opt -> Command
UnsetOpt Opt
x)
idemodeProcess fn :: FilePath
fn (CaseSplitAt False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
CaseSplitAt Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (AddProofClauseFrom False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddProofClauseFrom Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (AddClauseFrom False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddClauseFrom Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (AddMissing False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddMissing Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (MakeWith False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeWith Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (MakeCase False pos :: Int
pos str :: Name
str) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeCase Bool
False Int
pos Name
str)
idemodeProcess fn :: FilePath
fn (DoProofSearch False r :: Bool
r pos :: Int
pos str :: Name
str xs :: [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 fn :: FilePath
fn (SetConsoleWidth w :: 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 ""
idemodeProcess fn :: FilePath
fn (SetPrinterDepth d :: 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 ""
idemodeProcess fn :: FilePath
fn (Apropos pkg :: [PkgName]
pkg a :: 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 ""
idemodeProcess fn :: FilePath
fn (WhoCalls n :: Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
WhoCalls Name
n)
idemodeProcess fn :: FilePath
fn (CallsWho n :: Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
CallsWho Name
n)
idemodeProcess fn :: FilePath
fn (PrintDef n :: Name
n) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (Name -> Command
PrintDef Name
n)
idemodeProcess fn :: FilePath
fn (PPrint fmt :: OutputFmt
fmt n :: Int
n tm :: PTerm
tm) = FilePath -> Command -> StateT IState (ExceptT Err IO) ()
process FilePath
fn (OutputFmt -> Int -> PTerm -> Command
PPrint OutputFmt
fmt Int
n PTerm
tm)
idemodeProcess fn :: FilePath
fn _ = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "command not recognized or not supported"


-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
mkPrompt :: [FilePath] -> FilePath
mkPrompt [] = "Idris"
mkPrompt [x :: FilePath
x] = "*" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
dropExtension FilePath
x
mkPrompt (x :: FilePath
x:xs :: [FilePath]
xs) = "*" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
dropExtension FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
mkPrompt [FilePath]
xs

-- | Determine whether a file uses literate syntax
lit :: FilePath -> Bool
lit f :: FilePath
f = case FilePath -> (FilePath, FilePath)
splitExtension FilePath
f of
            (_, ".lidr") -> Bool
True
            _ -> Bool
False

reload :: IState -> [FilePath] -> Idris (Maybe [FilePath])
reload :: IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload orig :: IState
orig inputs :: [FilePath]
inputs = do
  IState
i <- StateT IState (ExceptT Err IO) IState
getIState
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
  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 orig :: IState
orig inputs :: [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
$ \mgr :: 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
$ \dir :: 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 _ -> 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) -- canceled, so nop
    Right _ -> 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 cmd :: FilePath
cmd orig :: IState
orig inputs :: [FilePath]
inputs efile :: 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] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
inputs)
         case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i "(input)" FilePath
cmd of
            Left err :: 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 Reload) ->
                IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs
            Right (Right Watch) ->
                if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
inputs then
                  do FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn "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
$ "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]
++ ", press enter to cancel."
                     IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs
            Right (Right (Load f :: FilePath
f toline :: Maybe Int
toline)) ->
                -- The $!! here prevents a space leak on reloading.
                -- This isn't a solution - but it's a temporary stopgap.
                -- See issue #2386
                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 f :: 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 Edit) -> do -- takeMVar stvar
                               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 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 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 "Bye bye")
            Right (Right cmd :: 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)
                                            (\e :: 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 err :: 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 n' :: 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
                 [x :: 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'
                 ns :: [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 n :: 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 "" orig :: IState
orig = FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn "Nothing to edit"
edit f :: FilePath
f orig :: 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 l :: FC
l -> '+' 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))
                        Nothing -> ""
         let cmdLine :: FilePath
cmdLine = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate " " [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
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
         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
--          clearOrigPats
         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 env :: [(FilePath, FilePath)]
env | Just ed :: FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "EDITOR" [(FilePath, FilePath)]
env = FilePath
ed
                       | Just ed :: FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "VISUAL" [(FilePath, FilePath)]
env = FilePath
ed
                       | Bool
otherwise = "vi"
         fixName :: FilePath -> FilePath
fixName file :: 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` [".lidr", ".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 "idr"
            where
                quoteChar :: Char
quoteChar = if Bool
isWindows then '"' else '\''
                quote :: FilePath -> FilePath
quote s :: 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 orig :: 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 "No proofs available"
            _  -> 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
$ "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 prf :: FilePath
prf [] = "\n---------- Proofs ----------" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: "" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath
prf]
insertScript prf :: FilePath
prf (p :: FilePath
p@FilePath
"---------- Proofs ----------" : "" : xs :: [FilePath]
xs)
    = FilePath
p FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: "" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
prf FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
xs
insertScript prf :: FilePath
prf (x :: FilePath
x : xs :: [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 fn :: FilePath
fn Help = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
displayHelp
process fn :: FilePath
fn ShowVersion = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
getIdrisVersion
process fn :: FilePath
fn Warranty = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintResult FilePath
warranty
process fn :: FilePath
fn (RunShellCommand cmd :: 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 fn :: FilePath
fn (ChangeDirectory f :: 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 fn :: FilePath
fn (ModImport f :: 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 pr :: FilePath
pr -> FilePath -> StateT IState (ExceptT Err IO) ()
isetPrompt FilePath
pr
                                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
$ "Can't find import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
process fn :: FilePath
fn (Eval t :: 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 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
                      (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 "foreign",
                                                   FilePath -> Name
sUN "prim_read",
                                                   FilePath -> Name
sUN "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
                      -- Add value to context, call it "it"
                      (Context -> Context) -> StateT IState (ExceptT Err IO) ()
updateContext (Name -> Def -> Context -> Context
addCtxtDef (FilePath -> Name
sUN "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 3 (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ "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 10 (FilePath -> StateT IState (ExceptT Err IO) ())
-> FilePath -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ "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'
                          -- errReverse to make type more readable
                          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 tm :: Type
tm | Int -> Type -> Bool
termSmallerThan 100 Type
tm = Type -> Type
forall a. NFData a => a -> a
force Type
tm
                        | Bool
otherwise = Type
tm

process fn :: FilePath
fn (NewDefn decls :: [PDecl]
decls) = do
        Int -> FilePath -> StateT IState (ExceptT Err IO) ()
logParser 3 ("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 (\d1 :: PDecl
d1 d2 :: 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 docs :: Docstring (Either Err PTerm)
docs argdocs :: [(Name, Docstring (Either Err PTerm))]
argdocs syn :: SyntaxInfo
syn fc :: FC
fc opts :: FnOpts
opts name :: Name
name _ ty :: PTerm
ty) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
  getName (PClauses fc :: FC
fc opts :: FnOpts
opts name :: Name
name (clause :: PClause' PTerm
clause:clauses :: [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 doc :: Docstring (Either Err PTerm)
doc argdocs :: [(Name, Docstring (Either Err PTerm))]
argdocs syn :: SyntaxInfo
syn fc :: FC
fc opts :: DataOpts
opts dataDecl :: 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 doc :: Docstring (Either Err PTerm)
doc syn :: SyntaxInfo
syn fc :: FC
fc constraints :: [(Name, PTerm)]
constraints name :: Name
name nfc :: FC
nfc parms :: [(Name, FC, PTerm)]
parms parmdocs :: [(Name, Docstring (Either Err PTerm))]
parmdocs fds :: [(Name, FC)]
fds decls :: [PDecl]
decls _ _) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
  getName _ = Maybe Name
forall a. Maybe a
Nothing
  -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
  getClauseName :: PClause' t -> Name
getClauseName (PClause fc :: FC
fc name :: Name
name whole :: t
whole with :: [t]
with rhs :: t
rhs whereBlock :: [PDecl' t]
whereBlock) = Name
name
  getClauseName (PWith fc :: FC
fc name :: Name
name whole :: t
whole with :: [t]
with rhs :: t
rhs pn :: Maybe (Name, FC)
pn whereBlock :: [PDecl' t]
whereBlock) = Name
name
  defineName :: [PDecl] -> Idris ()
  defineName :: [PDecl] -> StateT IState (ExceptT Err IO) ()
defineName (tyDecl :: PDecl
tyDecl@(PTy docs :: Docstring (Either Err PTerm)
docs argdocs :: [(Name, Docstring (Either Err PTerm))]
argdocs syn :: SyntaxInfo
syn fc :: FC
fc opts :: FnOpts
opts name :: Name
name _ ty :: PTerm
ty) : decls :: [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
fc opts :: FnOpts
opts _ [clause :: PClause' PTerm
clause]] = do
    let pterm :: PTerm
pterm = PClause' PTerm -> PTerm
getRHS PClause' PTerm
clause
    (tm :: Type
tm,ty :: 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{} : _) = 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 "Only one function body is allowed without a type declaration.")
  -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
  defineName (PFix fc :: FC
fc fixity :: Fixity
fixity strs :: [FilePath]
strs : defns :: [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 _ syntax :: Syntax
syntax:_) = 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 decls :: [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
fc opts :: FnOpts
opts name :: Name
name clauses :: [PClause' t]
clauses) = [PClause' t]
clauses
  getClauses _ = []
  getRHS :: PClause -> PTerm
  getRHS :: PClause' PTerm -> PTerm
getRHS (PClause fc :: FC
fc name :: Name
name whole :: PTerm
whole with :: [PTerm]
with rhs :: PTerm
rhs whereBlock :: [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PWith fc :: FC
fc name :: Name
name whole :: PTerm
whole with :: [PTerm]
with rhs :: PTerm
rhs pn :: Maybe (Name, FC)
pn whereBlock :: [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PClauseR fc :: FC
fc with :: [PTerm]
with rhs :: PTerm
rhs whereBlock :: [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PWithR fc :: FC
fc with :: [PTerm]
with rhs :: PTerm
rhs pn :: Maybe (Name, FC)
pn whereBlock :: [PDecl]
whereBlock) = PTerm
rhs
  setReplDefined :: Maybe Name -> Idris ()
  setReplDefined :: Maybe Name -> StateT IState (ExceptT Err IO) ()
setReplDefined Nothing = () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  setReplDefined (Just n :: 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]
:)
  -- the "name" field of PClauses seems to always be MN 2 "__", so we need to
  -- retrieve the actual name from deeper inside.
  -- This should really be a full recursive walk through the structure of PDecl, but
  -- I think it should work this way and I want to test sooner. Also lazy.
  fixClauses :: PDecl' t -> PDecl' t
  fixClauses :: PDecl' t -> PDecl' t
fixClauses (PClauses fc :: FC
fc opts :: FnOpts
opts _ css :: [PClause' t]
css@(clause :: PClause' t
clause:cs :: [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 doc :: Docstring (Either Err t)
doc argDocs :: [(Name, Docstring (Either Err t))]
argDocs syn :: SyntaxInfo
syn fc :: FC
fc constraints :: [(Name, t)]
constraints pnames :: [Name]
pnames acc :: Accessibility
acc opts :: FnOpts
opts cls :: Name
cls nfc :: FC
nfc parms :: [t]
parms pextra :: [(Name, t)]
pextra ty :: t
ty implName :: Maybe Name
implName decls :: [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 decl :: PDecl' t
decl = PDecl' t
decl

  info :: ElabInfo
info = FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "toplevel")

process fn :: FilePath
fn (Undefine names :: [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 []
    -- Keep track of which names you've removed so you can
    -- print them out to the user afterward
    undefine names :: [Name]
names = [Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
names []
    undefine' :: [Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [] list :: [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' (n :: Name
n:names :: [Name]
names) already :: [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 ("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]
++ " because it wasn't defined at the repl")
                 [Name] -> [Name] -> StateT IState (ExceptT Err IO) ()
undefine' [Name]
names [Name]
already
    undefOne :: Name -> m ()
undefOne n :: 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
                    -- for now just assume it's an interface. Eventually we'll want some kind of
                    -- smart detection of exactly what kind of name we're undefining.
                    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 n :: 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 ns :: [Name]
ns -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub [Name]
ns
                        Nothing -> FilePath -> [Name]
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail ("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 fn :: FilePath
fn (ExecVal t :: PTerm
t)
                  = do Context
ctxt <- Idris Context
getContext
                       IState
ist <- StateT IState (ExceptT Err IO) IState
getIState
                       (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "toplevel")) ElabMode
ERHS PTerm
t
--                       let tm' = normaliseAll ctxt [] tm
                       let ty' :: Type
ty' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty
                       Type
res <- Type -> Idris Type
execute Type
tm
                       let (resOut :: Doc OutputAnnotation
resOut, tyOut :: 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 fn :: FilePath
fn (Check (PRef _ _ n :: 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@(t :: Name
t:_) ->
            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 (_, i :: Int
i, _, _, _) -> 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
                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 (\n :: 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
$ "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 n :: Name
n ctxt :: 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 ppo :: PPOption
ppo ist :: IState
ist n :: Name
n i :: Int
i
         = case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
                (ty :: Type
ty:_) -> 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 ppo :: PPOption
ppo ist :: IState
ist 0 bnd :: [(Name, Bool)]
bnd sc :: 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 ppo :: PPOption
ppo ist :: IState
ist i :: Int
i bnd :: [(Name, Bool)]
bnd (PPi p :: Plicity
p n :: Name
n _ t :: PTerm
t sc :: PTerm
sc)
               = let current :: Doc OutputAnnotation
current = case Name
n of
                                   MN _ _ -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text ""
                                   UN nm :: Text
nm | ('_':'_':_) <- Text -> FilePath
str Text
nm -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text ""
                                   _ -> 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
-1) ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) PTerm
sc
    putTy ppo :: PPOption
ppo ist :: IState
ist _ bnd :: [(Name, Bool)]
bnd sc :: 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 ppo :: p
ppo ist :: IState
ist bnd :: [(Name, Bool)]
bnd g :: PTerm
g
               = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "--------------------------------------" 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)

    -- Only display count if linear types extension is enabled
    countOf :: RigCount -> Bool -> Doc a
countOf Rig0 True = FilePath -> Doc a
forall a. FilePath -> Doc a
text "0"
    countOf Rig1 True = FilePath -> Doc a
forall a. FilePath -> Doc a
text "1"
    countOf _ _ = FilePath -> Doc a
forall a. FilePath -> Doc a
text " "

    tPretty :: [(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty bnd :: [(Name, Bool)]
bnd ist :: IState
ist t :: 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 fn :: FilePath
fn (Check t :: PTerm
t)
   = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 _ ->
             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
           _ -> 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 fn :: FilePath
fn (Core t :: PTerm
t)
   = case PTerm
t of
       PRef _ _ n :: 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 _ _ _ _ _ _] -> 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
              _ -> PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm PTerm
t
       t :: PTerm
t -> PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm PTerm
t
   where coreTerm :: PTerm -> StateT IState (ExceptT Err IO) ()
coreTerm t :: PTerm
t =
           do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 fn :: FilePath
fn (DocStr (Left n :: Name
n) w :: HowMuchDocs
w)
  | UN ty :: Text
ty <- Name
n, Text
ty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
T.pack "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 (\(n :: Name
n,d :: 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
$ "No documentation for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
          ns :: [(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 ist :: IState
ist (n :: Name
n, d :: 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 n :: Text
n) ns :: [Text]
ns) = Name -> [Text] -> Name
NS Name
modDocName (Text
nText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
ns)
          modDocN (UN n :: Text
n)         = Name -> [Text] -> Name
NS Name
modDocName [Text
n]
          modDocN _              = Int -> FilePath -> Name
sMN 1 "NotFoundForSure"

process fn :: FilePath
fn (DocStr (Right c :: Const
c) _) -- constants only have overviews
   = 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 fn :: FilePath
fn 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
--                        iputStrLn $ showSep "\n" (map show 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 "\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
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " constraints)"
                          case Set ConstraintFC -> TC ()
ucheck Set ConstraintFC
cs of
                            Error e :: 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 "Universes OK"
process fn :: FilePath
fn (Defn n :: 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 "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
                                [(d :: [([(Name, Type)], Type, Type)]
d, _)] -> FilePath -> Doc a
forall a. FilePath -> Doc a
text "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
                                 [t :: Totality
t] -> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
i
                                 _ -> 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 i :: IState
i (_, lhs :: Type
lhs, rhs :: 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 "=" 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 fn :: FilePath
fn (TotCheck n :: 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
$ "Unknown operator " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
           ts :: [(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 n :: 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 (\(n :: Name
n, t :: Totality
t) -> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
hang 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 "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 fn :: FilePath
fn (DebugUnify l :: PTerm
l r :: PTerm
r)
   = do (ltm :: Type
ltm, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "toplevel")) ElabMode
ERHS PTerm
l
        (rtm :: Type
rtm, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 ans :: ([(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 e :: Err
e -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn (Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e)

process fn :: FilePath
fn (DebugInfo n :: 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
$ "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
$ "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 "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 fn :: FilePath
fn (Search pkgs :: [PkgName]
pkgs t :: PTerm
t) = [PkgName] -> PTerm -> StateT IState (ExceptT Err IO) ()
searchByType [PkgName]
pkgs PTerm
t
process fn :: FilePath
fn (CaseSplitAt updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
caseSplitAt FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (AddClauseFrom updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (AddProofClauseFrom updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addProofClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (AddMissing updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (MakeWith updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeWith FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (MakeCase updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeCase FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (MakeLemma updatefile :: Bool
updatefile l :: Int
l n :: Name
n)
    = FilePath
-> Bool -> Int -> Name -> StateT IState (ExceptT Err IO) ()
makeLemma FilePath
fn Bool
updatefile Int
l Name
n
process fn :: FilePath
fn (DoProofSearch updatefile :: Bool
updatefile rec :: Bool
rec l :: Int
l n :: Name
n hints :: [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 fn :: FilePath
fn (Spec t :: PTerm
t)
                    = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 [] {- (idris_statics ist) -} 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 fn :: FilePath
fn (RmProof n' :: 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
            Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn "No proof to remove"
            Just _  -> 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
$ "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 n :: 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, 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 fn' :: FilePath
fn' (AddProof prf :: 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
/= ' ') 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
<.> "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
$ "Neither \""FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
fn''FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++"\" nor \""FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
fnExtFilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++"\" exist"
       let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "~"
       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 -- make a backup in case something goes wrong!
       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
                Nothing -> case [(Name, (Bool, [FilePath]))]
proofs of
                             [] -> FilePath -> Idris Name
forall a. FilePath -> Idris a
ifail "No proof to add"
                             ((x :: Name
x, _) : _) -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
                Just nm :: 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
            Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn "No proof to add"
            Just (mode :: Bool
mode, prf :: [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
$ "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 fn :: FilePath
fn (ShowProof n' :: 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
            Nothing -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "No proof to show"
            Just (m :: Bool
m, p :: [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 fn :: FilePath
fn (Prove mode :: Bool
mode n' :: 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 (\n :: 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
$ "Cannot find metavariable " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n')
              [(n :: Name
n, (_,_,_,False,_))] -> Name -> Idris Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
              [(_, (_,_,_,_,False))] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg "Can't prove this hole as it depends on other holes")
              [(_, (_,_,_,True,_))]  -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg "Declarations not solvable using prover")
              ns :: [(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
          -- recheck totality
          IState
i <- StateT IState (ExceptT Err IO) IState
getIState
          (FC, Name) -> StateT IState (ExceptT Err IO) ()
totcheck (FilePath -> FC
fileFC "(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_ (\ (f :: FC
f,n :: 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 fn :: FilePath
fn (WHNF t :: PTerm
t)
                    = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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
$ "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
$ "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 fn :: FilePath
fn (TestInline t :: PTerm
t)
                           = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 fn :: FilePath
fn (Execute tm :: 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
                           (m_in :: Type
m_in, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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
                           (tmpn :: FilePath
tmpn, tmph :: 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 ""
                           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
                           -- gcc adds .exe when it builds windows programs
                           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]
++ ".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 h :: 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
                                    ExitSuccess -> () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                    ExitFailure err :: 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
$ "Compiled program " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                              if Int
err Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0
                                              then "was killed by signal " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                                   Int -> FilePath
forall a. Show a => a -> FilePath
show (0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
err)
                                              else "terminated with exit code " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                                   Int -> FilePath
forall a. Show a => a -> FilePath
show Int
err
                             IdeMode n :: Integer
n h :: 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 "run-program" FilePath
tmpn Integer
n)
                       (\e :: 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 "main"
process fn :: FilePath
fn (Compile codegen :: Codegen
codegen f :: 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` [".idr", ".lidr", ".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
$ "Invalid filename for compiler output \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++"\""
      | 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 "main") ["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 (m' :: Type
m', _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "compiler")) ElabMode
ERHS
                                            (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (FilePath -> Name
sUN "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 "main"
process fn :: FilePath
fn (LogLvl i :: Int
i) = Int -> StateT IState (ExceptT Err IO) ()
setLogLevel Int
i
process fn :: FilePath
fn (LogCategory cs :: [LogCat]
cs) = [LogCat] -> StateT IState (ExceptT Err IO) ()
setLogCats [LogCat]
cs
-- Elaborate as if LHS of a pattern (debug command)
process fn :: FilePath
fn (Pattelab t :: PTerm
t)
     = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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]
++ "\n\n : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Type -> FilePath
forall a. Show a => a -> FilePath
show Type
ty

process fn :: FilePath
fn (Missing n :: 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
$ "Unknown name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
           [(_, tms :: [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))
           _ -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Ambiguous name"
process fn :: FilePath
fn (DynamicLink l :: 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
                                  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
$ "Could not load dynamic lib \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\""
                                  Just x :: 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 1 ("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 fn :: FilePath
fn ListDynamic
                       = do IState
i <- StateT IState (ExceptT Err IO) IState
getIState
                            FilePath -> StateT IState (ExceptT Err IO) ()
iputStrLn "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 name :: FilePath
name _):ls :: [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
$ "\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name; [DynamicLib] -> StateT IState (ExceptT Err IO) ()
showLibs [DynamicLib]
ls
process fn :: FilePath
fn 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 "No global holes to solve"
                        _ -> 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
$ "Global holes:\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
mvs
process fn :: FilePath
fn NOP      = () -> StateT IState (ExceptT Err IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

process fn :: FilePath
fn (SetOpt   ErrContext)  = Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
True
process fn :: FilePath
fn (UnsetOpt ErrContext)  = Bool -> StateT IState (ExceptT Err IO) ()
setErrContext Bool
False
process fn :: FilePath
fn (SetOpt ShowImpl)      = Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
True
process fn :: FilePath
fn (UnsetOpt ShowImpl)    = Bool -> StateT IState (ExceptT Err IO) ()
setImpShow Bool
False
process fn :: FilePath
fn (SetOpt ShowOrigErr)   = Bool -> StateT IState (ExceptT Err IO) ()
setShowOrigErr Bool
True
process fn :: FilePath
fn (UnsetOpt ShowOrigErr) = Bool -> StateT IState (ExceptT Err IO) ()
setShowOrigErr Bool
False
process fn :: FilePath
fn (SetOpt AutoSolve)     = Bool -> StateT IState (ExceptT Err IO) ()
setAutoSolve Bool
True
process fn :: FilePath
fn (UnsetOpt AutoSolve)   = Bool -> StateT IState (ExceptT Err IO) ()
setAutoSolve Bool
False
process fn :: FilePath
fn (SetOpt NoBanner)      = Bool -> StateT IState (ExceptT Err IO) ()
setNoBanner Bool
True
process fn :: FilePath
fn (UnsetOpt NoBanner)    = Bool -> StateT IState (ExceptT Err IO) ()
setNoBanner Bool
False
process fn :: FilePath
fn (SetOpt 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 fn :: FilePath
fn (UnsetOpt 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 fn :: FilePath
fn (SetOpt EvalTypes)     = Bool -> StateT IState (ExceptT Err IO) ()
setEvalTypes Bool
True
process fn :: FilePath
fn (UnsetOpt EvalTypes)   = Bool -> StateT IState (ExceptT Err IO) ()
setEvalTypes Bool
False

process fn :: FilePath
fn (SetOpt DesugarNats)   = Bool -> StateT IState (ExceptT Err IO) ()
setDesugarNats Bool
True
process fn :: FilePath
fn (UnsetOpt DesugarNats) = Bool -> StateT IState (ExceptT Err IO) ()
setDesugarNats Bool
False

process fn :: FilePath
fn (SetOpt _) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Not a valid option"
process fn :: FilePath
fn (UnsetOpt _) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Not a valid option"
process fn :: FilePath
fn (SetColour ty :: ColourType
ty c :: IdrisColour
c) = ColourType -> IdrisColour -> StateT IState (ExceptT Err IO) ()
setColour ColourType
ty IdrisColour
c
process fn :: FilePath
fn 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 fn :: FilePath
fn 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 fn :: FilePath
fn 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
       []       -> "No registered error handlers"
       handlers :: [Name]
handlers -> "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])
-> ([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 fn :: FilePath
fn (SetConsoleWidth w :: ConsoleWidth
w) = ConsoleWidth -> StateT IState (ExceptT Err IO) ()
setWidth ConsoleWidth
w
process fn :: FilePath
fn (SetPrinterDepth d :: Maybe Int
d) = Maybe Int -> StateT IState (ExceptT Err IO) ()
setDepth Maybe Int
d
process fn :: FilePath
fn (Apropos pkgs :: [PkgName]
pkgs a :: 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
$ "Searching packages: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep ", " ((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 (\(m :: FilePath
m, d :: Docstring DocTerm
d) -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "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 "No results found"
  where isUN :: Name -> Bool
isUN (UN _) = Bool
True
        isUN (NS n :: Name
n _) = Name -> Bool
isUN Name
n
        isUN _ = Bool
False
        ppD :: IState -> Docstring DocTerm -> Doc OutputAnnotation
ppD ist :: 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 fn :: FilePath
fn (WhoCalls n :: 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 (\(n :: Name
n, ns :: [Name]
ns) ->
             FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "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 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 "*" 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 fn :: FilePath
fn (CallsWho n :: 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 (\(n :: Name
n, ns :: [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 "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 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 "*" 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 fn :: FilePath
fn (Browse ns :: [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 "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 "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 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]]
underNSs)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
                  FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "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 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 (\n :: 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))

-- IdrisDoc
process fn :: FilePath
fn (MakeDoc s :: 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 n :: FilePath
n    | Right x :: 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 n :: FilePath
n    = FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left FilePath
n
             (bad :: [FilePath]
bad, nss :: [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
</> "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
$ "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 "IdrisDoc generated"
                        Left  err :: FilePath
err -> FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError FilePath
err
process fn :: FilePath
fn (PrintDef n :: 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 "Not found"
       outs :: [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

-- Show relevant transformation rules for the name 'n'
process fn :: FilePath
fn (TransformInfo n :: 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 i :: IState
i [] = []
          showTrans i :: IState
i ((lhs :: Type
lhs, rhs :: Type
rhs) : ts :: [(Type, Type)]
ts)
              = let ppTm :: Type -> Doc OutputAnnotation
ppTm tm :: 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 " ==> " 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 fn :: FilePath
fn (PPrint fmt :: OutputFmt
fmt width :: Int
width (PRef _ _ n :: 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 fn :: FilePath
fn (PPrint fmt :: OutputFmt
fmt width :: Int
width t :: PTerm
t)
   = do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 fn :: FilePath
fn Quit = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':quit' is currently unsupported"
process fn :: FilePath
fn Reload = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':reload' is currently unsupported"
process fn :: FilePath
fn Watch = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':watch' is currently unsupported"
process fn :: FilePath
fn (Load _ _) = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':load' is currently unsupported"
process fn :: FilePath
fn Edit = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':edit' is currently unsupported"
process fn :: FilePath
fn Proofs = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':proofs' is currently unsupported"
process fn :: FilePath
fn (Verbosity _)
   = FilePath -> StateT IState (ExceptT Err IO) ()
iPrintError "Command ':verbosity' is currently unsupported"


showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal t :: Totality
t@(Partial (Other ns :: [Name]
ns)) i :: IState
i
   = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "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 ns :: [Name]
ns)) i :: IState
i
   = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "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 (\n :: 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 t :: Totality
t i :: 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 ist :: IState
ist n :: Name
n = case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
ist) of
                        [t :: 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 ", 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
                        _ -> Doc OutputAnnotation
forall a. Doc a
empty
    where
       ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
       showN :: Name -> Doc OutputAnnotation
showN n :: 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
              "\nIdris version " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              "--------------" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Char
x -> '-') FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\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 (cmds :: [FilePath]
cmds, args :: a
args, text :: FilePath
text) = "   " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col 16 12 (FilePath -> [FilePath] -> FilePath
showSep " " [FilePath]
cmds) (a -> FilePath
forall a. Show a => a -> FilePath
show a
args) FilePath
text
        col :: Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col c1 :: Int
c1 c2 :: Int
c2 l :: FilePath
l m :: FilePath
m r :: 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 ' ') 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 ' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
r FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"

pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef asCore :: Bool
asCore n :: 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
> 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 ist :: IState
ist (n :: Name
n, (clauses :: [([(Name, Type)], Type, Type)]
clauses, missing :: [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 "Attempted pprintDef of TT of thing that doesn't exist"
            (ty :: Type
ty:_) -> 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 (\(vars :: [(Name, Type)]
vars, lhs :: Type
lhs, rhs :: 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 amb :: Bool
amb ist :: IState
ist (n :: Name
n, (clauses :: [([(Name, Type)], Type, Type)]
clauses, missing :: [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 ist :: IState
ist [] = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text "No clauses."
        ppClauses ist :: IState
ist cs :: [([(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 (varTys :: [(Name, Type)]
varTys, lhs :: Type
lhs, rhs :: 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 t :: 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 "=" 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 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 _ = Doc a
forall a. Doc a
empty

        ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
        ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
ppTy amb :: Bool
amb ist :: IState
ist (n :: Name
n, TI constructors :: [Name]
constructors isCodata :: Bool
isCodata _ _ _ _)
          = 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 "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 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 = "codata"
                | Bool
otherwise = "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 amb :: Bool
amb ist :: IState
ist n :: 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 =
  [ (["Command"], CmdArg
SpecialHeaderArg, "Purpose"),
    ([""], CmdArg
NoArg, "")
  ]


replSettings :: Maybe FilePath -> Settings Idris
replSettings :: Maybe FilePath -> Settings Idris
replSettings hFile :: 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
                     }