2842bac · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tidying of `idrisMain` (fixes #1454).

2842bacJan de Muijnck-Hughes10 years ago

codegen/idris-codegen-c/Main.hs+1−2

compare with master

unifiedsplit

@@ -3,8 +3,7 @@ module Main where

3import Idris.Core.TT

4import Idris.AbsSyntax

5import Idris.ElabDecls

6−import Idris.REPL

6+import Idris.Main

7−

8import IRTS.Compiler

7import IRTS.Compiler

9import IRTS.CodegenC

8import IRTS.CodegenC

codegen/idris-codegen-javascript/Main.hs+1−2

@@ -3,8 +3,7 @@ module Main where

3import Idris.Core.TT

4import Idris.AbsSyntax

5import Idris.ElabDecls

6−import Idris.REPL

6+import Idris.Main

7−

8import IRTS.Compiler

7import IRTS.Compiler

9import IRTS.CodegenJavaScript

8import IRTS.CodegenJavaScript

codegen/idris-codegen-node/Main.hs+1−1

@@ -3,7 +3,7 @@ module Main where

3import Idris.Core.TT

4import Idris.AbsSyntax

5import Idris.ElabDecls

6−import Idris.REPL

6+import Idris.Main

8import IRTS.Compiler

9import IRTS.CodegenJavaScript

idris.cabal+2

@@ -193,6 +193,8 @@ Library

193 , Idris.Inliner

194 , Idris.Interactive

195 , Idris.Output

196+ , Idris.Main

197+ , Idris.ModeCommon

196 , Idris.Parser

198 , Idris.Parser

197 , Idris.Parser.Helpers

199 , Idris.Parser.Helpers

198 , Idris.Parser.Ops

200 , Idris.Parser.Ops

main/Main.hs+11−3

@@ -5,14 +5,12 @@ import System.Exit ( exitSuccess )

5import Control.Monad ( when )

7import Idris.AbsSyntax

8−import Idris.REPL

9import Idris.Error

8import Idris.Error

10import Idris.CmdOptions

9import Idris.CmdOptions

11import Idris.Info

10import Idris.Info

12import Idris.Info.Show

11import Idris.Info.Show

13import Idris.Package

12import Idris.Package

14−

13+import Idris.Main

15−

17import Util.System ( setupBundledCC )

15import Util.System ( setupBundledCC )

@@ -25,21 +23,27 @@ main :: IO ()

25main = do opts <- runArgParser

23main = do opts <- runArgParser

26 runMain (runIdris opts)

24 runMain (runIdris opts)

26+-- | The main function for the Idris executable.

28runIdris :: [Opt] -> Idris ()

27runIdris :: [Opt] -> Idris ()

29runIdris opts = do

28runIdris opts = do

30 runIO setupBundledCC

29 runIO setupBundledCC

30+ -- Show information then quit.

31 when (ShowAll `elem` opts) $ runIO showExitIdrisInfo

32 when (ShowLoggingCats `elem` opts) $ runIO showExitIdrisLoggingCategories

33 when (ShowIncs `elem` opts) $ runIO showExitIdrisFlagsInc

34 when (ShowLibs `elem` opts) $ runIO showExitIdrisFlagsLibs

35 when (ShowLibdir `elem` opts) $ runIO showExitIdrisLibDir

36 when (ShowPkgs `elem` opts) $ runIO showExitIdrisInstalledPackages

37+

38+ -- Be a client to an IDE Mode server.

37 case opt getClient opts of

39 case opt getClient opts of

38 [] -> return ()

40 [] -> return ()

39 (c:_) -> do setVerbose False

41 (c:_) -> do setVerbose False

40 setQuiet True

42 setQuiet True

41 runIO $ runClient (getPort opts) c

43 runIO $ runClient (getPort opts) c

42 runIO exitSuccess

44 runIO exitSuccess

45+

46+ -- Work with Idris packages.

43 case opt getPkgCheck opts of

47 case opt getPkgCheck opts of

44 [] -> return ()

48 [] -> return ()

45 fs -> do runIO $ mapM_ (checkPkg opts (WarnOnly `elem` opts) True) fs

49 fs -> do runIO $ mapM_ (checkPkg opts (WarnOnly `elem` opts) True) fs

@@ -56,9 +60,13 @@ runIdris opts = do

56 [] -> return ()

60 [] -> return ()

57 fs -> do runIO $ mapM_ (testPkg opts) fs

61 fs -> do runIO $ mapM_ (testPkg opts) fs

58 runIO exitSuccess

62 runIO exitSuccess

63+

64+ -- Either launch one of the interaction modes, or install a

65+ -- package.

59 case opt getPkg opts of

66 case opt getPkg opts of

60 [] -> case opt getPkgREPL opts of

67 [] -> case opt getPkgREPL opts of

61 [] -> idrisMain opts

68 [] -> idrisMain opts

62 [f] -> replPkg opts f

69 [f] -> replPkg opts f

63 _ -> ifail "Too many packages"

70 _ -> ifail "Too many packages"

64 fs -> runIO $ mapM_ (buildPkg opts (WarnOnly `elem` opts)) fs

71 fs -> runIO $ mapM_ (buildPkg opts (WarnOnly `elem` opts)) fs

72+

src/Idris/Main.hsnew file+293

@@ -0,0 +1,293 @@

1+{-|

2+Module : Idris.REPL

3+Description : Main function to decide Idris' mode of use.

4+License : BSD3

5+Maintainer : The Idris Community.

6+-}

7+module Idris.Main

8+ ( idrisMain

9+ , idris

10+ , runMain

11+ , runClient -- taken from Idris.REPL.

12+ , loadInputs -- taken from Idris.ModeCommon

13+ ) where

14+

15+import Idris.AbsSyntax

16+import Idris.ModeCommon

17+import Idris.REPL.Parser

18+import Idris.Error

19+import Idris.IBC

20+import Idris.Parser hiding (indent)

21+import Idris.Output

22+

23+import Idris.REPL.Commands

24+import Idris.REPL

25+

26+import Idris.ElabDecls

27+import Idris.Elab.Value

28+import Idris.Elab.Term

29+import Idris.Info

30+

31+import Util.System

32+

33+import Idris.Core.Execute (execute)

34+import Idris.Core.TT

35+

36+import IRTS.CodegenCommon

37+

38+import Control.Category

39+import Prelude hiding ((<$>), (.), id)

40+

41+import Text.Trifecta.Result(Result(..), ErrInfo(..))

42+

43+import System.Console.Haskeline as H

44+import System.FilePath

45+import System.Exit

46+import System.Directory

47+import System.IO

48+import Control.Monad

49+import Control.Monad.Trans.Except (runExceptT)

50+import Control.Monad.Trans.State.Strict (execStateT)

51+import Control.Monad.Trans ( lift )

52+import Data.Maybe

53+import Control.DeepSeq

54+

55+

56+

57+-- | How to run Idris programs.

58+runMain :: Idris () -> IO ()

59+runMain prog = do res <- runExceptT $ execStateT prog idrisInit

60+ case res of

61+ Left err -> putStrLn $ "Uncaught error: " ++ show err

62+ Right _ -> return ()

63+

64+

65+-- | The main function of Idris that when given a set of Options will

66+-- launch Idris into the desired interaction mode either: REPL;

67+-- Compiler; Script execution; or IDE Mode.

68+idrisMain :: [Opt] -> Idris ()

69+idrisMain opts =

70+ do mapM_ setWidth (opt getConsoleWidth opts)

71+ let inputs = opt getFile opts

72+ let quiet = Quiet `elem` opts

73+ let nobanner = NoBanner `elem` opts

74+ let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

75+ let runrepl = not (NoREPL `elem` opts)

76+ let verbose = runrepl || Verbose `elem` opts

77+ let output = opt getOutput opts

78+ let ibcsubdir = opt getIBCSubDir opts

79+ let importdirs = opt getImportDir opts

80+ let sourcedirs = opt getSourceDir opts

81+ setSourceDirs sourcedirs

82+ let bcs = opt getBC opts

83+ let pkgdirs = opt getPkgDir opts

84+ -- Set default optimisations

85+ let optimise = case opt getOptLevel opts of

86+ [] -> 2

87+ xs -> last xs

88+

89+ setOptLevel optimise

90+ let outty = case opt getOutputTy opts of

91+ [] -> if Interface `elem` opts then

92+ Object else Executable

93+ xs -> last xs

94+ let cgn = case opt getCodegen opts of

95+ [] -> Via IBCFormat "c"

96+ xs -> last xs

97+ let cgFlags = opt getCodegenArgs opts

98+

99+ -- Now set/unset specifically chosen optimisations

100+ let os = opt getOptimisation opts

101+

102+ mapM_ processOptimisation os

103+

104+ script <- case opt getExecScript opts of

105+ [] -> return Nothing

106+ x:y:xs -> do iputStrLn "More than one interpreter expression found."

107+ runIO $ exitWith (ExitFailure 1)

108+ [expr] -> return (Just expr)

109+ let immediate = opt getEvalExpr opts

110+ let port = case getPort opts of

111+ Nothing -> defaultPort

112+ Just p -> p

113+

114+ when (DefaultTotal `elem` opts) $ do i <- getIState

115+ putIState (i { default_total = DefaultCheckingTotal })

116+ tty <- runIO isATTY

117+ setColourise $ not quiet && last (tty : opt getColour opts)

118+

119+

120+

121+ mapM_ addLangExt (opt getLanguageExt opts)

122+ setREPL runrepl

123+ setQuiet (quiet || isJust script || not (null immediate))

124+ setVerbose verbose

125+ setCmdLine opts

126+ setOutputTy outty

127+ setNoBanner nobanner

128+ setCodegen cgn

129+ mapM_ (addFlag cgn) cgFlags

130+ mapM_ makeOption opts

131+ -- if we have the --bytecode flag, drop into the bytecode assembler

132+ case bcs of

133+ [] -> return ()

134+ xs -> return () -- runIO $ mapM_ bcAsm xs

135+ case ibcsubdir of

136+ [] -> setIBCSubDir ""

137+ (d:_) -> setIBCSubDir d

138+ setImportDirs importdirs

139+

140+ setNoBanner nobanner

141+

142+ when (not (NoBasePkgs `elem` opts)) $ do

143+ addPkgDir "prelude"

144+ addPkgDir "base"

145+ mapM_ addPkgDir pkgdirs

146+ elabPrims

147+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)

148+ addAutoImport "Builtins"

149+ return ()

150+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)

151+ addAutoImport "Prelude"

152+ return ()

153+ when (runrepl && not idesl) initScript

154+

155+ nobanner <- getNoBanner

156+

157+ when (runrepl &&

158+ not quiet &&

159+ not idesl &&

160+ not (isJust script) &&

161+ not nobanner &&

162+ null immediate) $

163+ iputStrLn banner

164+

165+ orig <- getIState

166+

167+ mods <- if idesl then return [] else loadInputs inputs Nothing

168+ let efile = case inputs of

169+ [] -> ""

170+ (f:_) -> f

171+

172+ runIO $ hSetBuffering stdout LineBuffering

173+

174+ ok <- noErrors

175+ when ok $ case output of

176+ [] -> return ()

177+ (o:_) -> idrisCatch (process "" (Compile cgn o))

178+ (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

179+

180+ case immediate of

181+ [] -> return ()

182+ exprs -> do setWidth InfinitelyWide

183+ mapM_ (\str -> do ist <- getIState

184+ c <- colourise

185+ case parseExpr ist str of

186+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

187+ runIO $ exitWith (ExitFailure 1)

188+ Success e -> process "" (Eval e))

189+ exprs

190+ runIO exitSuccess

191+

192+

193+ case script of

194+ Nothing -> return ()

195+ Just expr -> execScript expr

196+

197+ -- Create Idris data dir + repl history and config dir

198+ idrisCatch (do dir <- runIO $ getIdrisUserDataDir

199+ exists <- runIO $ doesDirectoryExist dir

200+ unless exists $ logLvl 1 ("Creating " ++ dir)

201+ runIO $ createDirectoryIfMissing True (dir </> "repl"))

202+ (\e -> return ())

203+

204+ historyFile <- runIO $ getIdrisHistoryFile

205+

206+ when ok $ case opt getPkgIndex opts of

207+ (f : _) -> writePkgIndex f

208+ _ -> return ()

209+

210+ when (runrepl && not idesl) $ do

211+-- clearOrigPats

212+ startServer port orig mods

213+ runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile

214+ let idesock = IdemodeSocket `elem` opts

215+ when (idesl) $ idemodeStart idesock orig inputs

216+ ok <- noErrors

217+ when (not ok) $ runIO (exitWith (ExitFailure 1))

218+ where

219+ makeOption (OLogging i) = setLogLevel i

220+ makeOption (OLogCats cs) = setLogCats cs

221+ makeOption TypeCase = setTypeCase True

222+ makeOption TypeInType = setTypeInType True

223+ makeOption NoCoverage = setCoverage False

224+ makeOption ErrContext = setErrContext True

225+ makeOption _ = return ()

226+

227+ processOptimisation :: (Bool,Optimisation) -> Idris ()

228+ processOptimisation (True, p) = addOptimise p

229+ processOptimisation (False, p) = removeOptimise p

230+

231+ addPkgDir :: String -> Idris ()

232+ addPkgDir p = do ddir <- runIO getIdrisLibDir

233+ addImportDir (ddir </> p)

234+ addIBC (IBCImportDir (ddir </> p))

235+

236+

237+

238+-- | Invoke as if from command line. It is an error if there are

239+-- unresolved totality problems.

240+idris :: [Opt] -> IO (Maybe IState)

241+idris opts = do res <- runExceptT $ execStateT totalMain idrisInit

242+ case res of

243+ Left err -> do putStrLn $ pshow idrisInit err

244+ return Nothing

245+ Right ist -> return (Just ist)

246+ where totalMain = do idrisMain opts

247+ ist <- getIState

248+ case idris_totcheckfail ist of

249+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg

250+ [] -> return ()

251+

252+

253+-- | Execute the provided Idris expression.

254+execScript :: String -> Idris ()

255+execScript expr = do i <- getIState

256+ c <- colourise

257+ case parseExpr i expr of

258+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

259+ runIO $ exitWith (ExitFailure 1)

260+ Success term -> do ctxt <- getContext

261+ (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

262+ res <- execute tm

263+ runIO $ exitSuccess

264+

265+-- | Run the initialisation script

266+initScript :: Idris ()

267+initScript = do script <- runIO $ getIdrisInitScript

268+ idrisCatch (do go <- runIO $ doesFileExist script

269+ when go $ do

270+ h <- runIO $ openFile script ReadMode

271+ runInit h

272+ runIO $ hClose h)

273+ (\e -> iPrintError $ "Error reading init file: " ++ show e)

274+ where runInit :: Handle -> Idris ()

275+ runInit h = do eof <- lift . lift $ hIsEOF h

276+ ist <- getIState

277+ unless eof $ do

278+ line <- runIO $ hGetLine h

279+ script <- runIO $ getIdrisInitScript

280+ c <- colourise

281+ processLine ist line script c

282+ runInit h

283+ processLine i cmd input clr =

284+ case parseCmd i input cmd of

285+ Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)

286+ Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

287+ Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

288+ Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

289+ Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

290+ Success (Right Proofs) -> proofs i

291+ Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

292+ Success (Right cmd ) -> process [] cmd

293+ Success (Left err) -> runIO $ print err

src/Idris/ModeCommon.hsnew file+190

@@ -0,0 +1,190 @@

1+{-|

2+Module : Idris.ModeCommon

3+Description : Common utilities used by all modes.

4+License : BSD3

5+Maintainer : The Idris Community.

6+-}

7+module Idris.ModeCommon where

10+import Idris.AbsSyntax

11+import Idris.Erasure

12+import Idris.Error

13+import Idris.IBC

14+import Idris.Delaborate

15+import Idris.Parser hiding (indent)

16+import Idris.Chaser

17+import Idris.Imports

18+import Idris.Output

19+import Idris.Info

20+import Idris.Core.TT

21+

22+import IRTS.Exports

23+

24+import Control.Category

25+import Prelude hiding ((<$>), (.), id)

26+

27+import System.Directory

28+import Control.Monad

29+import Control.Monad.Trans.State.Strict (get)

30+import Network (PortID(PortNumber))

31+import Data.Maybe

32+import Data.List hiding (group)

33+import Control.DeepSeq

34+

35+

36+defaultPort :: PortID

37+defaultPort = PortNumber (fromIntegral 4294)

38+

39+

40+loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

41+loadInputs inputs toline -- furthest line to read in input source files

42+ = idrisCatch

43+ (do ist <- getIState

44+ -- if we're in --check and not outputting anything, don't bother

45+ -- loading, as it gets really slow if there's lots of modules in

46+ -- a package (instead, reload all at the end to check for

47+ -- consistency only)

48+ opts <- getCmdLine

49+

50+ let loadCode = case opt getOutput opts of

51+ [] -> not (NoREPL `elem` opts)

52+ _ -> True

53+

54+ -- For each ifile list, check it and build ibcs in the same clean IState

55+ -- so that they don't interfere with each other when checking

56+

57+ importlists <- getImports [] inputs

58+

59+ logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))

60+

61+ let ninputs = zip [1..] inputs

62+ ifiles <- mapWhileOK (\(num, input) ->

63+ do putIState ist

64+ modTree <- buildTree

65+ (map snd (take (num-1) ninputs))

66+ importlists

67+ input

68+ let ifiles = getModuleFiles modTree

69+ logParser 1 ("MODULE TREE : " ++ show modTree)

70+ logParser 1 ("RELOAD: " ++ show ifiles)

71+ when (not (all ibc ifiles) || loadCode) $

72+ tryLoad False IBC_Building (filter (not . ibc) ifiles)

73+ -- return the files that need rechecking

74+ return (input, ifiles))

75+ ninputs

76+ inew <- getIState

77+ let tidata = idris_tyinfodata inew

78+ -- If it worked, load the whole thing from all the ibcs together

79+ case errSpan inew of

80+ Nothing ->

81+ do putIState $!! ist { idris_tyinfodata = tidata }

82+ ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))

83+-- logLvl 0 $ "Loading from " ++ show ibcfiles

84+ tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

85+ _ -> return ()

86+ exports <- findExports

87+

88+ case opt getOutput opts of

89+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

90+ _ -> return [] -- batch, will be checked by the compiler

91+

92+ return (map fst ifiles))

93+ (\e -> do i <- getIState

94+ case e of

95+ At f e' -> do setErrSpan f

96+ iWarn f $ pprintErr i e'

97+ ProgramLineComment -> return () -- fail elsewhere

98+ _ -> do setErrSpan emptyFC -- FIXME! Propagate it

99+ -- Issue #1576 on the issue tracker.

100+ -- https://github.com/idris-lang/Idris-dev/issues/1576

101+ iWarn emptyFC $ pprintErr i e

102+ return [])

103+ where -- load all files, stop if any fail

104+ tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()

105+ tryLoad keepstate phase [] = warnTotality >> return ()

106+ tryLoad keepstate phase (f : fs)

107+ = do ist <- getIState

108+ let maxline

109+ = case toline of

110+ Nothing -> Nothing

111+ Just l -> case f of

112+ IDR fn -> if any (fmatch fn) inputs

113+ then Just l

114+ else Nothing

115+ LIDR fn -> if any (fmatch fn) inputs

116+ then Just l

117+ else Nothing

118+ _ -> Nothing

119+ loadFromIFile True phase f maxline

120+ inew <- getIState

121+ -- FIXME: Save these in IBC to avoid this hack! Need to

122+ -- preserve it all from source inputs

123+ --

124+ -- Issue #1577 on the issue tracker.

125+ -- https://github.com/idris-lang/Idris-dev/issues/1577

126+ let tidata = idris_tyinfodata inew

127+ let patdefs = idris_patdefs inew

128+ ok <- noErrors

129+ if ok then

130+ -- The $!! here prevents a space leak on reloading.

131+ -- This isn't a solution - but it's a temporary stopgap.

132+ -- See issue #2386

133+ do when (not keepstate) $ putIState $!! ist

134+ ist <- getIState

135+ putIState $!! ist { idris_tyinfodata = tidata,

136+ idris_patdefs = patdefs }

137+ tryLoad keepstate phase fs

138+ else warnTotality

139+

140+ ibc (IBC _ _) = True

141+ ibc _ = False

142+

143+ fmatch ('.':'/':xs) ys = fmatch xs ys

144+ fmatch xs ('.':'/':ys) = fmatch xs ys

145+ fmatch xs ys = xs == ys

146+

147+ findNewIBC :: IFileType -> Idris (Maybe IFileType)

148+ findNewIBC i@(IBC _ _) = return (Just i)

149+ findNewIBC s@(IDR f) = do ist <- get

150+ ibcsd <- valIBCSubDir ist

151+ let ibc = ibcPathNoFallback ibcsd f

152+ ok <- runIO $ doesFileExist ibc

153+ if ok then return (Just (IBC ibc s))

154+ else return Nothing

155+ findNewIBC s@(LIDR f) = do ist <- get

156+ ibcsd <- valIBCSubDir ist

157+ let ibc = ibcPathNoFallback ibcsd f

158+ ok <- runIO $ doesFileExist ibc

159+ if ok then return (Just (IBC ibc s))

160+ else return Nothing

161+

162+ -- Like mapM, but give up when there's an error

163+ mapWhileOK f [] = return []

164+ mapWhileOK f (x : xs) = do x' <- f x

165+ ok <- noErrors

166+ if ok then do xs' <- mapWhileOK f xs

167+ return (x' : xs')

168+ else return [x']

169+

170+banner = " ____ __ _ \n" ++

171+ " / _/___/ /____(_)____ \n" ++

172+ " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++

173+ " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

174+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

175+ "\n" ++

176+ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++

177+ "For details type :warranty."

178+

179+warranty = "\n" ++

180+ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++

181+ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++

182+ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++

183+ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++

184+ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++

185+ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++

186+ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++

187+ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++

188+ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++

189+ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++

190+ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"

src/Idris/Package.hs+1

@@ -37,6 +37,7 @@ import Idris.IBC

37import Idris.Output

38import Idris.Imports

39import Idris.Error (ifail)

40+import Idris.Main (idrisMain, idris)

41import Idris.Package.Common

42import Idris.Package.Common

42import Idris.Package.Parser

43import Idris.Package.Parser

src/Idris/REPL.hs+10−407

@@ -1,59 +1,53 @@

1{-|

2Module : Idris.REPL

3Description : Entry Point for the Idris REPL and CLI.

4−Copyright :

5License : BSD3

4License : BSD3

6Maintainer : The Idris Community.

5Maintainer : The Idris Community.

7-}

6-}

8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

7{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

9 PatternGuards, CPP #-}

8 PatternGuards, CPP #-}

10−

11−module Idris.REPL(

9+module Idris.REPL

12− idris, idrisMain, loadInputs

10+ ( idemodeStart

11+ , startServer

13− , runClient, runMain

12+ , runClient

13+ , process

14+ , replSettings

15+ , repl

16+ , proofs

14 ) where

17 ) where

16import Idris.AbsSyntax

19import Idris.AbsSyntax

17import Idris.ASTUtils

20import Idris.ASTUtils

18import Idris.Apropos (apropos, aproposModules)

21import Idris.Apropos (apropos, aproposModules)

19import Idris.REPL.Parser

22import Idris.REPL.Parser

20−import Idris.Erasure

21import Idris.Error

23import Idris.Error

22import Idris.IBC

24import Idris.IBC

23import Idris.ErrReverse

25import Idris.ErrReverse

24import Idris.Delaborate

26import Idris.Delaborate

25−import Idris.Docstrings (Docstring, overview, renderDocstring, renderDocTerm)

27+import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

26import Idris.Help

28import Idris.Help

27import Idris.IdrisDoc

29import Idris.IdrisDoc

28import Idris.Prover

30import Idris.Prover

29import Idris.Parser hiding (indent)

31import Idris.Parser hiding (indent)

30−import Idris.Primitives

31import Idris.Coverage

32import Idris.Coverage

32import Idris.Docs hiding (Doc)

33import Idris.Docs hiding (Doc)

33import Idris.Completion

34import Idris.Completion

34import qualified Idris.IdeMode as IdeMode

35import qualified Idris.IdeMode as IdeMode

35−import Idris.Chaser

36−import Idris.Imports

37import Idris.Colours hiding (colourise)

36import Idris.Colours hiding (colourise)

38import Idris.Inliner

37import Idris.Inliner

39−import Idris.CaseSplit

40−import Idris.DeepSeq

41import Idris.Output

38import Idris.Output

42import Idris.Interactive

39import Idris.Interactive

43import Idris.WhoCalls

40import Idris.WhoCalls

44import Idris.TypeSearch (searchByType)

41import Idris.TypeSearch (searchByType)

45−import Idris.IBC (loadPkgIndex, writePkgIndex)

47import Idris.REPL.Browse (namesInNS, namespacesInNS)

43import Idris.REPL.Browse (namesInNS, namespacesInNS)

48import Idris.REPL.Commands

44import Idris.REPL.Commands

50import Idris.ElabDecls

46import Idris.ElabDecls

51−import Idris.Elab.Type

52import Idris.Elab.Clause

47import Idris.Elab.Clause

53−import Idris.Elab.Data

54import Idris.Elab.Value

48import Idris.Elab.Value

55import Idris.Elab.Term

49import Idris.Elab.Term

56−

50+import Idris.ModeCommon

57import Idris.Info

51import Idris.Info

59import Version_idris (gitHash)

53import Version_idris (gitHash)

@@ -70,14 +64,11 @@ import Idris.Core.WHNF

70import Idris.Core.Constraints

64import Idris.Core.Constraints

72import IRTS.Compiler

66import IRTS.Compiler

73−import IRTS.CodegenCommon

74−import IRTS.Exports

76import Control.Category

68import Control.Category

77import qualified Control.Exception as X

69import qualified Control.Exception as X

78import Prelude hiding ((<$>), (.), id)

70import Prelude hiding ((<$>), (.), id)

79import Data.List.Split (splitOn)

71import Data.List.Split (splitOn)

80−import Data.List (groupBy)

81import qualified Data.Text as T

72import qualified Data.Text as T

83import Text.Trifecta.Result(Result(..), ErrInfo(..))

74import Text.Trifecta.Result(Result(..), ErrInfo(..))

@@ -101,7 +92,6 @@ import Data.List hiding (group)

101import Data.Char

92import Data.Char

102import qualified Data.Set as S

93import qualified Data.Set as S

103import Data.Version

94import Data.Version

104−import Data.Word (Word)

105import Data.Either (partitionEithers)

95import Data.Either (partitionEithers)

106import Control.DeepSeq

96import Control.DeepSeq

107

@@ -109,9 +99,7 @@ import Control.Concurrent.Async (race)

109import System.FSNotify (withManager, watchDir)

99import System.FSNotify (withManager, watchDir)

110import System.FSNotify.Devel (allEvents, doAllEvents)

100import System.FSNotify.Devel (allEvents, doAllEvents)

111

101

112−import Numeric ( readHex )

113

102

114−import Debug.Trace

115

103

116-- | Run the REPL

104-- | Run the REPL

117repl :: IState -- ^ The initial state

105repl :: IState -- ^ The initial state

@@ -1536,388 +1524,3 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

1536 historyFile = hFile

1524 historyFile = hFile

1537 }

1525 }

1538

1526

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"