git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Idris/REPL.hs
613 lines 24 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards #-}
4module Idris.REPL where
6import Idris.AbsSyntax
7import Idris.REPLParser
8import Idris.ElabDecls
9import Idris.ElabTerm
10import Idris.Error
11import Idris.Delaborate
12import Idris.Compiler
13import Idris.Prover
14import Idris.Parser
15import Idris.Primitives
16import Idris.Coverage
17import Idris.UnusedArgs
18import Idris.Docs
20import Paths_idris
21import Util.System
23import Core.Evaluate
24import Core.ProofShell
25import Core.TT
26import Core.Constraints
28import IRTS.Compiler
29import IRTS.LParser
30import IRTS.CodegenCommon
32-- import RTS.SC
33-- import RTS.Bytecode
34-- import RTS.PreC
35-- import RTS.CodegenC
37import System.Console.Haskeline as H
38import System.FilePath
39import System.Exit
40import System.Environment
41import System.Process
42import System.Directory
43import System.IO
44import Control.Monad
45import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )
46import Control.Monad.Trans ( liftIO, lift )
47import Data.Maybe
48import Data.List
49import Data.Char
50import Data.Version
52repl :: IState -> [FilePath] -> Idris ()
53repl orig mods
54 = H.catch
55 (do let prompt = mkPrompt mods
56 x <- lift $ getInputLine (prompt ++ "> ")
57 case x of
58 Nothing -> do iputStrLn "Bye bye"
59 return ()
60 Just input -> H.catch
61 (do ms <- processInput input orig mods
62 case ms of
63 Just mods -> repl orig mods
64 Nothing -> return ())
65 ctrlC)
66 ctrlC
67 where ctrlC :: SomeException -> Idris ()
68 ctrlC e = do iputStrLn (show e)
69 repl orig mods
71mkPrompt [] = "Idris"
72mkPrompt [x] = "*" ++ dropExtension x
73mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
75lit f = case splitExtension f of
76 (_, ".lidr") -> True
77 _ -> False
79processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
80processInput cmd orig inputs
81 = do i <- get
82 let fn = case inputs of
83 (f:_) -> f
84 _ -> ""
85 case parseCmd i cmd of
86 Left err -> do liftIO $ print err
87 return (Just inputs)
88 Right Reload ->
89 do put (orig { idris_options = idris_options i })
90 clearErr
91 mods <- mapM loadModule inputs
92 return (Just inputs)
93 Right (Load f) ->
94 do put (orig { idris_options = idris_options i })
95 clearErr
96 mod <- loadModule f
97 return (Just [f])
98 Right (ModImport f) ->
99 do clearErr
100 fmod <- loadModule f
101 return (Just (inputs ++ [fmod]))
102 Right Edit -> do edit fn orig
103 return (Just inputs)
104 Right Proofs -> do proofs orig
105 return (Just inputs)
106 Right Quit -> do iputStrLn "Bye bye"
107 return Nothing
108 Right cmd -> do idrisCatch (process fn cmd)
109 (\e -> iputStrLn (show e))
110 return (Just inputs)
112resolveProof :: Name -> Idris Name
113resolveProof n'
114 = do i <- get
115 ctxt <- getContext
116 n <- case lookupNames Nothing n' ctxt of
117 [x] -> return x
118 [] -> return n'
119 ns -> fail $ pshow i (CantResolveAlts (map show ns))
120 return n
122removeProof :: Name -> Idris ()
123removeProof n =
124 do i <- get
125 let proofs = proof_list i
126 let ps = filter ((/= n) . fst) proofs
127 put $ i { proof_list = ps }
129edit :: FilePath -> IState -> Idris ()
130edit "" orig = iputStrLn "Nothing to edit"
131edit f orig
132 = do i <- get
133 env <- liftIO $ getEnvironment
134 let editor = getEditor env
135 let line = case errLine i of
136 Just l -> " +" ++ show l ++ " "
137 Nothing -> " "
138 let cmd = editor ++ line ++ f
139 liftIO $ system cmd
140 clearErr
141 put (orig { idris_options = idris_options i })
142 loadModule f
143 iucheck
144 return ()
145 where getEditor env | Just ed <- lookup "EDITOR" env = ed
146 | Just ed <- lookup "VISUAL" env = ed
147 | otherwise = "vi"
150proofs :: IState -> Idris ()
151proofs orig
152 = do i <- get
153 let ps = proof_list i
154 case ps of
155 [] -> iputStrLn "No proofs available"
156 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
158insertScript :: String -> [String] -> [String]
159insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
160insertScript prf (p@"---------- Proofs ----------" : "" : xs)
161 = p : "" : prf : xs
162insertScript prf (x : xs) = x : insertScript prf xs
164process :: FilePath -> Command -> Idris ()
165process fn Help = iputStrLn displayHelp
166process fn (Eval t)
167 = do (tm, ty) <- elabVal toplevel False t
168 ctxt <- getContext
169 ist <- get
170 let tm' = normaliseAll ctxt [] tm
171 let ty' = normaliseAll ctxt [] ty
172 logLvl 3 $ "Raw: " ++ show (tm', ty')
173 imp <- impShow
174 iputStrLn (showImp imp (delab ist tm') ++ " : " ++
175 showImp imp (delab ist ty'))
176process fn (ExecVal t)
177 = do (tm, ty) <- elabVal toplevel False t
178-- (PApp fc (PRef fc (NS (UN "print") ["Prelude"]))
179-- [pexp t])
180 (tmpn, tmph) <- liftIO tempfile
181 liftIO $ hClose tmph
182 t <- target
183 compile t tmpn tm
184 liftIO $ system tmpn
185 return ()
186 where fc = FC "(input)" 0
187process fn (Check (PRef _ n))
188 = do ctxt <- getContext
189 ist <- get
190 imp <- impShow
191 case lookupTy Nothing n ctxt of
192 ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++
193 showImp imp (delab ist t)) ts
194 [] -> iputStrLn $ "No such variable " ++ show n
195process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
196 ctxt <- getContext
197 ist <- get
198 imp <- impShow
199 let ty' = normaliseC ctxt [] ty
200 iputStrLn (showImp imp (delab ist tm) ++ " : " ++
201 showImp imp (delab ist ty))
203process fn (DocStr n) = do i <- get
204 case lookupCtxtName Nothing n (idris_docstrings i) of
205 [] -> iputStrLn $ "No documentation for " ++ show n
206 ns -> mapM_ showDoc ns
207 where showDoc (n, d)
208 = do doc <- getDocs n
209 iputStrLn $ show doc
210process fn Universes = do i <- get
211 let cs = idris_constraints i
212-- iputStrLn $ showSep "\n" (map show cs)
213 liftIO $ print (map fst cs)
214 let n = length cs
215 iputStrLn $ "(" ++ show n ++ " constraints)"
216 case ucheck cs of
217 Error e -> iputStrLn $ pshow i e
218 OK _ -> iputStrLn "Universes OK"
219process fn (Defn n) = do i <- get
220 iputStrLn "Compiled patterns:\n"
221 liftIO $ print (lookupDef Nothing n (tt_ctxt i))
222 case lookupCtxt Nothing n (idris_patdefs i) of
223 [] -> return ()
224 [d] -> do iputStrLn "Original definiton:\n"
225 mapM_ (printCase i) d
226 case lookupTotal n (tt_ctxt i) of
227 [t] -> iputStrLn (showTotal t i)
228 _ -> return ()
229 where printCase i (_, lhs, rhs)
230 = do liftIO $ putStr $ showImp True (delab i lhs)
231 liftIO $ putStr " = "
232 liftIO $ putStrLn $ showImp True (delab i rhs)
233process fn (TotCheck n) = do i <- get
234 case lookupTotal n (tt_ctxt i) of
235 [t] -> iputStrLn (showTotal t i)
236 _ -> return ()
237process fn (DebugInfo n)
238 = do i <- get
239 let oi = lookupCtxtName Nothing n (idris_optimisation i)
240 when (not (null oi)) $ iputStrLn (show oi)
241 let si = lookupCtxt Nothing n (idris_statics i)
242 when (not (null si)) $ iputStrLn (show si)
243 let d = lookupDef Nothing n (tt_ctxt i)
244 when (not (null d)) $ liftIO $
245 do print (head d)
246 let cg = lookupCtxtName Nothing n (idris_callgraph i)
247 findUnusedArgs (map fst cg)
248 i <- get
249 let cg' = lookupCtxtName Nothing n (idris_callgraph i)
250 sc <- checkSizeChange n
251 iputStrLn $ "Size change: " ++ show sc
252 when (not (null cg')) $ do iputStrLn "Call graph:\n"
253 iputStrLn (show cg')
254process fn (Info n) = do i <- get
255 case lookupCtxt Nothing n (idris_classes i) of
256 [c] -> classInfo c
257 _ -> iputStrLn "Not a class"
258process fn (Search t) = iputStrLn "Not implemented"
259process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
260 ctxt <- getContext
261 ist <- get
262 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
263 iputStrLn (show (delab ist tm'))
265process fn (RmProof n')
266 = do i <- get
267 n <- resolveProof n'
268 let proofs = proof_list i
269 case lookup n proofs of
270 Nothing -> iputStrLn "No proof to remove"
271 Just _ -> do removeProof n
272 insertMetavar n
273 iputStrLn $ "Removed proof " ++ show n
274 where
275 insertMetavar :: Name -> Idris ()
276 insertMetavar n =
277 do i <- get
278 let ms = idris_metavars i
279 put $ i { idris_metavars = n : ms }
281process fn (AddProof prf)
282 = do let fb = fn ++ "~"
283 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
284 prog <- liftIO $ readFile fb
285 i <- get
286 let proofs = proof_list i
287 n' <- case prf of
288 Nothing -> case proofs of
289 [] -> fail "No proof to add"
290 ((x, p) : _) -> return x
291 Just nm -> return nm
292 n <- resolveProof n'
293 case lookup n proofs of
294 Nothing -> iputStrLn "No proof to add"
295 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
296 liftIO $ writeFile fn (unlines prog')
297 removeProof n
298 iputStrLn $ "Added proof " ++ show n
299 where ls = (lines prog)
301process fn (ShowProof n')
302 = do i <- get
303 n <- resolveProof n'
304 let proofs = proof_list i
305 case lookup n proofs of
306 Nothing -> iputStrLn "No proof to show"
307 Just p -> iputStrLn $ showProof False n p
309process fn (Prove n')
310 = do ctxt <- getContext
311 ist <- get
312 n <- case lookupNames Nothing n' ctxt of
313 [x] -> return x
314 [] -> return n'
315 ns -> fail $ pshow ist (CantResolveAlts (map show ns))
316 prover (lit fn) n
317 -- recheck totality
318 i <- get
319 totcheck (FC "(input)" 0, n)
320 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
321 mapM_ checkDeclTotality (idris_totcheck i)
323process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
324 ctxt <- getContext
325 ist <- get
326 let tm' = simplify ctxt True [] tm
327 iputStrLn (show (delab ist tm'))
328process fn TTShell = do ist <- get
329 let shst = initState (tt_ctxt ist)
330 shst' <- lift $ runShell shst
331 return ()
332process fn Execute = do (m, _) <- elabVal toplevel False
333 (PApp fc
334 (PRef fc (UN "run__IO"))
335 [pexp $ PRef fc (NS (UN "main") ["Main"])])
336-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
337 (tmpn, tmph) <- liftIO tempfile
338 liftIO $ hClose tmph
339 t <- target
340 compile t tmpn m
341 liftIO $ system tmpn
342 return ()
343 where fc = FC "main" 0
344process fn (NewCompile f)
345 = do (m, _) <- elabVal toplevel False
346 (PApp fc (PRef fc (UN "run__IO"))
347 [pexp $ PRef fc (NS (UN "main") ["Main"])])
348 compileEpic f m
349 where fc = FC "main" 0
350process fn (Compile target f)
351 = do (m, _) <- elabVal toplevel False
352 (PApp fc (PRef fc (UN "run__IO"))
353 [pexp $ PRef fc (NS (UN "main") ["Main"])])
354 compile target f m
355 where fc = FC "main" 0
356process fn (LogLvl i) = setLogLevel i
357-- Elaborate as if LHS of a pattern (debug command)
358process fn (Pattelab t)
359 = do (tm, ty) <- elabVal toplevel True t
360 iputStrLn $ show tm ++ "\n\n : " ++ show ty
362process fn (Missing n) = do i <- get
363 case lookupDef Nothing n (tt_ctxt i) of
364 [CaseOp _ _ _ _ _ args t _ _]
365 -> do tms <- genMissing n args t
366 iputStrLn (showSep "\n" (map (showImp True) tms))
367 [] -> iputStrLn $ show n ++ " undefined"
368 _ -> iputStrLn $ "Ambiguous name"
369process fn Metavars
370 = do ist <- get
371 let mvs = idris_metavars ist \\ primDefs
372 case mvs of
373 [] -> iputStrLn "No global metavariables to solve"
374 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
375process fn NOP = return ()
377process fn (SetOpt ErrContext) = setErrContext True
378process fn (UnsetOpt ErrContext) = setErrContext False
379process fn (SetOpt ShowImpl) = setImpShow True
380process fn (UnsetOpt ShowImpl) = setImpShow False
382process fn (SetOpt _) = iputStrLn "Not a valid option"
383process fn (UnsetOpt _) = iputStrLn "Not a valid option"
386classInfo :: ClassInfo -> Idris ()
387classInfo ci = do iputStrLn "Methods:\n"
388 mapM_ dumpMethod (class_methods ci)
389 iputStrLn ""
390 iputStrLn "Instances:\n"
391 mapM_ dumpInstance (class_instances ci)
393dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
394dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
396dumpInstance :: Name -> Idris ()
397dumpInstance n = do i <- get
398 ctxt <- getContext
399 imp <- impShow
400 case lookupTy Nothing n ctxt of
401 ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts
403showTotal t@(Partial (Other ns)) i
404 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
405showTotal t i = show t
406showTotalN i n = case lookupTotal n (tt_ctxt i) of
407 [t] -> showTotal t i
408 _ -> ""
410displayHelp = let vstr = showVersion version in
411 "\nIdris version " ++ vstr ++ "\n" ++
412 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
413 concatMap cmdInfo help
414 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text
415 col c1 c2 l m r =
416 l ++ take (c1 - length l) (repeat ' ') ++
417 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
419parseArgs :: [String] -> [Opt]
420parseArgs [] = []
421parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
422parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
423parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
424parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
425parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)
426parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
427parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
428parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
429parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
430parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
431parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
432parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
433parseArgs ("--help":ns) = Usage : (parseArgs ns)
434parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
435parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
436parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
437parseArgs ("--version":ns) = Ver : (parseArgs ns)
438parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
439parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
440parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
441parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
442parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
443parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
444parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
445parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
446parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
447parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
448parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)
449parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
450parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
451parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
452parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
453parseArgs (n:ns) = Filename n : (parseArgs ns)
455help =
456 [ (["Command"], "Arguments", "Purpose"),
457 ([""], "", ""),
458 (["<expr>"], "", "Evaluate an expression"),
459 ([":t"], "<expr>", "Check the type of an expression"),
460 ([":miss", ":missing"], "<name>", "Show missing clauses"),
461 ([":i", ":info"], "<name>", "Display information about a type class"),
462 ([":total"], "<name>", "Check the totality of a name"),
463 ([":r",":reload"], "", "Reload current file"),
464 ([":l",":load"], "<filename>", "Load a new file"),
465 ([":m",":module"], "<module>", "Import an extra module"),
466 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
467 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
468 ([":p",":prove"], "<name>", "Prove a metavariable"),
469 ([":a",":addproof"], "<name>", "Add proof to source file"),
470 ([":rmproof"], "<name>", "Remove proof from proof stack"),
471 ([":showproof"], "<name>", "Show proof"),
472 ([":proofs"], "", "Show available proofs"),
473 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
474 ([":exec",":execute"], "", "Compile to an executable and run"),
475 ([":?",":h",":help"], "", "Display this help text"),
476 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),
477 ([":unset"], "<option>", "Unset an option"),
478 ([":q",":quit"], "", "Exit the Idris system")
479 ]
481-- invoke as if from command line
482idris :: [Opt] -> IO IState
483idris opts = runInputT defaultSettings $ execStateT (idrisMain opts) idrisInit
485idrisMain :: [Opt] -> Idris ()
486idrisMain opts =
487 do let inputs = opt getFile opts
488 let runrepl = not (NoREPL `elem` opts)
489 let output = opt getOutput opts
490 let newoutput = opt getNewOutput opts
491 let ibcsubdir = opt getIBCSubDir opts
492 let importdirs = opt getImportDir opts
493 let bcs = opt getBC opts
494 let vm = opt getFOVM opts
495 let pkgdirs = opt getPkgDir opts
496 let outty = case opt getOutputTy opts of
497 [] -> Executable
498 xs -> last xs
499 let tgt = case opt getTarget opts of
500 [] -> ViaC
501 xs -> last xs
502 when (DefaultTotal `elem` opts) $ do i <- get
503 put (i { default_total = True })
504 setREPL runrepl
505 setVerbose runrepl
506 setCmdLine opts
507 setOutputTy outty
508 setTarget tgt
509 when (Verbose `elem` opts) $ setVerbose True
510 mapM_ makeOption opts
511 -- if we have the --fovm flag, drop into the first order VM testing
512 case vm of
513 [] -> return ()
514 xs -> liftIO $ mapM_ (fovm tgt outty) xs
515 -- if we have the --bytecode flag, drop into the bytecode assembler
516 case bcs of
517 [] -> return ()
518 xs -> return () -- liftIO $ mapM_ bcAsm xs
519 case ibcsubdir of
520 [] -> setIBCSubDir ""
521 (d:_) -> setIBCSubDir d
522 setImportDirs importdirs
523 addPkgDir "base"
524 mapM_ addPkgDir pkgdirs
525 elabPrims
526 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
527 return ()
528 when runrepl $ iputStrLn banner
529 ist <- get
530 mods <- mapM loadModule inputs
531 ok <- noErrors
532 when ok $ case output of
533 [] -> return ()
534 (o:_) -> process "" (Compile tgt o)
535 when ok $ case newoutput of
536 [] -> return ()
537 (o:_) -> process "" (NewCompile o)
538 when runrepl $ repl ist inputs
539 ok <- noErrors
540 when (not ok) $ liftIO (exitWith (ExitFailure 1))
541 where
542 makeOption (OLogging i) = setLogLevel i
543 makeOption TypeCase = setTypeCase True
544 makeOption TypeInType = setTypeInType True
545 makeOption NoCoverage = setCoverage False
546 makeOption ErrContext = setErrContext True
547 makeOption _ = return ()
549 addPkgDir :: String -> Idris ()
550 addPkgDir p = do ddir <- liftIO $ getDataDir
551 addImportDir (ddir </> p)
553getFile :: Opt -> Maybe String
554getFile (Filename str) = Just str
555getFile _ = Nothing
557getBC :: Opt -> Maybe String
558getBC (BCAsm str) = Just str
559getBC _ = Nothing
561getFOVM :: Opt -> Maybe String
562getFOVM (FOVM str) = Just str
563getFOVM _ = Nothing
565getOutput :: Opt -> Maybe String
566getOutput (Output str) = Just str
567getOutput _ = Nothing
569getNewOutput :: Opt -> Maybe String
570getNewOutput (NewOutput str) = Just str
571getNewOutput _ = Nothing
573getIBCSubDir :: Opt -> Maybe String
574getIBCSubDir (IBCSubDir str) = Just str
575getIBCSubDir _ = Nothing
577getImportDir :: Opt -> Maybe String
578getImportDir (ImportDir str) = Just str
579getImportDir _ = Nothing
581getPkgDir :: Opt -> Maybe String
582getPkgDir (Pkg str) = Just str
583getPkgDir _ = Nothing
585getPkg :: Opt -> Maybe (Bool, String)
586getPkg (PkgBuild str) = Just (False, str)
587getPkg (PkgInstall str) = Just (True, str)
588getPkg _ = Nothing
590getPkgClean :: Opt -> Maybe String
591getPkgClean (PkgClean str) = Just str
592getPkgClean _ = Nothing
594getTarget :: Opt -> Maybe Target
595getTarget (UseTarget x) = Just x
596getTarget _ = Nothing
598getOutputTy :: Opt -> Maybe OutputType
599getOutputTy (OutputTy t) = Just t
600getOutputTy _ = Nothing
602opt :: (Opt -> Maybe a) -> [Opt] -> [a]
603opt = mapMaybe
605ver = showVersion version
607banner = " ____ __ _ \n" ++
608 " / _/___/ /____(_)____ \n" ++
609 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
610 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
611 " /___/\\__,_/_/ /_/____/ Type :? for help \n"