1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
8import Idris.Apropos (apropos)
14import Idris.ErrReverse
15import Idris.Delaborate
16import Idris.Docstrings (Docstring, overview, renderDocstring)
19import Idris.Parser hiding (indent)
20import Idris.Primitives
22import Idris.Docs hiding (Doc)
24import Idris.Completion
25import qualified Idris.IdeSlave as IdeSlave
28import Idris.Colours hiding (colourise)
33import Idris.Interactive
37import Version_idris (gitHash)
39import Util.DynamicLinker
40import Util.Net (listenOnLocalhost)
41import Util.Pretty hiding ((</>))
43import Idris.Core.Evaluate
44import Idris.Core.Execute (execute)
46import Idris.Core.Constraints
49import IRTS.CodegenCommon
51import Data.List.Split (splitOn)
52import qualified Data.Text as T
54import Text.Trifecta.Result(Result(..))
61import LLVM.General.Target
65import System.Console.Haskeline as H
68import System.Environment
70import System.Directory
73import Control.Monad.Trans.Error (ErrorT(..))
74import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
75import Control.Monad.Trans ( lift )
76import Control.Concurrent.MVar
78import Control.Concurrent
83import Data.Word (Word)
84import Data.Either (partitionEithers)
90repl :: IState -- ^ The initial state
91 -> [FilePath] -- ^ The loaded modules
95 do let quiet = opt_quiet (idris_options orig)
97 let colour = idris_colourRepl i
98 let theme = idris_colourTheme i
99 let mvs = idris_metavars i
100 let prompt = if quiet
102 else showMVs colour theme mvs ++
103 let str = mkPrompt mods ++ ">" in
104 (if colour then colourisePrompt theme str else str) ++ " "
105 x <- H.catch (getInputLine prompt)
106 (ctrlC (return Nothing))
108 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
110 Just input -> -- H.catch
111 do ms <- H.catch (lift $ processInput input orig mods)
112 (ctrlC (return (Just mods)))
114 Just mods -> repl orig mods
118 where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
119 ctrlC act e = do lift $ iputStrLn (show e)
120 act -- repl orig mods
122 showMVs c thm [] = ""
123 showMVs c thm ms = "Metavariables: " ++
124 show' 4 c thm (map fst ms) ++ "\n"
126 show' 0 c thm ms = let l = length ms in
129 ++ if l == 1 then ")" else "s)"
130 show' n c thm [m] = showM c thm m
131 show' n c thm (m : ms) = showM c thm m ++ ", " ++
132 show' (n - 1) c thm ms
134 showM c thm n = if c then colouriseFun thm (show n)
137-- | Run the REPL server
138startServer :: IState -> [FilePath] -> Idris ()
139startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
141 where serverLoop :: IO ()
142 -- TODO: option for port number
143 serverLoop = withSocketsDo $
144 do sock <- listenOnLocalhost $ PortNumber 4294
152 = do (h,_,_) <- accept sock
154 (ist', fn) <- processNetCmd orig ist h fn cmd
158processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
159 IO (IState, FilePath)
160processNetCmd orig i h fn cmd
161 = do res <- case parseCmd i "(net)" cmd of
162 Failure err -> return (Left (Msg " invalid command"))
163 Success c -> runErrorT $ evalStateT (processNet fn c) i
166 Left err -> do hPutStrLn h (show err)
169 processNet fn Reload = processNet fn (Load fn)
170 processNet fn (Load f) =
171 do let ist = orig { idris_options = idris_options i
172 , idris_colourTheme = idris_colourTheme i
173 , idris_colourRepl = False
180 mods <- loadInputs h [f]
183 processNet fn c = do process h fn c
187-- | Run a command on the server on localhost
188runClient :: String -> IO ()
189runClient str = withSocketsDo $ do
190 h <- connectTo "localhost" (PortNumber 4294)
192 resp <- hGetResp "" h
195 where hGetResp acc h = do eof <- hIsEOF h
196 if eof then return acc
197 else do l <- hGetLine h
198 hGetResp (acc ++ l ++ "\n") h
201ideslaveStart :: IState -> [FilePath] -> Idris ()
202ideslaveStart orig mods
204 case idris_outputmode i of
206 when (mods /= []) (do isetPrompt (mkPrompt mods))
210ideslave :: IState -> [FilePath] -> Idris ()
213 (do l <- runIO $ getLine
214 (sexp, id) <- case IdeSlave.parseMessage l of
215 Left err -> ierror err
216 Right (sexp, id) -> return (sexp, id)
218 putIState $ i { idris_outputmode = (IdeSlave id) }
219 idrisCatch -- to report correct id back!
220 (do let fn = case mods of
223 case IdeSlave.sexpToCommand sexp of
224 Just cmd -> runIdeSlaveCommand id orig fn mods cmd
225 Nothing -> iPrintError "did not understand" )
226 (\e -> do iPrintError $ show e))
227 (\e -> do iPrintError $ show e)
230-- | Run IDESlave commands
231runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client
232 -> IState -- ^^ The original IState
233 -> FilePath -- ^^ The current open file
234 -> [FilePath] -- ^^ The currently loaded modules
235 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process
237runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
240 case parseCmd i "(input)" cmd of
241 Failure err -> iPrintError $ show (fixColour c err)
242 Success (Prove n') -> do iPrintResult ""
244 (process stdout fn (Prove n'))
245 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
246 isetPrompt (mkPrompt mods)
247 Success cmd -> idrisCatch
248 (ideslaveProcess fn cmd)
249 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
250runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =
251 do (unused, compls) <- replCompletion (reverse str, "")
252 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
253 IdeSlave.toSExp (map replacement compls,
255 runIO $ putStrLn $ IdeSlave.convSExp "return" good id
256runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =
259 putIState (orig { idris_options = idris_options i,
260 idris_outputmode = (IdeSlave id) })
261 loadInputs stdout [filename]
262 isetPrompt (mkPrompt [filename])
263 -- Report either success or failure
266 Nothing -> iPrintResult $ "loaded " ++ filename
267 Just x -> iPrintError $ "didn't load " ++ filename
268 ideslave orig [filename]
269runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
270 case splitName name of
271 Left err -> iPrintError err
272 Right n -> process stdout "(ideslave)"
273 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
274 where splitName :: String -> Either String Name
275 splitName s = case reverse $ splitOn "." s of
276 [] -> Left ("Didn't understand name '" ++ s ++ "'")
278 (n:ns) -> Right $ sNS (sUN n) ns
279runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
280 case parseConst orig name of
281 Success c -> process stdout "(ideslave)" (DocStr (Right c))
283 case splitName name of
284 Left err -> iPrintError err
285 Right n -> process stdout "(ideslave)" (DocStr (Left n))
286runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
287 process stdout fn (CaseSplitAt False line (sUN name))
288runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
289 process stdout fn (AddClauseFrom False line (sUN name))
290runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =
291 process stdout fn (AddProofClauseFrom False line (sUN name))
292runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =
293 process stdout fn (AddMissing False line (sUN name))
294runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
295 process stdout fn (MakeWith False line (sUN name))
296runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =
297 process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))
298runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =
299 case splitName name of
300 Left err -> iPrintError err
301 Right n -> process stdout fn (MakeLemma False line n)
302runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
303 process stdout fn (Apropos a)
304runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
306 let opts = idris_options ist
307 let impshow = opt_showimp opts
308 let errCtxt = opt_errContext opts
309 let options = (IdeSlave.SymbolAtom "ok",
310 [(IdeSlave.SymbolAtom "show-implicits", impshow),
311 (IdeSlave.SymbolAtom "error-context", errCtxt)])
312 runIO . putStrLn $ IdeSlave.convSExp "return" options id
313runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =
315 let msg = (IdeSlave.SymbolAtom "ok", b)
316 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
317runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
319 let msg = (IdeSlave.SymbolAtom "ok", b)
320 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
321runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
323 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
324 let ppo = ppOptionIst ist
325 let mvarTys = map (delabTy ist) mvs
326 let res = (IdeSlave.SymbolAtom "ok",
327 zipWith (\ n (prems, concl) -> (n, prems, concl))
328 (map (IdeSlave.StringAtom . show) mvs)
329 (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
330 runIO . putStrLn $ IdeSlave.convSExp "return" res id
331 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
332 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
333 in ((n, t):prems, conc)
334 getGoal tm = ([], tm)
335 sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
336 -> ([(String, String, SpanList OutputAnnotation)],
337 (String, SpanList OutputAnnotation))
338 sexpGoal ist cols ppo ns ([], concl) =
339 let infixes = idris_infixes ist
340 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
341 pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
343 sexpGoal ist cols ppo ns ((n, t):ps, concl) =
345 NS (UN nm) ns -> str nm
346 UN nm | ('_':'_':_) <- str nm -> "_"
347 | otherwise -> str nm
349 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
350 pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
351 rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
352 in ((n', t', spans) : fst rest, snd rest)
353runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
355 Left err -> iPrintError err
356 Right n -> do calls <- whoCalls n
358 let msg = (IdeSlave.SymbolAtom "ok",
359 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
360 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
361 where pn ist = displaySpans .
362 renderPretty 0.9 1000 .
363 fmap (fancifyAnnots ist) .
365runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
367 Left err -> iPrintError err
368 Right n -> do calls <- callsWho n
370 let msg = (IdeSlave.SymbolAtom "ok",
371 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
372 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
373 where pn ist = displaySpans .
374 renderPretty 0.9 1000 .
375 fmap (fancifyAnnots ist) .
378splitName :: String -> Either String Name
379splitName s = case reverse $ splitOn "." s of
380 [] -> Left ("Didn't understand name '" ++ s ++ "'")
382 (n:ns) -> Right $ sNS (sUN n) ns
384ideslaveProcess :: FilePath -> Command -> Idris ()
385ideslaveProcess fn Help = process stdout fn Help
386ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
387 iPrintResult "changed directory to"
388ideslaveProcess fn (Eval t) = process stdout fn (Eval t)
389ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)
390ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))
391ideslaveProcess fn (Check t) = process stdout fn (Check t)
392ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)
393ideslaveProcess fn Universes = process stdout fn Universes
394ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
396ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
397ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
399ideslaveProcess fn (Search t) = process stdout fn (Search t)
400ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
401-- RmProof and AddProof not supported!
402ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')
403ideslaveProcess fn (HNF t) = process stdout fn (HNF t)
404--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!
405ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)
407ideslaveProcess fn Execute = do process stdout fn Execute
409ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)
411ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)
413ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)
414ideslaveProcess fn (Missing n) = process stdout fn (Missing n)
415ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)
417ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic
419ideslaveProcess fn Metavars = process stdout fn Metavars
420ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)
422ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)
424ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)
426ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)
428ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)
430ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)
432ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)
433ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)
434ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)
435ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)
436ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
437ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
438ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
439ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)
440ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
442ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
444ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)
445ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)
446ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
449-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
451mkPrompt [x] = "*" ++ dropExtension x
452mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
454-- | Determine whether a file uses literate syntax
455lit f = case splitExtension f of
459processInput :: String ->
460 IState -> [FilePath] -> Idris (Maybe [FilePath])
461processInput cmd orig inputs
463 let opts = idris_options i
464 let quiet = opt_quiet opts
465 let fn = case inputs of
469 case parseCmd i "(input)" cmd of
470 Failure err -> do runIO $ print (fixColour c err)
473 do putIState $ orig { idris_options = idris_options i
474 , idris_colourTheme = idris_colourTheme i
477 mods <- loadInputs stdout inputs
480 do putIState orig { idris_options = idris_options i
481 , idris_colourTheme = idris_colourTheme i
484 mod <- loadInputs stdout [f]
486 Success (ModImport f) ->
488 fmod <- loadModule stdout f
489 return (Just (inputs ++ [fmod]))
490 Success Edit -> do -- takeMVar stvar
493 Success Proofs -> do proofs orig
495 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
497 Success cmd -> do idrisCatch (process stdout fn cmd)
498 (\e -> do msg <- showErr e ; iputStrLn msg)
501resolveProof :: Name -> Idris Name
505 n <- case lookupNames n' ctxt of
508 ns -> ierror (CantResolveAlts (map show ns))
511removeProof :: Name -> Idris ()
514 let proofs = proof_list i
515 let ps = filter ((/= n) . fst) proofs
516 putIState $ i { proof_list = ps }
518edit :: FilePath -> IState -> Idris ()
519edit "" orig = iputStrLn "Nothing to edit"
522 env <- runIO $ getEnvironment
523 let editor = getEditor env
524 let line = case errSpan i of
525 Just l -> " +" ++ show (fst (fc_start l)) ++ " "
527 let cmd = editor ++ line ++ fixName f
530 putIState $ orig { idris_options = idris_options i
531 , idris_colourTheme = idris_colourTheme i
533 loadInputs stdout [f]
537 where getEditor env | Just ed <- lookup "EDITOR" env = ed
538 | Just ed <- lookup "VISUAL" env = ed
540 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file
541 | otherwise = addExtension file "idr"
545proofs :: IState -> Idris ()
548 let ps = proof_list i
550 [] -> iputStrLn "No proofs available"
551 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
553insertScript :: String -> [String] -> [String]
554insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
555insertScript prf (p@"---------- Proofs ----------" : "" : xs)
557insertScript prf (x : xs) = x : insertScript prf xs
559process :: Handle -> FilePath -> Command -> Idris ()
560process h fn Help = iPrintResult displayHelp
561process h fn (ChangeDirectory f)
562 = do runIO $ setCurrentDirectory f
565 = withErrorReflection $ do logLvl 5 $ show t
566 (tm, ty) <- elabVal toplevel False t
568 let tm' = force (normaliseAll ctxt [] tm)
569 let ty' = force (normaliseAll ctxt [] ty)
570 -- Add value to context, call it "it"
571 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
573 logLvl 3 $ "Raw: " ++ show (tm', ty')
574 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
575 let tmDoc = prettyIst ist (delab ist tm')
576 tyDoc = prettyIst ist (delab ist ty')
577 ihPrintTermWithType h tmDoc tyDoc
579process h fn (ExecVal t)
580 = do ctxt <- getContext
582 (tm, ty) <- elabVal toplevel False t
583-- let tm' = normaliseAll ctxt [] tm
584 let ty' = normaliseAll ctxt [] ty
586 let (resOut, tyOut) = (prettyIst ist (delab ist res),
587 prettyIst ist (delab ist ty'))
588 ihPrintTermWithType h resOut tyOut
590process h fn (Check (PRef _ n))
591 = do ctxt <- getContext
593 let ppo = ppOptionIst ist
594 case lookupNames n ctxt of
596 case lookup t (idris_metavars ist) of
597 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
598 showMetavarInfo ppo ist n i
599 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
600 [] -> ihPrintError h $ "No such variable " ++ show n
602 showMetavarInfo ppo ist n i
603 = case lookupTy n (tt_ctxt ist) of
604 (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
605 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
606 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
607 putTy ppo ist i bnd (PPi _ n t sc)
608 = let current = text " " <>
611 UN nm | ('_':'_':_) <- str nm -> text "_"
612 _ -> bindingOf n False) <+>
613 colon <+> align (tPretty bnd ist t) <> line
615 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
616 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
617 putGoal ppo ist bnd g
618 = text "--------------------------------------" <$>
619 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
620 align (tPretty bnd ist g)
622 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
625process h fn (Check t)
626 = do (tm, ty) <- elabVal toplevel False t
629 let ppo = ppOptionIst ist
630 ty' = normaliseC ctxt [] ty
633 ihPrintTermWithType h (prettyIst ist PType) type1Doc
634 _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
635 (prettyIst ist (delab ist ty))
637process h fn (DocStr (Left n))
638 = do ist <- getIState
639 case lookupCtxtName n (idris_docstrings ist) of
640 [] -> iPrintError $ "No documentation for " ++ show n
641 ns -> do toShow <- mapM (showDoc ist) ns
642 ihRenderResult h (vsep toShow)
643 where showDoc ist (n, d) = do doc <- getDocs n
644 return $ pprintDocs ist doc
646process h fn (DocStr (Right c))
647 = do ist <- getIState
648 ihRenderResult h $ pprintConstDocs ist c (constDocs c)
650process h fn Universes
652 let cs = idris_constraints i
653-- iputStrLn $ showSep "\n" (map show cs)
654 iputStrLn $ show (map fst cs)
656 iputStrLn $ "(" ++ show n ++ " constraints)"
658 Error e -> iPrintError $ pshow i e
659 OK _ -> iPrintResult "Universes OK"
662 iputStrLn "Compiled patterns:\n"
663 iputStrLn $ show (lookupDef n (tt_ctxt i))
664 case lookupCtxt n (idris_patdefs i) of
666 [(d, _)] -> do iputStrLn "Original definiton:\n"
667 mapM_ (printCase i) d
668 case lookupTotal n (tt_ctxt i) of
669 [t] -> iputStrLn (showTotal t i)
671 where printCase i (_, lhs, rhs)
672 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
673 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
674 showTm i' (delab i rhs))
675process h fn (TotCheck n)
677 case lookupNameTotal n (tt_ctxt i) of
678 [] -> ihPrintError h $ "Unknown operator " ++ show n
679 ts -> do ist <- getIState
681 let ppo = ppOptionIst ist
682 let showN = showName (Just ist) [] ppo c
683 ihPrintResult h . concat . intersperse "\n" .
684 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
688process h fn (DebugInfo n)
690 let oi = lookupCtxtName n (idris_optimisation i)
691 when (not (null oi)) $ iputStrLn (show oi)
692 let si = lookupCtxt n (idris_statics i)
693 when (not (null si)) $ iputStrLn (show si)
694 let di = lookupCtxt n (idris_datatypes i)
695 when (not (null di)) $ iputStrLn (show di)
696 let d = lookupDef n (tt_ctxt i)
697 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
698 let cg = lookupCtxtName n (idris_callgraph i)
700 let cg' = lookupCtxtName n (idris_callgraph i)
701 sc <- checkSizeChange n
702 iputStrLn $ "Size change: " ++ show sc
703 when (not (null cg')) $ do iputStrLn "Call graph:\n"
705process h fn (Search t) = iPrintError "Not implemented"
706process h fn (CaseSplitAt updatefile l n)
707 = caseSplitAt h fn updatefile l n
708process h fn (AddClauseFrom updatefile l n)
709 = addClauseFrom h fn updatefile l n
710process h fn (AddProofClauseFrom updatefile l n)
711 = addProofClauseFrom h fn updatefile l n
712process h fn (AddMissing updatefile l n)
713 = addMissing h fn updatefile l n
714process h fn (MakeWith updatefile l n)
715 = makeWith h fn updatefile l n
716process h fn (MakeLemma updatefile l n)
717 = makeLemma h fn updatefile l n
718process h fn (DoProofSearch updatefile rec l n hints)
719 = doProofSearch h fn updatefile rec l n hints
721 = do (tm, ty) <- elabVal toplevel False t
724 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
725 iPrintResult (show (delab ist tm'))
727process h fn (RmProof n')
730 let proofs = proof_list i
731 case lookup n proofs of
732 Nothing -> iputStrLn "No proof to remove"
733 Just _ -> do removeProof n
735 iputStrLn $ "Removed proof " ++ show n
737 insertMetavar :: Name -> Idris ()
740 let ms = idris_metavars i
741 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
743process h fn' (AddProof prf)
745 let fn'' = takeWhile (/= ' ') fn'
746 ex <- runIO $ doesFileExist fn''
747 let fnExt = fn'' <.> "idr"
748 exExt <- runIO $ doesFileExist fnExt
753 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
755 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
756 prog <- runIO $ readFile fb
758 let proofs = proof_list i
760 Nothing -> case proofs of
761 [] -> ifail "No proof to add"
762 ((x, p) : _) -> return x
765 case lookup n proofs of
766 Nothing -> iputStrLn "No proof to add"
767 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
768 runIO $ writeFile fn (unlines prog')
770 iputStrLn $ "Added proof " ++ show n
771 where ls = (lines prog)
773process h fn (ShowProof n')
776 let proofs = proof_list i
777 case lookup n proofs of
778 Nothing -> iPrintError "No proof to show"
779 Just p -> iPrintResult $ showProof False n p
781process h fn (Prove n')
782 = do ctxt <- getContext
784 let ns = lookupNames n' ctxt
785 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
786 n <- case metavars of
787 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
788 [(n, (_,_,False))] -> return n
789 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
790 ns -> ierror (CantResolveAlts (map show ns))
794 totcheck (fileFC "(input)", n)
795 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
796 mapM_ checkDeclTotality (idris_totcheck i)
800 = do (tm, ty) <- elabVal toplevel False t
803 let tm' = hnf ctxt [] tm
804 iPrintResult (show (delab ist tm'))
805process h fn (TestInline t)
806 = do (tm, ty) <- elabVal toplevel False t
809 let tm' = inlineTerm ist tm
811 iPrintResult (showTm ist (delab ist tm'))
815 (m, _) <- elabVal toplevel False
817 (PRef fc (sUN "run__IO"))
818 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
819 (tmpn, tmph) <- runIO tempfile
823 case idris_outputmode ist of
824 RawOutput -> do runIO $ system tmpn
826 IdeSlave n -> runIO . hPutStrLn h $
827 IdeSlave.convSExp "run-program" tmpn n)
828 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
829 where fc = fileFC "main"
830process h fn (Compile codegen f)
831 = do (m, _) <- elabVal toplevel False
832 (PApp fc (PRef fc (sUN "run__IO"))
833 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
835 where fc = fileFC "main"
836process h fn (LogLvl i) = setLogLevel i
837-- Elaborate as if LHS of a pattern (debug command)
838process h fn (Pattelab t)
839 = do (tm, ty) <- elabVal toplevel True t
840 iPrintResult $ show tm ++ "\n\n : " ++ show ty
842process h fn (Missing n)
844 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
845 case lookupCtxt n (idris_patdefs i) of
848 iPrintResult (showSep "\n" (map (showTm i') tms))
849 _ -> iPrintError $ "Ambiguous name"
850process h fn (DynamicLink l)
852 let importdirs = opt_importdirs (idris_options i)
854 handle <- lift . lift $ tryLoadLib importdirs lib
856 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
857 Just x -> do let libs = idris_dynamic_libs i
859 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
861 else putIState $ i { idris_dynamic_libs = x:libs }
862 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
863process h fn ListDynamic
865 iputStrLn "Dynamic libraries:"
866 showLibs $ idris_dynamic_libs i
867 where showLibs [] = return ()
868 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
870 = do ist <- getIState
871 let mvs = map fst (idris_metavars ist) \\ primDefs
873 [] -> iPrintError "No global metavariables to solve"
874 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
875process h fn NOP = return ()
877process h fn (SetOpt ErrContext) = setErrContext True
878process h fn (UnsetOpt ErrContext) = setErrContext False
879process h fn (SetOpt ShowImpl) = setImpShow True
880process h fn (UnsetOpt ShowImpl) = setImpShow False
881process h fn (SetOpt ShowOrigErr) = setShowOrigErr True
882process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
883process h fn (SetOpt AutoSolve) = setAutoSolve True
884process h fn (UnsetOpt AutoSolve) = setAutoSolve False
885process h fn (SetOpt NoBanner) = setNoBanner True
886process h fn (UnsetOpt NoBanner) = setNoBanner False
887process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
888process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
890process h fn (SetOpt _) = iPrintError "Not a valid option"
891process h fn (UnsetOpt _) = iPrintError "Not a valid option"
892process h fn (SetColour ty c) = setColour ty c
894 = do ist <- getIState
895 putIState $ ist { idris_colourRepl = True }
896process h fn ColourOff
897 = do ist <- getIState
898 putIState $ ist { idris_colourRepl = False }
899process h fn ListErrorHandlers =
901 case idris_errorhandlers ist of
902 [] -> iPrintResult "No registered error handlers"
904 iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
905process h fn (SetConsoleWidth w) = setWidth w
907process h fn (Apropos a) =
909 let names = apropos ist (T.pack a)
910 let aproposInfo = [ (n,
912 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
913 | n <- sort names, isUN n ]
914 ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)
915 where renderApropos ist (name, ty, docs) =
916 prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>
917 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
919 isUN (NS n _) = isUN n
922process h fn (WhoCalls n) =
923 do calls <- whoCalls n
925 ihRenderResult h . vsep $
927 text "Callers of" <+> prettyName True [] n <$>
928 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
931process h fn (CallsWho n) =
932 do calls <- callsWho n
934 ihRenderResult h . vsep $
936 prettyName True [] n <+> text "calls:" <$>
937 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
940process h fn (MakeDoc s) =
941 do istate <- getIState
943 parse n | Success x <- runparser name istate fn n = Right x
945 (bad, nss) = partitionEithers $ map parse names
946 cd <- runIO $ getCurrentDirectory
947 let outputDir = cd </> "doc"
948 result <- if null bad then runIO $ generateDocs istate nss outputDir
949 else return . Left $ "Illegal name: " ++ head bad
950 case result of Right _ -> iputStrLn "IdrisDoc generated"
951 Left err -> iPrintError err
954showTotal :: Totality -> IState -> String
955showTotal t@(Partial (Other ns)) i
956 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
957showTotal t i = show t
958showTotalN i n = case lookupTotal n (tt_ctxt i) of
962displayHelp = let vstr = showVersion version in
963 "\nIdris version " ++ vstr ++ "\n" ++
964 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
965 concatMap cmdInfo helphead ++
966 concatMap cmdInfo help
967 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
969 l ++ take (c1 - length l) (repeat ' ') ++
970 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
972parseCodegen :: String -> Codegen
973parseCodegen "C" = ViaC
974parseCodegen "Java" = ViaJava
975parseCodegen "bytecode" = Bytecode
976parseCodegen "javascript" = ViaJavaScript
977parseCodegen "node" = ViaNode
978parseCodegen "llvm" = ViaLLVM
979parseCodegen _ = error "unknown codegen" -- FIXME: partial function
981parseArgs :: [String] -> [Opt]
983parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)
984parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
985parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
986parseArgs ("--client":ns) = [Client (showSep " " ns)]
987parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
988parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)
989parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
990parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)
991parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
992parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
993parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
994parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
995parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
996parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
997parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
998parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)
999parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
1000parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
1001parseArgs ("--help":ns) = Usage : (parseArgs ns)
1002parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
1003parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
1004parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
1005parseArgs ("--version":ns) = Ver : (parseArgs ns)
1006parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
1007parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
1008parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
1009parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
1010-- Package Related options
1011parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
1012parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1013parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1014parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1015parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)
1016parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1017parseArgs ("--mkdoc":n:ns) = PkgMkDoc n : (parseArgs ns) -- IdrisDoc
1018parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)
1020parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
1021parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
1022parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
1023parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)
1024parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
1025parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
1026parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
1027parseArgs ("--eval":expr:ns) = EvalExpr expr : parseArgs ns
1028parseArgs ("-e":expr:ns) = EvalExpr expr : parseArgs ns
1029parseArgs ["--exec"] = InterpretScript "Main.main" : []
1030parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
1031parseArgs (('-':'X':extName):ns) = case maybeRead extName of
1032 Just ext -> Extension ext : parseArgs ns
1033 -- Not sure what to do for the Nothing case
1034 Nothing -> error ("Unknown extension " ++ extName)
1035 where maybeRead = fmap fst . listToMaybe . reads
1036parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns
1037parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns
1038parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns
1039parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns
1040parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns
1041parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns
1042parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns
1043parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns
1044parseArgs ("--color":ns) = ColourREPL True : parseArgs ns
1045parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns
1046parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns
1047parseArgs (n:ns) = Filename n : (parseArgs ns)
1050 [ (["Command"], SpecialHeaderArg, "Purpose"),
1055replSettings :: Maybe FilePath -> Settings Idris
1056replSettings hFile = setComplete replCompletion $ defaultSettings {
1060-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1061idris :: [Opt] -> IO (Maybe IState)
1062idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
1064 Left err -> do putStrLn $ pshow idrisInit err
1066 Right ist -> return (Just ist)
1067 where totalMain = do idrisMain opts
1069 case idris_totcheckfail ist of
1070 ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1074loadInputs :: Handle -> [FilePath] -> Idris ()
1077 (do ist <- getIState
1078 -- if we're in --check and not outputting anything, don't bother
1079 -- loading, as it gets really slow if there's lots of modules in
1080 -- a package (instead, reload all at the end to check for
1081 -- consistency only)
1084 let loadCode = case opt getOutput opts of
1085 [] -> not (NoREPL `elem` opts)
1088 -- For each ifile list, check it and build ibcs in the same clean IState
1089 -- so that they don't interfere with each other when checking
1091 let ninputs = zip [1..] inputs
1092 ifiles <- mapWhileOK (\(num, input) ->
1094 modTree <- buildTree
1095 (map snd (take (num-1) ninputs))
1097 let ifiles = getModuleFiles modTree
1098 iLOG ("MODULE TREE : " ++ show modTree)
1099 iLOG ("RELOAD: " ++ show ifiles)
1100 when (not (all ibc ifiles) || loadCode) $
1101 tryLoad False (filter (not . ibc) ifiles)
1102 -- return the files that need rechecking
1106 let tidata = idris_tyinfodata inew
1107 let patdefs = idris_patdefs inew
1108 -- If it worked, load the whole thing from all the ibcs together
1109 case errSpan inew of
1111 do putIState (ist { idris_tyinfodata = tidata })
1112 ibcfiles <- mapM findNewIBC (nub (concat ifiles))
1113 tryLoad True (mapMaybe id ibcfiles)
1116 putIState (ist { idris_tyinfodata = tidata,
1117 idris_patdefs = patdefs })
1119 case opt getOutput opts of
1120 [] -> performUsageAnalysis -- interactive
1121 _ -> return [] -- batch, will be checked by the compiler
1124 (\e -> do i <- getIState
1126 At f e' -> do setErrSpan f
1127 ihWarn stdout f $ pprintErr i e'
1128 ProgramLineComment -> return () -- fail elsewhere
1129 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1130 ihWarn stdout emptyFC $ pprintErr i e)
1131 where -- load all files, stop if any fail
1132 tryLoad :: Bool -> [IFileType] -> Idris ()
1133 tryLoad keepstate [] = warnTotality >> return ()
1134 tryLoad keepstate (f : fs)
1135 = do ist <- getIState
1138 -- FIXME: Save these in IBC to avoid this hack! Need to
1139 -- preserve it all from source inputs
1140 let tidata = idris_tyinfodata inew
1141 let patdefs = idris_patdefs inew
1143 when ok $ do when (not keepstate) $ putIState ist
1145 putIState (ist { idris_tyinfodata = tidata,
1146 idris_patdefs = patdefs })
1147 tryLoad keepstate fs
1149 ibc (IBC _ _) = True
1152 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1153 findNewIBC i@(IBC _ _) = return (Just i)
1154 findNewIBC s@(IDR f) = do ist <- get
1155 ibcsd <- valIBCSubDir ist
1156 let ibc = ibcPathNoFallback ibcsd f
1157 ok <- runIO $ doesFileExist ibc
1158 if ok then return (Just (IBC ibc s))
1160 findNewIBC s@(LIDR f) = do ist <- get
1161 ibcsd <- valIBCSubDir ist
1162 let ibc = ibcPathNoFallback ibcsd f
1163 ok <- runIO $ doesFileExist ibc
1164 if ok then return (Just (IBC ibc s))
1167 -- Like mapM, but give up when there's an error
1168 mapWhileOK f [] = return []
1169 mapWhileOK f (x : xs) = do x' <- f x
1171 if ok then do xs' <- mapWhileOK f xs
1175idrisMain :: [Opt] -> Idris ()
1177 do let inputs = opt getFile opts
1178 let quiet = Quiet `elem` opts
1179 let nobanner = NoBanner `elem` opts
1180 let idesl = Ideslave `elem` opts
1181 let runrepl = not (NoREPL `elem` opts)
1182 let verbose = runrepl || Verbose `elem` opts
1183 let output = opt getOutput opts
1184 let ibcsubdir = opt getIBCSubDir opts
1185 let importdirs = opt getImportDir opts
1186 let bcs = opt getBC opts
1187 let pkgdirs = opt getPkgDir opts
1188 let optimize = case opt getOptLevel opts of
1191 trpl <- case opt getTriple opts of
1192 [] -> runIO $ getDefaultTargetTriple
1193 xs -> return (last xs)
1194 tcpu <- case opt getCPU opts of
1195 [] -> runIO $ getHostCPUName
1196 xs -> return (last xs)
1197 let outty = case opt getOutputTy opts of
1200 let cgn = case opt getCodegen opts of
1203 script <- case opt getExecScript opts of
1204 [] -> return Nothing
1205 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1206 runIO $ exitWith (ExitFailure 1)
1207 [expr] -> return (Just expr)
1208 let immediate = opt getEvalExpr opts
1210 when (DefaultTotal `elem` opts) $ do i <- getIState
1211 putIState (i { default_total = True })
1212 setColourise $ not quiet && last (True : opt getColour opts)
1213 when (not runrepl) $ setWidth InfinitelyWide
1214 mapM_ addLangExt (opt getLanguageExt opts)
1216 setQuiet (quiet || isJust script || not (null immediate))
1221 setNoBanner nobanner
1223 setTargetTriple trpl
1225 setOptLevel optimize
1226 mapM_ makeOption opts
1227 -- if we have the --bytecode flag, drop into the bytecode assembler
1230 xs -> return () -- runIO $ mapM_ bcAsm xs
1232 [] -> setIBCSubDir ""
1233 (d:_) -> setIBCSubDir d
1234 setImportDirs importdirs
1236 setNoBanner nobanner
1238 when (not (NoBasePkgs `elem` opts)) $ do
1241 mapM_ addPkgDir pkgdirs
1243 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"
1245 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1248 when (runrepl && not idesl) initScript
1250 nobanner <- getNoBanner
1255 not (isJust script) &&
1261 loadInputs stdout inputs
1263 runIO $ hSetBuffering stdout LineBuffering
1266 when ok $ case output of
1268 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1269 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1273 exprs -> do setWidth InfinitelyWide
1274 mapM_ (\str -> do ist <- getIState
1276 case parseExpr ist str of
1277 Failure err -> do iputStrLn $ show (fixColour c err)
1278 runIO $ exitWith (ExitFailure 1)
1279 Success e -> process stdout "" (Eval e))
1281 runIO $ exitWith ExitSuccess
1285 Nothing -> return ()
1286 Just expr -> execScript expr
1288 -- Create Idris data dir + repl history and config dir
1289 idrisCatch (do dir <- getIdrisUserDataDir
1290 exists <- runIO $ doesDirectoryExist dir
1291 unless exists $ iLOG ("Creating " ++ dir)
1292 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1295 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1297 when (runrepl && not idesl) $ do
1299 startServer orig inputs
1300 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1301 when (idesl) $ ideslaveStart orig inputs
1303 when (not ok) $ runIO (exitWith (ExitFailure 1))
1305 makeOption (OLogging i) = setLogLevel i
1306 makeOption TypeCase = setTypeCase True
1307 makeOption TypeInType = setTypeInType True
1308 makeOption NoCoverage = setCoverage False
1309 makeOption ErrContext = setErrContext True
1310 makeOption _ = return ()
1312 addPkgDir :: String -> Idris ()
1313 addPkgDir p = do ddir <- runIO $ getDataDir
1314 addImportDir (ddir </> p)
1316execScript :: String -> Idris ()
1317execScript expr = do i <- getIState
1319 case parseExpr i expr of
1320 Failure err -> do iputStrLn $ show (fixColour c err)
1321 runIO $ exitWith (ExitFailure 1)
1322 Success term -> do ctxt <- getContext
1323 (tm, _) <- elabVal toplevel False term
1325 runIO $ exitWith ExitSuccess
1327-- | Get the platform-specific, user-specific Idris dir
1328getIdrisUserDataDir :: Idris FilePath
1329getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1331-- | Locate the platform-specific location for the init script
1332getInitScript :: Idris FilePath
1333getInitScript = do idrisDir <- getIdrisUserDataDir
1334 return $ idrisDir </> "repl" </> "init"
1336-- | Run the initialisation script
1337initScript :: Idris ()
1338initScript = do script <- getInitScript
1339 idrisCatch (do go <- runIO $ doesFileExist script
1341 h <- runIO $ openFile script ReadMode
1344 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1345 where runInit :: Handle -> Idris ()
1346 runInit h = do eof <- lift . lift $ hIsEOF h
1349 line <- runIO $ hGetLine h
1350 script <- getInitScript
1352 processLine ist line script c
1354 processLine i cmd input clr =
1355 case parseCmd i input cmd of
1356 Failure err -> runIO $ print (fixColour clr err)
1357 Success Reload -> iPrintError "Init scripts cannot reload the file"
1358 Success (Load f) -> iPrintError "Init scripts cannot load files"
1359 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1360 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1361 Success Proofs -> proofs i
1362 Success Quit -> iPrintError "Init scripts cannot quit Idris"
1363 Success cmd -> process stdout [] cmd
1365getFile :: Opt -> Maybe String
1366getFile (Filename str) = Just str
1369getBC :: Opt -> Maybe String
1370getBC (BCAsm str) = Just str
1373getOutput :: Opt -> Maybe String
1374getOutput (Output str) = Just str
1375getOutput _ = Nothing
1377getIBCSubDir :: Opt -> Maybe String
1378getIBCSubDir (IBCSubDir str) = Just str
1379getIBCSubDir _ = Nothing
1381getImportDir :: Opt -> Maybe String
1382getImportDir (ImportDir str) = Just str
1383getImportDir _ = Nothing
1385getPkgDir :: Opt -> Maybe String
1386getPkgDir (Pkg str) = Just str
1387getPkgDir _ = Nothing
1389getPkg :: Opt -> Maybe (Bool, String)
1390getPkg (PkgBuild str) = Just (False, str)
1391getPkg (PkgInstall str) = Just (True, str)
1394getPkgClean :: Opt -> Maybe String
1395getPkgClean (PkgClean str) = Just str
1396getPkgClean _ = Nothing
1398getPkgREPL :: Opt -> Maybe String
1399getPkgREPL (PkgREPL str) = Just str
1400getPkgREPL _ = Nothing
1402getPkgCheck :: Opt -> Maybe String
1403getPkgCheck (PkgCheck str) = Just str
1404getPkgCheck _ = Nothing
1406-- | Returns None if given an Opt which is not PkgMkDoc
1407-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1408getPkgMkDoc :: Opt -- ^ Opt to extract
1409 -> Maybe String -- ^ Result
1410getPkgMkDoc (PkgMkDoc str) = Just str
1411getPkgMkDoc _ = Nothing
1413getCodegen :: Opt -> Maybe Codegen
1414getCodegen (UseCodegen x) = Just x
1415getCodegen _ = Nothing
1417getExecScript :: Opt -> Maybe String
1418getExecScript (InterpretScript expr) = Just expr
1419getExecScript _ = Nothing
1421getEvalExpr :: Opt -> Maybe String
1422getEvalExpr (EvalExpr expr) = Just expr
1423getEvalExpr _ = Nothing
1425getOutputTy :: Opt -> Maybe OutputType
1426getOutputTy (OutputTy t) = Just t
1427getOutputTy _ = Nothing
1429getLanguageExt :: Opt -> Maybe LanguageExt
1430getLanguageExt (Extension e) = Just e
1431getLanguageExt _ = Nothing
1433getTriple :: Opt -> Maybe String
1434getTriple (TargetTriple x) = Just x
1435getTriple _ = Nothing
1437getCPU :: Opt -> Maybe String
1438getCPU (TargetCPU x) = Just x
1441getOptLevel :: Opt -> Maybe Word
1442getOptLevel (OptLevel x) = Just x
1443getOptLevel _ = Nothing
1445getColour :: Opt -> Maybe Bool
1446getColour (ColourREPL b) = Just b
1447getColour _ = Nothing
1449opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1452ver = showVersion version ++ gitHash
1454banner = " ____ __ _ \n" ++
1455 " / _/___/ /____(_)____ \n" ++
1456 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1457 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1458 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list