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