git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/REPL.hs
1752 lines 77 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards, CPP #-}
4module Idris.REPL where
6import Idris.AbsSyntax
7import Idris.ASTUtils
8import Idris.Apropos (apropos)
9import Idris.REPLParser
10import Idris.ElabDecls
11import Idris.ElabTerm
12import Idris.Erasure
13import Idris.Error
14import Idris.ErrReverse
15import Idris.Delaborate
16import Idris.Docstrings (Docstring, overview, renderDocstring)
17import Idris.IdrisDoc
18import Idris.Prover
19import Idris.Parser hiding (indent)
20import Idris.Primitives
21import Idris.Coverage
22import Idris.Docs hiding (Doc)
23import Idris.Help
24import Idris.Completion
25import qualified Idris.IdeSlave as IdeSlave
26import Idris.Chaser
27import Idris.Imports
28import Idris.Colours hiding (colourise)
29import Idris.Inliner
30import Idris.CaseSplit
31import Idris.DeepSeq
32import Idris.Output
33import Idris.Interactive
34import Idris.WhoCalls
35import Idris.TypeSearch (searchByType)
37import Idris.Elab.Type
38import Idris.Elab.Clause
39import Idris.Elab.Data
40import Idris.Elab.Value
42import Version_idris (gitHash)
43import Util.System
44import Util.DynamicLinker
45import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)
46import Util.Pretty hiding ((</>))
48import Idris.Core.Evaluate
49import Idris.Core.Execute (execute)
50import Idris.Core.TT
51import Idris.Core.Constraints
53import IRTS.Compiler
54import IRTS.CodegenCommon
55import IRTS.System
57import Control.Category
58import Prelude hiding ((.), id)
59import Data.List.Split (splitOn)
60import Data.List (groupBy)
61import qualified Data.Text as T
63import Text.Trifecta.Result(Result(..))
65-- import RTS.SC
66-- import RTS.Bytecode
67-- import RTS.PreC
68-- import RTS.CodegenC
69import System.Console.Haskeline as H
70import System.FilePath
71import System.Exit
72import System.Environment
73import System.Process
74import System.Directory
75import System.IO
76import Control.Monad
77import Control.Monad.Trans.Error (ErrorT(..))
78import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
79import Control.Monad.Trans ( lift )
80import Control.Concurrent.MVar
81import Network
82import Control.Concurrent
83import Data.Maybe
84import Data.List hiding (group)
85import Data.Char
86import Data.Version
87import Data.Word (Word)
88import Data.Either (partitionEithers)
89import Control.DeepSeq
91import Numeric ( readHex )
93import Debug.Trace
95-- | Run the REPL
96repl :: IState -- ^ The initial state
97 -> [FilePath] -- ^ The loaded modules
98 -> InputT Idris ()
99repl orig mods
100 = -- H.catch
101 do let quiet = opt_quiet (idris_options orig)
102 i <- lift getIState
103 let colour = idris_colourRepl i
104 let theme = idris_colourTheme i
105 let mvs = idris_metavars i
106 let prompt = if quiet
107 then ""
108 else showMVs colour theme mvs ++
109 let str = mkPrompt mods ++ ">" in
110 (if colour then colourisePrompt theme str else str) ++ " "
111 x <- H.catch (getInputLine prompt)
112 (ctrlC (return Nothing))
113 case x of
114 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
115 return ()
116 Just input -> -- H.catch
117 do ms <- H.catch (lift $ processInput input orig mods)
118 (ctrlC (return (Just mods)))
119 case ms of
120 Just mods -> repl orig mods
121 Nothing -> return ()
122-- ctrlC)
123-- ctrlC
124 where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
125 ctrlC act e = do lift $ iputStrLn (show e)
126 act -- repl orig mods
128 showMVs c thm [] = ""
129 showMVs c thm ms = "Metavariables: " ++
130 show' 4 c thm (map fst ms) ++ "\n"
132 show' 0 c thm ms = let l = length ms in
133 "... ( + " ++ show l
134 ++ " other"
135 ++ if l == 1 then ")" else "s)"
136 show' n c thm [m] = showM c thm m
137 show' n c thm (m : ms) = showM c thm m ++ ", " ++
138 show' (n - 1) c thm ms
140 showM c thm n = if c then colouriseFun thm (show n)
141 else show n
143-- | Run the REPL seDver
144startServer :: PortID -> IState -> [FilePath] -> Idris ()
145startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)
146 return ()
147 where serverLoop port = withSocketsDo $
148 do sock <- listenOnLocalhost port
149 loop fn orig { idris_colourRepl = False } sock
151 fn = case fn_in of
152 (f:_) -> f
153 _ -> ""
155 loop fn ist sock
156 = do (h,_,_) <- accept sock
157 hSetEncoding h utf8
158 cmd <- hGetLine h
159 let isth = case idris_outputmode ist of
160 RawOutput _ -> ist {idris_outputmode = RawOutput h}
161 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}
162 (ist', fn) <- processNetCmd orig isth h fn cmd
163 hClose h
164 loop fn ist' sock
166processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
167 IO (IState, FilePath)
168processNetCmd orig i h fn cmd
169 = do res <- case parseCmd i "(net)" cmd of
170 Failure err -> return (Left (Msg " invalid command"))
171 Success (Right c) -> runErrorT $ evalStateT (processNet fn c) i
172 Success (Left err) -> return (Left (Msg err))
173 case res of
174 Right x -> return x
175 Left err -> do hPutStrLn h (show err)
176 return (i, fn)
177 where
178 processNet fn Reload = processNet fn (Load fn Nothing)
179 processNet fn (Load f toline) =
180 do let ist = orig { idris_options = idris_options i
181 , idris_colourTheme = idris_colourTheme i
182 , idris_colourRepl = False
183 }
184 putIState ist
185 setErrContext True
186 setOutH h
187 setQuiet True
188 setVerbose False
189 mods <- loadInputs [f] toline
190 ist <- getIState
191 return (ist, f)
192 processNet fn c = do process fn c
193 ist <- getIState
194 return (ist, fn)
195 setOutH :: Handle -> Idris ()
196 setOutH h =
197 do ist <- getIState
198 putIState $ case idris_outputmode ist of
199 RawOutput _ -> ist {idris_outputmode = RawOutput h}
200 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}
202-- | Run a command on the server on localhost
203runClient :: PortID -> String -> IO ()
204runClient port str = withSocketsDo $ do
205 h <- connectTo "localhost" port
206 hSetEncoding h utf8
207 hPutStrLn h str
208 resp <- hGetResp "" h
209 putStr resp
210 hClose h
211 where hGetResp acc h = do eof <- hIsEOF h
212 if eof then return acc
213 else do l <- hGetLine h
214 hGetResp (acc ++ l ++ "\n") h
216initIdeslaveSocket :: IO Handle
217initIdeslaveSocket = do
218 (sock, port) <- listenOnLocalhostAnyPort
219 putStrLn $ show port
220 (h, _, _) <- accept sock
221 hSetEncoding h utf8
222 return h
224-- | Run the IdeSlave
225ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()
226ideslaveStart s orig mods
227 = do h <- runIO $ if s then initIdeslaveSocket else return stdout
228 setIdeSlave True h
229 i <- getIState
230 case idris_outputmode i of
231 IdeSlave n h ->
232 do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n
233 case mods of
234 a:_ -> runIdeSlaveCommand h n i "" [] (IdeSlave.LoadFile a Nothing)
235 _ -> return ()
236 ideslave h orig mods
238ideslave :: Handle -> IState -> [FilePath] -> Idris ()
239ideslave h orig mods
240 = do idrisCatch
241 (do let inh = if h == stdout then stdin else h
242 len' <- runIO $ IdeSlave.getLen inh
243 len <- case len' of
244 Left err -> ierror err
245 Right n -> return n
246 l <- runIO $ IdeSlave.getNChar inh len ""
247 (sexp, id) <- case IdeSlave.parseMessage l of
248 Left err -> ierror err
249 Right (sexp, id) -> return (sexp, id)
250 i <- getIState
251 putIState $ i { idris_outputmode = (IdeSlave id h) }
252 idrisCatch -- to report correct id back!
253 (do let fn = case mods of
254 (f:_) -> f
255 _ -> ""
256 case IdeSlave.sexpToCommand sexp of
257 Just cmd -> runIdeSlaveCommand h id orig fn mods cmd
258 Nothing -> iPrintError "did not understand" )
259 (\e -> do iPrintError $ show e))
260 (\e -> do iPrintError $ show e)
261 ideslave h orig mods
263-- | Run IDESlave commands
264runIdeSlaveCommand :: Handle -- ^^ The handle for communication
265 -> Integer -- ^^ The continuation ID for the client
266 -> IState -- ^^ The original IState
267 -> FilePath -- ^^ The current open file
268 -> [FilePath] -- ^^ The currently loaded modules
269 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process
270 -> Idris ()
271runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =
272 do c <- colourise
273 i <- getIState
274 case parseCmd i "(input)" cmd of
275 Failure err -> iPrintError $ show (fixColour False err)
276 Success (Right (Prove n')) ->
277 idrisCatch
278 (do process fn (Prove n')
279 isetPrompt (mkPrompt mods)
280 case idris_outputmode i of
281 IdeSlave n h -> -- signal completion of proof to ide
282 runIO . hPutStrLn h $
283 IdeSlave.convSExp "return"
284 (IdeSlave.SymbolAtom "ok", "")
285 n
286 _ -> return ())
287 (\e -> do ist <- getIState
288 isetPrompt (mkPrompt mods)
289 case idris_outputmode i of
290 IdeSlave n h ->
291 runIO . hPutStrLn h $
292 IdeSlave.convSExp "abandon-proof" "Abandoned" n
293 _ -> return ()
294 iRenderError $ pprintErr ist e)
295 Success (Right cmd) -> idrisCatch
296 (ideslaveProcess fn cmd)
297 (\e -> getIState >>= iRenderError . flip pprintErr e)
298runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =
299 do (unused, compls) <- replCompletion (reverse str, "")
300 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
301 IdeSlave.toSExp (map replacement compls,
302 reverse unused)]
303 runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id
304runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
305 do i <- getIState
306 clearErr
307 putIState (orig { idris_options = idris_options i,
308 idris_outputmode = (IdeSlave id h) })
309 loadInputs [filename] toline
310 isetPrompt (mkPrompt [filename])
311 -- Report either success or failure
312 i <- getIState
313 case (errSpan i) of
314 Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
315 IdeSlave.SexpList []])
316 (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
317 IdeSlave.toSExp fc])
318 (idris_parsedSpan i)
319 in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
320 Just x -> iPrintError $ "didn't load " ++ filename
321 ideslave h orig [filename]
322runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
323 case splitName name of
324 Left err -> iPrintError err
325 Right n -> process "(ideslave)"
326 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
327 where splitName :: String -> Either String Name
328 splitName s = case reverse $ splitOn "." s of
329 [] -> Left ("Didn't understand name '" ++ s ++ "'")
330 [n] -> Right $ sUN n
331 (n:ns) -> Right $ sNS (sUN n) ns
332runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =
333 case parseConst orig name of
334 Success c -> process "(ideslave)" (DocStr (Right c))
335 Failure _ ->
336 case splitName name of
337 Left err -> iPrintError err
338 Right n -> process "(ideslave)" (DocStr (Left n))
339runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =
340 process fn (CaseSplitAt False line (sUN name))
341runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =
342 process fn (AddClauseFrom False line (sUN name))
343runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =
344 process fn (AddProofClauseFrom False line (sUN name))
345runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =
346 process fn (AddMissing False line (sUN name))
347runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =
348 process fn (MakeWith False line (sUN name))
349runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =
350 doProofSearch fn False r line (sUN name) (map sUN hints) depth
351runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =
352 case splitName name of
353 Left err -> iPrintError err
354 Right n -> process fn (MakeLemma False line n)
355runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =
356 process fn (Apropos a)
357runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =
358 do ist <- getIState
359 let opts = idris_options ist
360 let impshow = opt_showimp opts
361 let errCtxt = opt_errContext opts
362 let options = (IdeSlave.SymbolAtom "ok",
363 [(IdeSlave.SymbolAtom "show-implicits", impshow),
364 (IdeSlave.SymbolAtom "error-context", errCtxt)])
365 runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id
366runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =
367 do setImpShow b
368 let msg = (IdeSlave.SymbolAtom "ok", b)
369 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
370runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
371 do setErrContext b
372 let msg = (IdeSlave.SymbolAtom "ok", b)
373 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
374runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =
375 do ist <- getIState
376 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
377 let ppo = ppOptionIst ist
378 -- splitMvs is a list of pairs of names and their split types
379 let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
380 -- mvOutput is the pretty-printed version ready for conversion to SExpr
381 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
382 mapPair show
383 (\(hs, c, pc) ->
384 let bnd = [ n | (n,_,_) <- hs ] in
385 let bnds = inits bnd in
386 (map (\(bnd, h) -> processPremise ist bnd h)
387 (zip bnds hs),
388 render ist bnd c pc))
389 splitMvs
390 runIO . hPutStrLn h $
391 IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
392 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
393 mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
395 -- | Split a function type into a pair of premises, conclusion.
396 -- Each maintains both the original and delaborated versions.
397 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
398 splitPi ist (Bind n (Pi t _) rest) =
399 let (hs, c, pc) = splitPi ist rest in
400 ((n, t, delabTy' ist [] t False False):hs,
401 c, delabTy' ist [] c False False)
402 splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
404 -- | Get the types of a list of metavariable names
405 mvTys :: IState -> [Name] -> [(Name, Type)]
406 mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
408 -- | Show a type and its corresponding PTerm in a format suitable
409 -- for the IDE - that is, pretty-printed and annotated.
410 render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
411 render ist bnd t pt =
412 let prettyT = pprintPTerm (ppOptionIst ist)
413 (zip bnd (repeat False))
414 []
415 (idris_infixes ist)
416 pt
417 in
418 displaySpans .
419 renderPretty 0.9 cols .
420 fmap (fancifyAnnots ist) .
421 annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
422 prettyT
424 -- | Juggle the bits of a premise to prepare for output.
425 processPremise :: IState
426 -> [Name] -- ^ the names to highlight as bound
427 -> (Name, Type, PTerm)
428 -> (String,
429 String,
430 SpanList OutputAnnotation)
431 processPremise ist bnd (n, t, pt) =
432 let (out, spans) = render ist bnd t pt in
433 (show n , out, spans)
435runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =
436 case splitName n of
437 Left err -> iPrintError err
438 Right n -> do calls <- whoCalls n
439 ist <- getIState
440 let msg = (IdeSlave.SymbolAtom "ok",
441 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
442 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
443 where pn ist = displaySpans .
444 renderPretty 0.9 1000 .
445 fmap (fancifyAnnots ist) .
446 prettyName True True []
447runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =
448 case splitName n of
449 Left err -> iPrintError err
450 Right n -> do calls <- callsWho n
451 ist <- getIState
452 let msg = (IdeSlave.SymbolAtom "ok",
453 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
454 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
455 where pn ist = displaySpans .
456 renderPretty 0.9 1000 .
457 fmap (fancifyAnnots ist) .
458 prettyName True True []
460runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =
461 do ctxt <- getContext
462 ist <- getIState
463 let tm' = force (normaliseAll ctxt [] tm)
464 ptm = annotate (AnnTerm bnd tm')
465 (pprintPTerm (ppOptionIst ist)
466 bnd
467 []
468 (idris_infixes ist)
469 (delab ist tm'))
470 msg = (IdeSlave.SymbolAtom "ok",
471 displaySpans .
472 renderPretty 0.9 80 .
473 fmap (fancifyAnnots ist) $ ptm)
474 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
475runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
476 ideSlaveForceTermImplicits h id bnd True tm
477runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
478 ideSlaveForceTermImplicits h id bnd False tm
479runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =
480 case splitName name of
481 Left err -> iPrintError err
482 Right n -> process "(ideslave)" (PrintDef n)
483 where splitName :: String -> Either String Name
484 splitName s = case reverse $ splitOn "." s of
485 [] -> Left ("Didn't understand name '" ++ s ++ "'")
486 [n] -> Right $ sUN n
487 (n:ns) -> Right $ sNS (sUN n) ns
490-- | Show a term for IDESlave with the specified implicitness
491ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
492ideSlaveForceTermImplicits h id bnd impl tm =
493 do ist <- getIState
494 let expl = annotate (AnnTerm bnd tm)
495 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
496 bnd [] (idris_infixes ist)
497 (delab ist tm))
498 msg = (IdeSlave.SymbolAtom "ok",
499 displaySpans .
500 renderPretty 0.9 80 .
501 fmap (fancifyAnnots ist) $ expl)
502 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
504splitName :: String -> Either String Name
505splitName s = case reverse $ splitOn "." s of
506 [] -> Left ("Didn't understand name '" ++ s ++ "'")
507 [n] -> Right $ sUN n
508 (n:ns) -> Right $ sNS (sUN n) ns
510ideslaveProcess :: FilePath -> Command -> Idris ()
511ideslaveProcess fn Warranty = process fn Warranty
512ideslaveProcess fn Help = process fn Help
513ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
514 iPrintResult "changed directory to"
515ideslaveProcess fn (Eval t) = process fn (Eval t)
516ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)
517 iPrintResult "defined"
518ideslaveProcess fn (Undefine n) = process fn (Undefine n)
519ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
520ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
521ideslaveProcess fn (Check t) = process fn (Check t)
522ideslaveProcess fn (DocStr n) = process fn (DocStr n)
523ideslaveProcess fn Universes = process fn Universes
524ideslaveProcess fn (Defn n) = do process fn (Defn n)
525 iPrintResult ""
526ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
527ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
528 iPrintResult ""
529ideslaveProcess fn (Search t) = process fn (Search t)
530ideslaveProcess fn (Spec t) = process fn (Spec t)
531-- RmProof and AddProof not supported!
532ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
533ideslaveProcess fn (HNF t) = process fn (HNF t)
534--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
535ideslaveProcess fn (TestInline t) = process fn (TestInline t)
537ideslaveProcess fn Execute = do process fn Execute
538 iPrintResult ""
539ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)
540 iPrintResult ""
541ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
542 iPrintResult ""
543ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
544ideslaveProcess fn (Missing n) = process fn (Missing n)
545ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
546 iPrintResult ""
547ideslaveProcess fn ListDynamic = do process fn ListDynamic
548 iPrintResult ""
549ideslaveProcess fn Metavars = process fn Metavars
550ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
551 iPrintResult ""
552ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
553 iPrintResult ""
554ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
555 iPrintResult ""
556ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
557 iPrintResult ""
558ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)
559 iPrintResult ""
560ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)
561 iPrintResult ""
562ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
563ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
564ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)
565ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)
566ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
567ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
568ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
569ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
570ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
571 iPrintResult ""
572ideslaveProcess fn (Apropos a) = do process fn (Apropos a)
573 iPrintResult ""
574ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)
575ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)
576ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)
577ideslaveProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm)
578ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
581-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
582mkPrompt [] = "Idris"
583mkPrompt [x] = "*" ++ dropExtension x
584mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
586-- | Determine whether a file uses literate syntax
587lit f = case splitExtension f of
588 (_, ".lidr") -> True
589 _ -> False
591processInput :: String ->
592 IState -> [FilePath] -> Idris (Maybe [FilePath])
593processInput cmd orig inputs
594 = do i <- getIState
595 let opts = idris_options i
596 let quiet = opt_quiet opts
597 let fn = case inputs of
598 (f:_) -> f
599 _ -> ""
600 c <- colourise
601 case parseCmd i "(input)" cmd of
602 Failure err -> do iputStrLn $ show (fixColour c err)
603 return (Just inputs)
604 Success (Right Reload) ->
605 do putIState $ orig { idris_options = idris_options i
606 , idris_colourTheme = idris_colourTheme i
607 }
608 clearErr
609 mods <- loadInputs inputs Nothing
610 return (Just inputs)
611 Success (Right (Load f toline)) ->
612 do putIState orig { idris_options = idris_options i
613 , idris_colourTheme = idris_colourTheme i
614 }
615 clearErr
616 mod <- loadInputs [f] toline
617 return (Just [f])
618 Success (Right (ModImport f)) ->
619 do clearErr
620 fmod <- loadModule f
621 return (Just (inputs ++ [fmod]))
622 Success (Right Edit) -> do -- takeMVar stvar
623 edit fn orig
624 return (Just inputs)
625 Success (Right Proofs) -> do proofs orig
626 return (Just inputs)
627 Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")
628 return Nothing
629 Success (Right cmd ) -> do idrisCatch (process fn cmd)
630 (\e -> do msg <- showErr e ; iputStrLn msg)
631 return (Just inputs)
632 Success (Left err) -> do runIO $ putStrLn err
633 return (Just inputs)
635resolveProof :: Name -> Idris Name
636resolveProof n'
637 = do i <- getIState
638 ctxt <- getContext
639 n <- case lookupNames n' ctxt of
640 [x] -> return x
641 [] -> return n'
642 ns -> ierror (CantResolveAlts ns)
643 return n
645removeProof :: Name -> Idris ()
646removeProof n =
647 do i <- getIState
648 let proofs = proof_list i
649 let ps = filter ((/= n) . fst) proofs
650 putIState $ i { proof_list = ps }
652edit :: FilePath -> IState -> Idris ()
653edit "" orig = iputStrLn "Nothing to edit"
654edit f orig
655 = do i <- getIState
656 env <- runIO $ getEnvironment
657 let editor = getEditor env
658 let line = case errSpan i of
659 Just l -> " +" ++ show (fst (fc_start l)) ++ " "
660 Nothing -> " "
661 let cmd = editor ++ line ++ fixName f
662 runIO $ system cmd
663 clearErr
664 putIState $ orig { idris_options = idris_options i
665 , idris_colourTheme = idris_colourTheme i
666 }
667 loadInputs [f] Nothing
668-- clearOrigPats
669 iucheck
670 return ()
671 where getEditor env | Just ed <- lookup "EDITOR" env = ed
672 | Just ed <- lookup "VISUAL" env = ed
673 | otherwise = "vi"
674 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file
675 | otherwise = addExtension file "idr"
679proofs :: IState -> Idris ()
680proofs orig
681 = do i <- getIState
682 let ps = proof_list i
683 case ps of
684 [] -> iputStrLn "No proofs available"
685 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
687insertScript :: String -> [String] -> [String]
688insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
689insertScript prf (p@"---------- Proofs ----------" : "" : xs)
690 = p : "" : prf : xs
691insertScript prf (x : xs) = x : insertScript prf xs
693process :: FilePath -> Command -> Idris ()
694process fn Help = iPrintResult displayHelp
695process fn Warranty = iPrintResult warranty
696process fn (ChangeDirectory f)
697 = do runIO $ setCurrentDirectory f
698 return ()
699process fn (Eval t)
700 = withErrorReflection $ do logLvl 5 $ show t
701 getIState >>= flip warnDisamb t
702 (tm, ty) <- elabVal recinfo ERHS t
703 ctxt <- getContext
704 let tm' = force (normaliseAll ctxt [] tm)
705 let ty' = force (normaliseAll ctxt [] ty)
706 -- Add value to context, call it "it"
707 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
708 ist <- getIState
709 logLvl 3 $ "Raw: " ++ show (tm', ty')
710 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
711 let tmDoc = pprintDelab ist tm'
712 tyDoc = pprintDelab ist ty'
713 iPrintTermWithType tmDoc tyDoc
716process fn (NewDefn decls) = do
717 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
718 mapM_ defineName namedGroups where
719 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls
720 getName :: PDecl -> Maybe Name
721 getName (PTy docs argdocs syn fc opts name ty) = Just name
722 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
723 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)
724 getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name
725 getName _ = Nothing
726 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
727 getClauseName (PClause fc name whole with rhs whereBlock) = name
728 getClauseName (PWith fc name whole with rhs whereBlock) = name
729 defineName :: [PDecl] -> Idris ()
730 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
731 elabDecl EAll recinfo tyDecl
732 elabClauses recinfo fc opts name (concatMap getClauses decls)
733 setReplDefined (Just name)
734 defineName [PClauses fc opts _ [clause]] = do
735 let pterm = getRHS clause
736 (tm,ty) <- elabVal recinfo ERHS pterm
737 ctxt <- getContext
738 let tm' = force (normaliseAll ctxt [] tm)
739 let ty' = force (normaliseAll ctxt [] ty)
740 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
741 setReplDefined (Just $ getClauseName clause)
742 defineName (PClauses{} : _) = tclift $ tfail (Msg "Only one function body is allowed without a type declaration.")
743 -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
744 defineName (PFix fc fixity strs : defns) = do
745 fmodifyState idris_fixities (map (Fix fixity) strs ++)
746 unless (null defns) $ defineName defns
747 defineName (PSyntax _ syntax:_) = do
748 i <- get
749 put (addReplSyntax i syntax)
750 defineName decls = do
751 elabDecls toplevel (map fixClauses decls)
752 setReplDefined (getName (head decls))
753 getClauses (PClauses fc opts name clauses) = clauses
754 getClauses _ = []
755 getRHS :: PClause -> PTerm
756 getRHS (PClause fc name whole with rhs whereBlock) = rhs
757 getRHS (PWith fc name whole with rhs whereBlock) = rhs
758 getRHS (PClauseR fc with rhs whereBlock) = rhs
759 getRHS (PWithR fc with rhs whereBlock) = rhs
760 setReplDefined :: Maybe Name -> Idris ()
761 setReplDefined Nothing = return ()
762 setReplDefined (Just n) = do
763 oldState <- get
764 fmodifyState repl_definitions (n:)
765 -- the "name" field of PClauses seems to always be MN 2 "__", so we need to
766 -- retrieve the actual name from deeper inside.
767 -- This should really be a full recursive walk through the structure of PDecl, but
768 -- I think it should work this way and I want to test sooner. Also lazy.
769 fixClauses :: PDecl' t -> PDecl' t
770 fixClauses (PClauses fc opts _ css@(clause:cs)) =
771 PClauses fc opts (getClauseName clause) css
772 fixClauses (PInstance syn fc constraints cls parms ty instName decls) =
773 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
774 fixClauses decl = decl
776process fn (Undefine names) = undefine names
777 where
778 undefine :: [Name] -> Idris ()
779 undefine [] = do
780 allDefined <- idris_repl_defs `fmap` get
781 undefine' allDefined []
782 -- Keep track of which names you've removed so you can
783 -- print them out to the user afterward
784 undefine names = undefine' names []
785 undefine' [] list = do iRenderOutput $ printUndefinedNames list
786 return ()
787 undefine' (n:names) already = do
788 allDefined <- idris_repl_defs `fmap` get
789 if n `elem` allDefined
790 then do undefinedJustNow <- undefClosure n
791 undefine' names (undefinedJustNow ++ already)
792 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
793 undefine' names already
794 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
795 -- for now just assume it's a class. Eventually we'll want some kind of
796 -- smart detection of exactly what kind of name we're undefining.
797 fputState (ctxt_lookup n . known_classes) Nothing
798 fmodifyState repl_definitions (delete n)
799 undefClosure n =
800 do replDefs <- idris_repl_defs `fmap` get
801 callGraph <- whoCalls n
802 let users = case lookup n callGraph of
803 Just ns -> nub ns
804 Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
805 undefinedJustNow <- concat `fmap` mapM undefClosure users
806 undefOne n
807 return (nub (n : undefinedJustNow))
811process fn (ExecVal t)
812 = do ctxt <- getContext
813 ist <- getIState
814 (tm, ty) <- elabVal recinfo ERHS t
815-- let tm' = normaliseAll ctxt [] tm
816 let ty' = normaliseAll ctxt [] ty
817 res <- execute tm
818 let (resOut, tyOut) = (prettyIst ist (delab ist res),
819 prettyIst ist (delab ist ty'))
820 iPrintTermWithType resOut tyOut
822process fn (Check (PRef _ n))
823 = do ctxt <- getContext
824 ist <- getIState
825 let ppo = ppOptionIst ist
826 case lookupNames n ctxt of
827 ts@(t:_) ->
828 case lookup t (idris_metavars ist) of
829 Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $
830 showMetavarInfo ppo ist n i
831 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
832 [] -> iPrintError $ "No such variable " ++ show n
833 where
834 showMetavarInfo ppo ist n i
835 = case lookupTy n (tt_ctxt ist) of
836 (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
837 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
838 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
839 putTy ppo ist i bnd (PPi _ n t sc)
840 = let current = text " " <>
841 (case n of
842 MN _ _ -> text "_"
843 UN nm | ('_':'_':_) <- str nm -> text "_"
844 _ -> bindingOf n False) <+>
845 colon <+> align (tPretty bnd ist t) <> line
846 in
847 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
848 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
849 putGoal ppo ist bnd g
850 = text "--------------------------------------" <$>
851 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
852 align (tPretty bnd ist g)
854 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
857process fn (Check t)
858 = do (tm, ty) <- elabVal recinfo ERHS t
859 ctxt <- getContext
860 ist <- getIState
861 let ppo = ppOptionIst ist
862 ty' = normaliseC ctxt [] ty
863 case tm of
864 TType _ ->
865 iPrintTermWithType (prettyIst ist PType) type1Doc
866 _ -> iPrintTermWithType (pprintDelab ist tm)
867 (pprintDelab ist ty)
869process fn (DocStr (Left n))
870 = do ist <- getIState
871 case lookupCtxtName n (idris_docstrings ist) of
872 [] -> iPrintError $ "No documentation for " ++ show n
873 ns -> do toShow <- mapM (showDoc ist) ns
874 iRenderResult (vsep toShow)
875 where showDoc ist (n, d) = do doc <- getDocs n
876 return $ pprintDocs ist doc
878process fn (DocStr (Right c))
879 = do ist <- getIState
880 iRenderResult $ pprintConstDocs ist c (constDocs c)
882process fn Universes
883 = do i <- getIState
884 let cs = idris_constraints i
885-- iputStrLn $ showSep "\n" (map show cs)
886 iputStrLn $ show (map fst cs)
887 let n = length cs
888 iputStrLn $ "(" ++ show n ++ " constraints)"
889 case ucheck cs of
890 Error e -> iPrintError $ pshow i e
891 OK _ -> iPrintResult "Universes OK"
892process fn (Defn n)
893 = do i <- getIState
894 iputStrLn "Compiled patterns:\n"
895 iputStrLn $ show (lookupDef n (tt_ctxt i))
896 case lookupCtxt n (idris_patdefs i) of
897 [] -> return ()
898 [(d, _)] -> do iputStrLn "Original definiton:\n"
899 mapM_ (printCase i) d
900 case lookupTotal n (tt_ctxt i) of
901 [t] -> iputStrLn (showTotal t i)
902 _ -> return ()
903 where printCase i (_, lhs, rhs)
904 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
905 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
906 showTm i' (delab i rhs))
907process fn (TotCheck n)
908 = do i <- getIState
909 case lookupNameTotal n (tt_ctxt i) of
910 [] -> iPrintError $ "Unknown operator " ++ show n
911 ts -> do ist <- getIState
912 c <- colourise
913 let ppo = ppOptionIst ist
914 let showN = showName (Just ist) [] ppo c
915 iPrintResult . concat . intersperse "\n" .
916 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
917 ts
920process fn (DebugInfo n)
921 = do i <- getIState
922 let oi = lookupCtxtName n (idris_optimisation i)
923 when (not (null oi)) $ iputStrLn (show oi)
924 let si = lookupCtxt n (idris_statics i)
925 when (not (null si)) $ iputStrLn (show si)
926 let di = lookupCtxt n (idris_datatypes i)
927 when (not (null di)) $ iputStrLn (show di)
928 let d = lookupDef n (tt_ctxt i)
929 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
930 let cg = lookupCtxtName n (idris_callgraph i)
931 i <- getIState
932 let cg' = lookupCtxtName n (idris_callgraph i)
933 sc <- checkSizeChange n
934 iputStrLn $ "Size change: " ++ show sc
935 let fn = lookupCtxtName n (idris_fninfo i)
936 when (not (null cg')) $ do iputStrLn "Call graph:\n"
937 iputStrLn (show cg')
938 when (not (null fn)) $ iputStrLn (show fn)
939process fn (Search t) = searchByType t
940process fn (CaseSplitAt updatefile l n)
941 = caseSplitAt fn updatefile l n
942process fn (AddClauseFrom updatefile l n)
943 = addClauseFrom fn updatefile l n
944process fn (AddProofClauseFrom updatefile l n)
945 = addProofClauseFrom fn updatefile l n
946process fn (AddMissing updatefile l n)
947 = addMissing fn updatefile l n
948process fn (MakeWith updatefile l n)
949 = makeWith fn updatefile l n
950process fn (MakeLemma updatefile l n)
951 = makeLemma fn updatefile l n
952process fn (DoProofSearch updatefile rec l n hints)
953 = doProofSearch fn updatefile rec l n hints Nothing
954process fn (Spec t)
955 = do (tm, ty) <- elabVal recinfo ERHS t
956 ctxt <- getContext
957 ist <- getIState
958 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
959 iPrintResult (show (delab ist tm'))
961process fn (RmProof n')
962 = do i <- getIState
963 n <- resolveProof n'
964 let proofs = proof_list i
965 case lookup n proofs of
966 Nothing -> iputStrLn "No proof to remove"
967 Just _ -> do removeProof n
968 insertMetavar n
969 iputStrLn $ "Removed proof " ++ show n
970 where
971 insertMetavar :: Name -> Idris ()
972 insertMetavar n =
973 do i <- getIState
974 let ms = idris_metavars i
975 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
977process fn' (AddProof prf)
978 = do fn <- do
979 let fn'' = takeWhile (/= ' ') fn'
980 ex <- runIO $ doesFileExist fn''
981 let fnExt = fn'' <.> "idr"
982 exExt <- runIO $ doesFileExist fnExt
983 if ex
984 then return fn''
985 else if exExt
986 then return fnExt
987 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
988 let fb = fn ++ "~"
989 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
990 prog <- runIO $ readFile fb
991 i <- getIState
992 let proofs = proof_list i
993 n' <- case prf of
994 Nothing -> case proofs of
995 [] -> ifail "No proof to add"
996 ((x, p) : _) -> return x
997 Just nm -> return nm
998 n <- resolveProof n'
999 case lookup n proofs of
1000 Nothing -> iputStrLn "No proof to add"
1001 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
1002 runIO $ writeFile fn (unlines prog')
1003 removeProof n
1004 iputStrLn $ "Added proof " ++ show n
1005 where ls = (lines prog)
1007process fn (ShowProof n')
1008 = do i <- getIState
1009 n <- resolveProof n'
1010 let proofs = proof_list i
1011 case lookup n proofs of
1012 Nothing -> iPrintError "No proof to show"
1013 Just p -> iPrintResult $ showProof False n p
1015process fn (Prove n')
1016 = do ctxt <- getContext
1017 ist <- getIState
1018 let ns = lookupNames n' ctxt
1019 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
1020 n <- case metavars of
1021 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
1022 [(n, (_,_,False))] -> return n
1023 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
1024 ns -> ierror (CantResolveAlts (map fst ns))
1025 prover (lit fn) n
1026 -- recheck totality
1027 i <- getIState
1028 totcheck (fileFC "(input)", n)
1029 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
1030 mapM_ checkDeclTotality (idris_totcheck i)
1031 warnTotality
1033process fn (HNF t)
1034 = do (tm, ty) <- elabVal recinfo ERHS t
1035 ctxt <- getContext
1036 ist <- getIState
1037 let tm' = hnf ctxt [] tm
1038 iPrintResult (show (delab ist tm'))
1039process fn (TestInline t)
1040 = do (tm, ty) <- elabVal recinfo ERHS t
1041 ctxt <- getContext
1042 ist <- getIState
1043 let tm' = inlineTerm ist tm
1044 c <- colourise
1045 iPrintResult (showTm ist (delab ist tm'))
1046process fn Execute
1047 = idrisCatch
1048 (do ist <- getIState
1049 (m, _) <- elabVal recinfo ERHS
1050 (PApp fc
1051 (PRef fc (sUN "run__IO"))
1052 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1053 (tmpn, tmph) <- runIO tempfile
1054 runIO $ hClose tmph
1055 t <- codegen
1056 ir <- compile t tmpn m
1057 runIO $ generate t (head (idris_imported ist)) ir
1058 case idris_outputmode ist of
1059 RawOutput h -> do runIO $ system tmpn
1060 return ()
1061 IdeSlave n h -> runIO . hPutStrLn h $
1062 IdeSlave.convSExp "run-program" tmpn n)
1063 (\e -> getIState >>= iRenderError . flip pprintErr e)
1064 where fc = fileFC "main"
1065process fn (Compile codegen f)
1066 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =
1067 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""
1068 | otherwise = do (m, _) <- elabVal recinfo ERHS
1069 (PApp fc (PRef fc (sUN "run__IO"))
1070 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1071 ir <- compile codegen f m
1072 i <- getIState
1073 runIO $ generate codegen (head (idris_imported i)) ir
1074 where fc = fileFC "main"
1075process fn (LogLvl i) = setLogLevel i
1076-- Elaborate as if LHS of a pattern (debug command)
1077process fn (Pattelab t)
1078 = do (tm, ty) <- elabVal recinfo ELHS t
1079 iPrintResult $ show tm ++ "\n\n : " ++ show ty
1081process fn (Missing n)
1082 = do i <- getIState
1083 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
1084 case lookupCtxt n (idris_patdefs i) of
1085 [] -> iPrintError $ "Unknown operator " ++ show n
1086 [(_, tms)] ->
1087 iPrintResult (showSep "\n" (map (showTm i') tms))
1088 _ -> iPrintError $ "Ambiguous name"
1089process fn (DynamicLink l)
1090 = do i <- getIState
1091 let importdirs = opt_importdirs (idris_options i)
1092 lib = trim l
1093 handle <- lift . lift $ tryLoadLib importdirs lib
1094 case handle of
1095 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
1096 Just x -> do let libs = idris_dynamic_libs i
1097 if x `elem` libs
1098 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
1099 return ()
1100 else putIState $ i { idris_dynamic_libs = x:libs }
1101 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
1102process fn ListDynamic
1103 = do i <- getIState
1104 iputStrLn "Dynamic libraries:"
1105 showLibs $ idris_dynamic_libs i
1106 where showLibs [] = return ()
1107 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
1108process fn Metavars
1109 = do ist <- getIState
1110 let mvs = map fst (idris_metavars ist) \\ primDefs
1111 case mvs of
1112 [] -> iPrintError "No global metavariables to solve"
1113 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
1114process fn NOP = return ()
1116process fn (SetOpt ErrContext) = setErrContext True
1117process fn (UnsetOpt ErrContext) = setErrContext False
1118process fn (SetOpt ShowImpl) = setImpShow True
1119process fn (UnsetOpt ShowImpl) = setImpShow False
1120process fn (SetOpt ShowOrigErr) = setShowOrigErr True
1121process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1122process fn (SetOpt AutoSolve) = setAutoSolve True
1123process fn (UnsetOpt AutoSolve) = setAutoSolve False
1124process fn (SetOpt NoBanner) = setNoBanner True
1125process fn (UnsetOpt NoBanner) = setNoBanner False
1126process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1127process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1129process fn (SetOpt _) = iPrintError "Not a valid option"
1130process fn (UnsetOpt _) = iPrintError "Not a valid option"
1131process fn (SetColour ty c) = setColour ty c
1132process fn ColourOn
1133 = do ist <- getIState
1134 putIState $ ist { idris_colourRepl = True }
1135process fn ColourOff
1136 = do ist <- getIState
1137 putIState $ ist { idris_colourRepl = False }
1138process fn ListErrorHandlers =
1139 do ist <- getIState
1140 iPrintResult $ case idris_errorhandlers ist of
1141 [] -> "No registered error handlers"
1142 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1143process fn (SetConsoleWidth w) = setWidth w
1145process fn (Apropos a) =
1146 do ist <- getIState
1147 let names = apropos ist (T.pack a)
1148 let aproposInfo = [ (n,
1149 delabTy ist n,
1150 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1151 | n <- sort names, isUN n ]
1152 iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)
1153 where isUN (UN _) = True
1154 isUN (NS n _) = isUN n
1155 isUN _ = False
1157process fn (WhoCalls n) =
1158 do calls <- whoCalls n
1159 ist <- getIState
1160 iRenderResult . vsep $
1161 map (\(n, ns) ->
1162 text "Callers of" <+> prettyName True True [] n <$>
1163 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1164 calls
1166process fn (CallsWho n) =
1167 do calls <- callsWho n
1168 ist <- getIState
1169 iRenderResult . vsep $
1170 map (\(n, ns) ->
1171 prettyName True True [] n <+> text "calls:" <$>
1172 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1173 calls
1174-- IdrisDoc
1175process fn (MakeDoc s) =
1176 do istate <- getIState
1177 let names = words s
1178 parse n | Success x <- runparser name istate fn n = Right x
1179 parse n = Left n
1180 (bad, nss) = partitionEithers $ map parse names
1181 cd <- runIO $ getCurrentDirectory
1182 let outputDir = cd </> "doc"
1183 result <- if null bad then runIO $ generateDocs istate nss outputDir
1184 else return . Left $ "Illegal name: " ++ head bad
1185 case result of Right _ -> iputStrLn "IdrisDoc generated"
1186 Left err -> iPrintError err
1187process fn (PrintDef n) =
1188 do result <- pprintDef n
1189 case result of
1190 [] -> iPrintError "Not found"
1191 outs -> iRenderResult . vsep $ outs
1193-- Show relevant transformation rules for the name 'n'
1194process fn (TransformInfo n)
1195 = do i <- getIState
1196 let ts = lookupCtxt n (idris_transforms i)
1197 let res = map (showTrans i) ts
1198 iRenderResult . vsep $ concat res
1199 where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
1200 showTrans i [] = []
1201 showTrans i ((lhs, rhs) : ts)
1202 = let ppTm tm = annotate (AnnTerm [] tm) .
1203 pprintPTerm (ppOptionIst i) [] [] [] .
1204 delab i $ tm
1205 ts' = showTrans i ts in
1206 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'
1208-- iRenderOutput (pretty lhs)
1209-- iputStrLn " ==> "
1210-- iPrintTermWithType (pprintDelab i rhs)
1211-- iputStrLn "---------------"
1212-- showTrans i ts
1214process fn (PPrint fmt width (PRef _ n))
1215 = do outs <- pprintDef n
1216 iPrintResult =<< renderExternal fmt width (vsep outs)
1219process fn (PPrint fmt width t)
1220 = do (tm, ty) <- elabVal recinfo ERHS t
1221 ctxt <- getContext
1222 ist <- getIState
1223 let ppo = ppOptionIst ist
1224 ty' = normaliseC ctxt [] ty
1225 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
1228showTotal :: Totality -> IState -> String
1229showTotal t@(Partial (Other ns)) i
1230 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
1231showTotal t i = show t
1232showTotalN i n = case lookupTotal n (tt_ctxt i) of
1233 [t] -> showTotal t i
1234 _ -> ""
1236displayHelp = let vstr = showVersion version in
1237 "\nIdris version " ++ vstr ++ "\n" ++
1238 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
1239 concatMap cmdInfo helphead ++
1240 concatMap cmdInfo help
1241 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
1242 col c1 c2 l m r =
1243 l ++ take (c1 - length l) (repeat ' ') ++
1244 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1246pprintDef :: Name -> Idris [Doc OutputAnnotation]
1247pprintDef n =
1248 do ist <- getIState
1249 ctxt <- getContext
1250 let ambiguous = length (lookupNames n ctxt) > 1
1251 patdefs = idris_patdefs ist
1252 tyinfo = idris_datatypes ist
1253 return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1254 map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1255 map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1256 where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1257 ppDef amb ist (n, (clauses, missing)) =
1258 prettyName True amb [] n <+> colon <+>
1259 align (pprintDelabTy ist n) <$>
1260 ppClauses ist clauses <> ppMissing missing
1261 ppClauses ist [] = text "No clauses."
1262 ppClauses ist cs = vsep (map pp cs)
1263 where pp (vars, lhs, rhs) =
1264 let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1265 pprintPTerm (ppOptionIst ist)
1266 (zip vars (repeat False))
1267 [] [] .
1268 delab ist $
1270 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1271 ppMissing _ = empty
1273 ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1274 ppTy amb ist (n, TI constructors isCodata _ _ _)
1275 = kwd key <+> prettyName True amb [] n <+> colon <+>
1276 align (pprintDelabTy ist n) <+> kwd "where" <$>
1277 indent 2 (vsep (map (ppCon False ist) constructors))
1278 where
1279 key | isCodata = "codata"
1280 | otherwise = "data"
1281 kwd = annotate AnnKeyword . text
1282 ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n)
1285helphead =
1286 [ (["Command"], SpecialHeaderArg, "Purpose"),
1287 ([""], NoArg, "")
1291replSettings :: Maybe FilePath -> Settings Idris
1292replSettings hFile = setComplete replCompletion $ defaultSettings {
1293 historyFile = hFile
1296-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1297idris :: [Opt] -> IO (Maybe IState)
1298idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
1299 case res of
1300 Left err -> do putStrLn $ pshow idrisInit err
1301 return Nothing
1302 Right ist -> return (Just ist)
1303 where totalMain = do idrisMain opts
1304 ist <- getIState
1305 case idris_totcheckfail ist of
1306 ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1307 [] -> return ()
1310loadInputs :: [FilePath] -> Maybe Int -> Idris ()
1311loadInputs inputs toline -- furthest line to read in input source files
1312 = idrisCatch
1313 (do ist <- getIState
1314 -- if we're in --check and not outputting anything, don't bother
1315 -- loading, as it gets really slow if there's lots of modules in
1316 -- a package (instead, reload all at the end to check for
1317 -- consistency only)
1318 opts <- getCmdLine
1320 let loadCode = case opt getOutput opts of
1321 [] -> not (NoREPL `elem` opts)
1322 _ -> True
1324 -- For each ifile list, check it and build ibcs in the same clean IState
1325 -- so that they don't interfere with each other when checking
1327 let ninputs = zip [1..] inputs
1328 ifiles <- mapWhileOK (\(num, input) ->
1329 do putIState ist
1330 modTree <- buildTree
1331 (map snd (take (num-1) ninputs))
1332 input
1333 let ifiles = getModuleFiles modTree
1334 iLOG ("MODULE TREE : " ++ show modTree)
1335 iLOG ("RELOAD: " ++ show ifiles)
1336 when (not (all ibc ifiles) || loadCode) $
1337 tryLoad False (filter (not . ibc) ifiles)
1338 -- return the files that need rechecking
1339 return ifiles)
1340 ninputs
1341 inew <- getIState
1342 let tidata = idris_tyinfodata inew
1343 let patdefs = idris_patdefs inew
1344 -- If it worked, load the whole thing from all the ibcs together
1345 case errSpan inew of
1346 Nothing ->
1347 do putIState (ist { idris_tyinfodata = tidata })
1348 ibcfiles <- mapM findNewIBC (nub (concat ifiles))
1349 tryLoad True (mapMaybe id ibcfiles)
1350 _ -> return ()
1351 ist <- getIState
1352 putIState (ist { idris_tyinfodata = tidata,
1353 idris_patdefs = patdefs })
1355 case opt getOutput opts of
1356 [] -> performUsageAnalysis -- interactive
1357 _ -> return [] -- batch, will be checked by the compiler
1359 return ())
1360 (\e -> do i <- getIState
1361 case e of
1362 At f e' -> do setErrSpan f
1363 iWarn f $ pprintErr i e'
1364 ProgramLineComment -> return () -- fail elsewhere
1365 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1366 -- Issue #1576 on the issue tracker.
1367 -- https://github.com/idris-lang/Idris-dev/issues/1576
1368 iWarn emptyFC $ pprintErr i e)
1369 where -- load all files, stop if any fail
1370 tryLoad :: Bool -> [IFileType] -> Idris ()
1371 tryLoad keepstate [] = warnTotality >> return ()
1372 tryLoad keepstate (f : fs)
1373 = do ist <- getIState
1374 let maxline
1375 = case toline of
1376 Nothing -> Nothing
1377 Just l -> case f of
1378 IDR fn -> if any (fmatch fn) inputs
1379 then Just l
1380 else Nothing
1381 LIDR fn -> if any (fmatch fn) inputs
1382 then Just l
1383 else Nothing
1384 _ -> Nothing
1385 loadFromIFile f maxline
1386 inew <- getIState
1387 -- FIXME: Save these in IBC to avoid this hack! Need to
1388 -- preserve it all from source inputs
1389 --
1390 -- Issue #1577 on the issue tracker.
1391 -- https://github.com/idris-lang/Idris-dev/issues/1577
1392 let tidata = idris_tyinfodata inew
1393 let patdefs = idris_patdefs inew
1394 ok <- noErrors
1395 when ok $ do when (not keepstate) $ putIState ist
1396 ist <- getIState
1397 putIState (ist { idris_tyinfodata = tidata,
1398 idris_patdefs = patdefs })
1399 tryLoad keepstate fs
1401 ibc (IBC _ _) = True
1402 ibc _ = False
1404 fmatch ('.':'/':xs) ys = fmatch xs ys
1405 fmatch xs ('.':'/':ys) = fmatch xs ys
1406 fmatch xs ys = xs == ys
1408 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1409 findNewIBC i@(IBC _ _) = return (Just i)
1410 findNewIBC s@(IDR f) = do ist <- get
1411 ibcsd <- valIBCSubDir ist
1412 let ibc = ibcPathNoFallback ibcsd f
1413 ok <- runIO $ doesFileExist ibc
1414 if ok then return (Just (IBC ibc s))
1415 else return Nothing
1416 findNewIBC s@(LIDR f) = do ist <- get
1417 ibcsd <- valIBCSubDir ist
1418 let ibc = ibcPathNoFallback ibcsd f
1419 ok <- runIO $ doesFileExist ibc
1420 if ok then return (Just (IBC ibc s))
1421 else return Nothing
1423 -- Like mapM, but give up when there's an error
1424 mapWhileOK f [] = return []
1425 mapWhileOK f (x : xs) = do x' <- f x
1426 ok <- noErrors
1427 if ok then do xs' <- mapWhileOK f xs
1428 return (x' : xs')
1429 else return [x']
1431idrisMain :: [Opt] -> Idris ()
1432idrisMain opts =
1433 do let inputs = opt getFile opts
1434 let quiet = Quiet `elem` opts
1435 let nobanner = NoBanner `elem` opts
1436 let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts
1437 let runrepl = not (NoREPL `elem` opts)
1438 let verbose = runrepl || Verbose `elem` opts
1439 let output = opt getOutput opts
1440 let ibcsubdir = opt getIBCSubDir opts
1441 let importdirs = opt getImportDir opts
1442 let bcs = opt getBC opts
1443 let pkgdirs = opt getPkgDir opts
1444 let optimize = case opt getOptLevel opts of
1445 [] -> 2
1446 xs -> last xs
1447 let outty = case opt getOutputTy opts of
1448 [] -> Executable
1449 xs -> last xs
1450 let cgn = case opt getCodegen opts of
1451 [] -> Via "c"
1452 xs -> last xs
1453 script <- case opt getExecScript opts of
1454 [] -> return Nothing
1455 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1456 runIO $ exitWith (ExitFailure 1)
1457 [expr] -> return (Just expr)
1458 let immediate = opt getEvalExpr opts
1459 let port = getPort opts
1461 when (DefaultTotal `elem` opts) $ do i <- getIState
1462 putIState (i { default_total = True })
1463 setColourise $ not quiet && last (True : opt getColour opts)
1464 when (not runrepl) $ setWidth InfinitelyWide
1465 mapM_ addLangExt (opt getLanguageExt opts)
1466 setREPL runrepl
1467 setQuiet (quiet || isJust script || not (null immediate))
1468 setVerbose verbose
1469 setCmdLine opts
1470 setOutputTy outty
1471 setNoBanner nobanner
1472 setCodegen cgn
1473 mapM_ makeOption opts
1474 -- if we have the --bytecode flag, drop into the bytecode assembler
1475 case bcs of
1476 [] -> return ()
1477 xs -> return () -- runIO $ mapM_ bcAsm xs
1478 case ibcsubdir of
1479 [] -> setIBCSubDir ""
1480 (d:_) -> setIBCSubDir d
1481 setImportDirs importdirs
1483 setNoBanner nobanner
1485 when (not (NoBasePkgs `elem` opts)) $ do
1486 addPkgDir "prelude"
1487 addPkgDir "base"
1488 mapM_ addPkgDir pkgdirs
1489 elabPrims
1490 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"
1491 addAutoImport "Builtins"
1492 return ()
1493 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
1494 addAutoImport "Prelude"
1495 return ()
1497 when (runrepl && not idesl) initScript
1499 nobanner <- getNoBanner
1501 when (runrepl &&
1502 not quiet &&
1503 not idesl &&
1504 not (isJust script) &&
1505 not nobanner &&
1506 null immediate) $
1507 iputStrLn banner
1509 orig <- getIState
1510 when (not idesl) $ loadInputs inputs Nothing
1512 runIO $ hSetBuffering stdout LineBuffering
1514 ok <- noErrors
1515 when ok $ case output of
1516 [] -> return ()
1517 (o:_) -> idrisCatch (process "" (Compile cgn o))
1518 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1520 case immediate of
1521 [] -> return ()
1522 exprs -> do setWidth InfinitelyWide
1523 mapM_ (\str -> do ist <- getIState
1524 c <- colourise
1525 case parseExpr ist str of
1526 Failure err -> do iputStrLn $ show (fixColour c err)
1527 runIO $ exitWith (ExitFailure 1)
1528 Success e -> process "" (Eval e))
1529 exprs
1530 runIO $ exitWith ExitSuccess
1533 case script of
1534 Nothing -> return ()
1535 Just expr -> execScript expr
1537 -- Create Idris data dir + repl history and config dir
1538 idrisCatch (do dir <- getIdrisUserDataDir
1539 exists <- runIO $ doesDirectoryExist dir
1540 unless exists $ iLOG ("Creating " ++ dir)
1541 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1542 (\e -> return ())
1544 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1546 when (runrepl && not idesl) $ do
1547-- clearOrigPats
1548 startServer port orig inputs
1549 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1550 let idesock = IdeslaveSocket `elem` opts
1551 when (idesl) $ ideslaveStart idesock orig inputs
1552 ok <- noErrors
1553 when (not ok) $ runIO (exitWith (ExitFailure 1))
1554 where
1555 makeOption (OLogging i) = setLogLevel i
1556 makeOption TypeCase = setTypeCase True
1557 makeOption TypeInType = setTypeInType True
1558 makeOption NoCoverage = setCoverage False
1559 makeOption ErrContext = setErrContext True
1560 makeOption _ = return ()
1562 addPkgDir :: String -> Idris ()
1563 addPkgDir p = do ddir <- runIO $ getDataDir
1564 addImportDir (ddir </> p)
1565 addIBC (IBCImportDir (ddir </> p))
1567runMain :: Idris () -> IO ()
1568runMain prog = do res <- runErrorT $ execStateT prog idrisInit
1569 case res of
1570 Left err -> putStrLn $ "Uncaught error: " ++ show err
1571 Right _ -> return ()
1573execScript :: String -> Idris ()
1574execScript expr = do i <- getIState
1575 c <- colourise
1576 case parseExpr i expr of
1577 Failure err -> do iputStrLn $ show (fixColour c err)
1578 runIO $ exitWith (ExitFailure 1)
1579 Success term -> do ctxt <- getContext
1580 (tm, _) <- elabVal recinfo ERHS term
1581 res <- execute tm
1582 runIO $ exitWith ExitSuccess
1584-- | Get the platform-specific, user-specific Idris dir
1585getIdrisUserDataDir :: Idris FilePath
1586getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1588-- | Locate the platform-specific location for the init script
1589getInitScript :: Idris FilePath
1590getInitScript = do idrisDir <- getIdrisUserDataDir
1591 return $ idrisDir </> "repl" </> "init"
1593-- | Run the initialisation script
1594initScript :: Idris ()
1595initScript = do script <- getInitScript
1596 idrisCatch (do go <- runIO $ doesFileExist script
1597 when go $ do
1598 h <- runIO $ openFile script ReadMode
1599 runInit h
1600 runIO $ hClose h)
1601 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1602 where runInit :: Handle -> Idris ()
1603 runInit h = do eof <- lift . lift $ hIsEOF h
1604 ist <- getIState
1605 unless eof $ do
1606 line <- runIO $ hGetLine h
1607 script <- getInitScript
1608 c <- colourise
1609 processLine ist line script c
1610 runInit h
1611 processLine i cmd input clr =
1612 case parseCmd i input cmd of
1613 Failure err -> runIO $ print (fixColour clr err)
1614 Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
1615 Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
1616 Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
1617 Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
1618 Success (Right Proofs) -> proofs i
1619 Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
1620 Success (Right cmd ) -> process [] cmd
1621 Success (Left err) -> runIO $ print err
1623getFile :: Opt -> Maybe String
1624getFile (Filename str) = Just str
1625getFile _ = Nothing
1627getBC :: Opt -> Maybe String
1628getBC (BCAsm str) = Just str
1629getBC _ = Nothing
1631getOutput :: Opt -> Maybe String
1632getOutput (Output str) = Just str
1633getOutput _ = Nothing
1635getIBCSubDir :: Opt -> Maybe String
1636getIBCSubDir (IBCSubDir str) = Just str
1637getIBCSubDir _ = Nothing
1639getImportDir :: Opt -> Maybe String
1640getImportDir (ImportDir str) = Just str
1641getImportDir _ = Nothing
1643getPkgDir :: Opt -> Maybe String
1644getPkgDir (Pkg str) = Just str
1645getPkgDir _ = Nothing
1647getPkg :: Opt -> Maybe (Bool, String)
1648getPkg (PkgBuild str) = Just (False, str)
1649getPkg (PkgInstall str) = Just (True, str)
1650getPkg _ = Nothing
1652getPkgClean :: Opt -> Maybe String
1653getPkgClean (PkgClean str) = Just str
1654getPkgClean _ = Nothing
1656getPkgREPL :: Opt -> Maybe String
1657getPkgREPL (PkgREPL str) = Just str
1658getPkgREPL _ = Nothing
1660getPkgCheck :: Opt -> Maybe String
1661getPkgCheck (PkgCheck str) = Just str
1662getPkgCheck _ = Nothing
1664-- | Returns None if given an Opt which is not PkgMkDoc
1665-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1666getPkgMkDoc :: Opt -- ^ Opt to extract
1667 -> Maybe String -- ^ Result
1668getPkgMkDoc (PkgMkDoc str) = Just str
1669getPkgMkDoc _ = Nothing
1671getPkgTest :: Opt -- ^ the option to extract
1672 -> Maybe String -- ^ the package file to test
1673getPkgTest (PkgTest f) = Just f
1674getPkgTest _ = Nothing
1676getCodegen :: Opt -> Maybe Codegen
1677getCodegen (UseCodegen x) = Just x
1678getCodegen _ = Nothing
1680getExecScript :: Opt -> Maybe String
1681getExecScript (InterpretScript expr) = Just expr
1682getExecScript _ = Nothing
1684getEvalExpr :: Opt -> Maybe String
1685getEvalExpr (EvalExpr expr) = Just expr
1686getEvalExpr _ = Nothing
1688getOutputTy :: Opt -> Maybe OutputType
1689getOutputTy (OutputTy t) = Just t
1690getOutputTy _ = Nothing
1692getLanguageExt :: Opt -> Maybe LanguageExt
1693getLanguageExt (Extension e) = Just e
1694getLanguageExt _ = Nothing
1696getTriple :: Opt -> Maybe String
1697getTriple (TargetTriple x) = Just x
1698getTriple _ = Nothing
1700getCPU :: Opt -> Maybe String
1701getCPU (TargetCPU x) = Just x
1702getCPU _ = Nothing
1704getOptLevel :: Opt -> Maybe Word
1705getOptLevel (OptLevel x) = Just x
1706getOptLevel _ = Nothing
1708getColour :: Opt -> Maybe Bool
1709getColour (ColourREPL b) = Just b
1710getColour _ = Nothing
1712getClient :: Opt -> Maybe String
1713getClient (Client x) = Just x
1714getClient _ = Nothing
1716-- Get the first valid port
1717getPort :: [Opt] -> PortID
1718getPort [] = defaultPort
1719getPort (Port p:xs)
1720 | all (`elem` ['0'..'9']) p = PortNumber $ fromIntegral (read p)
1721 | otherwise = getPort xs
1722getPort (_:xs) = getPort xs
1724opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1725opt = mapMaybe
1727ver = showVersion version ++ gitHash
1729defaultPort :: PortID
1730defaultPort = PortNumber (fromIntegral 4294)
1732banner = " ____ __ _ \n" ++
1733 " / _/___/ /____(_)____ \n" ++
1734 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1735 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1736 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1737 "\n" ++
1738 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1739 "For details type :warranty."
1741warranty = "\n" ++
1742 "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1743 "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1744 "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1745 "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1746 "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1747 "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1748 "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1749 "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1750 "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1751 "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1752 "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"