@@ -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
@@ -1536,388 +1524,3 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
15361524 historyFile = hFile
15371525 }
15381526
1539−-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1540−idris :: [Opt] -> IO (Maybe IState)
1541−idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
1542− case res of
1543− Left err -> do putStrLn $ pshow idrisInit err
1544− return Nothing
1545− Right ist -> return (Just ist)
1546− where totalMain = do idrisMain opts
1547− ist <- getIState
1548− case idris_totcheckfail ist of
1549− ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1550− [] -> return ()
1551−
1552−
1553−loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
1554−loadInputs inputs toline -- furthest line to read in input source files
1555− = idrisCatch
1556− (do ist <- getIState
1557− -- if we're in --check and not outputting anything, don't bother
1558− -- loading, as it gets really slow if there's lots of modules in
1559− -- a package (instead, reload all at the end to check for
1560− -- consistency only)
1561− opts <- getCmdLine
1562−
1563− let loadCode = case opt getOutput opts of
1564− [] -> not (NoREPL `elem` opts)
1565− _ -> True
1566−
1567− -- For each ifile list, check it and build ibcs in the same clean IState
1568− -- so that they don't interfere with each other when checking
1569−
1570− importlists <- getImports [] inputs
1571−
1572− logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))
1573−
1574− let ninputs = zip [1..] inputs
1575− ifiles <- mapWhileOK (\(num, input) ->
1576− do putIState ist
1577− modTree <- buildTree
1578− (map snd (take (num-1) ninputs))
1579− importlists
1580− input
1581− let ifiles = getModuleFiles modTree
1582− logParser 1 ("MODULE TREE : " ++ show modTree)
1583− logParser 1 ("RELOAD: " ++ show ifiles)
1584− when (not (all ibc ifiles) || loadCode) $
1585− tryLoad False IBC_Building (filter (not . ibc) ifiles)
1586− -- return the files that need rechecking
1587− return (input, ifiles))
1588− ninputs
1589− inew <- getIState
1590− let tidata = idris_tyinfodata inew
1591− -- If it worked, load the whole thing from all the ibcs together
1592− case errSpan inew of
1593− Nothing ->
1594− do putIState $!! ist { idris_tyinfodata = tidata }
1595− ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))
1596−-- logLvl 0 $ "Loading from " ++ show ibcfiles
1597− tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)
1598− _ -> return ()
1599− exports <- findExports
1600−
1601− case opt getOutput opts of
1602− [] -> performUsageAnalysis (getExpNames exports) -- interactive
1603− _ -> return [] -- batch, will be checked by the compiler
1604−
1605− return (map fst ifiles))
1606− (\e -> do i <- getIState
1607− case e of
1608− At f e' -> do setErrSpan f
1609− iWarn f $ pprintErr i e'
1610− ProgramLineComment -> return () -- fail elsewhere
1611− _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1612− -- Issue #1576 on the issue tracker.
1613− -- https://github.com/idris-lang/Idris-dev/issues/1576
1614− iWarn emptyFC $ pprintErr i e
1615− return [])
1616− where -- load all files, stop if any fail
1617− tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
1618− tryLoad keepstate phase [] = warnTotality >> return ()
1619− tryLoad keepstate phase (f : fs)
1620− = do ist <- getIState
1621− let maxline
1622− = case toline of
1623− Nothing -> Nothing
1624− Just l -> case f of
1625− IDR fn -> if any (fmatch fn) inputs
1626− then Just l
1627− else Nothing
1628− LIDR fn -> if any (fmatch fn) inputs
1629− then Just l
1630− else Nothing
1631− _ -> Nothing
1632− loadFromIFile True phase f maxline
1633− inew <- getIState
1634− -- FIXME: Save these in IBC to avoid this hack! Need to
1635− -- preserve it all from source inputs
1636− --
1637− -- Issue #1577 on the issue tracker.
1638− -- https://github.com/idris-lang/Idris-dev/issues/1577
1639− let tidata = idris_tyinfodata inew
1640− let patdefs = idris_patdefs inew
1641− ok <- noErrors
1642− if ok then
1643− -- The $!! here prevents a space leak on reloading.
1644− -- This isn't a solution - but it's a temporary stopgap.
1645− -- See issue #2386
1646− do when (not keepstate) $ putIState $!! ist
1647− ist <- getIState
1648− putIState $!! ist { idris_tyinfodata = tidata,
1649− idris_patdefs = patdefs }
1650− tryLoad keepstate phase fs
1651− else warnTotality
1652−
1653− ibc (IBC _ _) = True
1654− ibc _ = False
1655−
1656− fmatch ('.':'/':xs) ys = fmatch xs ys
1657− fmatch xs ('.':'/':ys) = fmatch xs ys
1658− fmatch xs ys = xs == ys
1659−
1660− findNewIBC :: IFileType -> Idris (Maybe IFileType)
1661− findNewIBC i@(IBC _ _) = return (Just i)
1662− findNewIBC s@(IDR f) = do ist <- get
1663− ibcsd <- valIBCSubDir ist
1664− let ibc = ibcPathNoFallback ibcsd f
1665− ok <- runIO $ doesFileExist ibc
1666− if ok then return (Just (IBC ibc s))
1667− else return Nothing
1668− findNewIBC s@(LIDR f) = do ist <- get
1669− ibcsd <- valIBCSubDir ist
1670− let ibc = ibcPathNoFallback ibcsd f
1671− ok <- runIO $ doesFileExist ibc
1672− if ok then return (Just (IBC ibc s))
1673− else return Nothing
1674−
1675− -- Like mapM, but give up when there's an error
1676− mapWhileOK f [] = return []
1677− mapWhileOK f (x : xs) = do x' <- f x
1678− ok <- noErrors
1679− if ok then do xs' <- mapWhileOK f xs
1680− return (x' : xs')
1681− else return [x']
1682−
1683−idrisMain :: [Opt] -> Idris ()
1684−idrisMain opts =
1685− do mapM_ setWidth (opt getConsoleWidth opts)
1686− let inputs = opt getFile opts
1687− let quiet = Quiet `elem` opts
1688− let nobanner = NoBanner `elem` opts
1689− let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts
1690− let runrepl = not (NoREPL `elem` opts)
1691− let verbose = runrepl || Verbose `elem` opts
1692− let output = opt getOutput opts
1693− let ibcsubdir = opt getIBCSubDir opts
1694− let importdirs = opt getImportDir opts
1695− let sourcedirs = opt getSourceDir opts
1696− let bcs = opt getBC opts
1697− let pkgdirs = opt getPkgDir opts
1698− -- Set default optimisations
1699− let optimise = case opt getOptLevel opts of
1700− [] -> 2
1701− xs -> last xs
1702−
1703− setOptLevel optimise
1704− let outty = case opt getOutputTy opts of
1705− [] -> if Interface `elem` opts then
1706− Object else Executable
1707− xs -> last xs
1708− let cgn = case opt getCodegen opts of
1709− [] -> Via IBCFormat "c"
1710− xs -> last xs
1711− let cgFlags = opt getCodegenArgs opts
1712−
1713− -- Now set/unset specifically chosen optimisations
1714− let os = opt getOptimisation opts
1715−
1716− mapM_ processOptimisation os
1717−
1718− script <- case opt getExecScript opts of
1719− [] -> return Nothing
1720− x:y:xs -> do iputStrLn "More than one interpreter expression found."
1721− runIO $ exitWith (ExitFailure 1)
1722− [expr] -> return (Just expr)
1723− let immediate = opt getEvalExpr opts
1724− let port = case getPort opts of
1725− Nothing -> defaultPort
1726− Just p -> p
1727−
1728− when (DefaultTotal `elem` opts) $ do i <- getIState
1729− putIState (i { default_total = DefaultCheckingTotal })
1730− tty <- runIO isATTY
1731− setColourise $ not quiet && last (tty : opt getColour opts)
1732−
1733−
1734−
1735− mapM_ addLangExt (opt getLanguageExt opts)
1736− setREPL runrepl
1737− setQuiet (quiet || isJust script || not (null immediate))
1738− setVerbose verbose
1739− setCmdLine opts
1740− setOutputTy outty
1741− setNoBanner nobanner
1742− setCodegen cgn
1743− mapM_ (addFlag cgn) cgFlags
1744− mapM_ makeOption opts
1745− -- if we have the --bytecode flag, drop into the bytecode assembler
1746− case bcs of
1747− [] -> return ()
1748− xs -> return () -- runIO $ mapM_ bcAsm xs
1749− case ibcsubdir of
1750− [] -> setIBCSubDir ""
1751− (d:_) -> setIBCSubDir d
1752− setImportDirs importdirs
1753− setSourceDirs sourcedirs
1754−
1755− setNoBanner nobanner
1756−
1757− when (not (NoBasePkgs `elem` opts)) $ do
1758− addPkgDir "prelude"
1759− addPkgDir "base"
1760− mapM_ addPkgDir pkgdirs
1761− elabPrims
1762− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)
1763− addAutoImport "Builtins"
1764− return ()
1765− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)
1766− addAutoImport "Prelude"
1767− return ()
1768− when (runrepl && not idesl) initScript
1769−
1770− nobanner <- getNoBanner
1771−
1772− when (runrepl &&
1773− not quiet &&
1774− not idesl &&
1775− not (isJust script) &&
1776− not nobanner &&
1777− null immediate) $
1778− iputStrLn banner
1779−
1780− orig <- getIState
1781−
1782− mods <- if idesl then return [] else loadInputs inputs Nothing
1783− let efile = case inputs of
1784− [] -> ""
1785− (f:_) -> f
1786−
1787− runIO $ hSetBuffering stdout LineBuffering
1788−
1789− ok <- noErrors
1790− when ok $ case output of
1791− [] -> return ()
1792− (o:_) -> idrisCatch (process "" (Compile cgn o))
1793− (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1794−
1795− case immediate of
1796− [] -> return ()
1797− exprs -> do setWidth InfinitelyWide
1798− mapM_ (\str -> do ist <- getIState
1799− c <- colourise
1800− case parseExpr ist str of
1801− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
1802− runIO $ exitWith (ExitFailure 1)
1803− Success e -> process "" (Eval e))
1804− exprs
1805− runIO exitSuccess
1806−
1807−
1808− case script of
1809− Nothing -> return ()
1810− Just expr -> execScript expr
1811−
1812− -- Create Idris data dir + repl history and config dir
1813− idrisCatch (do dir <- runIO $ getIdrisUserDataDir
1814− exists <- runIO $ doesDirectoryExist dir
1815− unless exists $ logLvl 1 ("Creating " ++ dir)
1816− runIO $ createDirectoryIfMissing True (dir </> "repl"))
1817− (\e -> return ())
1818−
1819− historyFile <- runIO $ getIdrisHistoryFile
1820−
1821− when ok $ case opt getPkgIndex opts of
1822− (f : _) -> writePkgIndex f
1823− _ -> return ()
1824−
1825− when (runrepl && not idesl) $ do
1826−-- clearOrigPats
1827− startServer port orig mods
1828− runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile
1829− let idesock = IdemodeSocket `elem` opts
1830− when (idesl) $ idemodeStart idesock orig inputs
1831− ok <- noErrors
1832− when (not ok) $ runIO (exitWith (ExitFailure 1))
1833− where
1834− makeOption (OLogging i) = setLogLevel i
1835− makeOption (OLogCats cs) = setLogCats cs
1836− makeOption TypeCase = setTypeCase True
1837− makeOption TypeInType = setTypeInType True
1838− makeOption NoCoverage = setCoverage False
1839− makeOption ErrContext = setErrContext True
1840− makeOption _ = return ()
1841−
1842− processOptimisation :: (Bool,Optimisation) -> Idris ()
1843− processOptimisation (True, p) = addOptimise p
1844− processOptimisation (False, p) = removeOptimise p
1845−
1846− addPkgDir :: String -> Idris ()
1847− addPkgDir p = do ddir <- runIO getIdrisLibDir
1848− addImportDir (ddir </> p)
1849− addIBC (IBCImportDir (ddir </> p))
1850−
1851−runMain :: Idris () -> IO ()
1852−runMain prog = do res <- runExceptT $ execStateT prog idrisInit
1853− case res of
1854− Left err -> putStrLn $ "Uncaught error: " ++ show err
1855− Right _ -> return ()
1856−
1857−execScript :: String -> Idris ()
1858−execScript expr = do i <- getIState
1859− c <- colourise
1860− case parseExpr i expr of
1861− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
1862− runIO $ exitWith (ExitFailure 1)
1863− Success term -> do ctxt <- getContext
1864− (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
1865− res <- execute tm
1866− runIO $ exitSuccess
1867−
1868−
1869−-- | Run the initialisation script
1870−initScript :: Idris ()
1871−initScript = do script <- runIO $ getIdrisInitScript
1872− idrisCatch (do go <- runIO $ doesFileExist script
1873− when go $ do
1874− h <- runIO $ openFile script ReadMode
1875− runInit h
1876− runIO $ hClose h)
1877− (\e -> iPrintError $ "Error reading init file: " ++ show e)
1878− where runInit :: Handle -> Idris ()
1879− runInit h = do eof <- lift . lift $ hIsEOF h
1880− ist <- getIState
1881− unless eof $ do
1882− line <- runIO $ hGetLine h
1883− script <- runIO $ getIdrisInitScript
1884− c <- colourise
1885− processLine ist line script c
1886− runInit h
1887− processLine i cmd input clr =
1888− case parseCmd i input cmd of
1889− Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)
1890− Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
1891− Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
1892− Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
1893− Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
1894− Success (Right Proofs) -> proofs i
1895− Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
1896− Success (Right cmd ) -> process [] cmd
1897− Success (Left err) -> runIO $ print err
1898−
1899−
1900−defaultPort :: PortID
1901−defaultPort = PortNumber (fromIntegral 4294)
1902−
1903−banner = " ____ __ _ \n" ++
1904− " / _/___/ /____(_)____ \n" ++
1905− " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
1906− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1907− " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1908− "\n" ++
1909− "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1910− "For details type :warranty."
1911−
1912−warranty = "\n" ++
1913− "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1914− "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1915− "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1916− "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1917− "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1918− "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1919− "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1920− "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1921− "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1922− "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1923− "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"