git.iko.soy/Idris-dev
on be22ac6 help sign in
Idris-dev/src/Idris/REPL.hs
1871 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 t) = do process fn (Execute t)
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 $ readSource 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 $ writeSource 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 tm)
1119 = idrisCatch
1120 (do ist <- getIState
1121 (m, _) <- elabVal recinfo ERHS (elabExec fc tm)
1122 (tmpn, tmph) <- runIO tempfile
1123 runIO $ hClose tmph
1124 t <- codegen
1125 -- gcc adds .exe when it builds windows programs
1126 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
1127 ir <- compile t tmpn (Just m)
1128 runIO $ generate t (fst (head (idris_imported ist))) ir
1129 case idris_outputmode ist of
1130 RawOutput h -> do runIO $ rawSystem progName []
1131 return ()
1132 IdeMode n h -> runIO . hPutStrLn h $
1133 IdeMode.convSExp "run-program" tmpn n)
1134 (\e -> getIState >>= iRenderError . flip pprintErr e)
1135 where fc = fileFC "main"
1136process fn (Compile codegen f)
1137 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =
1138 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""
1139 | otherwise = do opts <- getCmdLine
1140 let iface = Interface `elem` opts
1141 m <- if iface then return Nothing else
1142 do (m', _) <- elabVal recinfo ERHS
1143 (PApp fc (PRef fc (sUN "run__IO"))
1144 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1145 return (Just m')
1146 ir <- compile codegen f m
1147 i <- getIState
1148 runIO $ generate codegen (fst (head (idris_imported i))) ir
1149 where fc = fileFC "main"
1150process fn (LogLvl i) = setLogLevel i
1151-- Elaborate as if LHS of a pattern (debug command)
1152process fn (Pattelab t)
1153 = do (tm, ty) <- elabVal recinfo ELHS t
1154 iPrintResult $ show tm ++ "\n\n : " ++ show ty
1156process fn (Missing n)
1157 = do i <- getIState
1158 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
1159 case lookupCtxt n (idris_patdefs i) of
1160 [] -> iPrintError $ "Unknown operator " ++ show n
1161 [(_, tms)] ->
1162 iPrintResult (showSep "\n" (map (showTm i') tms))
1163 _ -> iPrintError $ "Ambiguous name"
1164process fn (DynamicLink l)
1165 = do i <- getIState
1166 let importdirs = opt_importdirs (idris_options i)
1167 lib = trim l
1168 handle <- lift . lift $ tryLoadLib importdirs lib
1169 case handle of
1170 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
1171 Just x -> do let libs = idris_dynamic_libs i
1172 if x `elem` libs
1173 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
1174 return ()
1175 else putIState $ i { idris_dynamic_libs = x:libs }
1176 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
1177process fn ListDynamic
1178 = do i <- getIState
1179 iputStrLn "Dynamic libraries:"
1180 showLibs $ idris_dynamic_libs i
1181 where showLibs [] = return ()
1182 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
1183process fn Metavars
1184 = do ist <- getIState
1185 let mvs = map fst (idris_metavars ist) \\ primDefs
1186 case mvs of
1187 [] -> iPrintError "No global metavariables to solve"
1188 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
1189process fn NOP = return ()
1191process fn (SetOpt ErrContext) = setErrContext True
1192process fn (UnsetOpt ErrContext) = setErrContext False
1193process fn (SetOpt ShowImpl) = setImpShow True
1194process fn (UnsetOpt ShowImpl) = setImpShow False
1195process fn (SetOpt ShowOrigErr) = setShowOrigErr True
1196process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1197process fn (SetOpt AutoSolve) = setAutoSolve True
1198process fn (UnsetOpt AutoSolve) = setAutoSolve False
1199process fn (SetOpt NoBanner) = setNoBanner True
1200process fn (UnsetOpt NoBanner) = setNoBanner False
1201process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1202process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1204process fn (SetOpt _) = iPrintError "Not a valid option"
1205process fn (UnsetOpt _) = iPrintError "Not a valid option"
1206process fn (SetColour ty c) = setColour ty c
1207process fn ColourOn
1208 = do ist <- getIState
1209 putIState $ ist { idris_colourRepl = True }
1210process fn ColourOff
1211 = do ist <- getIState
1212 putIState $ ist { idris_colourRepl = False }
1213process fn ListErrorHandlers =
1214 do ist <- getIState
1215 iPrintResult $ case idris_errorhandlers ist of
1216 [] -> "No registered error handlers"
1217 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1218process fn (SetConsoleWidth w) = setWidth w
1220process fn (Apropos pkgs a) =
1221 do orig <- getIState
1222 when (not (null pkgs)) $
1223 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
1224 mapM_ loadPkgIndex pkgs
1225 ist <- getIState
1226 let mods = aproposModules ist (T.pack a)
1227 let names = apropos ist (T.pack a)
1228 let aproposInfo = [ (n,
1229 delabTy ist n,
1230 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1231 | n <- sort names, isUN n ]
1232 if (not (null mods)) || (not (null aproposInfo))
1233 then iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$>
1234 ppD ist d <> line) mods) <$>
1235 vsep (map (prettyDocumentedIst ist) aproposInfo)
1236 else iRenderError $ text "No results found"
1237 where isUN (UN _) = True
1238 isUN (NS n _) = isUN n
1239 isUN _ = False
1240 ppD ist = renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) []))
1243process fn (WhoCalls n) =
1244 do calls <- whoCalls n
1245 ist <- getIState
1246 iRenderResult . vsep $
1247 map (\(n, ns) ->
1248 text "Callers of" <+> prettyName True True [] n <$>
1249 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1250 calls
1252process fn (CallsWho n) =
1253 do calls <- callsWho n
1254 ist <- getIState
1255 iRenderResult . vsep $
1256 map (\(n, ns) ->
1257 prettyName True True [] n <+> text "calls:" <$>
1258 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1259 calls
1260-- IdrisDoc
1261process fn (MakeDoc s) =
1262 do istate <- getIState
1263 let names = words s
1264 parse n | Success x <- runparser name istate fn n = Right x
1265 parse n = Left n
1266 (bad, nss) = partitionEithers $ map parse names
1267 cd <- runIO $ getCurrentDirectory
1268 let outputDir = cd </> "doc"
1269 result <- if null bad then runIO $ generateDocs istate nss outputDir
1270 else return . Left $ "Illegal name: " ++ head bad
1271 case result of Right _ -> iputStrLn "IdrisDoc generated"
1272 Left err -> iPrintError err
1273process fn (PrintDef n) =
1274 do result <- pprintDef n
1275 case result of
1276 [] -> iPrintError "Not found"
1277 outs -> iRenderResult . vsep $ outs
1279-- Show relevant transformation rules for the name 'n'
1280process fn (TransformInfo n)
1281 = do i <- getIState
1282 let ts = lookupCtxt n (idris_transforms i)
1283 let res = map (showTrans i) ts
1284 iRenderResult . vsep $ concat res
1285 where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
1286 showTrans i [] = []
1287 showTrans i ((lhs, rhs) : ts)
1288 = let ppTm tm = annotate (AnnTerm [] tm) .
1289 pprintPTerm (ppOptionIst i) [] [] [] .
1290 delab i $ tm
1291 ts' = showTrans i ts in
1292 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'
1294-- iRenderOutput (pretty lhs)
1295-- iputStrLn " ==> "
1296-- iPrintTermWithType (pprintDelab i rhs)
1297-- iputStrLn "---------------"
1298-- showTrans i ts
1300process fn (PPrint fmt width (PRef _ n))
1301 = do outs <- pprintDef n
1302 iPrintResult =<< renderExternal fmt width (vsep outs)
1305process fn (PPrint fmt width t)
1306 = do (tm, ty) <- elabVal recinfo ERHS t
1307 ctxt <- getContext
1308 ist <- getIState
1309 let ppo = ppOptionIst ist
1310 ty' = normaliseC ctxt [] ty
1311 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
1314showTotal :: Totality -> IState -> String
1315showTotal t@(Partial (Other ns)) i
1316 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
1317showTotal t i = show t
1318showTotalN i n = case lookupTotal n (tt_ctxt i) of
1319 [t] -> showTotal t i
1320 _ -> ""
1322displayHelp = let vstr = showVersion version in
1323 "\nIdris version " ++ vstr ++ "\n" ++
1324 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
1325 concatMap cmdInfo helphead ++
1326 concatMap cmdInfo help
1327 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
1328 col c1 c2 l m r =
1329 l ++ take (c1 - length l) (repeat ' ') ++
1330 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1332pprintDef :: Name -> Idris [Doc OutputAnnotation]
1333pprintDef n =
1334 do ist <- getIState
1335 ctxt <- getContext
1336 let ambiguous = length (lookupNames n ctxt) > 1
1337 patdefs = idris_patdefs ist
1338 tyinfo = idris_datatypes ist
1339 return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1340 map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1341 map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1342 where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1343 ppDef amb ist (n, (clauses, missing)) =
1344 prettyName True amb [] n <+> colon <+>
1345 align (pprintDelabTy ist n) <$>
1346 ppClauses ist clauses <> ppMissing missing
1347 ppClauses ist [] = text "No clauses."
1348 ppClauses ist cs = vsep (map pp cs)
1349 where pp (vars, lhs, rhs) =
1350 let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1351 pprintPTerm (ppOptionIst ist)
1352 (zip vars (repeat False))
1353 [] [] .
1354 delab ist $
1356 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1357 ppMissing _ = empty
1359 ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1360 ppTy amb ist (n, TI constructors isCodata _ _ _)
1361 = kwd key <+> prettyName True amb [] n <+> colon <+>
1362 align (pprintDelabTy ist n) <+> kwd "where" <$>
1363 indent 2 (vsep (map (ppCon False ist) constructors))
1364 where
1365 key | isCodata = "codata"
1366 | otherwise = "data"
1367 kwd = annotate AnnKeyword . text
1368 ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n)
1371helphead =
1372 [ (["Command"], SpecialHeaderArg, "Purpose"),
1373 ([""], NoArg, "")
1377replSettings :: Maybe FilePath -> Settings Idris
1378replSettings hFile = setComplete replCompletion $ defaultSettings {
1379 historyFile = hFile
1382-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1383idris :: [Opt] -> IO (Maybe IState)
1384idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
1385 case res of
1386 Left err -> do putStrLn $ pshow idrisInit err
1387 return Nothing
1388 Right ist -> return (Just ist)
1389 where totalMain = do idrisMain opts
1390 ist <- getIState
1391 case idris_totcheckfail ist of
1392 ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1393 [] -> return ()
1396loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
1397loadInputs inputs toline -- furthest line to read in input source files
1398 = idrisCatch
1399 (do ist <- getIState
1400 -- if we're in --check and not outputting anything, don't bother
1401 -- loading, as it gets really slow if there's lots of modules in
1402 -- a package (instead, reload all at the end to check for
1403 -- consistency only)
1404 opts <- getCmdLine
1406 let loadCode = case opt getOutput opts of
1407 [] -> not (NoREPL `elem` opts)
1408 _ -> True
1410 -- For each ifile list, check it and build ibcs in the same clean IState
1411 -- so that they don't interfere with each other when checking
1413 let ninputs = zip [1..] inputs
1414 ifiles <- mapWhileOK (\(num, input) ->
1415 do putIState ist
1416 modTree <- buildTree
1417 (map snd (take (num-1) ninputs))
1418 input
1419 let ifiles = getModuleFiles modTree
1420 iLOG ("MODULE TREE : " ++ show modTree)
1421 iLOG ("RELOAD: " ++ show ifiles)
1422 when (not (all ibc ifiles) || loadCode) $
1423 tryLoad False (filter (not . ibc) ifiles)
1424 -- return the files that need rechecking
1425 return (input, ifiles))
1426 ninputs
1427 inew <- getIState
1428 let tidata = idris_tyinfodata inew
1429 let patdefs = idris_patdefs inew
1430 -- If it worked, load the whole thing from all the ibcs together
1431 case errSpan inew of
1432 Nothing ->
1433 do putIState (ist { idris_tyinfodata = tidata })
1434 ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))
1435 tryLoad True (mapMaybe id ibcfiles)
1436 _ -> return ()
1437 ist <- getIState
1438 putIState (ist { idris_tyinfodata = tidata,
1439 idris_patdefs = patdefs })
1440 exports <- findExports
1442 case opt getOutput opts of
1443 [] -> performUsageAnalysis (getExpNames exports) -- interactive
1444 _ -> return [] -- batch, will be checked by the compiler
1446 return (map fst ifiles))
1447 (\e -> do i <- getIState
1448 case e of
1449 At f e' -> do setErrSpan f
1450 iWarn f $ pprintErr i e'
1451 ProgramLineComment -> return () -- fail elsewhere
1452 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1453 -- Issue #1576 on the issue tracker.
1454 -- https://github.com/idris-lang/Idris-dev/issues/1576
1455 iWarn emptyFC $ pprintErr i e
1456 return [])
1457 where -- load all files, stop if any fail
1458 tryLoad :: Bool -> [IFileType] -> Idris ()
1459 tryLoad keepstate [] = warnTotality >> return ()
1460 tryLoad keepstate (f : fs)
1461 = do ist <- getIState
1462 let maxline
1463 = case toline of
1464 Nothing -> Nothing
1465 Just l -> case f of
1466 IDR fn -> if any (fmatch fn) inputs
1467 then Just l
1468 else Nothing
1469 LIDR fn -> if any (fmatch fn) inputs
1470 then Just l
1471 else Nothing
1472 _ -> Nothing
1473 loadFromIFile True f maxline
1474 inew <- getIState
1475 -- FIXME: Save these in IBC to avoid this hack! Need to
1476 -- preserve it all from source inputs
1477 --
1478 -- Issue #1577 on the issue tracker.
1479 -- https://github.com/idris-lang/Idris-dev/issues/1577
1480 let tidata = idris_tyinfodata inew
1481 let patdefs = idris_patdefs inew
1482 ok <- noErrors
1483 when ok $ do when (not keepstate) $ putIState ist
1484 ist <- getIState
1485 putIState (ist { idris_tyinfodata = tidata,
1486 idris_patdefs = patdefs })
1487 tryLoad keepstate fs
1489 ibc (IBC _ _) = True
1490 ibc _ = False
1492 fmatch ('.':'/':xs) ys = fmatch xs ys
1493 fmatch xs ('.':'/':ys) = fmatch xs ys
1494 fmatch xs ys = xs == ys
1496 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1497 findNewIBC i@(IBC _ _) = return (Just i)
1498 findNewIBC s@(IDR f) = do ist <- get
1499 ibcsd <- valIBCSubDir ist
1500 let ibc = ibcPathNoFallback ibcsd f
1501 ok <- runIO $ doesFileExist ibc
1502 if ok then return (Just (IBC ibc s))
1503 else return Nothing
1504 findNewIBC s@(LIDR f) = do ist <- get
1505 ibcsd <- valIBCSubDir ist
1506 let ibc = ibcPathNoFallback ibcsd f
1507 ok <- runIO $ doesFileExist ibc
1508 if ok then return (Just (IBC ibc s))
1509 else return Nothing
1511 -- Like mapM, but give up when there's an error
1512 mapWhileOK f [] = return []
1513 mapWhileOK f (x : xs) = do x' <- f x
1514 ok <- noErrors
1515 if ok then do xs' <- mapWhileOK f xs
1516 return (x' : xs')
1517 else return [x']
1519idrisMain :: [Opt] -> Idris ()
1520idrisMain opts =
1521 do mapM_ setWidth (opt getConsoleWidth opts)
1522 let inputs = opt getFile opts
1523 let quiet = Quiet `elem` opts
1524 let nobanner = NoBanner `elem` opts
1525 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts
1526 let runrepl = not (NoREPL `elem` opts)
1527 let verbose = runrepl || Verbose `elem` opts
1528 let output = opt getOutput opts
1529 let ibcsubdir = opt getIBCSubDir opts
1530 let importdirs = opt getImportDir opts
1531 let bcs = opt getBC opts
1532 let pkgdirs = opt getPkgDir opts
1533 -- Set default optimisations
1534 let optimise = case opt getOptLevel opts of
1535 [] -> 2
1536 xs -> last xs
1538 setOptLevel optimise
1539 let outty = case opt getOutputTy opts of
1540 [] -> if Interface `elem` opts then
1541 Object else Executable
1542 xs -> last xs
1543 let cgn = case opt getCodegen opts of
1544 [] -> Via "c"
1545 xs -> last xs
1546 -- Now set/unset specifically chosen optimisations
1547 sequence_ (opt getOptimisation opts)
1548 script <- case opt getExecScript opts of
1549 [] -> return Nothing
1550 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1551 runIO $ exitWith (ExitFailure 1)
1552 [expr] -> return (Just expr)
1553 let immediate = opt getEvalExpr opts
1554 let port = getPort opts
1556 when (DefaultTotal `elem` opts) $ do i <- getIState
1557 putIState (i { default_total = True })
1558 setColourise $ not quiet && last (True : opt getColour opts)
1562 mapM_ addLangExt (opt getLanguageExt opts)
1563 setREPL runrepl
1564 setQuiet (quiet || isJust script || not (null immediate))
1565 setVerbose verbose
1566 setCmdLine opts
1567 setOutputTy outty
1568 setNoBanner nobanner
1569 setCodegen cgn
1570 mapM_ makeOption opts
1571 -- if we have the --bytecode flag, drop into the bytecode assembler
1572 case bcs of
1573 [] -> return ()
1574 xs -> return () -- runIO $ mapM_ bcAsm xs
1575 case ibcsubdir of
1576 [] -> setIBCSubDir ""
1577 (d:_) -> setIBCSubDir d
1578 setImportDirs importdirs
1580 setNoBanner nobanner
1582 when (not (NoBasePkgs `elem` opts)) $ do
1583 addPkgDir "prelude"
1584 addPkgDir "base"
1585 mapM_ addPkgDir pkgdirs
1586 elabPrims
1587 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"
1588 addAutoImport "Builtins"
1589 return ()
1590 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
1591 addAutoImport "Prelude"
1592 return ()
1594 when (runrepl && not idesl) initScript
1596 nobanner <- getNoBanner
1598 when (runrepl &&
1599 not quiet &&
1600 not idesl &&
1601 not (isJust script) &&
1602 not nobanner &&
1603 null immediate) $
1604 iputStrLn banner
1606 orig <- getIState
1607 mods <- if idesl then return [] else loadInputs inputs Nothing
1608 let efile = case inputs of
1609 [] -> ""
1610 (f:_) -> f
1612 runIO $ hSetBuffering stdout LineBuffering
1614 ok <- noErrors
1615 when ok $ case output of
1616 [] -> return ()
1617 (o:_) -> idrisCatch (process "" (Compile cgn o))
1618 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1620 case immediate of
1621 [] -> return ()
1622 exprs -> do setWidth InfinitelyWide
1623 mapM_ (\str -> do ist <- getIState
1624 c <- colourise
1625 case parseExpr ist str of
1626 Failure err -> do iputStrLn $ show (fixColour c err)
1627 runIO $ exitWith (ExitFailure 1)
1628 Success e -> process "" (Eval e))
1629 exprs
1630 runIO $ exitWith ExitSuccess
1633 case script of
1634 Nothing -> return ()
1635 Just expr -> execScript expr
1637 -- Create Idris data dir + repl history and config dir
1638 idrisCatch (do dir <- getIdrisUserDataDir
1639 exists <- runIO $ doesDirectoryExist dir
1640 unless exists $ iLOG ("Creating " ++ dir)
1641 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1642 (\e -> return ())
1644 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1646 when ok $ case opt getPkgIndex opts of
1647 (f : _) -> writePkgIndex f
1648 _ -> return ()
1650 when (runrepl && not idesl) $ do
1651-- clearOrigPats
1652 startServer port orig mods
1653 runInputT (replSettings (Just historyFile)) $ repl orig mods efile
1654 let idesock = IdemodeSocket `elem` opts
1655 when (idesl) $ idemodeStart idesock orig inputs
1656 ok <- noErrors
1657 when (not ok) $ runIO (exitWith (ExitFailure 1))
1658 where
1659 makeOption (OLogging i) = setLogLevel i
1660 makeOption TypeCase = setTypeCase True
1661 makeOption TypeInType = setTypeInType True
1662 makeOption NoCoverage = setCoverage False
1663 makeOption ErrContext = setErrContext True
1664 makeOption _ = return ()
1666 addPkgDir :: String -> Idris ()
1667 addPkgDir p = do ddir <- runIO $ getIdrisLibDir
1668 addImportDir (ddir </> p)
1669 addIBC (IBCImportDir (ddir </> p))
1671runMain :: Idris () -> IO ()
1672runMain prog = do res <- runExceptT $ execStateT prog idrisInit
1673 case res of
1674 Left err -> putStrLn $ "Uncaught error: " ++ show err
1675 Right _ -> return ()
1677execScript :: String -> Idris ()
1678execScript expr = do i <- getIState
1679 c <- colourise
1680 case parseExpr i expr of
1681 Failure err -> do iputStrLn $ show (fixColour c err)
1682 runIO $ exitWith (ExitFailure 1)
1683 Success term -> do ctxt <- getContext
1684 (tm, _) <- elabVal recinfo ERHS term
1685 res <- execute tm
1686 runIO $ exitWith ExitSuccess
1688-- | Get the platform-specific, user-specific Idris dir
1689getIdrisUserDataDir :: Idris FilePath
1690getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1692-- | Locate the platform-specific location for the init script
1693getInitScript :: Idris FilePath
1694getInitScript = do idrisDir <- getIdrisUserDataDir
1695 return $ idrisDir </> "repl" </> "init"
1697-- | Run the initialisation script
1698initScript :: Idris ()
1699initScript = do script <- getInitScript
1700 idrisCatch (do go <- runIO $ doesFileExist script
1701 when go $ do
1702 h <- runIO $ openFile script ReadMode
1703 runInit h
1704 runIO $ hClose h)
1705 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1706 where runInit :: Handle -> Idris ()
1707 runInit h = do eof <- lift . lift $ hIsEOF h
1708 ist <- getIState
1709 unless eof $ do
1710 line <- runIO $ hGetLine h
1711 script <- getInitScript
1712 c <- colourise
1713 processLine ist line script c
1714 runInit h
1715 processLine i cmd input clr =
1716 case parseCmd i input cmd of
1717 Failure err -> runIO $ print (fixColour clr err)
1718 Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
1719 Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
1720 Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
1721 Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
1722 Success (Right Proofs) -> proofs i
1723 Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
1724 Success (Right cmd ) -> process [] cmd
1725 Success (Left err) -> runIO $ print err
1727getFile :: Opt -> Maybe String
1728getFile (Filename str) = Just str
1729getFile _ = Nothing
1731getBC :: Opt -> Maybe String
1732getBC (BCAsm str) = Just str
1733getBC _ = Nothing
1735getOutput :: Opt -> Maybe String
1736getOutput (Output str) = Just str
1737getOutput _ = Nothing
1739getIBCSubDir :: Opt -> Maybe String
1740getIBCSubDir (IBCSubDir str) = Just str
1741getIBCSubDir _ = Nothing
1743getImportDir :: Opt -> Maybe String
1744getImportDir (ImportDir str) = Just str
1745getImportDir _ = Nothing
1747getPkgDir :: Opt -> Maybe String
1748getPkgDir (Pkg str) = Just str
1749getPkgDir _ = Nothing
1751getPkg :: Opt -> Maybe (Bool, String)
1752getPkg (PkgBuild str) = Just (False, str)
1753getPkg (PkgInstall str) = Just (True, str)
1754getPkg _ = Nothing
1756getPkgClean :: Opt -> Maybe String
1757getPkgClean (PkgClean str) = Just str
1758getPkgClean _ = Nothing
1760getPkgREPL :: Opt -> Maybe String
1761getPkgREPL (PkgREPL str) = Just str
1762getPkgREPL _ = Nothing
1764getPkgCheck :: Opt -> Maybe String
1765getPkgCheck (PkgCheck str) = Just str
1766getPkgCheck _ = Nothing
1768-- | Returns None if given an Opt which is not PkgMkDoc
1769-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1770getPkgMkDoc :: Opt -- ^ Opt to extract
1771 -> Maybe String -- ^ Result
1772getPkgMkDoc (PkgMkDoc str) = Just str
1773getPkgMkDoc _ = Nothing
1775getPkgTest :: Opt -- ^ the option to extract
1776 -> Maybe String -- ^ the package file to test
1777getPkgTest (PkgTest f) = Just f
1778getPkgTest _ = Nothing
1780getCodegen :: Opt -> Maybe Codegen
1781getCodegen (UseCodegen x) = Just x
1782getCodegen _ = Nothing
1785getConsoleWidth :: Opt -> Maybe ConsoleWidth
1786getConsoleWidth (UseConsoleWidth x) = Just x
1787getConsoleWidth _ = Nothing
1790getExecScript :: Opt -> Maybe String
1791getExecScript (InterpretScript expr) = Just expr
1792getExecScript _ = Nothing
1794getPkgIndex :: Opt -> Maybe FilePath
1795getPkgIndex (PkgIndex file) = Just file
1796getPkgIndex _ = Nothing
1798getEvalExpr :: Opt -> Maybe String
1799getEvalExpr (EvalExpr expr) = Just expr
1800getEvalExpr _ = Nothing
1802getOutputTy :: Opt -> Maybe OutputType
1803getOutputTy (OutputTy t) = Just t
1804getOutputTy _ = Nothing
1806getLanguageExt :: Opt -> Maybe LanguageExt
1807getLanguageExt (Extension e) = Just e
1808getLanguageExt _ = Nothing
1810getTriple :: Opt -> Maybe String
1811getTriple (TargetTriple x) = Just x
1812getTriple _ = Nothing
1814getCPU :: Opt -> Maybe String
1815getCPU (TargetCPU x) = Just x
1816getCPU _ = Nothing
1818getOptLevel :: Opt -> Maybe Int
1819getOptLevel (OptLevel x) = Just x
1820getOptLevel _ = Nothing
1822getOptimisation :: Opt -> Maybe (Idris ())
1823getOptimisation (AddOpt p) = Just $ addOptimise p
1824getOptimisation (RemoveOpt p) = Just $ removeOptimise p
1825getOptimisation _ = Nothing
1827getColour :: Opt -> Maybe Bool
1828getColour (ColourREPL b) = Just b
1829getColour _ = Nothing
1831getClient :: Opt -> Maybe String
1832getClient (Client x) = Just x
1833getClient _ = Nothing
1835-- Get the first valid port
1836getPort :: [Opt] -> PortID
1837getPort [] = defaultPort
1838getPort (Port p:xs)
1839 | all (`elem` ['0'..'9']) p = PortNumber $ fromIntegral (read p)
1840 | otherwise = getPort xs
1841getPort (_:xs) = getPort xs
1843opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1844opt = mapMaybe
1846ver = showVersion version ++ "-" ++ gitHash
1848defaultPort :: PortID
1849defaultPort = PortNumber (fromIntegral 4294)
1851banner = " ____ __ _ \n" ++
1852 " / _/___/ /____(_)____ \n" ++
1853 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1854 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1855 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1856 "\n" ++
1857 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1858 "For details type :warranty."
1860warranty = "\n" ++
1861 "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1862 "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1863 "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1864 "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1865 "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1866 "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1867 "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1868 "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1869 "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1870 "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1871 "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"