git.iko.soy/Idris-dev
on baff441 help sign in
Idris-dev/src/Idris/REPL.hs
649 lines 26 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
19import Idris.Help
20import Idris.Completion
22import Paths_idris
23import Util.System
24import Util.DynamicLinker
26import Core.Evaluate
27import Core.Execute (execute)
28import Core.ProofShell
29import Core.TT
30import Core.Constraints
32import IRTS.Compiler
33import IRTS.LParser
34import IRTS.CodegenCommon
36-- import RTS.SC
37-- import RTS.Bytecode
38-- import RTS.PreC
39-- import RTS.CodegenC
41import System.Console.Haskeline as H
42import System.FilePath
43import System.Exit
44import System.Environment
45import System.Process
46import System.Directory
47import System.IO
48import Control.Monad
49import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )
50import Control.Monad.Trans ( liftIO, lift )
51import Data.Maybe
52import Data.List
53import Data.Char
54import Data.Version
56import Debug.Trace
58-- | Run the REPL
59repl :: IState -- ^ The initial state
60 -> [FilePath] -- ^ The loaded modules
61 -> InputT Idris ()
62repl orig mods
63 = H.catch
64 (do let quiet = opt_quiet (idris_options orig)
65 let prompt = if quiet
66 then ""
67 else mkPrompt mods ++ "> "
68 x <- getInputLine prompt
69 case x of
70 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
71 return ()
72 Just input -> H.catch
73 (do ms <- lift $ processInput input orig mods
74 case ms of
75 Just mods -> repl orig mods
76 Nothing -> return ())
77 ctrlC)
78 ctrlC
79 where ctrlC :: SomeException -> InputT Idris ()
80 ctrlC e = do lift $ iputStrLn (show e)
81 repl orig mods
83-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
84mkPrompt [] = "Idris"
85mkPrompt [x] = "*" ++ dropExtension x
86mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
88-- | Determine whether a file uses literate syntax
89lit f = case splitExtension f of
90 (_, ".lidr") -> True
91 _ -> False
93processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
94processInput cmd orig inputs
95 = do i <- getIState
96 let opts = idris_options i
97 let quiet = opt_quiet opts
98 let fn = case inputs of
99 (f:_) -> f
100 _ -> ""
101 case parseCmd i cmd of
102 Left err -> do liftIO $ print err
103 return (Just inputs)
104 Right Reload ->
105 do putIState (orig { idris_options = idris_options i })
106 clearErr
107 mods <- mapM loadModule inputs
108 return (Just inputs)
109 Right (Load f) ->
110 do putIState (orig { idris_options = idris_options i })
111 clearErr
112 mod <- loadModule f
113 return (Just [f])
114 Right (ModImport f) ->
115 do clearErr
116 fmod <- loadModule f
117 return (Just (inputs ++ [fmod]))
118 Right Edit -> do edit fn orig
119 return (Just inputs)
120 Right Proofs -> do proofs orig
121 return (Just inputs)
122 Right Quit -> do when (not quiet) (iputStrLn "Bye bye")
123 return Nothing
124 Right cmd -> do idrisCatch (process fn cmd)
125 (\e -> iputStrLn (show e))
126 return (Just inputs)
128resolveProof :: Name -> Idris Name
129resolveProof n'
130 = do i <- getIState
131 ctxt <- getContext
132 n <- case lookupNames Nothing n' ctxt of
133 [x] -> return x
134 [] -> return n'
135 ns -> fail $ pshow i (CantResolveAlts (map show ns))
136 return n
138removeProof :: Name -> Idris ()
139removeProof n =
140 do i <- getIState
141 let proofs = proof_list i
142 let ps = filter ((/= n) . fst) proofs
143 putIState $ i { proof_list = ps }
145edit :: FilePath -> IState -> Idris ()
146edit "" orig = iputStrLn "Nothing to edit"
147edit f orig
148 = do i <- getIState
149 env <- liftIO $ getEnvironment
150 let editor = getEditor env
151 let line = case errLine i of
152 Just l -> " +" ++ show l ++ " "
153 Nothing -> " "
154 let cmd = editor ++ line ++ f
155 liftIO $ system cmd
156 clearErr
157 putIState (orig { idris_options = idris_options i })
158 loadModule f
159 iucheck
160 return ()
161 where getEditor env | Just ed <- lookup "EDITOR" env = ed
162 | Just ed <- lookup "VISUAL" env = ed
163 | otherwise = "vi"
166proofs :: IState -> Idris ()
167proofs orig
168 = do i <- getIState
169 let ps = proof_list i
170 case ps of
171 [] -> iputStrLn "No proofs available"
172 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
174insertScript :: String -> [String] -> [String]
175insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
176insertScript prf (p@"---------- Proofs ----------" : "" : xs)
177 = p : "" : prf : xs
178insertScript prf (x : xs) = x : insertScript prf xs
180process :: FilePath -> Command -> Idris ()
181process fn Help = iputStrLn displayHelp
182process fn (ChangeDirectory f)
183 = do liftIO $ setCurrentDirectory f
184 return ()
185process fn (Eval t)
186 = do (tm, ty) <- elabVal toplevel False t
187 ctxt <- getContext
188 ist <- getIState
189 let tm' = normaliseAll ctxt [] tm
190 let ty' = normaliseAll ctxt [] ty
191 logLvl 3 $ "Raw: " ++ show (tm', ty')
192 imp <- impShow
193 iputStrLn (showImp imp (delab ist tm') ++ " : " ++
194 showImp imp (delab ist ty'))
195process fn (ExecVal t)
196 = do ctxt <- getContext
197 ist <- getIState
198 (tm, ty) <- elabVal toplevel False t
199 let tm' = normaliseAll ctxt [] tm
200 let ty' = normaliseAll ctxt [] ty
201 res <- execute tm'
202 imp <- impShow
203 iputStrLn (showImp imp (delab ist res) ++ " : " ++
204 showImp imp (delab ist ty'))
205 return ()
206process fn (Check (PRef _ n))
207 = do ctxt <- getContext
208 ist <- getIState
209 imp <- impShow
210 case lookupTy Nothing n ctxt of
211 ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++
212 showImp imp (delab ist t)) ts
213 [] -> iputStrLn $ "No such variable " ++ show n
214process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
215 ctxt <- getContext
216 ist <- getIState
217 imp <- impShow
218 let ty' = normaliseC ctxt [] ty
219 iputStrLn (showImp imp (delab ist tm) ++ " : " ++
220 showImp imp (delab ist ty))
222process fn (DocStr n) = do i <- getIState
223 case lookupCtxtName Nothing n (idris_docstrings i) of
224 [] -> iputStrLn $ "No documentation for " ++ show n
225 ns -> mapM_ showDoc ns
226 where showDoc (n, d)
227 = do doc <- getDocs n
228 iputStrLn $ show doc
229process fn Universes = do i <- getIState
230 let cs = idris_constraints i
231-- iputStrLn $ showSep "\n" (map show cs)
232 liftIO $ print (map fst cs)
233 let n = length cs
234 iputStrLn $ "(" ++ show n ++ " constraints)"
235 case ucheck cs of
236 Error e -> iputStrLn $ pshow i e
237 OK _ -> iputStrLn "Universes OK"
238process fn (Defn n) = do i <- getIState
239 iputStrLn "Compiled patterns:\n"
240 liftIO $ print (lookupDef Nothing n (tt_ctxt i))
241 case lookupCtxt Nothing n (idris_patdefs i) of
242 [] -> return ()
243 [d] -> do iputStrLn "Original definiton:\n"
244 mapM_ (printCase i) d
245 case lookupTotal n (tt_ctxt i) of
246 [t] -> iputStrLn (showTotal t i)
247 _ -> return ()
248 where printCase i (_, lhs, rhs)
249 = do liftIO $ putStr $ showImp True (delab i lhs)
250 liftIO $ putStr " = "
251 liftIO $ putStrLn $ showImp True (delab i rhs)
252process fn (TotCheck n) = do i <- getIState
253 case lookupTotal n (tt_ctxt i) of
254 [t] -> iputStrLn (showTotal t i)
255 _ -> return ()
256process fn (DebugInfo n)
257 = do i <- getIState
258 let oi = lookupCtxtName Nothing n (idris_optimisation i)
259 when (not (null oi)) $ iputStrLn (show oi)
260 let si = lookupCtxt Nothing n (idris_statics i)
261 when (not (null si)) $ iputStrLn (show si)
262 let di = lookupCtxt Nothing n (idris_datatypes i)
263 when (not (null di)) $ iputStrLn (show di)
264 let d = lookupDef Nothing n (tt_ctxt i)
265 when (not (null d)) $ liftIO $
266 do print (head d)
267 let cg = lookupCtxtName Nothing n (idris_callgraph i)
268 findUnusedArgs (map fst cg)
269 i <- getIState
270 let cg' = lookupCtxtName Nothing n (idris_callgraph i)
271 sc <- checkSizeChange n
272 iputStrLn $ "Size change: " ++ show sc
273 when (not (null cg')) $ do iputStrLn "Call graph:\n"
274 iputStrLn (show cg')
275process fn (Info n) = do i <- getIState
276 case lookupCtxt Nothing n (idris_classes i) of
277 [c] -> classInfo c
278 _ -> iputStrLn "Not a class"
279process fn (Search t) = iputStrLn "Not implemented"
280process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
281 ctxt <- getContext
282 ist <- getIState
283 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
284 iputStrLn (show (delab ist tm'))
286process fn (RmProof n')
287 = do i <- getIState
288 n <- resolveProof n'
289 let proofs = proof_list i
290 case lookup n proofs of
291 Nothing -> iputStrLn "No proof to remove"
292 Just _ -> do removeProof n
293 insertMetavar n
294 iputStrLn $ "Removed proof " ++ show n
295 where
296 insertMetavar :: Name -> Idris ()
297 insertMetavar n =
298 do i <- getIState
299 let ms = idris_metavars i
300 putIState $ i { idris_metavars = n : ms }
302process fn (AddProof prf)
303 = do let fb = fn ++ "~"
304 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
305 prog <- liftIO $ readFile fb
306 i <- getIState
307 let proofs = proof_list i
308 n' <- case prf of
309 Nothing -> case proofs of
310 [] -> fail "No proof to add"
311 ((x, p) : _) -> return x
312 Just nm -> return nm
313 n <- resolveProof n'
314 case lookup n proofs of
315 Nothing -> iputStrLn "No proof to add"
316 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
317 liftIO $ writeFile fn (unlines prog')
318 removeProof n
319 iputStrLn $ "Added proof " ++ show n
320 where ls = (lines prog)
322process fn (ShowProof n')
323 = do i <- getIState
324 n <- resolveProof n'
325 let proofs = proof_list i
326 case lookup n proofs of
327 Nothing -> iputStrLn "No proof to show"
328 Just p -> iputStrLn $ showProof False n p
330process fn (Prove n')
331 = do ctxt <- getContext
332 ist <- getIState
333 n <- case lookupNames Nothing n' ctxt of
334 [x] -> return x
335 [] -> return n'
336 ns -> fail $ pshow ist (CantResolveAlts (map show ns))
337 prover (lit fn) n
338 -- recheck totality
339 i <- getIState
340 totcheck (FC "(input)" 0, n)
341 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
342 mapM_ checkDeclTotality (idris_totcheck i)
344process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
345 ctxt <- getContext
346 ist <- getIState
347 let tm' = hnf ctxt [] tm
348 iputStrLn (show (delab ist tm'))
349process fn TTShell = do ist <- getIState
350 let shst = initState (tt_ctxt ist)
351 runShell shst
352 return ()
353process fn Execute = do (m, _) <- elabVal toplevel False
354 (PApp fc
355 (PRef fc (UN "run__IO"))
356 [pexp $ PRef fc (NS (UN "main") ["Main"])])
357-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
358 (tmpn, tmph) <- liftIO tempfile
359 liftIO $ hClose tmph
360 t <- target
361 compile t tmpn m
362 liftIO $ system tmpn
363 return ()
364 where fc = FC "main" 0
365process fn (NewCompile f)
366 = do (m, _) <- elabVal toplevel False
367 (PApp fc (PRef fc (UN "run__IO"))
368 [pexp $ PRef fc (NS (UN "main") ["Main"])])
369 compileEpic f m
370 where fc = FC "main" 0
371process fn (Compile target f)
372 = do (m, _) <- elabVal toplevel False
373 (PApp fc (PRef fc (UN "run__IO"))
374 [pexp $ PRef fc (NS (UN "main") ["Main"])])
375 compile target f m
376 where fc = FC "main" 0
377process fn (LogLvl i) = setLogLevel i
378-- Elaborate as if LHS of a pattern (debug command)
379process fn (Pattelab t)
380 = do (tm, ty) <- elabVal toplevel True t
381 iputStrLn $ show tm ++ "\n\n : " ++ show ty
383process fn (Missing n) = do i <- getIState
384 case lookupDef Nothing n (tt_ctxt i) of
385 [CaseOp _ _ _ _ _ args t _ _]
386 -> do tms <- genMissing n args t
387 iputStrLn (showSep "\n" (map (showImp True) tms))
388 [] -> iputStrLn $ show n ++ " undefined"
389 _ -> iputStrLn $ "Ambiguous name"
390process fn (DynamicLink l) = do i <- getIState
391 let lib = trim l
392 handle <- lift $ tryLoadLib lib
393 case handle of
394 Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""
395 Just x -> do let libs = idris_dynamic_libs i
396 putIState $ i { idris_dynamic_libs = x:libs }
397 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
398process fn ListDynamic = do i <- getIState
399 iputStrLn "Dynamic libraries:"
400 showLibs $ idris_dynamic_libs i
401 where showLibs [] = return ()
402 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
403process fn Metavars
404 = do ist <- getIState
405 let mvs = idris_metavars ist \\ primDefs
406 case mvs of
407 [] -> iputStrLn "No global metavariables to solve"
408 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
409process fn NOP = return ()
411process fn (SetOpt ErrContext) = setErrContext True
412process fn (UnsetOpt ErrContext) = setErrContext False
413process fn (SetOpt ShowImpl) = setImpShow True
414process fn (UnsetOpt ShowImpl) = setImpShow False
416process fn (SetOpt _) = iputStrLn "Not a valid option"
417process fn (UnsetOpt _) = iputStrLn "Not a valid option"
420classInfo :: ClassInfo -> Idris ()
421classInfo ci = do iputStrLn "Methods:\n"
422 mapM_ dumpMethod (class_methods ci)
423 iputStrLn ""
424 iputStrLn "Instances:\n"
425 mapM_ dumpInstance (class_instances ci)
427dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
428dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
430dumpInstance :: Name -> Idris ()
431dumpInstance n = do i <- getIState
432 ctxt <- getContext
433 imp <- impShow
434 case lookupTy Nothing n ctxt of
435 ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts
437showTotal t@(Partial (Other ns)) i
438 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
439showTotal t i = show t
440showTotalN i n = case lookupTotal n (tt_ctxt i) of
441 [t] -> showTotal t i
442 _ -> ""
444displayHelp = let vstr = showVersion version in
445 "\nIdris version " ++ vstr ++ "\n" ++
446 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
447 concatMap cmdInfo helphead ++
448 concatMap cmdInfo help
449 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
450 col c1 c2 l m r =
451 l ++ take (c1 - length l) (repeat ' ') ++
452 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
454parseTarget :: String -> Target
455parseTarget "C" = ViaC
456parseTarget "Java" = ViaJava
457parseTarget "bytecode" = Bytecode
458parseTarget "javascript" = ViaJavaScript
459parseTarget "node" = ViaNode
460parseTarget _ = error "unknown target" -- FIXME: partial function
462parseArgs :: [String] -> [Opt]
463parseArgs [] = []
464parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
465parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
466parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
467parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
468parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
469parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)
470parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
471parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
472parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
473parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
474parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
475parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
476parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
477parseArgs ("--help":ns) = Usage : (parseArgs ns)
478parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
479parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
480parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
481parseArgs ("--version":ns) = Ver : (parseArgs ns)
482parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
483parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
484parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
485parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
486parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
487parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
488parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
489parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
490parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
491parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
492parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)
493parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
494parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
495parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
496parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
497parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
498parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)
499parseArgs (n:ns) = Filename n : (parseArgs ns)
501helphead =
502 [ (["Command"], SpecialHeaderArg, "Purpose"),
503 ([""], NoArg, "")
504 ]
507replSettings :: Settings Idris
508replSettings = setComplete replCompletion defaultSettings
510-- invoke as if from command line
511idris :: [Opt] -> IO IState
512idris opts = execStateT (idrisMain opts) idrisInit
514idrisMain :: [Opt] -> Idris ()
515idrisMain opts =
516 do let inputs = opt getFile opts
517 let quiet = Quiet `elem` opts
518 let runrepl = not (NoREPL `elem` opts)
519 let output = opt getOutput opts
520 let newoutput = opt getNewOutput opts
521 let ibcsubdir = opt getIBCSubDir opts
522 let importdirs = opt getImportDir opts
523 let bcs = opt getBC opts
524 let vm = opt getFOVM opts
525 let pkgdirs = opt getPkgDir opts
526 let outty = case opt getOutputTy opts of
527 [] -> Executable
528 xs -> last xs
529 let tgt = case opt getTarget opts of
530 [] -> ViaC
531 xs -> last xs
532 when (DefaultTotal `elem` opts) $ do i <- getIState
533 putIState (i { default_total = True })
534 mapM_ addLangExt (opt getLanguageExt opts)
535 setREPL runrepl
536 setQuiet quiet
537 setVerbose runrepl
538 setCmdLine opts
539 setOutputTy outty
540 setTarget tgt
541 when (Verbose `elem` opts) $ setVerbose True
542 mapM_ makeOption opts
543 -- if we have the --fovm flag, drop into the first order VM testing
544 case vm of
545 [] -> return ()
546 xs -> liftIO $ mapM_ (fovm tgt outty) xs
547 -- if we have the --bytecode flag, drop into the bytecode assembler
548 case bcs of
549 [] -> return ()
550 xs -> return () -- liftIO $ mapM_ bcAsm xs
551 case ibcsubdir of
552 [] -> setIBCSubDir ""
553 (d:_) -> setIBCSubDir d
554 setImportDirs importdirs
555 addPkgDir "base"
556 mapM_ addPkgDir pkgdirs
557 elabPrims
558 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
559 return ()
560 when (runrepl && not quiet) $ iputStrLn banner
561 ist <- getIState
562 mods <- mapM loadModule inputs
563 ok <- noErrors
564 when ok $ case output of
565 [] -> return ()
566 (o:_) -> process "" (Compile tgt o)
567 when ok $ case newoutput of
568 [] -> return ()
569 (o:_) -> process "" (NewCompile o)
570 when runrepl $ runInputT replSettings $ repl ist inputs
571 ok <- noErrors
572 when (not ok) $ liftIO (exitWith (ExitFailure 1))
573 where
574 makeOption (OLogging i) = setLogLevel i
575 makeOption TypeCase = setTypeCase True
576 makeOption TypeInType = setTypeInType True
577 makeOption NoCoverage = setCoverage False
578 makeOption ErrContext = setErrContext True
579 makeOption _ = return ()
581 addPkgDir :: String -> Idris ()
582 addPkgDir p = do ddir <- liftIO $ getDataDir
583 addImportDir (ddir </> p)
585getFile :: Opt -> Maybe String
586getFile (Filename str) = Just str
587getFile _ = Nothing
589getBC :: Opt -> Maybe String
590getBC (BCAsm str) = Just str
591getBC _ = Nothing
593getFOVM :: Opt -> Maybe String
594getFOVM (FOVM str) = Just str
595getFOVM _ = Nothing
597getOutput :: Opt -> Maybe String
598getOutput (Output str) = Just str
599getOutput _ = Nothing
601getNewOutput :: Opt -> Maybe String
602getNewOutput (NewOutput str) = Just str
603getNewOutput _ = Nothing
605getIBCSubDir :: Opt -> Maybe String
606getIBCSubDir (IBCSubDir str) = Just str
607getIBCSubDir _ = Nothing
609getImportDir :: Opt -> Maybe String
610getImportDir (ImportDir str) = Just str
611getImportDir _ = Nothing
613getPkgDir :: Opt -> Maybe String
614getPkgDir (Pkg str) = Just str
615getPkgDir _ = Nothing
617getPkg :: Opt -> Maybe (Bool, String)
618getPkg (PkgBuild str) = Just (False, str)
619getPkg (PkgInstall str) = Just (True, str)
620getPkg _ = Nothing
622getPkgClean :: Opt -> Maybe String
623getPkgClean (PkgClean str) = Just str
624getPkgClean _ = Nothing
626getTarget :: Opt -> Maybe Target
627getTarget (UseTarget x) = Just x
628getTarget _ = Nothing
630getOutputTy :: Opt -> Maybe OutputType
631getOutputTy (OutputTy t) = Just t
632getOutputTy _ = Nothing
634getLanguageExt :: Opt -> Maybe LanguageExt
635getLanguageExt (Extension e) = Just e
636getLanguageExt _ = Nothing
638opt :: (Opt -> Maybe a) -> [Opt] -> [a]
639opt = mapMaybe
641ver = showVersion version
643banner = " ____ __ _ \n" ++
644 " / _/___/ /____(_)____ \n" ++
645 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
646 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
647 " /___/\\__,_/_/ /_/____/ Type :? for help \n"