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