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