{-|
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 IState
orig [FilePath]
mods FilePath
efile
   = -- H.catch
     do let quiet :: Bool
quiet = IOption -> Bool
opt_quiet (IState -> IOption
idris_options IState
orig)
        i <- Idris IState -> InputT Idris IState
forall (m :: * -> *) a. Monad m => m a -> InputT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris IState
getIState
        let colour = IState -> Bool
idris_colourRepl IState
i
        let theme = IState -> ColourTheme
idris_colourTheme IState
i
        let mvs = IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i
        let prompt = if Bool
quiet
                        then FilePath
""
                        else Bool
-> ColourTheme
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> FilePath
forall {a} {b}.
Show a =>
Bool -> ColourTheme -> [(a, b)] -> FilePath
showMVs Bool
colour ColourTheme
theme [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
mvs FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                             let str :: FilePath
str = [FilePath] -> FilePath
mkPrompt [FilePath]
mods FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
">" in
                             (if Bool
colour Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isWindows
                                then ColourTheme -> FilePath -> FilePath
colourisePrompt ColourTheme
theme FilePath
str
                                else FilePath
str) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" "
        x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt)
        case x of
            Maybe FilePath
Nothing -> do Idris () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => m a -> InputT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris () -> InputT Idris ()) -> Idris () -> InputT Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
quiet) (FilePath -> Idris ()
iputStrLn FilePath
"Bye bye")
                          () -> InputT Idris ()
forall a. a -> InputT Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just FilePath
input -> -- H.catch
                do ms <- InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
H.handleInterrupt (InputT Idris (Maybe [FilePath]) -> InputT Idris (Maybe [FilePath])
forall a. InputT Idris a -> InputT Idris a
ctrlC (Maybe [FilePath] -> InputT Idris (Maybe [FilePath])
forall a. a -> InputT Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
mods))) (InputT Idris (Maybe [FilePath]) -> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
H.withInterrupt (InputT Idris (Maybe [FilePath])
 -> InputT Idris (Maybe [FilePath]))
-> InputT Idris (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall (m :: * -> *) a. Monad m => m a -> InputT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT IState (ExceptT Err IO) (Maybe [FilePath])
 -> InputT Idris (Maybe [FilePath]))
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> InputT Idris (Maybe [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath
-> IState
-> [FilePath]
-> FilePath
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
processInput FilePath
input IState
orig [FilePath]
mods FilePath
efile)
                   case ms of
                        Just [FilePath]
mods -> let efile' :: FilePath
efile' = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
efile ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
mods)
                                     in IState -> [FilePath] -> FilePath -> InputT Idris ()
repl IState
orig [FilePath]
mods FilePath
efile'
                        Maybe [FilePath]
Nothing -> () -> InputT Idris ()
forall a. a -> InputT Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--                             ctrlC)
--       ctrlC
   where ctrlC :: InputT Idris a -> InputT Idris a
         ctrlC :: forall a. InputT Idris a -> InputT Idris a
ctrlC InputT Idris a
act = do Idris () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => m a -> InputT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Idris () -> InputT Idris ()) -> Idris () -> InputT Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Idris ()
iputStrLn FilePath
"Interrupted"
                        InputT Idris a
act -- repl orig mods

         showMVs :: Bool -> ColourTheme -> [(a, b)] -> FilePath
showMVs Bool
c ColourTheme
thm [] = FilePath
""
         showMVs Bool
c ColourTheme
thm [(a, b)]
ms = FilePath
"Holes: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                 Integer -> Bool -> ColourTheme -> [a] -> FilePath
forall {t} {a}.
(Eq t, Num t, Show a) =>
t -> Bool -> ColourTheme -> [a] -> FilePath
show' Integer
4 Bool
c ColourTheme
thm (((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
ms) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n"

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

         showM :: Bool -> ColourTheme -> a -> FilePath
showM Bool
c ColourTheme
thm a
n = if Bool
c then ColourTheme -> FilePath -> FilePath
colouriseFun ColourTheme
thm (a -> FilePath
forall a. Show a => a -> FilePath
show a
n)
                              else a -> FilePath
forall a. Show a => a -> FilePath
show a
n

-- | Run the REPL server
startServer :: PortNumber -> IState -> [FilePath] -> Idris ()
startServer :: PortNumber -> IState -> [FilePath] -> Idris ()
startServer PortNumber
port IState
orig [FilePath]
fn_in = do 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)
                                 return ()
  where serverLoop :: PortNumber -> IO a
serverLoop PortNumber
port = IO a -> IO a
forall a. IO a -> IO a
withSocketsDo (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$
                              do sock <- PortNumber -> IO Socket
listenOnLocalhost PortNumber
port
                                 loop fn orig { idris_colourRepl = False } sock

        fn :: FilePath
fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
fn_in)

        loop :: FilePath -> IState -> Socket -> IO b
loop FilePath
fn IState
ist Socket
sock
            = do (s, _) <- Socket -> IO (Socket, SockAddr)
accept Socket
sock
                 h <- socketToHandle s ReadWriteMode
                 hSetEncoding h utf8
                 cmd <- hGetLine h
                 let isth = case IState -> OutputMode
idris_outputmode IState
ist of
                              RawOutput Handle
_ -> IState
ist {idris_outputmode = RawOutput h}
                              IdeMode Integer
n Handle
_ -> IState
ist {idris_outputmode = IdeMode n h}
                 (ist', fn) <- processNetCmd orig isth h fn cmd
                 hClose h
                 loop fn ist' sock

processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
                 IO (IState, FilePath)
processNetCmd :: IState
-> IState
-> Handle
-> FilePath
-> FilePath
-> IO (IState, FilePath)
processNetCmd IState
orig IState
i Handle
h FilePath
fn FilePath
cmd
    = do res <- case IState
-> FilePath
-> FilePath
-> Either ParseError (Either FilePath Command)
parseCmd IState
i FilePath
"(net)" FilePath
cmd of
                  Left ParseError
err -> Either Err (IState, FilePath) -> IO (Either Err (IState, FilePath))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err -> Either Err (IState, FilePath)
forall a b. a -> Either a b
Left (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
" invalid command"))
                  Right (Right Command
c) -> ExceptT Err IO (IState, FilePath)
-> IO (Either Err (IState, FilePath))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Err IO (IState, FilePath)
 -> IO (Either Err (IState, FilePath)))
-> ExceptT Err IO (IState, FilePath)
-> IO (Either Err (IState, FilePath))
forall a b. (a -> b) -> a -> b
$ StateT IState (ExceptT Err IO) (IState, FilePath)
-> IState -> ExceptT Err IO (IState, FilePath)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn Command
c) IState
i
                  Right (Left FilePath
err) -> Either Err (IState, FilePath) -> IO (Either Err (IState, FilePath))
forall a. a -> IO a
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 res of
              Right (IState, FilePath)
x -> (IState, FilePath) -> IO (IState, FilePath)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IState, FilePath)
x
              Left Err
err -> do Handle -> FilePath -> IO ()
hPutStrLn Handle
h (Err -> FilePath
forall a. Show a => a -> FilePath
show Err
err)
                             (IState, FilePath) -> IO (IState, FilePath)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IState
i, FilePath
fn)
  where
    processNet :: FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn Command
Reload = FilePath
-> Command -> StateT IState (ExceptT Err IO) (IState, FilePath)
processNet FilePath
fn (FilePath -> Maybe Int -> Command
Load FilePath
fn Maybe Int
forall a. Maybe a
Nothing)
    processNet FilePath
fn (Load FilePath
f Maybe Int
toline) =
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
        do IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options = idris_options i
                              , idris_colourTheme = idris_colourTheme i
                              , idris_colourRepl = False
                              }
           Bool -> Idris ()
setErrContext Bool
True
           Handle -> Idris ()
setOutH Handle
h
           Bool -> Idris ()
setQuiet Bool
True
           Int -> Idris ()
setVerbose Int
0
           mods <- [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
f] Maybe Int
toline
           ist <- getIState
           return (ist, f)
    processNet FilePath
fn Command
c = do FilePath -> Command -> Idris ()
process FilePath
fn Command
c
                         ist <- Idris IState
getIState
                         return (ist, fn)
    setOutH :: Handle -> Idris ()
    setOutH :: Handle -> Idris ()
setOutH Handle
h =
      do ist <- Idris IState
getIState
         putIState $ case idris_outputmode ist of
           RawOutput Handle
_ -> IState
ist {idris_outputmode = RawOutput h}
           IdeMode Integer
n Handle
_ -> IState
ist {idris_outputmode = IdeMode n h}

-- | Run a command on the server on localhost
runClient :: Maybe PortNumber -> String -> IO ()
runClient :: Maybe PortNumber -> FilePath -> IO ()
runClient Maybe PortNumber
port FilePath
str = IO () -> IO ()
forall a. IO a -> IO a
withSocketsDo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
              let port' :: PortNumber
port' = PortNumber -> Maybe PortNumber -> PortNumber
forall a. a -> Maybe a -> a
fromMaybe PortNumber
defaultPort Maybe PortNumber
port
              s <- Family -> SocketType -> ProtocolNumber -> IO Socket
socket Family
AF_INET SocketType
Stream ProtocolNumber
defaultProtocol
              res <- X.try (connect s (SockAddrInet port' $ tupleToHostAddress (127,0,0,1)))
              case res of
                Right () -> do
                  h <- Socket -> IOMode -> IO Handle
socketToHandle Socket
s IOMode
ReadWriteMode
                  hSetEncoding h utf8
                  hPutStrLn h str
                  resp <- hGetResp "" h
                  putStr resp
                  hClose h

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

    where hGetResp :: FilePath -> Handle -> IO FilePath
hGetResp FilePath
acc Handle
h = do eof <- Handle -> IO Bool
hIsEOF Handle
h
                              if eof then return acc
                                     else do l <- hGetLine h
                                             hGetResp (acc ++ l ++ "\n") h

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


initIdemodeSocket :: IO Handle
initIdemodeSocket :: IO Handle
initIdemodeSocket = do
  (sock, port) <- IO (Socket, PortNumber)
listenOnLocalhostAnyPort
  putStrLn $ show port
  (s, _) <- accept sock
  h <- socketToHandle s ReadWriteMode
  hSetEncoding h utf8
  return h

-- | Run the IdeMode
idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()
idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()
idemodeStart Bool
s IState
orig [FilePath]
mods
  = do 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Handle
stdout
       setIdeMode True h
       runIO $ hSetNewlineMode h (NewlineMode { inputNL = CRLF, outputNL = LF })
       i <- getIState
       case idris_outputmode i of
         IdeMode Integer
n Handle
h ->
           do IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Int -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"protocol-version" Int
IdeMode.ideModeEpoch Integer
n
              case [FilePath]
mods of
                FilePath
a:[FilePath]
_ -> Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> Idris ()
runIdeModeCommand Handle
h Integer
n IState
i FilePath
"" [] (FilePath -> Maybe Int -> IdeModeCommand
IdeMode.LoadFile FilePath
a Maybe Int
forall a. Maybe a
Nothing)
                [FilePath]
_   -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       idemode h orig mods

idemode :: Handle -> IState -> [FilePath] -> Idris ()
idemode :: Handle -> IState -> [FilePath] -> Idris ()
idemode Handle
h IState
orig [FilePath]
mods
  = do Idris () -> (Err -> Idris ()) -> Idris ()
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
             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
             len <- case len' of
               Left Err
err -> Err -> StateT IState (ExceptT Err IO) Int
forall a. Err -> Idris a
ierror Err
err
               Right Int
n  -> Int -> StateT IState (ExceptT Err IO) Int
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
             l <- runIO $ IdeMode.getNChar inh len ""
             (sexp, id) <- case IdeMode.parseMessage l of
                             Left Err
err -> Err -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall a. Err -> Idris a
ierror Err
err
                             Right (SExp
sexp, Integer
id) -> (SExp, Integer) -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SExp
sexp, Integer
id)
             i <- getIState
             putIState $ i { idris_outputmode = (IdeMode id h) }
             idrisCatch -- to report correct id back!
               (do let fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
mods)
                   case IdeMode.sexpToCommand sexp of
                     Just IdeModeCommand
cmd -> Handle
-> Integer
-> IState
-> FilePath
-> [FilePath]
-> IdeModeCommand
-> Idris ()
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods IdeModeCommand
cmd
                     Maybe IdeModeCommand
Nothing  -> FilePath -> Idris ()
iPrintError FilePath
"did not understand" )
               (\Err
e -> do FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e))
         (\Err
e -> do FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e)
       Handle -> IState -> [FilePath] -> Idris ()
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
-> Idris ()
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Interpret FilePath
cmd) =
  do c <- Idris Bool
colourise
     i <- getIState
     case parseCmd i "(input)" cmd of
       Left ParseError
err -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ())
-> (ParseError -> FilePath) -> ParseError -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (ParseError -> Doc) -> ParseError -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Doc -> Doc
fixColour Bool
False (Doc -> Doc) -> (ParseError -> Doc) -> ParseError -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ParseError -> Doc
parseErrorDoc (ParseError -> Idris ()) -> ParseError -> Idris ()
forall a b. (a -> b) -> a -> b
$ ParseError
err
       Right (Right (Prove Bool
mode Name
n')) ->
         Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
           (do FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Name -> Command
Prove Bool
mode Name
n')
               FilePath -> Idris ()
isetPrompt ([FilePath] -> FilePath
mkPrompt [FilePath]
mods)
               case IState -> OutputMode
idris_outputmode IState
i of
                 IdeMode Integer
n Handle
h -> -- signal completion of proof to ide
                   IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$
                     FilePath -> (SExp, FilePath) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return"
                       (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath
"")
                       Integer
n
                 OutputMode
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           (\Err
e -> do ist <- Idris IState
getIState
                     isetPrompt (mkPrompt mods)
                     case idris_outputmode i of
                       IdeMode Integer
n Handle
h ->
                         IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$
                           FilePath -> FilePath -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"abandon-proof" FilePath
"Abandoned" Integer
n
                       OutputMode
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                     iRenderError $ pprintErr ist e)
       Right (Right Command
cmd) -> Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
                        (FilePath -> Command -> Idris ()
idemodeProcess FilePath
fn Command
cmd)
                        (\Err
e -> Idris IState
getIState Idris IState -> (IState -> Idris ()) -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> Idris ()
iRenderError (Doc OutputAnnotation -> Idris ())
-> (IState -> Doc OutputAnnotation) -> IState -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Err -> Doc OutputAnnotation)
-> Err -> IState -> Doc OutputAnnotation
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> Err -> Doc OutputAnnotation
pprintErr Err
e)
       Right (Left FilePath
err) -> FilePath -> Idris ()
iPrintError FilePath
err
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.REPLCompletions FilePath
str) =
  do (unused, compls) <- CompletionFunc Idris
replCompletion (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
str, FilePath
"")
     let good = [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                                   ([FilePath], FilePath) -> SExp
forall a. SExpable a => a -> SExp
IdeMode.toSExp ((Completion -> FilePath) -> [Completion] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Completion -> FilePath
replacement [Completion]
compls,
                                   FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
unused)]
     runIO . hPutStrLn h $ IdeMode.convSExp "return" good id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.LoadFile FilePath
filename 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 i <- Idris IState
getIState
     clearErr
     putIState $!! orig { idris_options = idris_options i,
                          idris_outputmode = (IdeMode id h) }
     mods <- loadInputs [filename] toline
     isetPrompt (mkPrompt mods)
     -- Report either success or failure
     i <- getIState
     case (errSpan i) of
       Maybe FC
Nothing -> let msg :: SExp
msg = SExp -> (FC -> SExp) -> Maybe FC -> SExp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                                                      [SExp] -> SExp
IdeMode.SexpList []])
                                  (\FC
fc -> [SExp] -> SExp
IdeMode.SexpList [FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                                                             FC -> SExp
forall a. SExpable a => a -> SExp
IdeMode.toSExp FC
fc])
                                  (IState -> Maybe FC
idris_parsedSpan IState
i)
                  in IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> SExp -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" SExp
msg Integer
id
       Just FC
x -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"didn't load " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
filename
     idemode h orig mods
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.TypeOf FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
    Right Name
n -> FilePath -> Command -> Idris ()
process FilePath
"(idemode)"
                 (PTerm -> Command
Check (FC -> [FC] -> Name -> PTerm
PRef (FilePath -> (Int, Int) -> (Int, Int) -> FC
FC FilePath
"(idemode)" (Int
0,Int
0) (Int
0,Int
0)) [] Name
n))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.DocsFor FilePath
name WhatDocs
w) =
  case IState -> FilePath -> Either ParseError Const
parseConst IState
orig FilePath
name of
    Right Const
c -> FilePath -> Command -> Idris ()
process FilePath
"(idemode)" (Either Name Const -> HowMuchDocs -> Command
DocStr (Const -> Either Name Const
forall a b. b -> Either a b
Right Const
c) (WhatDocs -> HowMuchDocs
howMuch WhatDocs
w))
    Left ParseError
_ ->
     case FilePath -> Either FilePath Name
splitName FilePath
name of
       Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
       Right Name
n -> FilePath -> Command -> Idris ()
process FilePath
"(idemode)" (Either Name Const -> HowMuchDocs -> Command
DocStr (Name -> Either Name Const
forall a b. a -> Either a b
Left Name
n) (WhatDocs -> HowMuchDocs
howMuch WhatDocs
w))
  where howMuch :: WhatDocs -> HowMuchDocs
howMuch WhatDocs
IdeMode.Overview = HowMuchDocs
OverviewDocs
        howMuch WhatDocs
IdeMode.Full     = HowMuchDocs
FullDocs
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.CaseSplit Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
CaseSplitAt Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddClause Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddClauseFrom Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddProofClause Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddProofClauseFrom Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.AddMissing Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
AddMissing Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeWithBlock Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeWith Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeCaseBlock Int
line FilePath
name) =
  FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeCase Bool
False Int
line (FilePath -> Name
sUN FilePath
name))
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.ProofSearch Bool
r Int
line FilePath
name [FilePath]
hints Maybe Int
depth) =
  FilePath
-> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris ()
doProofSearch FilePath
fn Bool
False Bool
r Int
line (FilePath -> Name
sUN FilePath
name) ((FilePath -> Name) -> [FilePath] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Name
sUN [FilePath]
hints) Maybe Int
depth
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.MakeLemma Int
line FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
    Right Name
n -> FilePath -> Command -> Idris ()
process FilePath
fn (Bool -> Int -> Name -> Command
MakeLemma Bool
False Int
line Name
n)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Apropos FilePath
a) =
  FilePath -> Command -> Idris ()
process FilePath
fn ([PkgName] -> FilePath -> Command
Apropos [] FilePath
a)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeModeCommand
IdeMode.GetOpts) =
  do ist <- Idris IState
getIState
     let opts = IState -> IOption
idris_options IState
ist
     let impshow = IOption -> Bool
opt_showimp IOption
opts
     let errCtxt = IOption -> Bool
opt_errContext IOption
opts
     let options = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                    [(FilePath -> SExp
IdeMode.SymbolAtom FilePath
"show-implicits", Bool
impshow),
                     (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"error-context", Bool
errCtxt)])
     runIO . hPutStrLn h $ IdeMode.convSExp "return" options id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.SetOpt Opt
IdeMode.ShowImpl Bool
b) =
  do Bool -> Idris ()
setImpShow Bool
b
     let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", Bool
b)
     IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, Bool) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, Bool)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.SetOpt Opt
IdeMode.ErrContext Bool
b) =
  do Bool -> Idris ()
setErrContext Bool
b
     let msg :: (SExp, Bool)
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", Bool
b)
     IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, Bool) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, Bool)
msg Integer
id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.Metavariables Int
cols) =
  do ist <- Idris IState
getIState
     let mvs = [(Name, Int)] -> [(Name, Int)]
forall a. [a] -> [a]
reverse ([(Name, Int)] -> [(Name, Int)]) -> [(Name, Int)] -> [(Name, Int)]
forall a b. (a -> b) -> a -> b
$ [ (Name
n, Int
i)
                         | (Name
n, (Maybe Name
_, Int
i, [Name]
_, Bool
_, Bool
_)) <- IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist
                         , Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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
n, ([(Name, Term, PTerm)]
premises, Term
concl, PTerm
tm))
                    | (Name
n, Int
i, Term
ty) <- IState -> [(Name, Int)] -> [(Name, Int, Term)]
mvTys IState
ist [(Name, Int)]
mvs
                    , let ([(Name, Term, PTerm)]
premises, Term
concl, PTerm
tm) = IState -> Int -> Term -> ([(Name, Term, PTerm)], Term, PTerm)
splitPi IState
ist Int
i Term
ty]
     -- mvOutput is the pretty-printed version ready for conversion to SExpr
     let mvOutput = ((FilePath,
  ([(FilePath, FilePath, SpanList OutputAnnotation)],
   (FilePath, SpanList OutputAnnotation)))
 -> (FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
     (FilePath, SpanList OutputAnnotation)))
-> [(FilePath,
     ([(FilePath, FilePath, SpanList OutputAnnotation)],
      (FilePath, SpanList OutputAnnotation)))]
-> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
     (FilePath, SpanList OutputAnnotation))]
forall a b. (a -> b) -> [a] -> [b]
map (\(FilePath
n, ([(FilePath, FilePath, SpanList OutputAnnotation)]
hs, (FilePath, SpanList OutputAnnotation)
c)) -> (FilePath
n, [(FilePath, FilePath, SpanList OutputAnnotation)]
hs, (FilePath, SpanList OutputAnnotation)
c)) ([(FilePath,
   ([(FilePath, FilePath, SpanList OutputAnnotation)],
    (FilePath, SpanList OutputAnnotation)))]
 -> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
      (FilePath, SpanList OutputAnnotation))])
-> [(FilePath,
     ([(FilePath, FilePath, SpanList OutputAnnotation)],
      (FilePath, SpanList OutputAnnotation)))]
-> [(FilePath, [(FilePath, FilePath, SpanList OutputAnnotation)],
     (FilePath, SpanList OutputAnnotation))]
forall a b. (a -> b) -> a -> b
$
                    (Name -> FilePath)
-> (([(Name, Term, PTerm)], Term, PTerm)
    -> ([(FilePath, FilePath, SpanList OutputAnnotation)],
        (FilePath, SpanList OutputAnnotation)))
-> [(Name, ([(Name, Term, PTerm)], Term, PTerm))]
-> [(FilePath,
     ([(FilePath, FilePath, SpanList OutputAnnotation)],
      (FilePath, SpanList OutputAnnotation)))]
forall {b} {a} {b} {b}.
(b -> a) -> (b -> b) -> [(b, b)] -> [(a, b)]
mapPair Name -> FilePath
forall a. Show a => a -> FilePath
show
                            (\([(Name, Term, PTerm)]
hs, Term
c, PTerm
pc) ->
                             let bnd :: [Name]
bnd = [ Name
n | (Name
n,Term
_,PTerm
_) <- [(Name, Term, PTerm)]
hs ] in
                             let bnds :: [[Name]]
bnds = [Name] -> [[Name]]
forall a. [a] -> [[a]]
inits [Name]
bnd in
                             ((([Name], (Name, Term, PTerm))
 -> (FilePath, FilePath, SpanList OutputAnnotation))
-> [([Name], (Name, Term, PTerm))]
-> [(FilePath, FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\([Name]
bnd, (Name, Term, PTerm)
h) -> IState
-> [Name]
-> (Name, Term, PTerm)
-> (FilePath, FilePath, SpanList OutputAnnotation)
processPremise IState
ist [Name]
bnd (Name, Term, PTerm)
h)
                                  ([[Name]]
-> [(Name, Term, PTerm)] -> [([Name], (Name, Term, PTerm))]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Name]]
bnds [(Name, Term, PTerm)]
hs),
                              IState
-> [Name] -> Term -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Term
c PTerm
pc))
                            [(Name, ([(Name, Term, PTerm)], Term, PTerm))]
splitMvs
     runIO . hPutStrLn h $
       IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
  where mapPair :: (b -> a) -> (b -> b) -> [(b, b)] -> [(a, b)]
mapPair b -> a
f b -> b
g [(b, b)]
xs = [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((b, b) -> a) -> [(b, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (b -> a
f (b -> a) -> ((b, b) -> b) -> (b, b) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (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 -> Term -> ([(Name, Term, PTerm)], Term, PTerm)
splitPi IState
ist Int
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
t Term
_) Term
rest) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
          let ([(Name, Term, PTerm)]
hs, Term
c, PTerm
_) = IState -> Int -> Term -> ([(Name, Term, PTerm)], Term, PTerm)
splitPi IState
ist (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
rest in
            ((Name
n, Term
t, IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Term
t Bool
False Bool
False Bool
True)(Name, Term, PTerm)
-> [(Name, Term, PTerm)] -> [(Name, Term, PTerm)]
forall a. a -> [a] -> [a]
:[(Name, Term, PTerm)]
hs,
             Term
c, IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Term
c Bool
False Bool
False Bool
True)
        splitPi IState
ist Int
i Term
tm = ([], Term
tm, IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [] [] Term
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, Term)]
mvTys IState
ist [(Name, Int)]
mvs = [ (Name
n, Int
i, Term
ty)
                        | (Name
n, Int
i) <- [(Name, Int)]
mvs
                        , Term
ty <- Maybe Term -> [Term]
forall a. Maybe a -> [a]
maybeToList (((Name, Term) -> Term) -> Maybe (Name, Term) -> Maybe Term
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> Term
forall n. TT n -> TT n
vToP (Term -> Term) -> ((Name, Term) -> Term) -> (Name, Term) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, Term) -> Term
forall a b. (a, b) -> b
snd) (Name -> Context -> Maybe (Name, Term)
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] -> Term -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Term
t PTerm
pt =
          let prettyT :: Doc OutputAnnotation
prettyT = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist)
                                    ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
bnd (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False))
                                    []
                                    (IState -> [FixDecl]
idris_infixes IState
ist)
                                    PTerm
pt
          in
            SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
            Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
cols (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
            (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
            OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
bnd) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False))) Term
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, Term, PTerm)
-> (FilePath, FilePath, SpanList OutputAnnotation)
processPremise IState
ist [Name]
bnd (Name
n, Term
t, PTerm
pt) =
          let (FilePath
out, SpanList OutputAnnotation
spans) = IState
-> [Name] -> Term -> PTerm -> (FilePath, SpanList OutputAnnotation)
render IState
ist [Name]
bnd Term
t PTerm
pt in
          (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n , FilePath
out, SpanList OutputAnnotation
spans)

runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.WhoCalls FilePath
n) =
  case FilePath -> Either FilePath Name
splitName FilePath
n of
       Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
       Right Name
n -> do calls <- Name -> Idris [(Name, [Name])]
whoCalls Name
n
                     ist <- getIState
                     let msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                                ((Name, [Name])
 -> ((FilePath, SpanList OutputAnnotation),
     [(FilePath, SpanList OutputAnnotation)]))
-> [(Name, [Name])]
-> [((FilePath, SpanList OutputAnnotation),
     [(FilePath, SpanList OutputAnnotation)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n,[Name]
ns) -> (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist Name
n, (Name -> (FilePath, SpanList OutputAnnotation))
-> [Name] -> [(FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist) [Name]
ns)) [(Name, [Name])]
calls)
                     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
  where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist = SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Name -> SimpleDoc OutputAnnotation)
-> Name
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
1000 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Name -> Doc OutputAnnotation)
-> Name
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []

runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.CallsWho FilePath
n) =
  case FilePath -> Either FilePath Name
splitName FilePath
n of
       Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
       Right Name
n -> do calls <- Name -> Idris [(Name, [Name])]
callsWho Name
n
                     ist <- getIState
                     let msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                                ((Name, [Name])
 -> ((FilePath, SpanList OutputAnnotation),
     [(FilePath, SpanList OutputAnnotation)]))
-> [(Name, [Name])]
-> [((FilePath, SpanList OutputAnnotation),
     [(FilePath, SpanList OutputAnnotation)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n,[Name]
ns) -> (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist Name
n, (Name -> (FilePath, SpanList OutputAnnotation))
-> [Name] -> [(FilePath, SpanList OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist) [Name]
ns)) [(Name, [Name])]
calls)
                     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
  where pn :: IState -> Name -> (FilePath, SpanList OutputAnnotation)
pn IState
ist = SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Name -> SimpleDoc OutputAnnotation)
-> Name
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
1000 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Name -> Doc OutputAnnotation)
-> Name
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                 Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []

runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.BrowseNS FilePath
ns) =
  case FilePath -> FilePath -> [FilePath]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn FilePath
"." FilePath
ns of
    [] -> FilePath -> Idris ()
iPrintError FilePath
"No namespace provided"
    [FilePath]
ns -> do underNSs <- ([[FilePath]] -> [FilePath])
-> StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath]
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse FilePath
".") (StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath])
-> StateT IState (ExceptT Err IO) [[FilePath]] -> Idris [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> StateT IState (ExceptT Err IO) [[FilePath]]
namespacesInNS [FilePath]
ns
             names <- namesInNS ns
             if null underNSs && null names
                then iPrintError "Invalid or empty namespace"
                else do ist <- getIState
                        underNs <- mapM pn names
                        let msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", ([FilePath]
underNSs, [(FilePath, SpanList OutputAnnotation)]
underNs))
                        runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
  where pn :: Name
-> StateT
     IState (ExceptT Err IO) (FilePath, SpanList OutputAnnotation)
pn Name
n =
          do ctxt <- Idris Context
getContext
             ist <- getIState
             return $
               displaySpans .
               renderPretty 0.9 1000 .
               fmap (fancifyAnnots ist True) $
                 prettyName True False [] n <>
                 case lookupTyExact n ctxt of
                   Just Term
t ->
                     Doc OutputAnnotation
forall a. Doc a
space Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' IState
ist Name
n Term
t))
                   Maybe Term
Nothing ->
                     Doc OutputAnnotation
forall a. Doc a
empty

runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermNormalise [(Name, Bool)]
bnd Term
tm) =
  do ctxt <- Idris Context
getContext
     ist <- getIState
     let tm' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
tm
         ptm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Term
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 -> Term -> PTerm
delab IState
ist Term
tm'))
         msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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)
     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermShowImplicits [(Name, Bool)]
bnd Term
tm) =
  Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
True Term
tm
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermNoImplicits [(Name, Bool)]
bnd Term
tm) =
  Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
False Term
tm
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.TermElab [(Name, Bool)]
bnd Term
tm) =
  do ist <- Idris IState
getIState
     let ptm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Term
tm)
                 ([Name] -> Term -> 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) Term
tm)
         msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
70 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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)
     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
mods (IdeMode.PrintDef FilePath
name) =
  case FilePath -> Either FilePath Name
splitName FilePath
name of
    Left FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
    Right Name
n -> FilePath -> Command -> Idris ()
process FilePath
"(idemode)" (Name -> Command
PrintDef Name
n)
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.ErrString Err
e) =
  do ist <- Idris IState
getIState
     let 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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
60 (Doc OutputAnnotation -> FilePath -> FilePath)
-> Doc OutputAnnotation -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
e
         msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath -> SExp
IdeMode.StringAtom (FilePath -> SExp) -> FilePath -> SExp
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
out FilePath
"")
     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes (IdeMode.ErrPPrint Err
e) =
  do ist <- Idris IState
getIState
     let (out, spans) =
           displaySpans .
           renderPretty 0.9 80 .
           fmap (fancifyAnnots ist True) $ pprintErr ist e
         msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", FilePath
out, SpanList OutputAnnotation
spans)
     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
runIdeModeCommand Handle
h Integer
id IState
orig FilePath
fn [FilePath]
modes IdeModeCommand
IdeMode.GetIdrisVersion =
  let idrisVersion :: ([Int], [FilePath])
idrisVersion = (Version -> [Int]
versionBranch Version
getIdrisVersionNoGit,
                      if Bool -> Bool
not (FilePath -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
gitHash)
                        then [FilePath
gitHash]
                        else [])
      msg :: (SExp, ([Int], [FilePath]))
msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok", ([Int], [FilePath])
idrisVersion)
  in IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> (SExp, ([Int], [FilePath])) -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"return" (SExp, ([Int], [FilePath]))
msg Integer
id


-- | Show a term for IDEMode with the specified implicitness
ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
ideModeForceTermImplicits Handle
h Integer
id [(Name, Bool)]
bnd Bool
impl Term
tm =
  do ist <- Idris IState
getIState
     let expl = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Term
tm)
                (PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm ((IState -> PPOption
ppOptionIst IState
ist) { ppopt_impl = impl })
                             [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist)
                             (IState -> Term -> PTerm
delab IState
ist Term
tm))
         msg = (FilePath -> SExp
IdeMode.SymbolAtom FilePath
"ok",
                SimpleDoc OutputAnnotation -> (FilePath, SpanList OutputAnnotation)
forall a. SimpleDoc a -> (FilePath, SpanList a)
displaySpans (SimpleDoc OutputAnnotation
 -> (FilePath, SpanList OutputAnnotation))
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> (FilePath, SpanList OutputAnnotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
0.9 Int
80 (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> SimpleDoc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
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)
     runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

splitName :: String -> Either String Name
splitName :: FilePath -> Either FilePath Name
splitName FilePath
s | FilePath
"{{{{{" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
s =
              FilePath -> Either FilePath Name
forall {b}. Binary b => FilePath -> Either FilePath b
decode (FilePath -> Either FilePath Name)
-> FilePath -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
drop Int
5 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
drop Int
5 (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
s
  where decode :: FilePath -> Either FilePath b
decode FilePath
x =
          case ByteString -> Either FilePath ByteString
Base64.decode (FilePath -> ByteString
UTF8.fromString FilePath
x) of
            Left FilePath
err -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left FilePath
err
            Right ByteString
ok ->
              case ByteString
-> Either
     (ByteString, ByteOffset, FilePath) (ByteString, ByteOffset, b)
forall a.
Binary a =>
ByteString
-> Either
     (ByteString, ByteOffset, FilePath) (ByteString, ByteOffset, a)
Binary.decodeOrFail (ByteString -> ByteString
Lazy.fromStrict ByteString
ok) of
                Left (ByteString, ByteOffset, FilePath)
_ -> FilePath -> Either FilePath b
forall a b. a -> Either a b
Left FilePath
"Bad binary instance for Name"
                Right (ByteString
_, ByteOffset
_, b
n) -> b -> Either FilePath b
forall a b. b -> Either a b
Right b
n

splitName FilePath
s = case [FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [FilePath]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn FilePath
"." FilePath
s of
                [] -> FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left (FilePath
"Didn't understand name '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'")
                [FilePath
n] -> Name -> Either FilePath Name
forall a b. b -> Either a b
Right (Name -> Either FilePath Name)
-> (FilePath -> Name) -> FilePath -> Either FilePath Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Name
sUN (FilePath -> Either FilePath Name)
-> FilePath -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
unparen FilePath
n
                (FilePath
n:[FilePath]
ns) -> Name -> Either FilePath Name
forall a b. b -> Either a b
Right (Name -> Either FilePath Name) -> Name -> Either FilePath Name
forall a b. (a -> b) -> a -> b
$ Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN (FilePath -> FilePath
unparen FilePath
n)) [FilePath]
ns
  where unparen :: FilePath -> FilePath
unparen FilePath
"" = FilePath
""
        unparen (Char
'(':Char
x:FilePath
xs) | FilePath -> Char
forall a. HasCallStack => [a] -> a
last FilePath
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' = FilePath -> FilePath
forall a. HasCallStack => [a] -> [a]
init (Char
xChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)
        unparen FilePath
str = FilePath
str

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

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


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

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

reload :: IState -> [FilePath] -> Idris (Maybe [FilePath])
reload :: IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs = do
  i <- Idris IState
getIState
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
  putIState $!! orig { idris_options = idris_options i
    , idris_colourTheme = idris_colourTheme i
    , imported = imported i
  }
  clearErr
  fmap Just $ loadInputs inputs Nothing

watch :: IState -> [FilePath] -> Idris (Maybe [FilePath])
watch :: IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs = do
  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
    inputSet <- ([FilePath] -> Set FilePath) -> IO [FilePath] -> IO (Set FilePath)
forall a b. (a -> b) -> IO a -> IO b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO FilePath
canonicalizePath [FilePath]
inputs
    signal <- newEmptyMVar
    withManager $ \WatchManager
mgr -> do
      [FilePath] -> (FilePath -> IO (IO ())) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [FilePath]
dirs ((FilePath -> IO (IO ())) -> IO ())
-> (FilePath -> IO (IO ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FilePath
dir ->
        WatchManager -> FilePath -> ActionPredicate -> Action -> IO (IO ())
watchDir WatchManager
mgr FilePath
dir ((FilePath -> Bool) -> ActionPredicate
allEvents ((FilePath -> Bool) -> ActionPredicate)
-> (FilePath -> Bool) -> ActionPredicate
forall a b. (a -> b) -> a -> b
$ (FilePath -> Set FilePath -> Bool)
-> Set FilePath -> FilePath -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set FilePath
inputSet) ((FilePath -> IO ()) -> Action
forall (m :: * -> *).
Monad m =>
(FilePath -> m ()) -> Event -> m ()
doAllEvents ((FilePath -> IO ()) -> Action) -> (FilePath -> IO ()) -> Action
forall a b. (a -> b) -> a -> b
$ MVar FilePath -> FilePath -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar FilePath
signal)
      IO FilePath -> IO FilePath -> IO (Either FilePath FilePath)
forall a b. IO a -> IO b -> IO (Either a b)
race IO FilePath
getLine (MVar FilePath -> IO FilePath
forall a. MVar a -> IO a
takeMVar MVar FilePath
signal)
  case resp of
    Left FilePath
_ -> Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs) -- canceled, so nop
    Right FilePath
_ -> IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs

processInput :: String ->
                IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])
processInput :: FilePath
-> IState
-> [FilePath]
-> FilePath
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
processInput FilePath
cmd IState
orig [FilePath]
inputs FilePath
efile
    = do i <- Idris IState
getIState
         let opts = IState -> IOption
idris_options IState
i
         let quiet = IOption -> Bool
opt_quiet IOption
opts
         let fn = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"" ([FilePath] -> Maybe FilePath
forall a. [a] -> Maybe a
listToMaybe [FilePath]
inputs)
         case parseCmd i "(input)" cmd of
            Left ParseError
err -> [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs Maybe [FilePath]
-> Idris () -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a b.
a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
            Right (Right Command
Reload) ->
                IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
reload IState
orig [FilePath]
inputs
            Right (Right Command
Watch) ->
                if [FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
inputs then
                  do FilePath -> Idris ()
iputStrLn FilePath
"No loaded files to watch."
                     Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
                else
                  do FilePath -> Idris ()
iputStrLn FilePath
efile
                     FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Watching for .idr changes in " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
inputs FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
", press enter to cancel."
                     IState
-> [FilePath] -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
watch IState
orig [FilePath]
inputs
            Right (Right (Load FilePath
f Maybe Int
toline)) ->
                -- The $!! here prevents a space leak on reloading.
                -- This isn't a solution - but it's a temporary stopgap.
                -- See issue #2386
                do IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. NFData a => (a -> b) -> a -> b
$!! IState
orig { idris_options = idris_options i
                                      , idris_colourTheme = idris_colourTheme i
                                      }
                   Idris ()
clearErr
                   mod <- [FilePath] -> Maybe Int -> Idris [FilePath]
loadInputs [FilePath
f] Maybe Int
toline
                   return (Just mod)
            Right (Right (ModImport FilePath
f)) ->
                do Idris ()
clearErr
                   fmod <- FilePath -> IBCPhase -> Idris (Maybe FilePath)
loadModule FilePath
f (Bool -> IBCPhase
IBC_REPL Bool
True)
                   return (Just (inputs ++ maybe [] (:[]) fmod))
            Right (Right Command
Edit) -> do -- takeMVar stvar
                               FilePath -> IState -> Idris ()
edit FilePath
efile IState
orig
                               Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
            Right (Right Command
Proofs) -> [FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs Maybe [FilePath]
-> Idris () -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a b.
a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IState -> Idris ()
proofs IState
orig
            Right (Right Command
Quit) -> Maybe [FilePath]
forall a. Maybe a
Nothing Maybe [FilePath]
-> Idris () -> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a b.
a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
quiet) (FilePath -> Idris ()
iputStrLn FilePath
"Bye bye")
            Right (Right Command
cmd ) -> do Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (FilePath -> Command -> Idris ()
process FilePath
fn Command
cmd)
                                            (\Err
e -> do msg <- Err -> Idris FilePath
showErr Err
e ; iputStrLn msg)
                                     Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)
            Right (Left FilePath
err) -> do IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn FilePath
err
                                   Maybe [FilePath]
-> StateT IState (ExceptT Err IO) (Maybe [FilePath])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> Maybe [FilePath]
forall a. a -> Maybe a
Just [FilePath]
inputs)

resolveProof :: Name -> Idris Name
resolveProof :: Name -> Idris Name
resolveProof Name
n'
  = do i <- Idris IState
getIState
       ctxt <- getContext
       n <- case lookupNames n' ctxt of
                 [Name
x] -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
                 [] -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
                 [Name]
ns -> Err -> Idris Name
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts [Name]
ns)
       return n

removeProof :: Name -> Idris ()
removeProof :: Name -> Idris ()
removeProof Name
n =
  do i <- Idris IState
getIState
     let proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
     let 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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, (Bool, [FilePath])) -> Name
forall a b. (a, b) -> a
fst) [(Name, (Bool, [FilePath]))]
proofs
     putIState $ i { proof_list = ps }

edit :: FilePath -> IState -> Idris ()
edit :: FilePath -> IState -> Idris ()
edit FilePath
"" IState
orig = FilePath -> Idris ()
iputStrLn FilePath
"Nothing to edit"
edit FilePath
f IState
orig
    = do i <- Idris IState
getIState
         env <- runIO getEnvironment
         let editor = [(FilePath, FilePath)] -> FilePath
getEditor [(FilePath, FilePath)]
env
         let line = case IState -> Maybe FC
errSpan IState
i of
                        Just FC
l -> Char
'+' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Int -> FilePath
forall a. Show a => a -> FilePath
show ((Int, Int) -> Int
forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_start FC
l))
                        Maybe FC
Nothing -> FilePath
""
         let cmdLine = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
" " [FilePath
editor, FilePath
line, FilePath -> FilePath
fixName FilePath
f]
         runIO $ system cmdLine
         clearErr
  -- The $!! here prevents a space leak on reloading.
  -- This isn't a solution - but it's a temporary stopgap.
  -- See issue #2386
         putIState $!! orig { idris_options = idris_options i
                            , idris_colourTheme = idris_colourTheme i
                            }
         loadInputs [f] Nothing
--          clearOrigPats
         iucheck
         return ()
   where getEditor :: [(FilePath, FilePath)] -> FilePath
getEditor [(FilePath, FilePath)]
env | Just FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"EDITOR" [(FilePath, FilePath)]
env = FilePath
ed
                       | Just FilePath
ed <- FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
"VISUAL" [(FilePath, FilePath)]
env = FilePath
ed
                       | Bool
otherwise = FilePath
"vi"
         fixName :: FilePath -> FilePath
fixName FilePath
file | (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath
takeExtension FilePath
file) FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".lidr", FilePath
".idr"] = FilePath -> FilePath
quote FilePath
file
                      | Bool
otherwise = FilePath -> FilePath
quote (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath
addExtension FilePath
file FilePath
"idr"
            where
                quoteChar :: Char
quoteChar = if Bool
isWindows then Char
'"' else Char
'\''
                quote :: FilePath -> FilePath
quote FilePath
s = [Char
quoteChar] FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Char
quoteChar]



proofs :: IState -> Idris ()
proofs :: IState -> Idris ()
proofs IState
orig
  = do i <- Idris IState
getIState
       let ps = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
       case ps of
            [] -> FilePath -> Idris ()
iputStrLn FilePath
"No proofs available"
            [(Name, (Bool, [FilePath]))]
_  -> FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Proofs:\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ([Name] -> FilePath
forall a. Show a => a -> FilePath
show ([Name] -> FilePath) -> [Name] -> FilePath
forall a b. (a -> b) -> a -> b
$ ((Name, (Bool, [FilePath])) -> Name)
-> [(Name, (Bool, [FilePath]))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, [FilePath])) -> Name
forall a b. (a, b) -> a
fst [(Name, (Bool, [FilePath]))]
ps)

insertScript :: String -> [String] -> [String]
insertScript :: FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
prf [] = FilePath
"\n---------- Proofs ----------" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
"" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath
prf]
insertScript FilePath
prf (p :: FilePath
p@FilePath
"---------- Proofs ----------" : FilePath
"" : [FilePath]
xs)
    = FilePath
p FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
"" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath
prf FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
xs
insertScript FilePath
prf (FilePath
x : [FilePath]
xs) = FilePath
x FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
prf [FilePath]
xs

process :: FilePath -> Command -> Idris ()
process :: FilePath -> Command -> Idris ()
process FilePath
fn Command
Help = FilePath -> Idris ()
iPrintResult FilePath
displayHelp
process FilePath
fn Command
ShowVersion = FilePath -> Idris ()
iPrintResult FilePath
getIdrisVersion
process FilePath
fn Command
Warranty = FilePath -> Idris ()
iPrintResult FilePath
warranty
process FilePath
fn (RunShellCommand FilePath
cmd) = IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ExitCode
system FilePath
cmd IO ExitCode -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
process FilePath
fn (ChangeDirectory FilePath
f)
                 = do IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
setCurrentDirectory FilePath
f
                      () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
process FilePath
fn (ModImport FilePath
f) = do fmod <- FilePath -> IBCPhase -> Idris (Maybe FilePath)
loadModule FilePath
f (Bool -> IBCPhase
IBC_REPL Bool
True)
                              case fmod of
                                Just FilePath
pr -> FilePath -> Idris ()
isetPrompt FilePath
pr
                                Maybe FilePath
Nothing -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Can't find import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
process FilePath
fn (Eval PTerm
t)
                 = Idris () -> Idris ()
forall a. Idris a -> Idris a
withErrorReflection (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
                   do Int -> FilePath -> Idris ()
logParser Int
5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ PTerm -> FilePath
forall a. Show a => a -> FilePath
show PTerm
t
                      Idris IState
getIState Idris IState -> (IState -> Idris ()) -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IState -> PTerm -> Idris ()) -> PTerm -> IState -> Idris ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> PTerm -> Idris ()
warnDisamb PTerm
t
                      (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
                      ctxt <- getContext
                      let tm' = Term -> Term
perhapsForce (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Context -> Env -> [Name] -> Term -> Term
normaliseBlocking Context
ctxt []
                                                  [FilePath -> Name
sUN FilePath
"foreign",
                                                   FilePath -> Name
sUN FilePath
"prim_read",
                                                   FilePath -> Name
sUN FilePath
"prim_write"]
                                                 Term
tm
                      let ty' = Term -> Term
perhapsForce (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
ty
                      -- Add value to context, call it "it"
                      updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
                      ist <- getIState
                      logParser 3 $ "Raw: " ++ show (tm', ty')
                      logParser 10 $ "Debug: " ++ showEnvDbg [] tm'
                      let tmDoc = IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist Term
tm'
                          -- errReverse to make type more readable
                          tyDoc =  IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist (IState -> Term -> Term
errReverse IState
ist Term
ty')
                      iPrintTermWithType tmDoc tyDoc
  where perhapsForce :: Term -> Term
perhapsForce Term
tm | Int -> Term -> Bool
termSmallerThan Int
100 Term
tm = Term -> Term
forall a. NFData a => a -> a
force Term
tm
                        | Bool
otherwise = Term
tm

process FilePath
fn (NewDefn [PDecl]
decls) = do
        Int -> FilePath -> Idris ()
logParser Int
3 (FilePath
"Defining names using these decls: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Doc OutputAnnotation -> FilePath
forall a. Show a => a -> FilePath
show (PPOption -> [PDecl] -> Doc OutputAnnotation
showDecls PPOption
verbosePPOption [PDecl]
decls))
        ([PDecl] -> Idris ()) -> [[PDecl]] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [PDecl] -> Idris ()
defineName [[PDecl]]
namedGroups where
  namedGroups :: [[PDecl]]
namedGroups = (PDecl -> PDecl -> Bool) -> [PDecl] -> [[PDecl]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\PDecl
d1 PDecl
d2 -> PDecl -> Maybe Name
getName PDecl
d1 Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== PDecl -> Maybe Name
getName PDecl
d2) [PDecl]
decls
  getName :: PDecl -> Maybe Name
  getName :: PDecl -> Maybe Name
getName (PTy Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
opts Name
name FC
_ PTerm
ty) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
  getName (PClauses FC
fc FnOpts
opts Name
name (PClause' PTerm
clause:[PClause' PTerm]
clauses)) = Name -> Maybe Name
forall a. a -> Maybe a
Just (PClause' PTerm -> Name
forall {t}. PClause' t -> Name
getClauseName PClause' PTerm
clause)
  getName (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc DataOpts
opts PData' PTerm
dataDecl) = Name -> Maybe Name
forall a. a -> Maybe a
Just (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
dataDecl)
  getName (PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc [(Name, PTerm)]
constraints Name
name FC
nfc [(Name, FC, PTerm)]
parms [(Name, Docstring (Either Err PTerm))]
parmdocs [(Name, FC)]
fds [PDecl]
decls Maybe (Name, FC)
_ Docstring (Either Err PTerm)
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
  getName PDecl
_ = Maybe Name
forall a. Maybe a
Nothing
  -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
  getClauseName :: PClause' t -> Name
getClauseName (PClause FC
fc Name
name t
whole [t]
with t
rhs [PDecl' t]
whereBlock) = Name
name
  getClauseName (PWith FC
fc Name
name t
whole [t]
with t
rhs Maybe (Name, FC)
pn [PDecl' t]
whereBlock) = Name
name
  defineName :: [PDecl] -> Idris ()
  defineName :: [PDecl] -> Idris ()
defineName (tyDecl :: PDecl
tyDecl@(PTy Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
opts Name
name FC
_ PTerm
ty) : [PDecl]
decls) = do
    ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
EAll ElabInfo
info PDecl
tyDecl
    ElabInfo -> FC -> FnOpts -> Name -> [PClause' PTerm] -> Idris ()
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 -> Idris ()
setReplDefined (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name)
  defineName [PClauses FC
fc FnOpts
opts Name
_ [PClause' PTerm
clause]] = do
    let pterm :: PTerm
pterm = PClause' PTerm -> PTerm
getRHS PClause' PTerm
clause
    (tm,ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal ElabInfo
info ElabMode
ERHS PTerm
pterm
    ctxt <- getContext
    let tm' = Term -> Term
forall a. NFData a => a -> a
force (Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
tm)
    let ty' = Term -> Term
forall a. NFData a => a -> a
force (Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
ty)
    updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
    setReplDefined (Just $ getClauseName clause)
  defineName (PClauses{} : [PDecl]
_) = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Only one function body is allowed without a type declaration.")
  -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
  defineName (PFix FC
fc Fixity
fixity [FilePath]
strs : [PDecl]
defns) = do
    Field IState [FixDecl] -> ([FixDecl] -> [FixDecl]) -> Idris ()
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 -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([PDecl] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PDecl]
defns) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ [PDecl] -> Idris ()
defineName [PDecl]
defns
  defineName (PSyntax FC
_ Syntax
syntax:[PDecl]
_) = do
    i <- Idris IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
    put (addReplSyntax i syntax)
  defineName [PDecl]
decls = do
    ElabInfo -> [PDecl] -> Idris ()
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 -> Idris ()
setReplDefined (PDecl -> Maybe Name
getName ([PDecl] -> PDecl
forall a. HasCallStack => [a] -> a
head [PDecl]
decls))
  getClauses :: PDecl' t -> [PClause' t]
getClauses (PClauses FC
fc FnOpts
opts Name
name [PClause' t]
clauses) = [PClause' t]
clauses
  getClauses PDecl' t
_ = []
  getRHS :: PClause -> PTerm
  getRHS :: PClause' PTerm -> PTerm
getRHS (PClause FC
fc Name
name PTerm
whole [PTerm]
with PTerm
rhs [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PWith FC
fc Name
name PTerm
whole [PTerm]
with PTerm
rhs Maybe (Name, FC)
pn [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PClauseR FC
fc [PTerm]
with PTerm
rhs [PDecl]
whereBlock) = PTerm
rhs
  getRHS (PWithR FC
fc [PTerm]
with PTerm
rhs Maybe (Name, FC)
pn [PDecl]
whereBlock) = PTerm
rhs
  setReplDefined :: Maybe Name -> Idris ()
  setReplDefined :: Maybe Name -> Idris ()
setReplDefined Maybe Name
Nothing = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  setReplDefined (Just Name
n) = do
    oldState <- Idris IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
    fmodifyState repl_definitions (n:)
  -- 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 :: forall t. PDecl' t -> PDecl' t
fixClauses (PClauses FC
fc FnOpts
opts Name
_ css :: [PClause' t]
css@(PClause' t
clause:[PClause' t]
cs)) =
    FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts (PClause' t -> Name
forall {t}. PClause' t -> Name
getClauseName PClause' t
clause) [PClause' t]
css
  fixClauses (PImplementation Docstring (Either Err t)
doc [(Name, Docstring (Either Err t))]
argDocs SyntaxInfo
syn FC
fc [(Name, t)]
constraints [Name]
pnames Accessibility
acc FnOpts
opts Name
cls FC
nfc [t]
parms [(Name, t)]
pextra t
ty Maybe Name
implName [PDecl' t]
decls) =
    Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err t)
doc [(Name, Docstring (Either Err t))]
argDocs SyntaxInfo
syn FC
fc [(Name, t)]
constraints [Name]
pnames Accessibility
acc FnOpts
opts Name
cls FC
nfc [t]
parms [(Name, t)]
pextra t
ty Maybe Name
implName ((PDecl' t -> PDecl' t) -> [PDecl' t] -> [PDecl' t]
forall a b. (a -> b) -> [a] -> [b]
map PDecl' t -> PDecl' t
forall t. PDecl' t -> PDecl' t
fixClauses [PDecl' t]
decls)
  fixClauses PDecl' t
decl = PDecl' t
decl

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

process FilePath
fn (Undefine [Name]
names) = [Name] -> Idris ()
undefine [Name]
names
  where
    undefine :: [Name] -> Idris ()
    undefine :: [Name] -> Idris ()
undefine [] = do
      allDefined <- IState -> [Name]
idris_repl_defs (IState -> [Name]) -> Idris IState -> Idris [Name]
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Idris IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
      undefine' allDefined []
    -- Keep track of which names you've removed so you can
    -- print them out to the user afterward
    undefine [Name]
names = [Name] -> [Name] -> Idris ()
undefine' [Name]
names []
    undefine' :: [Name] -> [Name] -> Idris ()
undefine' [] [Name]
list = do Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Name] -> Doc OutputAnnotation
printUndefinedNames [Name]
list
                           () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    undefine' (Name
n:[Name]
names) [Name]
already = do
      allDefined <- IState -> [Name]
idris_repl_defs (IState -> [Name]) -> Idris IState -> Idris [Name]
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Idris IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
      if n `elem` allDefined
         then do undefinedJustNow <- undefClosure n
                 undefine' names (undefinedJustNow ++ already)
         else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
                 undefine' names already
    undefOne :: Name -> m ()
undefOne Name
n = do Field
  IState
  (Maybe
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Maybe
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> m ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Name
-> Field
     (Ctxt
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
     (Maybe
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n Field
  (Ctxt
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
  (Maybe
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Field
     IState
     (Ctxt
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Field
     IState
     (Maybe
        (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
forall b c a. Field b c -> Field a b -> Field a c
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 b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Field IState (Ctxt InterfaceInfo)
known_interfaces) Maybe InterfaceInfo
forall a. Maybe a
Nothing
                    Field IState [Name] -> ([Name] -> [Name]) -> m ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Name]
repl_definitions (Name -> [Name] -> [Name]
forall a. Eq a => a -> [a] -> [a]
delete Name
n)
    undefClosure :: Name -> Idris [Name]
undefClosure Name
n =
      do replDefs <- IState -> [Name]
idris_repl_defs (IState -> [Name]) -> Idris IState -> Idris [Name]
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Idris IState
forall (m :: * -> *) s. Monad m => StateT s m s
get
         callGraph <- whoCalls n
         let users = case Name -> [(Name, [Name])] -> Maybe [Name]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, [Name])]
callGraph of
                        Just [Name]
ns -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub [Name]
ns
                        Maybe [Name]
Nothing -> FilePath -> [Name]
forall a. FilePath -> [a]
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath
"Tried to undefine nonexistent name" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n)
         undefinedJustNow <- concat `fmap` mapM undefClosure users
         undefOne n
         return (nub (n : undefinedJustNow))



process FilePath
fn (ExecVal PTerm
t)
                  = do ctxt <- Idris Context
getContext
                       ist <- getIState
                       (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
--                       let tm' = normaliseAll ctxt [] tm
                       let ty' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
ty
                       res <- execute tm
                       let (resOut, tyOut) = (prettyIst ist (delab ist res),
                                              prettyIst ist (delab ist ty'))
                       iPrintTermWithType resOut tyOut

process FilePath
fn (Check (PRef FC
_ [FC]
_ Name
n))
   = do ctxt <- Idris Context
getContext
        ist <- getIState
        let ppo = IState -> PPOption
ppOptionIst IState
ist
        case lookupVisibleNames n ctxt of
          ts :: [Name]
ts@(Name
t:[Name]
_) ->
            case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
t (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
                Just (Maybe Name
_, Int
i, [Name]
_, Bool
_, Bool
_) -> Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Idris ())
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
True) (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation -> Idris ()
forall a b. (a -> b) -> a -> b
$
                                        PPOption -> IState -> Name -> Int -> Doc OutputAnnotation
showMetavarInfo PPOption
ppo IState
ist Name
n Int
i
                Maybe (Maybe Name, Int, [Name], Bool, Bool)
Nothing -> [(Name, Bool)]
-> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iPrintFunTypes [] Name
n ((Name -> (Name, Doc OutputAnnotation))
-> [Name] -> [(Name, Doc OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n)) [Name]
ts)
          [] -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"No such variable " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
  where
    lookupVisibleNames :: Name -> Context -> [Name]
    lookupVisibleNames :: Name -> Context -> [Name]
lookupVisibleNames Name
n Context
ctxt = ((Name,
  (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
 -> Name)
-> [(Name,
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name,
 (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> Name
forall a b. (a, b) -> a
fst ([(Name,
   (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
 -> [Name])
-> [(Name,
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
-> [Name]
forall a b. (a -> b) -> a -> b
$ Name
-> Ctxt
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> [(Name,
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Context
-> Ctxt
     (Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
visibleDefinitions Context
ctxt)

    showMetavarInfo :: PPOption -> IState -> Name -> Int -> Doc OutputAnnotation
showMetavarInfo PPOption
ppo IState
ist Name
n Int
i
         = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
                (Term
ty:[Term]
_) -> let ty' :: Term
ty' = Context -> Env -> Term -> Term
normaliseC (IState -> Context
tt_ctxt IState
ist) [] Term
ty in
                              PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist Int
i [] (IState -> Term -> PTerm
delab IState
ist (IState -> Term -> Term
errReverse IState
ist Term
ty'))
    putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
    putTy :: PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist Int
0 [(Name, Bool)]
bnd PTerm
sc = PPOption
-> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
forall {p}.
p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal PPOption
ppo IState
ist [(Name, Bool)]
bnd PTerm
sc
    putTy PPOption
ppo IState
ist Int
i [(Name, Bool)]
bnd (PPi Plicity
p Name
n FC
_ PTerm
t PTerm
sc)
               = let current :: Doc OutputAnnotation
current = case Name
n of
                                   MN Int
_ Text
_ -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
""
                                   UN Text
nm | (Char
'_':Char
'_':FilePath
_) <- Text -> FilePath
str Text
nm -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
""
                                   Name
_ -> RigCount -> Bool -> Doc OutputAnnotation
forall {a}. RigCount -> Bool -> Doc a
countOf (Plicity -> RigCount
pcount Plicity
p)
                                            (LanguageExt
LinearTypes LanguageExt -> [LanguageExt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
ist) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                        Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False
                                            Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon
                                            Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
t)
                                            Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
                 in
                    Doc OutputAnnotation
current Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> PPOption
-> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy PPOption
ppo IState
ist (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) PTerm
sc
    putTy PPOption
ppo IState
ist Int
_ [(Name, Bool)]
bnd PTerm
sc = PPOption
-> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
forall {p}.
p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal PPOption
ppo IState
ist ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) PTerm
sc
    putGoal :: p -> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putGoal p
ppo IState
ist [(Name, Bool)]
bnd PTerm
g
               = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"--------------------------------------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
                 OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> FilePath -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                 Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
g)

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

    tPretty :: [(Name, Bool)] -> IState -> PTerm -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd IState
ist PTerm
t = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) PTerm
t


process FilePath
fn (Check PTerm
t)
   = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
        ctxt <- getContext
        ist <- getIState
        let ty' = if IOption -> Bool
opt_evaltypes (IState -> IOption
idris_options IState
ist)
                     then Context -> Env -> Term -> Term
normaliseC Context
ctxt [] Term
ty
                     else Term
ty
        case tm of
           TType UExp
_ ->
             Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (FC -> PTerm
PType FC
emptyFC)) Doc OutputAnnotation
type1Doc
           Term
_ -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist Term
tm)
                                   (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist Term
ty')

process FilePath
fn (Core PTerm
t)
   = case PTerm
t of
       PRef FC
_ [FC]
_ Name
n ->
         do ist <- Idris IState
getIState
            case lookupDef n (tt_ctxt ist) of
              [CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
_] -> Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
True Name
n Idris [Doc OutputAnnotation]
-> ([Doc OutputAnnotation] -> Idris ()) -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Idris ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep
              [Def]
_ -> PTerm -> Idris ()
coreTerm PTerm
t
       PTerm
t -> PTerm -> Idris ()
coreTerm PTerm
t
   where coreTerm :: PTerm -> Idris ()
coreTerm PTerm
t =
           do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabREPL (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
              iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

process FilePath
fn (DocStr (Left Name
n) HowMuchDocs
w)
  | UN Text
ty <- Name
n, Text
ty Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
T.pack FilePath
"Type" = Idris IState
getIState Idris IState -> (IState -> Idris ()) -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Idris ())
-> (IState -> Doc OutputAnnotation) -> IState -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Doc OutputAnnotation
pprintTypeDoc
  | Bool
otherwise = do
        ist <- Idris IState
getIState
        let docs = Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. [a] -> [a] -> [a]
++
                   ((Name, Docstring DocTerm)
 -> (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)])))
-> [(Name, Docstring DocTerm)]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Docstring DocTerm
d)-> (Name
n, (Docstring DocTerm
d, [])))
                       (Name -> Ctxt (Docstring DocTerm) -> [(Name, Docstring DocTerm)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName (Name -> Name
modDocN Name
n) (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
ist))
        case docs of
          [] -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"No documentation for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
          [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns -> do 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
                   iRenderResult (vsep toShow)
    where showDoc :: IState
-> (Name, b)
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
showDoc IState
ist (Name
n, b
d) = do doc <- Name -> HowMuchDocs -> Idris Docs
getDocs Name
n HowMuchDocs
w
                                  return $ pprintDocs ist doc

          modDocN :: Name -> Name
modDocN (NS (UN Text
n) [Text]
ns) = Name -> [Text] -> Name
NS Name
modDocName (Text
nText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
ns)
          modDocN (UN Text
n)         = Name -> [Text] -> Name
NS Name
modDocName [Text
n]
          modDocN Name
_              = Int -> FilePath -> Name
sMN Int
1 FilePath
"NotFoundForSure"

process FilePath
fn (DocStr (Right Const
c) HowMuchDocs
_) -- constants only have overviews
   = do ist <- Idris IState
getIState
        iRenderResult $ pprintConstDocs ist c (constDocs c)

process FilePath
fn Command
Universes
                     = do i <- Idris IState
getIState
                          let cs = IState -> Set ConstraintFC
idris_constraints IState
i
                          let cslist = Set ConstraintFC -> [ConstraintFC]
forall a. Set a -> [a]
S.toAscList Set ConstraintFC
cs
--                        iputStrLn $ showSep "\n" (map show cs)
                          iputStrLn $ showSep "\n" (map show cslist)
                          let n = [ConstraintFC] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstraintFC]
cslist
                          iputStrLn $ "(" ++ show n ++ " constraints)"
                          case ucheck cs of
                            Error Err
e -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> FilePath
pshow IState
i Err
e
                            OK ()
_ -> FilePath -> Idris ()
iPrintResult FilePath
"Universes OK"
process FilePath
fn (Defn Name
n)
                    = do i <- Idris IState
getIState
                         let head = FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"Compiled patterns:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<$>
                                    FilePath -> Doc a
forall a. FilePath -> Doc a
text ([Def] -> FilePath
forall a. Show a => a -> FilePath
show (Name -> Context -> [Def]
lookupDef Name
n (IState -> Context
tt_ctxt IState
i)))
                         let defs =
                              case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> [([([(Name, Term)], Term, Term)], [PTerm])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
i) of
                                [] -> Doc a
forall a. Doc a
empty
                                [([([(Name, Term)], Term, Term)]
d, [PTerm]
_)] -> FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"Original definiton:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<$>
                                            [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
vsep ((([(Name, Term)], Term, Term) -> Doc a)
-> [([(Name, Term)], Term, Term)] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ([(Name, Term)], Term, Term) -> Doc a
forall {a} {a}. IState -> (a, Term, Term) -> Doc a
printCase IState
i) [([(Name, Term)], Term, Term)]
d)
                         let tot =
                              case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
i) of
                                 [Totality
t] -> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
i
                                 [Totality]
_ -> Doc OutputAnnotation
forall a. Doc a
empty
                         iRenderResult $ vsep [head, defs, tot]
    where printCase :: IState -> (a, Term, Term) -> Doc a
printCase IState
i (a
_, Term
lhs, Term
rhs)
             = let i' :: IState
i' = IState
i { idris_options = (idris_options i) { opt_showimp = True } }
               in FilePath -> Doc a
forall a. FilePath -> Doc a
text (IState -> PTerm -> FilePath
showTm IState
i' (IState -> Term -> PTerm
delab IState
i Term
lhs)) Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc a
forall a. FilePath -> Doc a
text FilePath
"=" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+>
                  FilePath -> Doc a
forall a. FilePath -> Doc a
text (IState -> PTerm -> FilePath
showTm IState
i' (IState -> Term -> PTerm
delab IState
i Term
rhs))
process FilePath
fn (TotCheck Name
n)
   = do i <- Idris IState
getIState
        case lookupNameTotal n (tt_ctxt i) of
           []  -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Unknown operator " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
           [(Name, Totality)]
ts  -> do ist <- Idris IState
getIState
                     c <- colourise
                     let ppo =  IState -> PPOption
ppOptionIst IState
ist
                     let showN Name
n = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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
                     iRenderResult . vsep .
                      map (\(Name
n, Totality
t) -> Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
hang Int
4 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Name -> Doc OutputAnnotation
showN Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
i) $
                      ts

process FilePath
fn (DebugUnify PTerm
l PTerm
r)
   = do (ltm, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
l
        (rtm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS r
        ctxt <- getContext
        case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of
             OK ([(Name, Term)], Fails)
ans -> FilePath -> Idris ()
iputStrLn (([(Name, Term)], Fails) -> FilePath
forall a. Show a => a -> FilePath
show ([(Name, Term)], Fails)
ans)
             Error Err
e -> FilePath -> Idris ()
iputStrLn (Err -> FilePath
forall a. Show a => a -> FilePath
show Err
e)

process FilePath
fn (DebugInfo Name
n)
   = do i <- Idris IState
getIState
        let oi = Name -> Ctxt OptInfo -> [(Name, OptInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt OptInfo
idris_optimisation IState
i)
        when (not (null oi)) $ iputStrLn (show oi)
        let si = Name -> Ctxt [Bool] -> [[Bool]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [Bool]
idris_statics IState
i)
        when (not (null si)) $ iputStrLn (show si)
        let di = Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i)
        when (not (null di)) $ iputStrLn (show di)
        let imps = Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i)
        when (not (null imps)) $ iputStrLn (show imps)
        let d = Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAcc Name
n Bool
False (IState -> Context
tt_ctxt IState
i)
        when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
        i <- getIState
        let cg' = Name -> Ctxt CGInfo -> [(Name, CGInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt CGInfo
idris_callgraph IState
i)
        sc <- checkSizeChange n
        iputStrLn $ "Size change: " ++ show sc
        let fn = Name -> Ctxt FnInfo -> [(Name, FnInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt FnInfo
idris_fninfo IState
i)
        when (not (null cg')) $ do iputStrLn "Call graph:\n"
                                   iputStrLn (show cg')
        when (not (null fn)) $ iputStrLn (show fn)
process FilePath
fn (Search [PkgName]
pkgs PTerm
t) = [PkgName] -> PTerm -> Idris ()
searchByType [PkgName]
pkgs PTerm
t
process FilePath
fn (CaseSplitAt Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
caseSplitAt FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddClauseFrom Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddProofClauseFrom Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (AddMissing Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeWith Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
makeWith FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeCase Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
makeCase FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (MakeLemma Bool
updatefile Int
l Name
n)
    = FilePath -> Bool -> Int -> Name -> Idris ()
makeLemma FilePath
fn Bool
updatefile Int
l Name
n
process FilePath
fn (DoProofSearch Bool
updatefile Bool
rec Int
l Name
n [Name]
hints)
    = FilePath
-> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris ()
doProofSearch FilePath
fn Bool
updatefile Bool
rec Int
l Name
n [Name]
hints Maybe Int
forall a. Maybe a
Nothing
process FilePath
fn (Spec PTerm
t)
                    = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
                         ctxt <- getContext
                         ist <- getIState
                         let tm' = Context -> Env -> Term -> Term
simplify Context
ctxt [] {- (idris_statics ist) -} Term
tm
                         iPrintResult (show (delab ist tm'))

process FilePath
fn (RmProof Name
n')
  = do i <- Idris IState
getIState
       n <- resolveProof n'
       let proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
       case lookup n proofs of
            Maybe (Bool, [FilePath])
Nothing -> FilePath -> Idris ()
iputStrLn FilePath
"No proof to remove"
            Just (Bool, [FilePath])
_  -> do Name -> Idris ()
removeProof Name
n
                          Name -> Idris ()
insertMetavar Name
n
                          FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Removed proof " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
                          where
                            insertMetavar :: Name -> Idris ()
                            insertMetavar :: Name -> Idris ()
insertMetavar Name
n =
                              do i <- Idris IState
getIState
                                 let ms = IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i
                                 putIState $ i { idris_metavars = (n, (Nothing, 0, [], False, False)) : ms }

process FilePath
fn' (AddProof Maybe Name
prf)
  = do fn <- do
         let fn'' :: FilePath
fn'' = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') FilePath
fn'
         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
fn'' FilePath -> FilePath -> FilePath
<.> FilePath
"idr"
         exExt <- runIO $ doesFileExist fnExt
         if ex
            then return fn''
            else if exExt
                    then return fnExt
                    else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
       let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
       runIO $ copyFile fn fb -- make a backup in case something goes wrong!
       prog <- runIO $ readSource fb
       i <- getIState
       let proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
       n' <- case prf of
                Maybe Name
Nothing -> case [(Name, (Bool, [FilePath]))]
proofs of
                             [] -> FilePath -> Idris Name
forall a. FilePath -> Idris a
ifail FilePath
"No proof to add"
                             ((Name
x, (Bool, [FilePath])
_) : [(Name, (Bool, [FilePath]))]
_) -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
                Just Name
nm -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
nm
       n <- resolveProof n'
       case lookup n proofs of
            Maybe (Bool, [FilePath])
Nothing -> FilePath -> Idris ()
iputStrLn FilePath
"No proof to add"
            Just (Bool
mode, [FilePath]
prf) ->
              do let script :: FilePath
script = if Bool
mode
                                 then Bool -> Name -> [FilePath] -> FilePath
showRunElab (FilePath -> Bool
lit FilePath
fn) Name
n [FilePath]
prf
                                 else Bool -> Name -> [FilePath] -> FilePath
showProof (FilePath -> Bool
lit FilePath
fn) Name
n [FilePath]
prf
                 let prog' :: [FilePath]
prog' = FilePath -> [FilePath] -> [FilePath]
insertScript FilePath
script [FilePath]
ls
                 IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fn ([FilePath] -> FilePath
unlines [FilePath]
prog')
                 Name -> Idris ()
removeProof Name
n
                 FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Added proof " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
             where ls :: [FilePath]
ls = (FilePath -> [FilePath]
lines FilePath
prog)

process FilePath
fn (ShowProof Name
n')
  = do i <- Idris IState
getIState
       n <- resolveProof n'
       let proofs = IState -> [(Name, (Bool, [FilePath]))]
proof_list IState
i
       case lookup n proofs of
            Maybe (Bool, [FilePath])
Nothing -> FilePath -> Idris ()
iPrintError FilePath
"No proof to show"
            Just (Bool
m, [FilePath]
p)  -> FilePath -> Idris ()
iPrintResult (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ if Bool
m
                                             then Bool -> Name -> [FilePath] -> FilePath
showRunElab Bool
False Name
n [FilePath]
p
                                             else Bool -> Name -> [FilePath] -> FilePath
showProof Bool
False Name
n [FilePath]
p

process FilePath
fn (Prove Bool
mode Name
n')
     = do ctxt <- Idris Context
getContext
          ist <- getIState
          let ns = Name -> Context -> [Name]
lookupNames Name
n' Context
ctxt
          let metavars = (Name -> Maybe (Name, (Maybe Name, Int, [Name], Bool, Bool)))
-> [Name] -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\Name
n -> do 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); return (n, c)) [Name]
ns
          n <- case metavars of
              [] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Err) -> FilePath -> Err
forall a b. (a -> b) -> a -> b
$ FilePath
"Cannot find metavariable " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n')
              [(Name
n, (Maybe Name
_,Int
_,[Name]
_,Bool
False,Bool
_))] -> Name -> Idris Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
              [(Name
_, (Maybe Name
_,Int
_,[Name]
_,Bool
_,Bool
False))] -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Can't prove this hole as it depends on other holes")
              [(Name
_, (Maybe Name
_,Int
_,[Name]
_,Bool
True,Bool
_))]  -> Err -> Idris Name
forall a. Err -> Idris a
ierror (FilePath -> Err
forall t. FilePath -> Err' t
Msg FilePath
"Declarations not solvable using prover")
              [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns -> Err -> Idris Name
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
ns))
          prover (toplevelWith fn) mode (lit fn) n
          -- recheck totality
          i <- getIState
          totcheck (fileFC "(input)", n)
          mapM_ (\ (FC
f,Name
n) -> Name -> Totality -> Idris ()
setTotality Name
n Totality
Unchecked) (idris_totcheck i)
          mapM_ checkDeclTotality (idris_totcheck i)
          warnTotality
process FilePath
fn (WHNF PTerm
t)
                    = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
                         ctxt <- getContext
                         ist <- getIState
                         let tm' = Context -> Env -> Term -> Term
whnf Context
ctxt [] Term
tm
                         let tmArgs' = Context -> Env -> Term -> Term
whnfArgs Context
ctxt [] Term
tm
                         iPrintResult $ "WHNF: " ++ (show (delab ist tm'))
                         iPrintResult $ "WHNF args: " ++ (show (delab ist tmArgs'))
process FilePath
fn (TestInline PTerm
t)
                           = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
                                ctxt <- getContext
                                ist <- getIState
                                let tm' = IState -> Term -> Term
inlineTerm IState
ist Term
tm
                                c <- colourise
                                iPrintResult (showTm ist (delab ist tm'))
process FilePath
fn (Execute PTerm
tm)
                   = Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
                       (do ist <- Idris IState
getIState
                           (m_in, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)
                           m <- applyOpts m_in
                           (tmpn, tmph) <- runIO $ tempfile ""
                           runIO $ hClose tmph
                           t <- codegen
                           -- gcc adds .exe when it builds windows programs
                           progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
                           ir <- compile t tmpn (Just m)
                           runIO $ generate t (fst (head (idris_imported ist))) ir
                           case idris_outputmode ist of
                             RawOutput Handle
h ->
                               do 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 res of
                                    ExitCode
ExitSuccess -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                    ExitFailure Int
err ->
                                      FilePath -> Idris ()
forall a. FilePath -> Idris a
ifail (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Compiled program " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                              if Int
err Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
                                              then FilePath
"was killed by signal " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                                   Int -> FilePath
forall a. Show a => a -> FilePath
show (Int
0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
err)
                                              else FilePath
"terminated with exit code " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                                   Int -> FilePath
forall a. Show a => a -> FilePath
show Int
err
                             IdeMode Integer
n Handle
h -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$
                                             FilePath -> FilePath -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
IdeMode.convSExp FilePath
"run-program" FilePath
tmpn Integer
n)
                       (\Err
e -> Idris IState
getIState Idris IState -> (IState -> Idris ()) -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Doc OutputAnnotation -> Idris ()
iRenderError (Doc OutputAnnotation -> Idris ())
-> (IState -> Doc OutputAnnotation) -> IState -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Err -> Doc OutputAnnotation)
-> Err -> IState -> Doc OutputAnnotation
forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> Err -> Doc OutputAnnotation
pprintErr Err
e)
  where fc :: FC
fc = FilePath -> FC
fileFC FilePath
"main"
process FilePath
fn (Compile Codegen
codegen FilePath
f)
      | (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath
takeExtension FilePath
f) FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".idr", FilePath
".lidr", FilePath
".idc"] =
          FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Invalid filename for compiler output \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++FilePath
"\""
      | Bool
otherwise = do opts <- Idris [Opt]
getCmdLine
                       let iface = Opt
Interface Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
                       let mainname = Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN FilePath
"main") [FilePath
"Main"]

                       m <- if iface then return Nothing else
                            do (m', _) <- elabVal (recinfo (fileFC "compiler")) ERHS
                                            (PApp fc (PRef fc [] (sUN "run__IO"))
                                            [pexp $ PRef fc [] mainname])
                               return (Just m')
                       ir <- compile codegen f m
                       i <- getIState
                       let ir' = CodegenInfo
ir {interfaces = iface}
                       runIO $ generate codegen (fst (head (idris_imported i))) ir'
  where fc :: FC
fc = FilePath -> FC
fileFC FilePath
"main"
process FilePath
fn (LogLvl Int
i) = Int -> Idris ()
setLogLevel Int
i
process FilePath
fn (LogCategory [LogCat]
cs) = [LogCat] -> Idris ()
setLogCats [LogCat]
cs
-- Elaborate as if LHS of a pattern (debug command)
process FilePath
fn (Pattelab PTerm
t)
     = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ELHS PTerm
t
          iPrintResult $ show tm ++ "\n\n : " ++ show ty

process FilePath
fn (Missing Name
n)
    = do i <- Idris IState
getIState
         ppOpts <- fmap ppOptionIst getIState
         case lookupCtxt n (idris_patdefs i) of
           [] -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Unknown name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
           [([([(Name, Term)], Term, Term)]
_, [PTerm]
tms)] ->
             Doc OutputAnnotation -> Idris ()
iRenderResult ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((PTerm -> Doc OutputAnnotation)
-> [PTerm] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppOpts
                                                   []
                                                   []
                                                   (IState -> [FixDecl]
idris_infixes IState
i))
                                      [PTerm]
tms))
           [([([(Name, Term)], Term, Term)], [PTerm])]
_ -> FilePath -> Idris ()
iPrintError FilePath
"Ambiguous name"
process FilePath
fn (DynamicLink FilePath
l)
                           = do i <- Idris IState
getIState
                                let importdirs = IOption -> [FilePath]
opt_importdirs (IState -> IOption
idris_options IState
i)
                                    lib = FilePath -> FilePath
trim FilePath
l
                                handle <- lift . lift $ tryLoadLib importdirs lib
                                case handle of
                                  Maybe DynamicLib
Nothing -> FilePath -> Idris ()
iPrintError (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Could not load dynamic lib \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\""
                                  Just DynamicLib
x -> do let libs :: [DynamicLib]
libs = IState -> [DynamicLib]
idris_dynamic_libs IState
i
                                               if DynamicLib
x DynamicLib -> [DynamicLib] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DynamicLib]
libs
                                                  then do Int -> FilePath -> Idris ()
logParser Int
1 (FilePath
"Tried to load duplicate library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ DynamicLib -> FilePath
lib_name DynamicLib
x)
                                                          () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                                  else IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_dynamic_libs = x:libs }
    where trim :: FilePath -> FilePath
trim = FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
process FilePath
fn Command
ListDynamic
                       = do i <- Idris IState
getIState
                            iputStrLn "Dynamic libraries:"
                            showLibs $ idris_dynamic_libs i
    where showLibs :: [DynamicLib] -> Idris ()
showLibs []                = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          showLibs ((Lib FilePath
name DL
_):[DynamicLib]
ls) = do FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name; [DynamicLib] -> Idris ()
showLibs [DynamicLib]
ls
process FilePath
fn Command
Metavars
                 = do ist <- Idris IState
getIState
                      let 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 mvs of
                        [] -> FilePath -> Idris ()
iPrintError FilePath
"No global holes to solve"
                        [Name]
_ -> FilePath -> Idris ()
iPrintResult (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Global holes:\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
mvs
process FilePath
fn Command
NOP      = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

process FilePath
fn (SetOpt   Opt
ErrContext)  = Bool -> Idris ()
setErrContext Bool
True
process FilePath
fn (UnsetOpt Opt
ErrContext)  = Bool -> Idris ()
setErrContext Bool
False
process FilePath
fn (SetOpt Opt
ShowImpl)      = Bool -> Idris ()
setImpShow Bool
True
process FilePath
fn (UnsetOpt Opt
ShowImpl)    = Bool -> Idris ()
setImpShow Bool
False
process FilePath
fn (SetOpt Opt
ShowOrigErr)   = Bool -> Idris ()
setShowOrigErr Bool
True
process FilePath
fn (UnsetOpt Opt
ShowOrigErr) = Bool -> Idris ()
setShowOrigErr Bool
False
process FilePath
fn (SetOpt Opt
AutoSolve)     = Bool -> Idris ()
setAutoSolve Bool
True
process FilePath
fn (UnsetOpt Opt
AutoSolve)   = Bool -> Idris ()
setAutoSolve Bool
False
process FilePath
fn (SetOpt Opt
NoBanner)      = Bool -> Idris ()
setNoBanner Bool
True
process FilePath
fn (UnsetOpt Opt
NoBanner)    = Bool -> Idris ()
setNoBanner Bool
False
process FilePath
fn (SetOpt Opt
WarnReach)     = Field IState [Opt] -> ([Opt] -> [Opt]) -> Idris ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Opt]
opts_idrisCmdline (([Opt] -> [Opt]) -> Idris ()) -> ([Opt] -> [Opt]) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Opt] -> [Opt]
forall a. Eq a => [a] -> [a]
nub ([Opt] -> [Opt]) -> ([Opt] -> [Opt]) -> [Opt] -> [Opt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Opt
WarnReachOpt -> [Opt] -> [Opt]
forall a. a -> [a] -> [a]
:)
process FilePath
fn (UnsetOpt Opt
WarnReach)   = Field IState [Opt] -> ([Opt] -> [Opt]) -> Idris ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field IState [Opt]
opts_idrisCmdline (([Opt] -> [Opt]) -> Idris ()) -> ([Opt] -> [Opt]) -> Idris ()
forall a b. (a -> b) -> a -> b
$ Opt -> [Opt] -> [Opt]
forall a. Eq a => a -> [a] -> [a]
delete Opt
WarnReach
process FilePath
fn (SetOpt Opt
EvalTypes)     = Bool -> Idris ()
setEvalTypes Bool
True
process FilePath
fn (UnsetOpt Opt
EvalTypes)   = Bool -> Idris ()
setEvalTypes Bool
False

process FilePath
fn (SetOpt Opt
DesugarNats)   = Bool -> Idris ()
setDesugarNats Bool
True
process FilePath
fn (UnsetOpt Opt
DesugarNats) = Bool -> Idris ()
setDesugarNats Bool
False

process FilePath
fn (SetOpt Opt
_) = FilePath -> Idris ()
iPrintError FilePath
"Not a valid option"
process FilePath
fn (UnsetOpt Opt
_) = FilePath -> Idris ()
iPrintError FilePath
"Not a valid option"
process FilePath
fn (SetColour ColourType
ty IdrisColour
c) = ColourType -> IdrisColour -> Idris ()
setColour ColourType
ty IdrisColour
c
process FilePath
fn Command
ColourOn
                    = do ist <- Idris IState
getIState
                         putIState $ ist { idris_colourRepl = True }
process FilePath
fn Command
ColourOff
                     = do ist <- Idris IState
getIState
                          putIState $ ist { idris_colourRepl = False }
process FilePath
fn Command
ListErrorHandlers =
  do ist <- Idris IState
getIState
     iPrintResult $ case idris_errorhandlers ist of
       []       -> FilePath
"No registered error handlers"
       [Name]
handlers -> FilePath
"Registered error handlers: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ([FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([FilePath] -> FilePath)
-> ([Name] -> [FilePath]) -> [Name] -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse FilePath
", " ([FilePath] -> [FilePath])
-> ([Name] -> [FilePath]) -> [Name] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show) [Name]
handlers
process FilePath
fn (SetConsoleWidth ConsoleWidth
w) = ConsoleWidth -> Idris ()
setWidth ConsoleWidth
w
process FilePath
fn (SetPrinterDepth Maybe Int
d) = Maybe Int -> Idris ()
setDepth Maybe Int
d
process FilePath
fn (Apropos [PkgName]
pkgs FilePath
a) =
  do orig <- Idris IState
getIState
     when (not (null pkgs)) $
       iputStrLn $ "Searching packages: " ++ showSep ", " (map show pkgs)
     mapM_ loadPkgIndex pkgs
     ist <- getIState
     let mods = IState -> Text -> [(FilePath, Docstring DocTerm)]
aproposModules IState
ist (FilePath -> Text
T.pack FilePath
a)
     let names = IState -> Text -> [Name]
apropos IState
ist (FilePath -> Text
T.pack FilePath
a)
     let 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 a b. (a -> b) -> Maybe a -> Maybe b
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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (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 (not (null mods)) || (not (null aproposInfo))
        then iRenderResult $ vsep (map (\(FilePath
m, Docstring DocTerm
d) -> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Module" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
m Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
                                                   IState -> Docstring DocTerm -> Doc OutputAnnotation
ppD IState
ist Docstring DocTerm
d Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line) mods) <$>
                             vsep (map (prettyDocumentedIst ist) aproposInfo)
        else iRenderError $ text "No results found"
  where isUN :: Name -> Bool
isUN (UN Text
_) = Bool
True
        isUN (NS Name
n [Text]
_) = Name -> Bool
isUN Name
n
        isUN Name
_ = Bool
False
        ppD :: IState -> Docstring DocTerm -> Doc OutputAnnotation
ppD IState
ist = (DocTerm -> FilePath -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> FilePath -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> FilePath -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist) (Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) []))


process FilePath
fn (WhoCalls Name
n) =
  do calls <- Name -> Idris [(Name, [Name])]
whoCalls Name
n
     ist <- getIState
     iRenderResult . vsep $
       map (\(Name
n, [Name]
ns) ->
             FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"Callers of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
             Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
1 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"*" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []) [Name]
ns)))
           calls

process FilePath
fn (CallsWho Name
n) =
  do calls <- Name -> Idris [(Name, [Name])]
callsWho Name
n
     ist <- getIState
     iRenderResult . vsep $
       map (\(Name
n, [Name]
ns) ->
             Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"calls:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
             Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
1 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"*" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
True []) [Name]
ns)))
           calls

process FilePath
fn (Browse [FilePath]
ns) =
  do underNSs <- [FilePath] -> StateT IState (ExceptT Err IO) [[FilePath]]
namespacesInNS [FilePath]
ns
     names <- namesInNS ns
     if null underNSs && null names
        then iPrintError "Invalid or empty namespace"
        else do ist <- getIState
                iRenderResult $
                  text "Namespaces:" <$>
                  indent 2 (vsep (map (text . showSep ".") underNSs)) <$>
                  text "Names:" <$>
                  indent 2 (vsep (map (\Name
n -> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                             (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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))
                                      names))

-- IdrisDoc
process FilePath
fn (MakeDoc FilePath
s) =
  do     istate        <- Idris IState
getIState
         let names      = FilePath -> [FilePath]
words FilePath
s
             parse FilePath
n    | Right Name
x <- Parser IState Name
-> IState -> FilePath -> FilePath -> Either ParseError Name
forall st res.
Parser st res
-> st -> FilePath -> FilePath -> Either ParseError res
runparser Parser IState Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name IState
istate FilePath
fn FilePath
n = Name -> Either FilePath Name
forall a b. b -> Either a b
Right Name
x
             parse FilePath
n    = FilePath -> Either FilePath Name
forall a b. a -> Either a b
Left FilePath
n
             (bad, nss) = partitionEithers $ map parse names
         cd            <- runIO getCurrentDirectory
         let outputDir  = FilePath
cd FilePath -> FilePath -> FilePath
</> FilePath
"doc"
         result        <- if null bad then runIO $ generateDocs istate nss outputDir
                                      else return . Left $ "Illegal name: " ++ head bad
         case result of Right ()
_   -> FilePath -> Idris ()
iputStrLn FilePath
"IdrisDoc generated"
                        Left  FilePath
err -> FilePath -> Idris ()
iPrintError FilePath
err
process FilePath
fn (PrintDef Name
n) =
  do result <- Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
False Name
n
     case result of
       [] -> FilePath -> Idris ()
iPrintError FilePath
"Not found"
       [Doc OutputAnnotation]
outs -> Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Idris ())
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> Idris ())
-> [Doc OutputAnnotation] -> Idris ()
forall a b. (a -> b) -> a -> b
$ [Doc OutputAnnotation]
outs

-- Show relevant transformation rules for the name 'n'
process FilePath
fn (TransformInfo Name
n)
   = do i <- Idris IState
getIState
        let ts = Name -> Ctxt [(Term, Term)] -> [[(Term, Term)]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [(Term, Term)]
idris_transforms IState
i)
        let res = ([(Term, Term)] -> [Doc OutputAnnotation])
-> [[(Term, Term)]] -> [[Doc OutputAnnotation]]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> [(Term, Term)] -> [Doc OutputAnnotation]
showTrans IState
i) [[(Term, Term)]]
ts
        iRenderResult . vsep $ concat res
    where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
          showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
showTrans IState
i [] = []
          showTrans IState
i ((Term
lhs, Term
rhs) : [(Term, Term)]
ts)
              = let ppTm :: Term -> Doc OutputAnnotation
ppTm Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Term -> Doc OutputAnnotation) -> Term -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                                 PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
i) [] [] [] (PTerm -> Doc OutputAnnotation)
-> (Term -> PTerm) -> Term -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                                 IState -> Term -> PTerm
delab IState
i (Term -> Doc OutputAnnotation) -> Term -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Term
tm
                    ts' :: [Doc OutputAnnotation]
ts' = IState -> [(Term, Term)] -> [Doc OutputAnnotation]
showTrans IState
i [(Term, Term)]
ts in
                    Term -> Doc OutputAnnotation
ppTm Term
lhs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
" ==> " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation
ppTm Term
rhs Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. a -> [a] -> [a]
: [Doc OutputAnnotation]
ts'

process FilePath
fn (PPrint OutputFmt
fmt Int
width (PRef FC
_ [FC]
_ Name
n))
   = do outs <- Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
False Name
n
        iPrintResult =<< renderExternal fmt width (vsep outs)


process FilePath
fn (PPrint OutputFmt
fmt Int
width PTerm
t)
   = do (tm, ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"toplevel")) ElabMode
ERHS PTerm
t
        ist <- getIState
        iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)


process FilePath
fn Command
Quit = FilePath -> Idris ()
iPrintError FilePath
"Command ':quit' is currently unsupported"
process FilePath
fn Command
Reload = FilePath -> Idris ()
iPrintError FilePath
"Command ':reload' is currently unsupported"
process FilePath
fn Command
Watch = FilePath -> Idris ()
iPrintError FilePath
"Command ':watch' is currently unsupported"
process FilePath
fn (Load FilePath
_ Maybe Int
_) = FilePath -> Idris ()
iPrintError FilePath
"Command ':load' is currently unsupported"
process FilePath
fn Command
Edit = FilePath -> Idris ()
iPrintError FilePath
"Command ':edit' is currently unsupported"
process FilePath
fn Command
Proofs = FilePath -> Idris ()
iPrintError FilePath
"Command ':proofs' is currently unsupported"
process FilePath
fn (Verbosity Int
_)
   = FilePath -> Idris ()
iPrintError FilePath
"Command ':verbosity' is currently unsupported"


showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal :: Totality -> IState -> Doc OutputAnnotation
showTotal t :: Totality
t@(Partial (Other [Name]
ns)) IState
i
   = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"possibly not total due to:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
     [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> Doc OutputAnnotation
showTotalN IState
i) [Name]
ns)
showTotal t :: Totality
t@(Partial (Mutual [Name]
ns)) IState
i
   = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"possibly not total due to recursive path:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
     Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate Doc OutputAnnotation
forall a. Doc a
comma
       ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
                   FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n))
            [Name]
ns))))
showTotal Totality
t IState
i = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (Totality -> FilePath
forall a. Show a => a -> FilePath
show Totality
t)

showTotalN :: IState -> Name -> Doc OutputAnnotation
showTotalN :: IState -> Name -> Doc OutputAnnotation
showTotalN IState
ist Name
n = case Name -> Context -> [Totality]
lookupTotal Name
n (IState -> Context
tt_ctxt IState
ist) of
                        [Totality
t] -> Name -> Doc OutputAnnotation
showN Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
", which is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Totality -> IState -> Doc OutputAnnotation
showTotal Totality
t IState
ist
                        [Totality]
_ -> Doc OutputAnnotation
forall a. Doc a
empty
    where
       ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
       showN :: Name -> Doc OutputAnnotation
showN Name
n = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe FilePath
-> Maybe FilePath
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text (FilePath -> Doc OutputAnnotation)
-> FilePath -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
                 Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> FilePath
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
ist) [] PPOption
ppo Bool
False Name
n

displayHelp :: FilePath
displayHelp = let vstr :: FilePath
vstr = Version -> FilePath
showVersion Version
getIdrisVersionNoGit in
              FilePath
"\nIdris version " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              FilePath
"--------------" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map (\Char
x -> Char
'-') FilePath
vstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              (([FilePath], CmdArg, FilePath) -> FilePath)
-> [([FilePath], CmdArg, FilePath)] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([FilePath], CmdArg, FilePath) -> FilePath
forall {a}. Show a => ([FilePath], a, FilePath) -> FilePath
cmdInfo [([FilePath], CmdArg, FilePath)]
helphead FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              (([FilePath], CmdArg, FilePath) -> FilePath)
-> [([FilePath], CmdArg, FilePath)] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([FilePath], CmdArg, FilePath) -> FilePath
forall {a}. Show a => ([FilePath], a, FilePath) -> FilePath
cmdInfo [([FilePath], CmdArg, FilePath)]
help
  where cmdInfo :: ([FilePath], a, FilePath) -> FilePath
cmdInfo ([FilePath]
cmds, a
args, FilePath
text) = FilePath
"   " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col Int
16 Int
12 (FilePath -> [FilePath] -> FilePath
showSep FilePath
" " [FilePath]
cmds) (a -> FilePath
forall a. Show a => a -> FilePath
show a
args) FilePath
text
        col :: Int -> Int -> FilePath -> FilePath -> FilePath -> FilePath
col Int
c1 Int
c2 FilePath
l FilePath
m FilePath
r =
            FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (Int
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
l) (Char -> FilePath
forall a. a -> [a]
repeat Char
' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
            FilePath
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (Int
c2 Int -> Int -> Int
forall a. Num a => a -> a -> a
- FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
m) (Char -> FilePath
forall a. a -> [a]
repeat Char
' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
r FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n"

pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
pprintDef Bool
asCore Name
n =
  do ist <- Idris IState
getIState
     ctxt <- getContext
     let ambiguous = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Name -> Context -> [Name]
lookupNames Name
n Context
ctxt) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
         patdefs = IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist
         tyinfo = IState -> Ctxt TypeInfo
idris_datatypes IState
ist
     if asCore
       then return $ map (ppCoreDef ist) (lookupCtxtName n patdefs)
       else return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
                     map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
                     map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
  where ppCoreDef :: IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
        ppCoreDef :: IState
-> (Name, ([([(Name, Term)], Term, Term)], [PTerm]))
-> Doc OutputAnnotation
ppCoreDef IState
ist (Name
n, ([([(Name, Term)], Term, Term)]
clauses, [PTerm]
missing)) =
          case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
            [] -> FilePath -> Doc OutputAnnotation
forall a. HasCallStack => FilePath -> a
error FilePath
"Attempted pprintDef of TT of thing that doesn't exist"
            (Term
ty:[Term]
_) -> 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)] -> Term -> OutputAnnotation
AnnTerm [] Term
ty) ([Name] -> Term -> Doc OutputAnnotation
pprintTT [] Term
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, Term)], Term, Term) -> Doc OutputAnnotation)
-> [([(Name, Term)], Term, Term)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (\([(Name, Term)]
vars, Term
lhs, Term
rhs) ->  [(Name, Term)] -> Term -> Term -> Doc OutputAnnotation
pprintTTClause [(Name, Term)]
vars Term
lhs Term
rhs) [([(Name, Term)], Term, Term)]
clauses)
        ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
        ppDef :: Bool
-> IState
-> (Name, ([([(Name, Term)], Term, Term)], [PTerm]))
-> Doc OutputAnnotation
ppDef Bool
amb IState
ist (Name
n, ([([(Name, Term)], Term, Term)]
clauses, [PTerm]
missing)) =
          Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
          Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
          IState -> [([(Name, Term)], Term, Term)] -> Doc OutputAnnotation
ppClauses IState
ist [([(Name, Term)], Term, Term)]
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, Term)], Term, Term)] -> Doc OutputAnnotation
ppClauses IState
ist [] = FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"No clauses."
        ppClauses IState
ist [([(Name, Term)], Term, Term)]
cs = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((([(Name, Term)], Term, Term) -> Doc OutputAnnotation)
-> [([(Name, Term)], Term, Term)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)], Term, Term) -> Doc OutputAnnotation
pp [([(Name, Term)], Term, Term)]
cs)
          where pp :: ([(Name, Term)], Term, Term) -> Doc OutputAnnotation
pp ([(Name, Term)]
varTys, Term
lhs, Term
rhs) =
                  let vars :: [Name]
vars = ((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
varTys
                      ppTm :: Term -> Doc OutputAnnotation
ppTm Term
t = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> 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)) Term
t) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Term -> Doc OutputAnnotation) -> Term -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                               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)
-> (Term -> PTerm) -> Term -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                               IState -> [(Name, Term)] -> Term -> PTerm
delabWithEnv IState
ist [(Name, Term)]
varTys (Term -> Doc OutputAnnotation) -> Term -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
                               Term
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
$ Term -> Doc OutputAnnotation
ppTm Term
lhs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text FilePath
"=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
group (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
hang Int
2 (Doc OutputAnnotation -> Doc OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Term -> Doc OutputAnnotation
ppTm Term
rhs)
        ppMissing :: p -> Doc a
ppMissing p
_ = Doc a
forall a. Doc a
empty

        ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
        ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
ppTy Bool
amb IState
ist (Name
n, TI [Name]
constructors Bool
isCodata DataOpts
_ [Int]
_ [Name]
_ Bool
_)
          = FilePath -> Doc OutputAnnotation
kwd FilePath
key Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
            Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc OutputAnnotation
kwd FilePath
"where" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
            Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
indent Int
2 ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IState -> Name -> Doc OutputAnnotation
ppCon Bool
False IState
ist) [Name]
constructors))
          where
            key :: FilePath
key | Bool
isCodata = FilePath
"codata"
                | Bool
otherwise = FilePath
"data"
            kwd :: FilePath -> Doc OutputAnnotation
kwd = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate OutputAnnotation
AnnKeyword (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (FilePath -> Doc OutputAnnotation)
-> FilePath
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Doc OutputAnnotation
forall a. FilePath -> Doc a
text
        ppCon :: Bool -> IState -> Name -> Doc OutputAnnotation
ppCon Bool
amb IState
ist Name
n = Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
amb [] Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist Name
n)


helphead :: [([FilePath], CmdArg, FilePath)]
helphead =
  [ ([FilePath
"Command"], CmdArg
SpecialHeaderArg, FilePath
"Purpose"),
    ([FilePath
""], CmdArg
NoArg, FilePath
"")
  ]


replSettings :: Maybe FilePath -> Settings Idris
replSettings :: Maybe FilePath -> Settings Idris
replSettings Maybe FilePath
hFile = CompletionFunc Idris -> Settings Idris -> Settings Idris
forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete CompletionFunc Idris
replCompletion (Settings Idris -> Settings Idris)
-> Settings Idris -> Settings Idris
forall a b. (a -> b) -> a -> b
$ Settings Idris
forall (m :: * -> *). MonadIO m => Settings m
defaultSettings {
                       historyFile = hFile
                     }