@@ -1,59 +1,53 @@
11{-|
22Module : Idris.REPL
33Description : Entry Point for the Idris REPL and CLI.
4−Copyright :
54License : BSD3
65Maintainer : The Idris Community.
76-}
87{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
98 PatternGuards, CPP #-}
10−
11−module Idris.REPL(
12− idris, idrisMain, loadInputs
13− , runClient, runMain
9+module Idris.REPL
10+ ( idemodeStart
11+ , startServer
12+ , runClient
13+ , process
14+ , replSettings
15+ , repl
16+ , proofs
1417 ) where
1518
1619import Idris.AbsSyntax
1720import Idris.ASTUtils
1821import Idris.Apropos (apropos, aproposModules)
1922import Idris.REPL.Parser
20−import Idris.Erasure
2123import Idris.Error
2224import Idris.IBC
2325import Idris.ErrReverse
2426import Idris.Delaborate
25−import Idris.Docstrings (Docstring, overview, renderDocstring, renderDocTerm)
27+import Idris.Docstrings (overview, renderDocstring, renderDocTerm)
2628import Idris.Help
2729import Idris.IdrisDoc
2830import Idris.Prover
2931import Idris.Parser hiding (indent)
30−import Idris.Primitives
3132import Idris.Coverage
3233import Idris.Docs hiding (Doc)
3334import Idris.Completion
3435import qualified Idris.IdeMode as IdeMode
35−import Idris.Chaser
36−import Idris.Imports
3736import Idris.Colours hiding (colourise)
3837import Idris.Inliner
39−import Idris.CaseSplit
40−import Idris.DeepSeq
4138import Idris.Output
4239import Idris.Interactive
4340import Idris.WhoCalls
4441import Idris.TypeSearch (searchByType)
45−import Idris.IBC (loadPkgIndex, writePkgIndex)
4642
4743import Idris.REPL.Browse (namesInNS, namespacesInNS)
4844import Idris.REPL.Commands
4945
5046import Idris.ElabDecls
51−import Idris.Elab.Type
5247import Idris.Elab.Clause
53−import Idris.Elab.Data
5448import Idris.Elab.Value
5549import Idris.Elab.Term
56−
50+import Idris.ModeCommon
5751import Idris.Info
5852
5953import Version_idris (gitHash)
@@ -70,14 +64,11 @@ import Idris.Core.WHNF
7064import Idris.Core.Constraints
7165
7266import IRTS.Compiler
73−import IRTS.CodegenCommon
74−import IRTS.Exports
7567
7668import Control.Category
7769import qualified Control.Exception as X
7870import Prelude hiding ((<$>), (.), id)
7971import Data.List.Split (splitOn)
80−import Data.List (groupBy)
8172import qualified Data.Text as T
8273
8374import Text.Trifecta.Result(Result(..), ErrInfo(..))
@@ -101,7 +92,6 @@ import Data.List hiding (group)
10192import Data.Char
10293import qualified Data.Set as S
10394import Data.Version
104−import Data.Word (Word)
10595import Data.Either (partitionEithers)
10696import Control.DeepSeq
10797
@@ -109,9 +99,7 @@ import Control.Concurrent.Async (race)
10999import System.FSNotify (withManager, watchDir)
110100import System.FSNotify.Devel (allEvents, doAllEvents)
111101
112−import Numeric ( readHex )
113102
114−import Debug.Trace
115103
116104-- | Run the REPL
117105repl :: IState -- ^ The initial state
@@ -1553,388 +1541,3 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
15531541 historyFile = hFile
15541542 }
15551543
1556−-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1557−idris :: [Opt] -> IO (Maybe IState)
1558−idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
1559− case res of
1560− Left err -> do putStrLn $ pshow idrisInit err
1561− return Nothing
1562− Right ist -> return (Just ist)
1563− where totalMain = do idrisMain opts
1564− ist <- getIState
1565− case idris_totcheckfail ist of
1566− ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1567− [] -> return ()
1568−
1569−
1570−loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
1571−loadInputs inputs toline -- furthest line to read in input source files
1572− = idrisCatch
1573− (do ist <- getIState
1574− -- if we're in --check and not outputting anything, don't bother
1575− -- loading, as it gets really slow if there's lots of modules in
1576− -- a package (instead, reload all at the end to check for
1577− -- consistency only)
1578− opts <- getCmdLine
1579−
1580− let loadCode = case opt getOutput opts of
1581− [] -> not (NoREPL `elem` opts)
1582− _ -> True
1583−
1584− -- For each ifile list, check it and build ibcs in the same clean IState
1585− -- so that they don't interfere with each other when checking
1586−
1587− importlists <- getImports [] inputs
1588−
1589− logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))
1590−
1591− let ninputs = zip [1..] inputs
1592− ifiles <- mapWhileOK (\(num, input) ->
1593− do putIState ist
1594− modTree <- buildTree
1595− (map snd (take (num-1) ninputs))
1596− importlists
1597− input
1598− let ifiles = getModuleFiles modTree
1599− logParser 1 ("MODULE TREE : " ++ show modTree)
1600− logParser 1 ("RELOAD: " ++ show ifiles)
1601− when (not (all ibc ifiles) || loadCode) $
1602− tryLoad False IBC_Building (filter (not . ibc) ifiles)
1603− -- return the files that need rechecking
1604− return (input, ifiles))
1605− ninputs
1606− inew <- getIState
1607− let tidata = idris_tyinfodata inew
1608− -- If it worked, load the whole thing from all the ibcs together
1609− case errSpan inew of
1610− Nothing ->
1611− do putIState $!! ist { idris_tyinfodata = tidata }
1612− ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))
1613−-- logLvl 0 $ "Loading from " ++ show ibcfiles
1614− tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)
1615− _ -> return ()
1616− exports <- findExports
1617−
1618− case opt getOutput opts of
1619− [] -> performUsageAnalysis (getExpNames exports) -- interactive
1620− _ -> return [] -- batch, will be checked by the compiler
1621−
1622− return (map fst ifiles))
1623− (\e -> do i <- getIState
1624− case e of
1625− At f e' -> do setErrSpan f
1626− iWarn f $ pprintErr i e'
1627− ProgramLineComment -> return () -- fail elsewhere
1628− _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1629− -- Issue #1576 on the issue tracker.
1630− -- https://github.com/idris-lang/Idris-dev/issues/1576
1631− iWarn emptyFC $ pprintErr i e
1632− return [])
1633− where -- load all files, stop if any fail
1634− tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
1635− tryLoad keepstate phase [] = warnTotality >> return ()
1636− tryLoad keepstate phase (f : fs)
1637− = do ist <- getIState
1638− let maxline
1639− = case toline of
1640− Nothing -> Nothing
1641− Just l -> case f of
1642− IDR fn -> if any (fmatch fn) inputs
1643− then Just l
1644− else Nothing
1645− LIDR fn -> if any (fmatch fn) inputs
1646− then Just l
1647− else Nothing
1648− _ -> Nothing
1649− loadFromIFile True phase f maxline
1650− inew <- getIState
1651− -- FIXME: Save these in IBC to avoid this hack! Need to
1652− -- preserve it all from source inputs
1653− --
1654− -- Issue #1577 on the issue tracker.
1655− -- https://github.com/idris-lang/Idris-dev/issues/1577
1656− let tidata = idris_tyinfodata inew
1657− let patdefs = idris_patdefs inew
1658− ok <- noErrors
1659− if ok then
1660− -- The $!! here prevents a space leak on reloading.
1661− -- This isn't a solution - but it's a temporary stopgap.
1662− -- See issue #2386
1663− do when (not keepstate) $ putIState $!! ist
1664− ist <- getIState
1665− putIState $!! ist { idris_tyinfodata = tidata,
1666− idris_patdefs = patdefs }
1667− tryLoad keepstate phase fs
1668− else warnTotality
1669−
1670− ibc (IBC _ _) = True
1671− ibc _ = False
1672−
1673− fmatch ('.':'/':xs) ys = fmatch xs ys
1674− fmatch xs ('.':'/':ys) = fmatch xs ys
1675− fmatch xs ys = xs == ys
1676−
1677− findNewIBC :: IFileType -> Idris (Maybe IFileType)
1678− findNewIBC i@(IBC _ _) = return (Just i)
1679− findNewIBC s@(IDR f) = do ist <- get
1680− ibcsd <- valIBCSubDir ist
1681− let ibc = ibcPathNoFallback ibcsd f
1682− ok <- runIO $ doesFileExist ibc
1683− if ok then return (Just (IBC ibc s))
1684− else return Nothing
1685− findNewIBC s@(LIDR f) = do ist <- get
1686− ibcsd <- valIBCSubDir ist
1687− let ibc = ibcPathNoFallback ibcsd f
1688− ok <- runIO $ doesFileExist ibc
1689− if ok then return (Just (IBC ibc s))
1690− else return Nothing
1691−
1692− -- Like mapM, but give up when there's an error
1693− mapWhileOK f [] = return []
1694− mapWhileOK f (x : xs) = do x' <- f x
1695− ok <- noErrors
1696− if ok then do xs' <- mapWhileOK f xs
1697− return (x' : xs')
1698− else return [x']
1699−
1700−idrisMain :: [Opt] -> Idris ()
1701−idrisMain opts =
1702− do mapM_ setWidth (opt getConsoleWidth opts)
1703− let inputs = opt getFile opts
1704− let quiet = Quiet `elem` opts
1705− let nobanner = NoBanner `elem` opts
1706− let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts
1707− let runrepl = not (NoREPL `elem` opts)
1708− let verbose = runrepl || Verbose `elem` opts
1709− let output = opt getOutput opts
1710− let ibcsubdir = opt getIBCSubDir opts
1711− let importdirs = opt getImportDir opts
1712− let sourcedirs = opt getSourceDir opts
1713− let bcs = opt getBC opts
1714− let pkgdirs = opt getPkgDir opts
1715− -- Set default optimisations
1716− let optimise = case opt getOptLevel opts of
1717− [] -> 2
1718− xs -> last xs
1719−
1720− setOptLevel optimise
1721− let outty = case opt getOutputTy opts of
1722− [] -> if Interface `elem` opts then
1723− Object else Executable
1724− xs -> last xs
1725− let cgn = case opt getCodegen opts of
1726− [] -> Via IBCFormat "c"
1727− xs -> last xs
1728− let cgFlags = opt getCodegenArgs opts
1729−
1730− -- Now set/unset specifically chosen optimisations
1731− let os = opt getOptimisation opts
1732−
1733− mapM_ processOptimisation os
1734−
1735− script <- case opt getExecScript opts of
1736− [] -> return Nothing
1737− x:y:xs -> do iputStrLn "More than one interpreter expression found."
1738− runIO $ exitWith (ExitFailure 1)
1739− [expr] -> return (Just expr)
1740− let immediate = opt getEvalExpr opts
1741− let port = case getPort opts of
1742− Nothing -> defaultPort
1743− Just p -> p
1744−
1745− when (DefaultTotal `elem` opts) $ do i <- getIState
1746− putIState (i { default_total = DefaultCheckingTotal })
1747− tty <- runIO isATTY
1748− setColourise $ not quiet && last (tty : opt getColour opts)
1749−
1750−
1751−
1752− mapM_ addLangExt (opt getLanguageExt opts)
1753− setREPL runrepl
1754− setQuiet (quiet || isJust script || not (null immediate))
1755− setVerbose verbose
1756− setCmdLine opts
1757− setOutputTy outty
1758− setNoBanner nobanner
1759− setCodegen cgn
1760− mapM_ (addFlag cgn) cgFlags
1761− mapM_ makeOption opts
1762− -- if we have the --bytecode flag, drop into the bytecode assembler
1763− case bcs of
1764− [] -> return ()
1765− xs -> return () -- runIO $ mapM_ bcAsm xs
1766− case ibcsubdir of
1767− [] -> setIBCSubDir ""
1768− (d:_) -> setIBCSubDir d
1769− setImportDirs importdirs
1770− setSourceDirs sourcedirs
1771−
1772− setNoBanner nobanner
1773−
1774− when (not (NoBasePkgs `elem` opts)) $ do
1775− addPkgDir "prelude"
1776− addPkgDir "base"
1777− mapM_ addPkgDir pkgdirs
1778− elabPrims
1779− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)
1780− addAutoImport "Builtins"
1781− return ()
1782− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)
1783− addAutoImport "Prelude"
1784− return ()
1785− when (runrepl && not idesl) initScript
1786−
1787− nobanner <- getNoBanner
1788−
1789− when (runrepl &&
1790− not quiet &&
1791− not idesl &&
1792− not (isJust script) &&
1793− not nobanner &&
1794− null immediate) $
1795− iputStrLn banner
1796−
1797− orig <- getIState
1798−
1799− mods <- if idesl then return [] else loadInputs inputs Nothing
1800− let efile = case inputs of
1801− [] -> ""
1802− (f:_) -> f
1803−
1804− runIO $ hSetBuffering stdout LineBuffering
1805−
1806− ok <- noErrors
1807− when ok $ case output of
1808− [] -> return ()
1809− (o:_) -> idrisCatch (process "" (Compile cgn o))
1810− (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1811−
1812− case immediate of
1813− [] -> return ()
1814− exprs -> do setWidth InfinitelyWide
1815− mapM_ (\str -> do ist <- getIState
1816− c <- colourise
1817− case parseExpr ist str of
1818− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
1819− runIO $ exitWith (ExitFailure 1)
1820− Success e -> process "" (Eval e))
1821− exprs
1822− runIO exitSuccess
1823−
1824−
1825− case script of
1826− Nothing -> return ()
1827− Just expr -> execScript expr
1828−
1829− -- Create Idris data dir + repl history and config dir
1830− idrisCatch (do dir <- runIO $ getIdrisUserDataDir
1831− exists <- runIO $ doesDirectoryExist dir
1832− unless exists $ logLvl 1 ("Creating " ++ dir)
1833− runIO $ createDirectoryIfMissing True (dir </> "repl"))
1834− (\e -> return ())
1835−
1836− historyFile <- runIO $ getIdrisHistoryFile
1837−
1838− when ok $ case opt getPkgIndex opts of
1839− (f : _) -> writePkgIndex f
1840− _ -> return ()
1841−
1842− when (runrepl && not idesl) $ do
1843−-- clearOrigPats
1844− startServer port orig mods
1845− runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile
1846− let idesock = IdemodeSocket `elem` opts
1847− when (idesl) $ idemodeStart idesock orig inputs
1848− ok <- noErrors
1849− when (not ok) $ runIO (exitWith (ExitFailure 1))
1850− where
1851− makeOption (OLogging i) = setLogLevel i
1852− makeOption (OLogCats cs) = setLogCats cs
1853− makeOption TypeCase = setTypeCase True
1854− makeOption TypeInType = setTypeInType True
1855− makeOption NoCoverage = setCoverage False
1856− makeOption ErrContext = setErrContext True
1857− makeOption _ = return ()
1858−
1859− processOptimisation :: (Bool,Optimisation) -> Idris ()
1860− processOptimisation (True, p) = addOptimise p
1861− processOptimisation (False, p) = removeOptimise p
1862−
1863− addPkgDir :: String -> Idris ()
1864− addPkgDir p = do ddir <- runIO getIdrisLibDir
1865− addImportDir (ddir </> p)
1866− addIBC (IBCImportDir (ddir </> p))
1867−
1868−runMain :: Idris () -> IO ()
1869−runMain prog = do res <- runExceptT $ execStateT prog idrisInit
1870− case res of
1871− Left err -> putStrLn $ "Uncaught error: " ++ show err
1872− Right _ -> return ()
1873−
1874−execScript :: String -> Idris ()
1875−execScript expr = do i <- getIState
1876− c <- colourise
1877− case parseExpr i expr of
1878− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
1879− runIO $ exitWith (ExitFailure 1)
1880− Success term -> do ctxt <- getContext
1881− (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
1882− res <- execute tm
1883− runIO $ exitSuccess
1884−
1885−
1886−-- | Run the initialisation script
1887−initScript :: Idris ()
1888−initScript = do script <- runIO $ getIdrisInitScript
1889− idrisCatch (do go <- runIO $ doesFileExist script
1890− when go $ do
1891− h <- runIO $ openFile script ReadMode
1892− runInit h
1893− runIO $ hClose h)
1894− (\e -> iPrintError $ "Error reading init file: " ++ show e)
1895− where runInit :: Handle -> Idris ()
1896− runInit h = do eof <- lift . lift $ hIsEOF h
1897− ist <- getIState
1898− unless eof $ do
1899− line <- runIO $ hGetLine h
1900− script <- runIO $ getIdrisInitScript
1901− c <- colourise
1902− processLine ist line script c
1903− runInit h
1904− processLine i cmd input clr =
1905− case parseCmd i input cmd of
1906− Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)
1907− Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
1908− Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
1909− Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
1910− Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
1911− Success (Right Proofs) -> proofs i
1912− Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
1913− Success (Right cmd ) -> process [] cmd
1914− Success (Left err) -> runIO $ print err
1915−
1916−
1917−defaultPort :: PortID
1918−defaultPort = PortNumber (fromIntegral 4294)
1919−
1920−banner = " ____ __ _ \n" ++
1921− " / _/___/ /____(_)____ \n" ++
1922− " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
1923− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1924− " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1925− "\n" ++
1926− "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1927− "For details type :warranty."
1928−
1929−warranty = "\n" ++
1930− "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1931− "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1932− "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1933− "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1934− "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1935− "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1936− "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1937− "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1938− "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1939− "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1940− "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"