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