{-| 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 orig mods efile = -- H.catch do let quiet = opt_quiet (idris_options orig) i <- lift getIState let colour = idris_colourRepl i let theme = idris_colourTheme i let mvs = idris_metavars i let prompt = if quiet then "" else showMVs colour theme mvs ++ let str = mkPrompt mods ++ ">" in (if colour && not isWindows then colourisePrompt theme str else str) ++ " " x <- H.catch (H.withInterrupt $ getInputLine prompt) (ctrlC (return $ Just "")) case x of Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye") return () Just input -> -- H.catch do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile) (ctrlC (return (Just mods))) case ms of Just mods -> let efile' = fromMaybe efile (listToMaybe mods) in repl orig mods efile' Nothing -> return () -- ctrlC) -- ctrlC where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a ctrlC act e = do lift $ iputStrLn (show e) act -- repl orig mods showMVs c thm [] = "" showMVs c thm ms = "Holes: " ++ show' 4 c thm (map fst ms) ++ "\n" show' 0 c thm ms = let l = length ms in "... ( + " ++ show l ++ " other" ++ if l == 1 then ")" else "s)" show' n c thm [m] = showM c thm m show' n c thm (m : ms) = showM c thm m ++ ", " ++ show' (n - 1) c thm ms showM c thm n = if c then colouriseFun thm (show n) else show n -- | Run the REPL server startServer :: PortNumber -> IState -> [FilePath] -> Idris () startServer port orig fn_in = do tid <- runIO $ forkIO (serverLoop port) return () where serverLoop port = withSocketsDo $ do sock <- listenOnLocalhost port loop fn orig { idris_colourRepl = False } sock fn = fromMaybe "" (listToMaybe fn_in) loop fn ist sock = do (s, _) <- accept sock h <- socketToHandle s ReadWriteMode hSetEncoding h utf8 cmd <- hGetLine h let isth = case idris_outputmode ist of RawOutput _ -> ist {idris_outputmode = RawOutput h} IdeMode n _ -> 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 orig i h fn cmd = do res <- case parseCmd i "(net)" cmd of Left err -> return (Left (Msg " invalid command")) Right (Right c) -> runExceptT $ evalStateT (processNet fn c) i Right (Left err) -> return (Left (Msg err)) case res of Right x -> return x Left err -> do hPutStrLn h (show err) return (i, fn) where processNet fn Reload = processNet fn (Load fn Nothing) processNet fn (Load f toline) = -- The $!! here prevents a space leak on reloading. -- This isn't a solution - but it's a temporary stopgap. -- See issue #2386 do putIState $!! orig { idris_options = idris_options i , idris_colourTheme = idris_colourTheme i , idris_colourRepl = False } setErrContext True setOutH h setQuiet True setVerbose 0 mods <- loadInputs [f] toline ist <- getIState return (ist, f) processNet fn c = do process fn c ist <- getIState return (ist, fn) setOutH :: Handle -> Idris () setOutH h = do ist <- getIState putIState $ case idris_outputmode ist of RawOutput _ -> ist {idris_outputmode = RawOutput h} IdeMode n _ -> ist {idris_outputmode = IdeMode n h} -- | Run a command on the server on localhost runClient :: Maybe PortNumber -> String -> IO () runClient port str = withSocketsDo $ do let port' = fromMaybe defaultPort port s <- socket AF_INET Stream defaultProtocol res <- X.try (connect s (SockAddrInet port' $ tupleToHostAddress (127,0,0,1))) case res of Right () -> do h <- socketToHandle s ReadWriteMode hSetEncoding h utf8 hPutStrLn h str resp <- hGetResp "" h putStr resp hClose h Left err -> do connectionError err exitWith (ExitFailure 1) where hGetResp acc h = do eof <- hIsEOF h if eof then return acc else do l <- hGetLine h hGetResp (acc ++ l ++ "\n") h connectionError :: X.SomeException -> IO () connectionError _ = putStrLn "Unable to connect to a running Idris repl" initIdemodeSocket :: IO Handle initIdemodeSocket = do (sock, port) <- 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 s orig mods = do h <- runIO $ if s then initIdemodeSocket else return stdout setIdeMode True h i <- getIState case idris_outputmode i of IdeMode n h -> do runIO $ hPutStrLn h $ IdeMode.convSExp "protocol-version" IdeMode.ideModeEpoch n case mods of a:_ -> runIdeModeCommand h n i "" [] (IdeMode.LoadFile a Nothing) _ -> return () idemode h orig mods idemode :: Handle -> IState -> [FilePath] -> Idris () idemode h orig mods = do idrisCatch (do let inh = if h == stdout then stdin else h len' <- runIO $ IdeMode.getLen inh len <- case len' of Left err -> ierror err Right n -> return n l <- runIO $ IdeMode.getNChar inh len "" (sexp, id) <- case IdeMode.parseMessage l of Left err -> ierror err Right (sexp, id) -> return (sexp, id) i <- getIState putIState $ i { idris_outputmode = (IdeMode id h) } idrisCatch -- to report correct id back! (do let fn = fromMaybe "" (listToMaybe mods) case IdeMode.sexpToCommand sexp of Just cmd -> runIdeModeCommand h id orig fn mods cmd Nothing -> iPrintError "did not understand" ) (\e -> do iPrintError $ show e)) (\e -> do iPrintError $ show e) idemode h orig 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 h id orig fn mods (IdeMode.Interpret cmd) = do c <- colourise i <- getIState case parseCmd i "(input)" cmd of Left err -> iPrintError . show . fixColour False . parseErrorDoc $ err Right (Right (Prove mode n')) -> idrisCatch (do process fn (Prove mode n') isetPrompt (mkPrompt mods) case idris_outputmode i of IdeMode n h -> -- signal completion of proof to ide runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n _ -> return ()) (\e -> do ist <- getIState isetPrompt (mkPrompt mods) case idris_outputmode i of IdeMode n h -> runIO . hPutStrLn h $ IdeMode.convSExp "abandon-proof" "Abandoned" n _ -> return () iRenderError $ pprintErr ist e) Right (Right cmd) -> idrisCatch (idemodeProcess fn cmd) (\e -> getIState >>= iRenderError . flip pprintErr e) Right (Left err) -> iPrintError err runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) = do (unused, compls) <- replCompletion (reverse str, "") let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)] runIO . hPutStrLn h $ IdeMode.convSExp "return" good id runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename 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 <- 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 Nothing -> let msg = maybe (IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.SexpList []]) (\fc -> IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp fc]) (idris_parsedSpan i) in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id Just x -> iPrintError $ "didn't load " ++ filename idemode h orig mods runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) = case splitName name of Left err -> iPrintError err Right n -> process "(idemode)" (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n)) runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) = case parseConst orig name of Right c -> process "(idemode)" (DocStr (Right c) (howMuch w)) Left _ -> case splitName name of Left err -> iPrintError err Right n -> process "(idemode)" (DocStr (Left n) (howMuch w)) where howMuch IdeMode.Overview = OverviewDocs howMuch IdeMode.Full = FullDocs runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) = process fn (CaseSplitAt False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) = process fn (AddClauseFrom False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.AddProofClause line name) = process fn (AddProofClauseFrom False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) = process fn (AddMissing False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) = process fn (MakeWith False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) = process fn (MakeCase False line (sUN name)) runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) = doProofSearch fn False r line (sUN name) (map sUN hints) depth runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) = case splitName name of Left err -> iPrintError err Right n -> process fn (MakeLemma False line n) runIdeModeCommand h id orig fn mods (IdeMode.Apropos a) = process fn (Apropos [] a) runIdeModeCommand h id orig fn mods (IdeMode.GetOpts) = do ist <- getIState let opts = idris_options ist let impshow = opt_showimp opts let errCtxt = opt_errContext opts let options = (IdeMode.SymbolAtom "ok", [(IdeMode.SymbolAtom "show-implicits", impshow), (IdeMode.SymbolAtom "error-context", errCtxt)]) runIO . hPutStrLn h $ IdeMode.convSExp "return" options id runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ShowImpl b) = do setImpShow b let msg = (IdeMode.SymbolAtom "ok", b) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) = do setErrContext b let msg = (IdeMode.SymbolAtom "ok", b) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) = do ist <- getIState let mvs = reverse $ [ (n, i) | (n, (_, i, _, _, _)) <- idris_metavars ist , not (n `elem` primDefs) ] -- splitMvs is a list of pairs of names and their split types let splitMvs = [ (n, (premises, concl, tm)) | (n, i, ty) <- mvTys ist mvs , let (premises, concl, tm) = splitPi ist i ty] -- mvOutput is the pretty-printed version ready for conversion to SExpr let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $ mapPair show (\(hs, c, pc) -> let bnd = [ n | (n,_,_) <- hs ] in let bnds = inits bnd in (map (\(bnd, h) -> processPremise ist bnd h) (zip bnds hs), render ist bnd c pc)) splitMvs runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) 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 ist i (Bind n (Pi _ _ t _) rest) | i > 0 = let (hs, c, _) = splitPi ist (i - 1) rest in ((n, t, delabTy' ist [] [] t False False True):hs, c, delabTy' ist [] [] c False False True) splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True) -- | Get the types of a list of metavariable names mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)] mvTys ist mvs = [ (n, i, ty) | (n, i) <- mvs , ty <- maybeToList (fmap (vToP . snd) (lookupTyNameExact n (tt_ctxt 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 ist bnd t pt = let prettyT = pprintPTerm (ppOptionIst ist) (zip bnd (repeat False)) [] (idris_infixes ist) pt in displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist True) . annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $ 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 ist bnd (n, t, pt) = let (out, spans) = render ist bnd t pt in (show n , out, spans) runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) = case splitName n of Left err -> iPrintError err Right n -> do calls <- whoCalls n ist <- getIState let msg = (IdeMode.SymbolAtom "ok", map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id where pn ist = displaySpans . renderPretty 0.9 1000 . fmap (fancifyAnnots ist True) . prettyName True True [] runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) = case splitName n of Left err -> iPrintError err Right n -> do calls <- callsWho n ist <- getIState let msg = (IdeMode.SymbolAtom "ok", map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id where pn ist = displaySpans . renderPretty 0.9 1000 . fmap (fancifyAnnots ist True) . prettyName True True [] runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) = case splitOn "." ns of [] -> iPrintError "No namespace provided" ns -> do underNSs <- fmap (map $ concat . intersperse ".") $ namespacesInNS 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 = (IdeMode.SymbolAtom "ok", (underNSs, underNs)) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id where pn n = do ctxt <- getContext ist <- getIState return $ displaySpans . renderPretty 0.9 1000 . fmap (fancifyAnnots ist True) $ prettyName True False [] n <> case lookupTyExact n ctxt of Just t -> space <> colon <> space <> align (group (pprintDelab ist t)) Nothing -> empty runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) = do ctxt <- getContext ist <- getIState let tm' = normaliseAll ctxt [] tm ptm = annotate (AnnTerm bnd tm') (pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) (delab ist tm')) msg = (IdeMode.SymbolAtom "ok", displaySpans . renderPretty 0.9 80 . fmap (fancifyAnnots ist True) $ ptm) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) = ideModeForceTermImplicits h id bnd True tm runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) = ideModeForceTermImplicits h id bnd False tm runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) = do ist <- getIState let ptm = annotate (AnnTerm bnd tm) (pprintTT (map fst bnd) tm) msg = (IdeMode.SymbolAtom "ok", displaySpans . renderPretty 0.9 70 . fmap (fancifyAnnots ist True) $ ptm) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) = case splitName name of Left err -> iPrintError err Right n -> process "(idemode)" (PrintDef n) runIdeModeCommand h id orig fn modes (IdeMode.ErrString e) = do ist <- getIState let out = displayS . renderPretty 1.0 60 $ pprintErr ist e msg = (IdeMode.SymbolAtom "ok", IdeMode.StringAtom $ out "") runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) = do ist <- getIState let (out, spans) = displaySpans . renderPretty 0.9 80 . fmap (fancifyAnnots ist True) $ pprintErr ist e msg = (IdeMode.SymbolAtom "ok", out, spans) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion = let idrisVersion = (versionBranch getIdrisVersionNoGit, if not (null gitHash) then [gitHash] else []) msg = (IdeMode.SymbolAtom "ok", idrisVersion) in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id -- | Show a term for IDEMode with the specified implicitness ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris () ideModeForceTermImplicits h id bnd impl tm = do ist <- getIState let expl = annotate (AnnTerm bnd tm) (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl }) bnd [] (idris_infixes ist) (delab ist tm)) msg = (IdeMode.SymbolAtom "ok", displaySpans . renderPretty 0.9 80 . fmap (fancifyAnnots ist True) $ expl) runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id splitName :: String -> Either String Name splitName s | "{{{{{" `isPrefixOf` s = decode $ drop 5 $ reverse $ drop 5 $ reverse s where decode x = case Base64.decode (UTF8.fromString x) of Left err -> Left err Right ok -> case Binary.decodeOrFail (Lazy.fromStrict ok) of Left _ -> Left "Bad binary instance for Name" Right (_, _, n) -> Right n splitName s = case reverse $ splitOn "." s of [] -> Left ("Didn't understand name '" ++ s ++ "'") [n] -> Right . sUN $ unparen n (n:ns) -> Right $ sNS (sUN (unparen n)) ns where unparen "" = "" unparen ('(':x:xs) | last xs == ')' = init (x:xs) unparen str = str idemodeProcess :: FilePath -> Command -> Idris () idemodeProcess fn ShowVersion = process fn ShowVersion idemodeProcess fn Warranty = process fn Warranty idemodeProcess fn Help = process fn Help idemodeProcess fn (RunShellCommand cmd) = iPrintError ":! is not currently supported in IDE mode." idemodeProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f) dir <- runIO $ getCurrentDirectory iPrintResult $ "changed directory to " ++ dir idemodeProcess fn (ModImport f) = process fn (ModImport f) idemodeProcess fn (Eval t) = process fn (Eval t) idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls) iPrintResult "defined" idemodeProcess fn (Undefine n) = process fn (Undefine n) idemodeProcess fn (ExecVal t) = process fn (ExecVal t) idemodeProcess fn (Check (PRef x hls n)) = process fn (Check (PRef x hls n)) idemodeProcess fn (Check t) = process fn (Check t) idemodeProcess fn (Core t) = process fn (Core t) idemodeProcess fn (DocStr n w) = process fn (DocStr n w) idemodeProcess fn Universes = process fn Universes idemodeProcess fn (Defn n) = do process fn (Defn n) iPrintResult "" idemodeProcess fn (TotCheck n) = process fn (TotCheck n) idemodeProcess fn (DebugInfo n) = do process fn (DebugInfo n) iPrintResult "" idemodeProcess fn (Search ps t) = process fn (Search ps t) idemodeProcess fn (Spec t) = process fn (Spec t) -- RmProof and AddProof not supported! idemodeProcess fn (ShowProof n') = process fn (ShowProof n') idemodeProcess fn (WHNF t) = process fn (WHNF t) --idemodeProcess fn TTShell = process fn TTShell -- need some prove mode! idemodeProcess fn (TestInline t) = process fn (TestInline t) idemodeProcess fn (Execute t) = do process fn (Execute t) iPrintResult "" idemodeProcess fn (Compile codegen f) = do process fn (Compile codegen f) iPrintResult "" idemodeProcess fn (LogLvl i) = do process fn (LogLvl i) iPrintResult "" idemodeProcess fn (Pattelab t) = process fn (Pattelab t) idemodeProcess fn (Missing n) = process fn (Missing n) idemodeProcess fn (DynamicLink l) = do process fn (DynamicLink l) iPrintResult "" idemodeProcess fn ListDynamic = do process fn ListDynamic iPrintResult "" idemodeProcess fn Metavars = process fn Metavars idemodeProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext) iPrintResult "" idemodeProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext) iPrintResult "" idemodeProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl) iPrintResult "" idemodeProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl) iPrintResult "" idemodeProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr) iPrintResult "" idemodeProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr) iPrintResult "" idemodeProcess fn (SetOpt x) = process fn (SetOpt x) idemodeProcess fn (UnsetOpt x) = process fn (UnsetOpt x) idemodeProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str) idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str) idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str) idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str) idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str) idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str) idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs) idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w) iPrintResult "" idemodeProcess fn (SetPrinterDepth d) = do process fn (SetPrinterDepth d) iPrintResult "" idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a) iPrintResult "" idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n) idemodeProcess fn (CallsWho n) = process fn (CallsWho n) idemodeProcess fn (PrintDef n) = process fn (PrintDef n) idemodeProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm) idemodeProcess fn _ = iPrintError "command not recognized or not supported" -- | The prompt consists of the currently loaded modules, or "Idris" if there are none mkPrompt [] = "Idris" mkPrompt [x] = "*" ++ dropExtension x mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs -- | Determine whether a file uses literate syntax lit f = case splitExtension f of (_, ".lidr") -> True _ -> False reload :: IState -> [FilePath] -> Idris (Maybe [FilePath]) reload orig inputs = do i <- 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 orig inputs = do resp <- runIO $ do let dirs = nub $ map takeDirectory inputs inputSet <- fmap S.fromList $ mapM canonicalizePath inputs signal <- newEmptyMVar withManager $ \mgr -> do forM_ dirs $ \dir -> watchDir mgr dir (allEvents $ flip S.member inputSet) (doAllEvents $ putMVar signal) race getLine (takeMVar signal) case resp of Left _ -> return (Just inputs) -- canceled, so nop Right _ -> reload orig inputs >> watch orig inputs processInput :: String -> IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath]) processInput cmd orig inputs efile = do i <- getIState let opts = idris_options i let quiet = opt_quiet opts let fn = fromMaybe "" (listToMaybe inputs) case parseCmd i "(input)" cmd of Left err -> Just inputs <$ emitWarning err Right (Right Reload) -> reload orig inputs Right (Right Watch) -> if null inputs then do iputStrLn "No loaded files to watch." return (Just inputs) else do iputStrLn efile iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel." watch orig inputs Right (Right (Load f toline)) -> -- The $!! here prevents a space leak on reloading. -- This isn't a solution - but it's a temporary stopgap. -- See issue #2386 do putIState $!! orig { idris_options = idris_options i , idris_colourTheme = idris_colourTheme i } clearErr mod <- loadInputs [f] toline return (Just mod) Right (Right (ModImport f)) -> do clearErr fmod <- loadModule f (IBC_REPL True) return (Just (inputs ++ maybe [] (:[]) fmod)) Right (Right Edit) -> do -- takeMVar stvar edit efile orig return (Just inputs) Right (Right Proofs) -> Just inputs <$ proofs orig Right (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye") Right (Right cmd ) -> do idrisCatch (process fn cmd) (\e -> do msg <- showErr e ; iputStrLn msg) return (Just inputs) Right (Left err) -> do runIO $ putStrLn err return (Just inputs) resolveProof :: Name -> Idris Name resolveProof n' = do i <- getIState ctxt <- getContext n <- case lookupNames n' ctxt of [x] -> return x [] -> return n' ns -> ierror (CantResolveAlts ns) return n removeProof :: Name -> Idris () removeProof n = do i <- getIState let proofs = proof_list i let ps = filter ((/= n) . fst) proofs putIState $ i { proof_list = ps } edit :: FilePath -> IState -> Idris () edit "" orig = iputStrLn "Nothing to edit" edit f orig = do i <- getIState env <- runIO getEnvironment let editor = getEditor env let line = case errSpan i of Just l -> '+' : show (fst (fc_start l)) Nothing -> "" let cmdLine = intercalate " " [editor, line, fixName 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 env | Just ed <- lookup "EDITOR" env = ed | Just ed <- lookup "VISUAL" env = ed | otherwise = "vi" fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = quote file | otherwise = quote $ addExtension file "idr" where quoteChar = if isWindows then '"' else '\'' quote s = [quoteChar] ++ s ++ [quoteChar] proofs :: IState -> Idris () proofs orig = do i <- getIState let ps = proof_list i case ps of [] -> iputStrLn "No proofs available" _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps) insertScript :: String -> [String] -> [String] insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf] insertScript prf (p@"---------- Proofs ----------" : "" : xs) = p : "" : prf : xs insertScript prf (x : xs) = x : insertScript prf xs process :: FilePath -> Command -> Idris () process fn Help = iPrintResult displayHelp process fn ShowVersion = iPrintResult getIdrisVersion process fn Warranty = iPrintResult warranty process fn (RunShellCommand cmd) = runIO $ system cmd >> return () process fn (ChangeDirectory f) = do runIO $ setCurrentDirectory f return () process fn (ModImport f) = do fmod <- loadModule f (IBC_REPL True) case fmod of Just pr -> isetPrompt pr Nothing -> iPrintError $ "Can't find import " ++ f process fn (Eval t) = withErrorReflection $ do logParser 5 $ show t getIState >>= flip warnDisamb t (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t ctxt <- getContext let tm' = perhapsForce $ normaliseBlocking ctxt [] [sUN "foreign", sUN "prim_read", sUN "prim_write"] tm let ty' = perhapsForce $ normaliseAll ctxt [] 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 = pprintDelab ist tm' -- errReverse to make type more readable tyDoc = pprintDelab ist (errReverse ist ty') iPrintTermWithType tmDoc tyDoc where perhapsForce tm | termSmallerThan 100 tm = force tm | otherwise = tm process fn (NewDefn decls) = do logParser 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls)) mapM_ defineName namedGroups where namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls getName :: PDecl -> Maybe Name getName (PTy docs argdocs syn fc opts name _ ty) = Just name getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause) getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl) getName (PInterface doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name getName _ = Nothing -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes getClauseName (PClause fc name whole with rhs whereBlock) = name getClauseName (PWith fc name whole with rhs pn whereBlock) = name defineName :: [PDecl] -> Idris () defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do elabDecl EAll info tyDecl elabClauses info fc opts name (concatMap getClauses decls) setReplDefined (Just name) defineName [PClauses fc opts _ [clause]] = do let pterm = getRHS clause (tm,ty) <- elabVal info ERHS pterm ctxt <- getContext let tm' = force (normaliseAll ctxt [] tm) let ty' = force (normaliseAll ctxt [] ty) updateContext (addCtxtDef (getClauseName clause) (Function ty' tm')) setReplDefined (Just $ getClauseName clause) defineName (PClauses{} : _) = tclift $ tfail (Msg "Only one function body is allowed without a type declaration.") -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way defineName (PFix fc fixity strs : defns) = do fmodifyState idris_fixities (map (Fix fixity) strs ++) unless (null defns) $ defineName defns defineName (PSyntax _ syntax:_) = do i <- get put (addReplSyntax i syntax) defineName decls = do elabDecls (toplevelWith fn) (map fixClauses decls) setReplDefined (getName (head decls)) getClauses (PClauses fc opts name clauses) = clauses getClauses _ = [] getRHS :: PClause -> PTerm getRHS (PClause fc name whole with rhs whereBlock) = rhs getRHS (PWith fc name whole with rhs pn whereBlock) = rhs getRHS (PClauseR fc with rhs whereBlock) = rhs getRHS (PWithR fc with rhs pn whereBlock) = rhs setReplDefined :: Maybe Name -> Idris () setReplDefined Nothing = return () setReplDefined (Just n) = do oldState <- 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 (PClauses fc opts _ css@(clause:cs)) = PClauses fc opts (getClauseName clause) css fixClauses (PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName decls) = PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName (map fixClauses decls) fixClauses decl = decl info = recinfo (fileFC "toplevel") process fn (Undefine names) = undefine names where undefine :: [Name] -> Idris () undefine [] = do allDefined <- idris_repl_defs `fmap` get undefine' allDefined [] -- Keep track of which names you've removed so you can -- print them out to the user afterward undefine names = undefine' names [] undefine' [] list = do iRenderResult $ printUndefinedNames list return () undefine' (n:names) already = do allDefined <- idris_repl_defs `fmap` 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 n = do fputState (ctxt_lookup n . known_terms) 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. fputState (ctxt_lookup n . known_interfaces) Nothing fmodifyState repl_definitions (delete n) undefClosure n = do replDefs <- idris_repl_defs `fmap` get callGraph <- whoCalls n let users = case lookup n callGraph of Just ns -> nub ns Nothing -> fail ("Tried to undefine nonexistent name" ++ show n) undefinedJustNow <- concat `fmap` mapM undefClosure users undefOne n return (nub (n : undefinedJustNow)) process fn (ExecVal t) = do ctxt <- getContext ist <- getIState (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t -- let tm' = normaliseAll ctxt [] tm let ty' = normaliseAll ctxt [] ty res <- execute tm let (resOut, tyOut) = (prettyIst ist (delab ist res), prettyIst ist (delab ist ty')) iPrintTermWithType resOut tyOut process fn (Check (PRef _ _ n)) = do ctxt <- getContext ist <- getIState let ppo = ppOptionIst ist case lookupVisibleNames n ctxt of ts@(t:_) -> case lookup t (idris_metavars ist) of Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $ showMetavarInfo ppo ist n i Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts) [] -> iPrintError $ "No such variable " ++ show n where lookupVisibleNames :: Name -> Context -> [Name] lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt) showMetavarInfo ppo ist n i = case lookupTy n (tt_ctxt ist) of (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in putTy ppo ist i [] (delab ist (errReverse ist ty')) putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc putTy ppo ist i bnd (PPi p n _ t sc) = let current = case n of MN _ _ -> text "" UN nm | ('_':'_':_) <- str nm -> text "" _ -> countOf (pcount p) (LinearTypes `elem` idris_language_extensions ist) <+> bindingOf n False <+> colon <+> align (tPretty bnd ist t) <> line in current <> putTy ppo ist (i-1) ((n,False):bnd) sc putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc putGoal ppo ist bnd g = text "--------------------------------------" <$> annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+> align (tPretty bnd ist g) -- Only display count if linear types extension is enabled countOf Rig0 True = text "0" countOf Rig1 True = text "1" countOf _ _ = text " " tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t process fn (Check t) = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t ctxt <- getContext ist <- getIState let ty' = if opt_evaltypes (idris_options ist) then normaliseC ctxt [] ty else ty case tm of TType _ -> iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc _ -> iPrintTermWithType (pprintDelab ist tm) (pprintDelab ist ty') process fn (Core t) = case t of PRef _ _ n -> do ist <- getIState case lookupDef n (tt_ctxt ist) of [CaseOp _ _ _ _ _ _] -> pprintDef True n >>= iRenderResult . vsep _ -> coreTerm t t -> coreTerm t where coreTerm t = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty) process fn (DocStr (Left n) w) | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc | otherwise = do ist <- getIState let docs = lookupCtxtName n (idris_docstrings ist) ++ map (\(n,d)-> (n, (d, []))) (lookupCtxtName (modDocN n) (idris_moduledocs ist)) case docs of [] -> iPrintError $ "No documentation for " ++ show n ns -> do toShow <- mapM (showDoc ist) ns iRenderResult (vsep toShow) where showDoc ist (n, d) = do doc <- getDocs n w return $ pprintDocs ist doc modDocN (NS (UN n) ns) = NS modDocName (n:ns) modDocN (UN n) = NS modDocName [n] modDocN _ = sMN 1 "NotFoundForSure" process fn (DocStr (Right c) _) -- constants only have overviews = do ist <- getIState iRenderResult $ pprintConstDocs ist c (constDocs c) process fn Universes = do i <- getIState let cs = idris_constraints i let cslist = S.toAscList cs -- iputStrLn $ showSep "\n" (map show cs) iputStrLn $ showSep "\n" (map show cslist) let n = length cslist iputStrLn $ "(" ++ show n ++ " constraints)" case ucheck cs of Error e -> iPrintError $ pshow i e OK _ -> iPrintResult "Universes OK" process fn (Defn n) = do i <- getIState let head = text "Compiled patterns:" <$> text (show (lookupDef n (tt_ctxt i))) let defs = case lookupCtxt n (idris_patdefs i) of [] -> empty [(d, _)] -> text "Original definiton:" <$> vsep (map (printCase i) d) let tot = case lookupTotal n (tt_ctxt i) of [t] -> showTotal t i _ -> empty iRenderResult $ vsep [head, defs, tot] where printCase i (_, lhs, rhs) = let i' = i { idris_options = (idris_options i) { opt_showimp = True } } in text (showTm i' (delab i lhs)) <+> text "=" <+> text (showTm i' (delab i rhs)) process fn (TotCheck n) = do i <- getIState case lookupNameTotal n (tt_ctxt i) of [] -> iPrintError $ "Unknown operator " ++ show n ts -> do ist <- getIState c <- colourise let ppo = ppOptionIst ist let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $ showName (Just ist) [] ppo False n iRenderResult . vsep . map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $ ts process fn (DebugUnify l r) = do (ltm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS l (rtm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS r ctxt <- getContext case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of OK ans -> iputStrLn (show ans) Error e -> iputStrLn (show e) process fn (DebugInfo n) = do i <- getIState let oi = lookupCtxtName n (idris_optimisation i) when (not (null oi)) $ iputStrLn (show oi) let si = lookupCtxt n (idris_statics i) when (not (null si)) $ iputStrLn (show si) let di = lookupCtxt n (idris_datatypes i) when (not (null di)) $ iputStrLn (show di) let imps = lookupCtxt n (idris_implicits i) when (not (null imps)) $ iputStrLn (show imps) let d = lookupDefAcc n False (tt_ctxt i) when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d)) i <- getIState let cg' = lookupCtxtName n (idris_callgraph i) sc <- checkSizeChange n iputStrLn $ "Size change: " ++ show sc let fn = lookupCtxtName n (idris_fninfo i) when (not (null cg')) $ do iputStrLn "Call graph:\n" iputStrLn (show cg') when (not (null fn)) $ iputStrLn (show fn) process fn (Search pkgs t) = searchByType pkgs t process fn (CaseSplitAt updatefile l n) = caseSplitAt fn updatefile l n process fn (AddClauseFrom updatefile l n) = addClauseFrom fn updatefile l n process fn (AddProofClauseFrom updatefile l n) = addProofClauseFrom fn updatefile l n process fn (AddMissing updatefile l n) = addMissing fn updatefile l n process fn (MakeWith updatefile l n) = makeWith fn updatefile l n process fn (MakeCase updatefile l n) = makeCase fn updatefile l n process fn (MakeLemma updatefile l n) = makeLemma fn updatefile l n process fn (DoProofSearch updatefile rec l n hints) = doProofSearch fn updatefile rec l n hints Nothing process fn (Spec t) = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t ctxt <- getContext ist <- getIState let tm' = simplify ctxt [] {- (idris_statics ist) -} tm iPrintResult (show (delab ist tm')) process fn (RmProof n') = do i <- getIState n <- resolveProof n' let proofs = proof_list i case lookup n proofs of Nothing -> iputStrLn "No proof to remove" Just _ -> do removeProof n insertMetavar n iputStrLn $ "Removed proof " ++ show n where insertMetavar :: Name -> Idris () insertMetavar n = do i <- getIState let ms = idris_metavars i putIState $ i { idris_metavars = (n, (Nothing, 0, [], False, False)) : ms } process fn' (AddProof prf) = do fn <- do let fn'' = takeWhile (/= ' ') fn' ex <- runIO $ doesFileExist fn'' let fnExt = fn'' <.> "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 = fn ++ "~" runIO $ copyFile fn fb -- make a backup in case something goes wrong! prog <- runIO $ readSource fb i <- getIState let proofs = proof_list i n' <- case prf of Nothing -> case proofs of [] -> ifail "No proof to add" ((x, _) : _) -> return x Just nm -> return nm n <- resolveProof n' case lookup n proofs of Nothing -> iputStrLn "No proof to add" Just (mode, prf) -> do let script = if mode then showRunElab (lit fn) n prf else showProof (lit fn) n prf let prog' = insertScript script ls runIO $ writeSource fn (unlines prog') removeProof n iputStrLn $ "Added proof " ++ show n where ls = (lines prog) process fn (ShowProof n') = do i <- getIState n <- resolveProof n' let proofs = proof_list i case lookup n proofs of Nothing -> iPrintError "No proof to show" Just (m, p) -> iPrintResult $ if m then showRunElab False n p else showProof False n p process fn (Prove mode n') = do ctxt <- getContext ist <- getIState let ns = lookupNames n' ctxt let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns n <- case metavars of [] -> ierror (Msg $ "Cannot find metavariable " ++ show n') [(n, (_,_,_,False,_))] -> return n [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes") [(_, (_,_,_,True,_))] -> ierror (Msg "Declarations not solvable using prover") ns -> ierror (CantResolveAlts (map fst ns)) prover (toplevelWith fn) mode (lit fn) n -- recheck totality i <- getIState totcheck (fileFC "(input)", n) mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i) mapM_ checkDeclTotality (idris_totcheck i) warnTotality process fn (WHNF t) = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t ctxt <- getContext ist <- getIState let tm' = whnf ctxt [] tm let tmArgs' = whnfArgs ctxt [] tm iPrintResult $ "WHNF: " ++ (show (delab ist tm')) iPrintResult $ "WHNF args: " ++ (show (delab ist tmArgs')) process fn (TestInline t) = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t ctxt <- getContext ist <- getIState let tm' = inlineTerm ist tm c <- colourise iPrintResult (showTm ist (delab ist tm')) process fn (Execute tm) = idrisCatch (do ist <- 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 h -> do res <- runIO $ rawSystem progName [] case res of ExitSuccess -> return () ExitFailure err -> ifail $ "Compiled program " ++ if err < 0 then "was killed by signal " ++ show (0 - err) else "terminated with exit code " ++ show err IdeMode n h -> runIO . hPutStrLn h $ IdeMode.convSExp "run-program" tmpn n) (\e -> getIState >>= iRenderError . flip pprintErr e) where fc = fileFC "main" process fn (Compile codegen f) | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] = iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\"" | otherwise = do opts <- getCmdLine let iface = Interface `elem` opts let mainname = sNS (sUN "main") ["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' = ir {interfaces = iface} runIO $ generate codegen (fst (head (idris_imported i))) ir' where fc = fileFC "main" process fn (LogLvl i) = setLogLevel i process fn (LogCategory cs) = setLogCats cs -- Elaborate as if LHS of a pattern (debug command) process fn (Pattelab t) = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ELHS t iPrintResult $ show tm ++ "\n\n : " ++ show ty process fn (Missing n) = do i <- getIState ppOpts <- fmap ppOptionIst getIState case lookupCtxt n (idris_patdefs i) of [] -> iPrintError $ "Unknown name " ++ show n [(_, tms)] -> iRenderResult (vsep (map (pprintPTerm ppOpts [] [] (idris_infixes i)) tms)) _ -> iPrintError "Ambiguous name" process fn (DynamicLink l) = do i <- getIState let importdirs = opt_importdirs (idris_options i) lib = trim l handle <- lift . lift $ tryLoadLib importdirs lib case handle of Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\"" Just x -> do let libs = idris_dynamic_libs i if x `elem` libs then do logParser 1 ("Tried to load duplicate library " ++ lib_name x) return () else putIState $ i { idris_dynamic_libs = x:libs } where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace process fn ListDynamic = do i <- getIState iputStrLn "Dynamic libraries:" showLibs $ idris_dynamic_libs i where showLibs [] = return () showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls process fn Metavars = do ist <- getIState let mvs = map fst (idris_metavars ist) \\ primDefs case mvs of [] -> iPrintError "No global holes to solve" _ -> iPrintResult $ "Global holes:\n\t" ++ show mvs process fn NOP = return () process fn (SetOpt ErrContext) = setErrContext True process fn (UnsetOpt ErrContext) = setErrContext False process fn (SetOpt ShowImpl) = setImpShow True process fn (UnsetOpt ShowImpl) = setImpShow False process fn (SetOpt ShowOrigErr) = setShowOrigErr True process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False process fn (SetOpt AutoSolve) = setAutoSolve True process fn (UnsetOpt AutoSolve) = setAutoSolve False process fn (SetOpt NoBanner) = setNoBanner True process fn (UnsetOpt NoBanner) = setNoBanner False process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:) process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach process fn (SetOpt EvalTypes) = setEvalTypes True process fn (UnsetOpt EvalTypes) = setEvalTypes False process fn (SetOpt DesugarNats) = setDesugarNats True process fn (UnsetOpt DesugarNats) = setDesugarNats False process fn (SetOpt _) = iPrintError "Not a valid option" process fn (UnsetOpt _) = iPrintError "Not a valid option" process fn (SetColour ty c) = setColour ty c process fn ColourOn = do ist <- getIState putIState $ ist { idris_colourRepl = True } process fn ColourOff = do ist <- getIState putIState $ ist { idris_colourRepl = False } process fn ListErrorHandlers = do ist <- getIState iPrintResult $ case idris_errorhandlers ist of [] -> "No registered error handlers" handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers process fn (SetConsoleWidth w) = setWidth w process fn (SetPrinterDepth d) = setDepth d process fn (Apropos pkgs a) = do orig <- getIState when (not (null pkgs)) $ iputStrLn $ "Searching packages: " ++ showSep ", " (map show pkgs) mapM_ loadPkgIndex pkgs ist <- getIState let mods = aproposModules ist (T.pack a) let names = apropos ist (T.pack a) let aproposInfo = [ (n, delabTy ist n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist))) | n <- sort names, isUN n ] if (not (null mods)) || (not (null aproposInfo)) then iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$> ppD ist d <> line) mods) <$> vsep (map (prettyDocumentedIst ist) aproposInfo) else iRenderError $ text "No results found" where isUN (UN _) = True isUN (NS n _) = isUN n isUN _ = False ppD ist = renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) process fn (WhoCalls n) = do calls <- whoCalls n ist <- getIState iRenderResult . vsep $ map (\(n, ns) -> text "Callers of" <+> prettyName True True [] n <$> indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns))) calls process fn (CallsWho n) = do calls <- callsWho n ist <- getIState iRenderResult . vsep $ map (\(n, ns) -> prettyName True True [] n <+> text "calls:" <$> indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns))) calls process fn (Browse ns) = do underNSs <- namespacesInNS 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 (\n -> prettyName True False [] n <+> colon <+> (group . align $ pprintDelabTy ist n)) names)) -- IdrisDoc process fn (MakeDoc s) = do istate <- getIState let names = words s parse n | Right x <- runparser name istate fn n = Right x parse n = Left n (bad, nss) = partitionEithers $ map parse names cd <- runIO getCurrentDirectory let outputDir = cd "doc" result <- if null bad then runIO $ generateDocs istate nss outputDir else return . Left $ "Illegal name: " ++ head bad case result of Right _ -> iputStrLn "IdrisDoc generated" Left err -> iPrintError err process fn (PrintDef n) = do result <- pprintDef False n case result of [] -> iPrintError "Not found" outs -> iRenderResult . vsep $ outs -- Show relevant transformation rules for the name 'n' process fn (TransformInfo n) = do i <- getIState let ts = lookupCtxt n (idris_transforms i) let res = map (showTrans i) ts iRenderResult . vsep $ concat res where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation] showTrans i [] = [] showTrans i ((lhs, rhs) : ts) = let ppTm tm = annotate (AnnTerm [] tm) . pprintPTerm (ppOptionIst i) [] [] [] . delab i $ tm ts' = showTrans i ts in ppTm lhs <+> text " ==> " <+> ppTm rhs : ts' process fn (PPrint fmt width (PRef _ _ n)) = do outs <- pprintDef False n iPrintResult =<< renderExternal fmt width (vsep outs) process fn (PPrint fmt width t) = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t ist <- getIState iPrintResult =<< renderExternal fmt width (pprintDelab ist tm) process fn Quit = iPrintError "Command ':quit' is currently unsupported" process fn Reload = iPrintError "Command ':reload' is currently unsupported" process fn Watch = iPrintError "Command ':watch' is currently unsupported" process fn (Load _ _) = iPrintError "Command ':load' is currently unsupported" process fn Edit = iPrintError "Command ':edit' is currently unsupported" process fn Proofs = iPrintError "Command ':proofs' is currently unsupported" process fn (Verbosity _) = iPrintError "Command ':verbosity' is currently unsupported" showTotal :: Totality -> IState -> Doc OutputAnnotation showTotal t@(Partial (Other ns)) i = text "possibly not total due to:" <$> vsep (map (showTotalN i) ns) showTotal t@(Partial (Mutual ns)) i = text "possibly not total due to recursive path:" <$> align (group (vsep (punctuate comma (map (\n -> annotate (AnnName n Nothing Nothing Nothing) $ text (show n)) ns)))) showTotal t i = text (show t) showTotalN :: IState -> Name -> Doc OutputAnnotation showTotalN ist n = case lookupTotal n (tt_ctxt ist) of [t] -> showN n <> text ", which is" <+> showTotal t ist _ -> empty where ppo = ppOptionIst ist showN n = annotate (AnnName n Nothing Nothing Nothing) . text $ showName (Just ist) [] ppo False n displayHelp = let vstr = showVersion getIdrisVersionNoGit in "\nIdris version " ++ vstr ++ "\n" ++ "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++ concatMap cmdInfo helphead ++ concatMap cmdInfo help where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text col c1 c2 l m r = l ++ take (c1 - length l) (repeat ' ') ++ m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n" pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation] pprintDef asCore n = do ist <- getIState ctxt <- getContext let ambiguous = length (lookupNames n ctxt) > 1 patdefs = idris_patdefs ist tyinfo = idris_datatypes 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 ist (n, (clauses, missing)) = case lookupTy n (tt_ctxt ist) of [] -> error "Attempted pprintDef of TT of thing that doesn't exist" (ty:_) -> prettyName True True [] n <+> colon <+> align (annotate (AnnTerm [] ty) (pprintTT [] ty)) <$> vsep (map (\(vars, lhs, rhs) -> pprintTTClause vars lhs rhs) clauses) ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation ppDef amb ist (n, (clauses, missing)) = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n) <$> ppClauses ist clauses <> ppMissing missing ppClauses ist [] = text "No clauses." ppClauses ist cs = vsep (map pp cs) where pp (varTys, lhs, rhs) = let vars = map fst varTys ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) . pprintPTerm (ppOptionIst ist) (zip vars (repeat False)) [] (idris_infixes ist) . delabWithEnv ist varTys $ t in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs) ppMissing _ = empty ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation ppTy amb ist (n, TI constructors isCodata _ _ _ _) = kwd key <+> prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n) <+> kwd "where" <$> indent 2 (vsep (map (ppCon False ist) constructors)) where key | isCodata = "codata" | otherwise = "data" kwd = annotate AnnKeyword . text ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n) helphead = [ (["Command"], SpecialHeaderArg, "Purpose"), ([""], NoArg, "") ] replSettings :: Maybe FilePath -> Settings Idris replSettings hFile = setComplete replCompletion $ defaultSettings { historyFile = hFile }