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