git.iko.soy/Idris-dev
on ad995dc help sign in
Idris-dev/src/Idris/REPL.hs
1362 lines 59 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards, CPP #-}
4module Idris.REPL where
6import Idris.AbsSyntax
7import Idris.REPLParser
8import Idris.ElabDecls
9import Idris.ElabTerm
10import Idris.Error
11import Idris.Delaborate
12import Idris.Prover
13import Idris.Parser
14import Idris.Primitives
15import Idris.Coverage
16import Idris.UnusedArgs
17import Idris.Docs
18import Idris.Help
19import Idris.Completion
20import qualified Idris.IdeSlave as IdeSlave
21import Idris.Chaser
22import Idris.Imports
23import Idris.Colours
24import Idris.Inliner
25import Idris.CaseSplit
26import Idris.DeepSeq
28import Paths_idris
29import Version_idris (gitHash)
30import Util.System
31import Util.DynamicLinker
32import Util.Net (listenOnLocalhost)
34import Idris.Core.Evaluate
35import Idris.Core.Execute (execute)
36import Idris.Core.TT
37import Idris.Core.Constraints
39import IRTS.Compiler
40import IRTS.CodegenCommon
42import Text.Trifecta.Result(Result(..))
44-- import RTS.SC
45-- import RTS.Bytecode
46-- import RTS.PreC
47-- import RTS.CodegenC
48#ifdef IDRIS_LLVM
49import LLVM.General.Target
50#else
51import Util.LLVMStubs
52#endif
53import System.Console.Haskeline as H
54import System.FilePath
55import System.Exit
56import System.Environment
57import System.Process
58import System.Directory
59import System.IO
60import Control.Monad
61import Control.Monad.Trans.Error (ErrorT(..))
62import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
63import Control.Monad.Trans ( lift )
64import Control.Concurrent.MVar
65import Network
66import Control.Concurrent
67import Data.Maybe
68import Data.List
69import Data.Char
70import Data.Version
71import Data.Word (Word)
72import Control.DeepSeq
74import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
76import Debug.Trace
78-- | Run the REPL
79repl :: IState -- ^ The initial state
80 -> [FilePath] -- ^ The loaded modules
81 -> InputT Idris ()
82repl orig mods
83 = H.catch
84 (do let quiet = opt_quiet (idris_options orig)
85 i <- lift getIState
86 let colour = idris_colourRepl i
87 let theme = idris_colourTheme i
88 let mvs = idris_metavars i
89 let prompt = if quiet
90 then ""
91 else showMVs colour theme mvs ++
92 let str = mkPrompt mods ++ ">" in
93 (if colour then colourisePrompt theme str else str) ++ " "
94 x <- getInputLine prompt
95 case x of
96 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
97 return ()
98 Just input -> H.catch
99 (do ms <- lift $ processInput input orig mods
100 case ms of
101 Just mods -> repl orig mods
102 Nothing -> return ())
103 ctrlC)
104 ctrlC
105 where ctrlC :: SomeException -> InputT Idris ()
106 ctrlC e = do lift $ iputStrLn (show e)
107 repl orig mods
109 showMVs c thm [] = ""
110 showMVs c thm ms = "Metavariables: " ++
111 show' 4 c thm (map fst ms) ++ "\n"
113 show' 0 c thm ms = let l = length ms in
114 "... ( + " ++ show l
115 ++ " other"
116 ++ if l == 1 then ")" else "s)"
117 show' n c thm [m] = showM c thm m
118 show' n c thm (m : ms) = showM c thm m ++ ", " ++
119 show' (n - 1) c thm ms
121 showM c thm n = if c then colouriseFun thm (show n)
122 else show n
124-- | Run the REPL server
125startServer :: IState -> [FilePath] -> Idris ()
126startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
127 return ()
128 where serverLoop :: IO ()
129 -- TODO: option for port number
130 serverLoop = withSocketsDo $
131 do sock <- listenOnLocalhost $ PortNumber 4294
132 loop fn orig sock
134 fn = case fn_in of
135 (f:_) -> f
136 _ -> ""
138 loop fn ist sock
139 = do (h,host,_) <- accept sock
140 -- just use the local part of the hostname
141 -- for the "localhost.localdomain" case
142 if ((takeWhile (/= '.') host) == "localhost" ||
143 host == "127.0.0.1")
144 then do
145 cmd <- hGetLine h
146 (ist', fn) <- processNetCmd orig ist h fn cmd
147 hClose h
148 loop fn ist' sock
149 else do
150 putStrLn $ "Closing connection attempt from non-localhost " ++ host
151 hClose h
153processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
154 IO (IState, FilePath)
155processNetCmd orig i h fn cmd
156 = do res <- case parseCmd i "(net)" cmd of
157 Failure err -> return (Left (Msg " invalid command"))
158 Success c -> runErrorT $ evalStateT (processNet fn c) i
159 case res of
160 Right x -> return x
161 Left err -> do hPutStrLn h (show err)
162 return (i, fn)
163 where
164 processNet fn Reload = processNet fn (Load fn)
165 processNet fn (Load f) =
166 do let ist = orig { idris_options = idris_options i
167 , idris_colourTheme = idris_colourTheme i
168 , idris_colourRepl = False
169 }
170 putIState ist
171 setErrContext True
172 setOutH h
173 setQuiet True
174 setVerbose False
175 mods <- loadInputs h [f]
176 ist <- getIState
177 return (ist, f)
178 processNet fn c = do process h fn c
179 ist <- getIState
180 return (ist, fn)
182-- | Run a command on the server on localhost
183runClient :: String -> IO ()
184runClient str = withSocketsDo $ do
185 h <- connectTo "localhost" (PortNumber 4294)
186 hPutStrLn h str
187 resp <- hGetResp "" h
188 putStr resp
189 hClose h
190 where hGetResp acc h = do eof <- hIsEOF h
191 if eof then return acc
192 else do l <- hGetLine h
193 hGetResp (acc ++ l ++ "\n") h
195-- | Run the IdeSlave
196ideslaveStart :: IState -> [FilePath] -> Idris ()
197ideslaveStart orig mods
198 = do i <- getIState
199 case idris_outputmode i of
200 IdeSlave n ->
201 when (mods /= []) (do isetPrompt (mkPrompt mods))
202 ideslave orig mods
205ideslave :: IState -> [FilePath] -> Idris ()
206ideslave orig mods
207 = do idrisCatch
208 (do l <- runIO $ getLine
209 (sexp, id) <- case IdeSlave.parseMessage l of
210 Left err -> ierror err
211 Right (sexp, id) -> return (sexp, id)
212 i <- getIState
213 putIState $ i { idris_outputmode = (IdeSlave id) }
214 idrisCatch -- to report correct id back!
215 (do let fn = case mods of
216 (f:_) -> f
217 _ -> ""
218 case IdeSlave.sexpToCommand sexp of
219 Just (IdeSlave.Interpret cmd) ->
220 do c <- colourise
221 case parseCmd i "(input)" cmd of
222 Failure err -> iPrintError $ show (fixColour c err)
223 Success (Prove n') -> do iPrintResult ""
224 idrisCatch
225 (process stdout fn (Prove n'))
226 (\e -> getIState >>= iPrintError . flip pshow e)
227 isetPrompt (mkPrompt mods)
228 Success cmd -> idrisCatch
229 (ideslaveProcess fn cmd)
230 (\e -> getIState >>= iPrintError . flip pshow e)
231 Just (IdeSlave.REPLCompletions str) ->
232 do (unused, compls) <- replCompletion (reverse str, "")
233 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
234 runIO $ putStrLn $ IdeSlave.convSExp "return" good id
235 Just (IdeSlave.LoadFile filename) ->
236 do clearErr
237 putIState (orig { idris_options = idris_options i,
238 idris_outputmode = (IdeSlave id) })
239 loadInputs stdout [filename]
240 isetPrompt (mkPrompt [filename])
241 -- Report either success or failure
242 i <- getIState
243 case (errLine i) of
244 Nothing -> iPrintResult $ "loaded " ++ filename
245 Just x -> iPrintError $ "didn't load " ++ filename
246 ideslave orig [filename]
247 Just (IdeSlave.TypeOf name) ->
248 process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))
249 Just (IdeSlave.CaseSplit line name) ->
250 process stdout fn (CaseSplitAt False line (UN name))
251 Just (IdeSlave.AddClause line name) ->
252 process stdout fn (AddClauseFrom False line (UN name))
253 Just (IdeSlave.AddProofClause line name) ->
254 process stdout fn (AddProofClauseFrom False line (UN name))
255 Just (IdeSlave.AddMissing line name) ->
256 process stdout fn (AddMissing False line (UN name))
257 Just (IdeSlave.MakeWithBlock line name) ->
258 process stdout fn (MakeWith False line (UN name))
259 Just (IdeSlave.ProofSearch line name hints) ->
260 process stdout fn (DoProofSearch False line (UN name) (map UN hints))
261 Nothing -> do iPrintError "did not understand")
262 (\e -> do iPrintError $ show e))
263 (\e -> do iPrintError $ show e)
264 ideslave orig mods
266ideslaveProcess :: FilePath -> Command -> Idris ()
267ideslaveProcess fn Help = process stdout fn Help
268ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
269 iPrintResult "changed directory to"
270ideslaveProcess fn (Eval t) = process stdout fn (Eval t)
271ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)
272ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))
273ideslaveProcess fn (Check t) = process stdout fn (Check t)
274ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)
275ideslaveProcess fn Universes = process stdout fn Universes
276ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
277 iPrintResult ""
278ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
279ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
280 iPrintResult ""
281ideslaveProcess fn (Info n) = process stdout fn (Info n)
282ideslaveProcess fn (Search t) = process stdout fn (Search t)
283ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
284-- RmProof and AddProof not supported!
285ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')
286ideslaveProcess fn (HNF t) = process stdout fn (HNF t)
287--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!
288ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)
290--that most likely does not work, since we need to wrap
291--input/output of the executed binary...
292ideslaveProcess fn Execute = do process stdout fn Execute
293 iPrintResult ""
294ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)
295 iPrintResult ""
296ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)
297 iPrintResult ""
298ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)
299ideslaveProcess fn (Missing n) = process stdout fn (Missing n)
300ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)
301 iPrintResult ""
302ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic
303 iPrintResult ""
304ideslaveProcess fn Metavars = process stdout fn Metavars
305ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)
306 iPrintResult ""
307ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)
308 iPrintResult ""
309ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)
310 iPrintResult ""
311ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)
312 iPrintResult ""
313ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)
314ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)
315ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)
316ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)
317ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
318ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
319ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
320ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)
321ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
324-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
325mkPrompt [] = "Idris"
326mkPrompt [x] = "*" ++ dropExtension x
327mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
329-- | Determine whether a file uses literate syntax
330lit f = case splitExtension f of
331 (_, ".lidr") -> True
332 _ -> False
334processInput :: String ->
335 IState -> [FilePath] -> Idris (Maybe [FilePath])
336processInput cmd orig inputs
337 = do i <- getIState
338 let opts = idris_options i
339 let quiet = opt_quiet opts
340 let fn = case inputs of
341 (f:_) -> f
342 _ -> ""
343 c <- colourise
344 case parseCmd i "(input)" cmd of
345 Failure err -> do runIO $ print (fixColour c err)
346 return (Just inputs)
347 Success Reload ->
348 do putIState $ orig { idris_options = idris_options i
349 , idris_colourTheme = idris_colourTheme i
350 }
351 clearErr
352 mods <- loadInputs stdout inputs
353 return (Just inputs)
354 Success (Load f) ->
355 do putIState orig { idris_options = idris_options i
356 , idris_colourTheme = idris_colourTheme i
357 }
358 clearErr
359 mod <- loadInputs stdout [f]
360 return (Just [f])
361 Success (ModImport f) ->
362 do clearErr
363 fmod <- loadModule stdout f
364 return (Just (inputs ++ [fmod]))
365 Success Edit -> do -- takeMVar stvar
366 edit fn orig
367 return (Just inputs)
368 Success Proofs -> do proofs orig
369 return (Just inputs)
370 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
371 return Nothing
372 Success cmd -> do idrisCatch (process stdout fn cmd)
373 (\e -> do msg <- showErr e ; iputStrLn msg)
374 return (Just inputs)
376resolveProof :: Name -> Idris Name
377resolveProof n'
378 = do i <- getIState
379 ctxt <- getContext
380 n <- case lookupNames n' ctxt of
381 [x] -> return x
382 [] -> return n'
383 ns -> ierror (CantResolveAlts (map show ns))
384 return n
386removeProof :: Name -> Idris ()
387removeProof n =
388 do i <- getIState
389 let proofs = proof_list i
390 let ps = filter ((/= n) . fst) proofs
391 putIState $ i { proof_list = ps }
393edit :: FilePath -> IState -> Idris ()
394edit "" orig = iputStrLn "Nothing to edit"
395edit f orig
396 = do i <- getIState
397 env <- runIO $ getEnvironment
398 let editor = getEditor env
399 let line = case errLine i of
400 Just l -> " +" ++ show l ++ " "
401 Nothing -> " "
402 let cmd = editor ++ line ++ fixName f
403 runIO $ system cmd
404 clearErr
405 putIState $ orig { idris_options = idris_options i
406 , idris_colourTheme = idris_colourTheme i
407 }
408 loadInputs stdout [f]
409 iucheck
410 return ()
411 where getEditor env | Just ed <- lookup "EDITOR" env = ed
412 | Just ed <- lookup "VISUAL" env = ed
413 | otherwise = "vi"
414 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file
415 | otherwise = addExtension file "idr"
419proofs :: IState -> Idris ()
420proofs orig
421 = do i <- getIState
422 let ps = proof_list i
423 case ps of
424 [] -> iputStrLn "No proofs available"
425 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
427insertScript :: String -> [String] -> [String]
428insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
429insertScript prf (p@"---------- Proofs ----------" : "" : xs)
430 = p : "" : prf : xs
431insertScript prf (x : xs) = x : insertScript prf xs
433process :: Handle -> FilePath -> Command -> Idris ()
434process h fn Help = iPrintResult displayHelp
435process h fn (ChangeDirectory f)
436 = do runIO $ setCurrentDirectory f
437 return ()
438process h fn (Eval t)
439 = do (tm, ty) <- elabVal toplevel False t
440 ctxt <- getContext
441 let tm' = force (normaliseAll ctxt [] tm)
442 let ty' = force (normaliseAll ctxt [] ty)
443 -- Add value to context, call it "it"
444 updateContext (addCtxtDef (UN "it") (Function ty' tm'))
445 ist <- getIState
446 logLvl 3 $ "Raw: " ++ show (tm', ty')
447 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
448 imp <- impShow
449 c <- colourise
450 ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
451 showImp (Just ist) imp c (delab ist ty'))
452process h fn (ExecVal t)
453 = do ctxt <- getContext
454 ist <- getIState
455 (tm, ty) <- elabVal toplevel False t
456-- let tm' = normaliseAll ctxt [] tm
457 let ty' = normaliseAll ctxt [] ty
458 res <- execute tm
459 imp <- impShow
460 c <- colourise
461 ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++
462 showImp (Just ist) imp c (delab ist ty'))
463process h fn (Check (PRef _ n))
464 = do ctxt <- getContext
465 ist <- getIState
466 imp <- impShow
467 c <- colourise
468 case lookupNames n ctxt of
469 ts@(t:_) ->
470 case lookup t (idris_metavars ist) of
471 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
472 Nothing -> ihPrintResult h $
473 concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
474 showImp (Just ist) imp c (delabTy ist n)) $ ts
475 [] -> ihPrintError h $ "No such variable " ++ show n
476 where
477 showMetavarInfo c imp ist n i
478 = case lookupTy n (tt_ctxt ist) of
479 (ty:_) -> putTy c imp ist i (delab ist ty)
480 putTy c imp ist 0 sc = putGoal c imp ist sc
481 putTy c imp ist i (PPi _ n t sc)
482 = let current = " " ++
483 (case n of
484 MN _ _ -> "_"
485 UN ('_':'_':_) -> "_"
486 _ -> showName (Just ist) [] False c n) ++
487 " : " ++ showImp (Just ist) imp c t ++ "\n"
488 in
489 current ++ putTy c imp ist (i-1) sc
490 putTy c imp ist _ sc = putGoal c imp ist sc
491 putGoal c imp ist g
492 = "--------------------------------------\n" ++
493 showName (Just ist) [] False c n ++ " : " ++
494 showImp (Just ist) imp c g
497process h fn (Check t)
498 = do (tm, ty) <- elabVal toplevel False t
499 ctxt <- getContext
500 ist <- getIState
501 imp <- impShow
502 c <- colourise
503 let ty' = normaliseC ctxt [] ty
504 case tm of
505 TType _ -> ihPrintResult h ("Type : Type 1")
506 _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
507 showImp (Just ist) imp c (delab ist ty))
509process h fn (DocStr n)
510 = do i <- getIState
511 case lookupCtxtName n (idris_docstrings i) of
512 [] -> iPrintError $ "No documentation for " ++ show n
513 ns -> do mapM_ showDoc ns
514 iPrintResult ""
515 where showDoc (n, d)
516 = do doc <- getDocs n
517 iputStrLn $ show doc
518process h fn Universes
519 = do i <- getIState
520 let cs = idris_constraints i
521-- iputStrLn $ showSep "\n" (map show cs)
522 iputStrLn $ show (map fst cs)
523 let n = length cs
524 iputStrLn $ "(" ++ show n ++ " constraints)"
525 case ucheck cs of
526 Error e -> iPrintError $ pshow i e
527 OK _ -> iPrintResult "Universes OK"
528process h fn (Defn n)
529 = do i <- getIState
530 iputStrLn "Compiled patterns:\n"
531 iputStrLn $ show (lookupDef n (tt_ctxt i))
532 case lookupCtxt n (idris_patdefs i) of
533 [] -> return ()
534 [(d, _)] -> do iputStrLn "Original definiton:\n"
535 mapM_ (printCase i) d
536 case lookupTotal n (tt_ctxt i) of
537 [t] -> iputStrLn (showTotal t i)
538 _ -> return ()
539 where printCase i (_, lhs, rhs)
540 = do c <- colourise
541 iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++
542 showImp (Just i) True c (delab i rhs))
543process h fn (TotCheck n)
544 = do i <- getIState
545 case lookupNameTotal n (tt_ctxt i) of
546 [] -> ihPrintError h $ "Unknown operator " ++ show n
547 ts -> do ist <- getIState
548 c <- colourise
549 imp <- impShow
550 let showN = showName (Just ist) [] imp c
551 ihPrintResult h . concat . intersperse "\n" .
552 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
553 ts
556process h fn (DebugInfo n)
557 = do i <- getIState
558 let oi = lookupCtxtName n (idris_optimisation i)
559 when (not (null oi)) $ iputStrLn (show oi)
560 let si = lookupCtxt n (idris_statics i)
561 when (not (null si)) $ iputStrLn (show si)
562 let di = lookupCtxt n (idris_datatypes i)
563 when (not (null di)) $ iputStrLn (show di)
564 let d = lookupDef n (tt_ctxt i)
565 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
566 let cg = lookupCtxtName n (idris_callgraph i)
567 findUnusedArgs (map fst cg)
568 i <- getIState
569 let cg' = lookupCtxtName n (idris_callgraph i)
570 sc <- checkSizeChange n
571 iputStrLn $ "Size change: " ++ show sc
572 when (not (null cg')) $ do iputStrLn "Call graph:\n"
573 iputStrLn (show cg')
574process h fn (Info n)
575 = do i <- getIState
576 case lookupCtxt n (idris_classes i) of
577 [c] -> classInfo c
578 _ -> iPrintError "Not a class"
579process h fn (Search t) = iPrintError "Not implemented"
580-- FIXME: There is far too much repetition in the cases below!
581process h fn (CaseSplitAt updatefile l n)
582 = do src <- runIO $ readFile fn
583 res <- splitOnLine l n fn
584 iLOG (showSep "\n" (map show res))
585 let (before, (ap : later)) = splitAt (l-1) (lines src)
586 res' <- replaceSplits ap res
587 let new = concat res'
588 if updatefile
589 then do let fb = fn ++ "~" -- make a backup!
590 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
591 runIO $ copyFile fb fn
592 else -- do ihputStrLn h (show res)
593 ihPrintResult h new
594process h fn (AddClauseFrom updatefile l n)
595 = do src <- runIO $ readFile fn
596 let (before, tyline : later) = splitAt (l-1) (lines src)
597 let indent = getIndent 0 (show n) tyline
598 cl <- getClause l n fn
599 -- add clause before first blank line in 'later'
600 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
601 if updatefile
602 then do let fb = fn ++ "~"
603 runIO $ writeFile fb (unlines (before ++ nonblank) ++
604 replicate indent ' ' ++
605 cl ++ "\n" ++
606 unlines rest)
607 runIO $ copyFile fb fn
608 else ihPrintResult h cl
609 where
610 getIndent i n [] = 0
611 getIndent i n xs | take (length n) xs == n = i
612 getIndent i n (x : xs) = getIndent (i + 1) n xs
613process h fn (AddProofClauseFrom updatefile l n)
614 = do src <- runIO $ readFile fn
615 let (before, tyline : later) = splitAt (l-1) (lines src)
616 let indent = getIndent 0 (show n) tyline
617 cl <- getProofClause l n fn
618 -- add clause before first blank line in 'later'
619 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
620 if updatefile
621 then do let fb = fn ++ "~"
622 runIO $ writeFile fb (unlines (before ++ nonblank) ++
623 replicate indent ' ' ++
624 cl ++ "\n" ++
625 unlines rest)
626 runIO $ copyFile fb fn
627 else ihPrintResult h cl
628 where
629 getIndent i n [] = 0
630 getIndent i n xs | take (length n) xs == n = i
631 getIndent i n (x : xs) = getIndent (i + 1) n xs
632process h fn (AddMissing updatefile l n)
633 = do src <- runIO $ readFile fn
634 let (before, tyline : later) = splitAt (l-1) (lines src)
635 let indent = getIndent 0 (show n) tyline
636 i <- getIState
637 cl <- getInternalApp fn l
638 let n' = getAppName cl
640 extras <- case lookupCtxt n' (idris_patdefs i) of
641 [] -> return ""
642 [(_, tms)] -> do tms' <- nameMissing tms
643 showNew (show n ++ "_rhs") 1 indent tms'
644 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
645 if updatefile
646 then do let fb = fn ++ "~"
647 runIO $ writeFile fb (unlines (before ++ nonblank)
648 ++ extras ++ unlines rest)
649 runIO $ copyFile fb fn
650 else ihPrintResult h extras
651 where showPat = show . stripNS
652 stripNS tm = mapPT dens tm where
653 dens (PRef fc n) = PRef fc (nsroot n)
654 dens t = t
656 nsroot (NS n _) = nsroot n
657 nsroot (SN (WhereN _ _ n)) = nsroot n
658 nsroot n = n
660 getAppName (PApp _ r _) = getAppName r
661 getAppName (PRef _ r) = r
662 getAppName _ = n
664 showNew nm i ind (tm : tms)
665 = do (nm', i') <- getUniq nm i
666 rest <- showNew nm i' ind tms
667 return (replicate ind ' ' ++
668 showPat tm ++ " = ?" ++ nm' ++
669 "\n" ++ rest)
670 showNew nm i _ [] = return ""
672 getIndent i n [] = 0
673 getIndent i n xs | take (length n) xs == n = i
674 getIndent i n (x : xs) = getIndent (i + 1) n xs
676process h fn (MakeWith updatefile l n)
677 = do src <- runIO $ readFile fn
678 let (before, tyline : later) = splitAt (l-1) (lines src)
679 let ind = getIndent tyline
680 let with = mkWith tyline n
681 -- add clause before first blank line in 'later',
682 -- or (TODO) before first line with same indentation as tyline
683 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
684 not (ind == getIndent x)) later
685 if updatefile then
686 do let fb = fn ++ "~"
687 runIO $ writeFile fb (unlines (before ++ nonblank)
688 ++ with ++ "\n" ++
689 unlines rest)
690 runIO $ copyFile fb fn
691 else ihPrintResult h with
692 where getIndent s = length (takeWhile isSpace s)
694process h fn (DoProofSearch updatefile l n hints)
695 = do src <- runIO $ readFile fn
696 let (before, tyline : later) = splitAt (l-1) (lines src)
697 ctxt <- getContext
698 mn <- case lookupNames n ctxt of
699 [x] -> return x
700 [] -> return n
701 ns -> ierror (CantResolveAlts (map show ns))
702 i <- getIState
703 let (top, envlen, _) = case lookup mn (idris_metavars i) of
704 Just (t, e, False) -> (t, e, False)
705 _ -> (Nothing, 0, True)
706 let fc = fileFC fn
707 let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))
708 (ProofSearch t n hints)]
709 let def = PClause fc mn (PRef fc mn) [] (body top) []
710 newmv <- idrisCatch
711 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
712 (tm, ty) <- elabVal toplevel False (PRef fc mn)
713 ctxt <- getContext
714 i <- getIState
715 return $ show (stripNS
716 (dropCtxt envlen
717 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
718 (\e -> return ("?" ++ show n))
719 if updatefile then
720 do let fb = fn ++ "~"
721 runIO $ writeFile fb (unlines before ++
722 updateMeta False tyline (show n) newmv ++ "\n"
723 ++ unlines later)
724 runIO $ copyFile fb fn
725 else ihPrintResult h newmv
726 where dropCtxt 0 sc = sc
727 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
728 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
729 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
730 dropCtxt _ t = t
732 stripNS tm = mapPT dens tm where
733 dens (PRef fc n) = PRef fc (nsroot n)
734 dens t = t
736 nsroot (NS n _) = nsroot n
737 nsroot (SN (WhereN _ _ n)) = nsroot n
738 nsroot n = n
740 updateMeta brack ('?':cs) n new
741 | length cs >= length n
742 = case splitAt (length n) cs of
743 (mv, c:cs) ->
744 if (isSpace c && mv == n)
745 then addBracket brack new ++ (c : cs)
746 else '?' : mv ++ c : updateMeta True cs n new
747 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
748 updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
749 updateMeta brack (c:cs) n new
750 = c : updateMeta (brack || not (isSpace c)) cs n new
751 updateMeta brack [] n new = ""
753 addBracket False new = new
754 addBracket True new@('(':xs) | last xs == ')' = new
755 addBracket True new | any isSpace new = '(' : new ++ ")"
756 | otherwise = new
758process h fn (Spec t)
759 = do (tm, ty) <- elabVal toplevel False t
760 ctxt <- getContext
761 ist <- getIState
762 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
763 iPrintResult (show (delab ist tm'))
765process h fn (RmProof n')
766 = do i <- getIState
767 n <- resolveProof n'
768 let proofs = proof_list i
769 case lookup n proofs of
770 Nothing -> iputStrLn "No proof to remove"
771 Just _ -> do removeProof n
772 insertMetavar n
773 iputStrLn $ "Removed proof " ++ show n
774 where
775 insertMetavar :: Name -> Idris ()
776 insertMetavar n =
777 do i <- getIState
778 let ms = idris_metavars i
779 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
781process h fn' (AddProof prf)
782 = do fn <- do
783 ex <- runIO $ doesFileExist fn'
784 let fnExt = fn' <.> "idr"
785 exExt <- runIO $ doesFileExist fnExt
786 if ex
787 then return fn'
788 else if exExt
789 then return fnExt
790 else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
791 let fb = fn ++ "~"
792 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
793 prog <- runIO $ readFile fb
794 i <- getIState
795 let proofs = proof_list i
796 n' <- case prf of
797 Nothing -> case proofs of
798 [] -> ifail "No proof to add"
799 ((x, p) : _) -> return x
800 Just nm -> return nm
801 n <- resolveProof n'
802 case lookup n proofs of
803 Nothing -> iputStrLn "No proof to add"
804 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
805 runIO $ writeFile fn (unlines prog')
806 removeProof n
807 iputStrLn $ "Added proof " ++ show n
808 where ls = (lines prog)
810process h fn (ShowProof n')
811 = do i <- getIState
812 n <- resolveProof n'
813 let proofs = proof_list i
814 case lookup n proofs of
815 Nothing -> iPrintError "No proof to show"
816 Just p -> iPrintResult $ showProof False n p
818process h fn (Prove n')
819 = do ctxt <- getContext
820 ist <- getIState
821 let ns = lookupNames n' ctxt
822 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
823 n <- case metavars of
824 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
825 [(n, (_,_,False))] -> return n
826 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
827 ns -> ierror (CantResolveAlts (map show ns))
828 prover (lit fn) n
829 -- recheck totality
830 i <- getIState
831 totcheck (fileFC "(input)", n)
832 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
833 mapM_ checkDeclTotality (idris_totcheck i)
835process h fn (HNF t)
836 = do (tm, ty) <- elabVal toplevel False t
837 ctxt <- getContext
838 ist <- getIState
839 let tm' = hnf ctxt [] tm
840 iPrintResult (show (delab ist tm'))
841process h fn (TestInline t)
842 = do (tm, ty) <- elabVal toplevel False t
843 ctxt <- getContext
844 ist <- getIState
845 let tm' = inlineTerm ist tm
846 imp <- impShow
847 c <- colourise
848 iPrintResult (showImp (Just ist) imp c (delab ist tm'))
849process h fn Execute
850 = do (m, _) <- elabVal toplevel False
851 (PApp fc
852 (PRef fc (UN "run__IO"))
853 [pexp $ PRef fc (NS (UN "main") ["Main"])])
854-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
855 (tmpn, tmph) <- runIO tempfile
856 runIO $ hClose tmph
857 t <- codegen
858 compile t tmpn m
859 runIO $ system tmpn
860 return ()
861 where fc = fileFC "main"
862process h fn (Compile codegen f)
863 = do (m, _) <- elabVal toplevel False
864 (PApp fc (PRef fc (UN "run__IO"))
865 [pexp $ PRef fc (NS (UN "main") ["Main"])])
866 compile codegen f m
867 where fc = fileFC "main"
868process h fn (LogLvl i) = setLogLevel i
869-- Elaborate as if LHS of a pattern (debug command)
870process h fn (Pattelab t)
871 = do (tm, ty) <- elabVal toplevel True t
872 iPrintResult $ show tm ++ "\n\n : " ++ show ty
874process h fn (Missing n)
875 = do i <- getIState
876 c <- colourise
877 case lookupCtxt n (idris_patdefs i) of
878 [] -> return ()
879 [(_, tms)] ->
880 iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))
881 _ -> iPrintError $ "Ambiguous name"
882process h fn (DynamicLink l)
883 = do i <- getIState
884 let lib = trim l
885 handle <- lift . lift $ tryLoadLib lib
886 case handle of
887 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
888 Just x -> do let libs = idris_dynamic_libs i
889 if x `elem` libs
890 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
891 return ()
892 else putIState $ i { idris_dynamic_libs = x:libs }
893 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
894process h fn ListDynamic
895 = do i <- getIState
896 iputStrLn "Dynamic libraries:"
897 showLibs $ idris_dynamic_libs i
898 where showLibs [] = return ()
899 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
900process h fn Metavars
901 = do ist <- getIState
902 let mvs = map fst (idris_metavars ist) \\ primDefs
903 case mvs of
904 [] -> iPrintError "No global metavariables to solve"
905 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
906process h fn NOP = return ()
908process h fn (SetOpt ErrContext) = setErrContext True
909process h fn (UnsetOpt ErrContext) = setErrContext False
910process h fn (SetOpt ShowImpl) = setImpShow True
911process h fn (UnsetOpt ShowImpl) = setImpShow False
913process h fn (SetOpt _) = iPrintError "Not a valid option"
914process h fn (UnsetOpt _) = iPrintError "Not a valid option"
915process h fn (SetColour ty c) = setColour ty c
916process h fn ColourOn
917 = do ist <- getIState
918 putIState $ ist { idris_colourRepl = True }
919process h fn ColourOff
920 = do ist <- getIState
921 putIState $ ist { idris_colourRepl = False }
923classInfo :: ClassInfo -> Idris ()
924classInfo ci = do iputStrLn "Methods:\n"
925 mapM_ dumpMethod (class_methods ci)
926 iputStrLn ""
927 iputStrLn "Default superclass instances:\n"
928 mapM_ dumpDefaultInstance (class_default_superclasses ci)
929 iputStrLn ""
930 iputStrLn "Instances:\n"
931 mapM_ dumpInstance (class_instances ci)
932 iPrintResult ""
934dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
935dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
937dumpDefaultInstance :: PDecl -> Idris ()
938dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
940dumpInstance :: Name -> Idris ()
941dumpInstance n = do i <- getIState
942 ctxt <- getContext
943 imp <- impShow
944 case lookupTy n ctxt of
945 ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
947showTotal :: Totality -> IState -> String
948showTotal t@(Partial (Other ns)) i
949 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
950showTotal t i = show t
951showTotalN i n = case lookupTotal n (tt_ctxt i) of
952 [t] -> showTotal t i
953 _ -> ""
955displayHelp = let vstr = showVersion version in
956 "\nIdris version " ++ vstr ++ "\n" ++
957 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
958 concatMap cmdInfo helphead ++
959 concatMap cmdInfo help
960 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
961 col c1 c2 l m r =
962 l ++ take (c1 - length l) (repeat ' ') ++
963 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
965parseCodegen :: String -> Codegen
966parseCodegen "C" = ViaC
967parseCodegen "Java" = ViaJava
968parseCodegen "bytecode" = Bytecode
969parseCodegen "javascript" = ViaJavaScript
970parseCodegen "node" = ViaNode
971parseCodegen "llvm" = ViaLLVM
972parseCodegen _ = error "unknown codegen" -- FIXME: partial function
974parseArgs :: [String] -> [Opt]
975parseArgs [] = []
976parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)
977parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
978parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
979parseArgs ("--client":ns) = [Client (showSep " " ns)]
980parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
981parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)
982parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
983parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)
984parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
985parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
986parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
987parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
988parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
989parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
990parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
991parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
992parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
993parseArgs ("--help":ns) = Usage : (parseArgs ns)
994parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
995parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
996parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
997parseArgs ("--version":ns) = Ver : (parseArgs ns)
998parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
999parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
1000parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
1001parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
1002parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
1003parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1004parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1005parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1006parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1007parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
1008parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
1009parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
1010parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)
1011parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
1012parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
1013parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
1014parseArgs ["--exec"] = InterpretScript "Main.main" : []
1015parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
1016parseArgs (('-':'X':extName):ns) = case maybeRead extName of
1017 Just ext -> Extension ext : parseArgs ns
1018 -- Not sure what to do for the Nothing case
1019 Nothing -> error ("Unknown extension " ++ extName)
1020 where maybeRead = fmap fst . listToMaybe . reads
1021parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns
1022parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns
1023parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns
1024parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns
1025parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns
1026parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns
1027parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns
1028parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns
1029parseArgs ("--color":ns) = ColourREPL True : parseArgs ns
1030parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns
1031parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns
1032parseArgs (n:ns) = Filename n : (parseArgs ns)
1034helphead =
1035 [ (["Command"], SpecialHeaderArg, "Purpose"),
1036 ([""], NoArg, "")
1040replSettings :: Maybe FilePath -> Settings Idris
1041replSettings hFile = setComplete replCompletion $ defaultSettings {
1042 historyFile = hFile
1045-- invoke as if from command line
1046idris :: [Opt] -> IO (Maybe IState)
1047idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
1048 case res of
1049 Left err -> do putStrLn $ pshow idrisInit err
1050 return Nothing
1051 Right ist -> return (Just ist)
1054loadInputs :: Handle -> [FilePath] -> Idris ()
1055loadInputs h inputs
1056 = idrisCatch
1057 (do ist <- getIState
1058 -- if we're in --check and not outputting anything, don't bother
1059 -- loading, as it gets really slow if there's lots of modules in
1060 -- a package (instead, reload all at the end to check for
1061 -- consistency only)
1062 opts <- getCmdLine
1064 let loadCode = case opt getOutput opts of
1065 [] -> not (NoREPL `elem` opts)
1066 _ -> True
1068 -- For each ifile list, check it and build ibcs in the same clean IState
1069 -- so that they don't interfere with each other when checking
1071 let ninputs = zip [1..] inputs
1072 ifiles <- mapWhileOK (\(num, input) ->
1073 do putIState ist
1074 v <- verbose
1075 -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++
1076 -- show (length inputs) ++
1077 -- ") " ++ input
1078 modTree <- buildTree
1079 (map snd (take (num-1) ninputs))
1080 input
1081 let ifiles = getModuleFiles modTree
1082 iLOG ("MODULE TREE : " ++ show modTree)
1083 iLOG ("RELOAD: " ++ show ifiles)
1084 when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles
1085 -- return the files that need rechecking
1086 return (if (all ibc ifiles) then ifiles else []))
1087 ninputs
1088 inew <- getIState
1089 -- to check everything worked consistently (in particular, will catch
1090 -- if the ibc version is out of date) if we weren't loading per
1091 -- module
1092 case errLine inew of
1093 Nothing ->
1094 do putIState ist
1095 when (not loadCode) $ tryLoad $ nub (concat ifiles)
1096 _ -> return ()
1097 putIState inew)
1098 (\e -> do case e of
1099 At f _ -> do setErrLine (fc_line f)
1100 iputStrLn (show e)
1101 ProgramLineComment -> return () -- fail elsewhere
1102 _ -> do setErrLine 3 -- FIXME! Propagate it
1103 iputStrLn (show e))
1104 where -- load all files, stop if any fail
1105 tryLoad :: [IFileType] -> Idris ()
1106 tryLoad [] = return ()
1107 tryLoad (f : fs) = do loadFromIFile h f
1108 ok <- noErrors
1109 when ok $ tryLoad fs
1111 ibc (IBC _ _) = True
1112 ibc _ = False
1114 -- Like mapM, but give up when there's an error
1115 mapWhileOK f [] = return []
1116 mapWhileOK f (x : xs) = do x' <- f x
1117 ok <- noErrors
1118 if ok then do xs' <- mapWhileOK f xs
1119 return (x' : xs')
1120 else return [x']
1122idrisMain :: [Opt] -> Idris ()
1123idrisMain opts =
1124 do let inputs = opt getFile opts
1125 let quiet = Quiet `elem` opts
1126 let nobanner = NoBanner `elem` opts
1127 let idesl = Ideslave `elem` opts
1128 let runrepl = not (NoREPL `elem` opts)
1129 let verbose = runrepl || Verbose `elem` opts
1130 let output = opt getOutput opts
1131 let ibcsubdir = opt getIBCSubDir opts
1132 let importdirs = opt getImportDir opts
1133 let bcs = opt getBC opts
1134 let pkgdirs = opt getPkgDir opts
1135 let optimize = case opt getOptLevel opts of
1136 [] -> 2
1137 xs -> last xs
1138 trpl <- case opt getTriple opts of
1139 [] -> runIO $ getDefaultTargetTriple
1140 xs -> return (last xs)
1141 tcpu <- case opt getCPU opts of
1142 [] -> runIO $ getHostCPUName
1143 xs -> return (last xs)
1144 let outty = case opt getOutputTy opts of
1145 [] -> Executable
1146 xs -> last xs
1147 let cgn = case opt getCodegen opts of
1148 [] -> ViaC
1149 xs -> last xs
1150 script <- case opt getExecScript opts of
1151 [] -> return Nothing
1152 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1153 runIO $ exitWith (ExitFailure 1)
1154 [expr] -> return (Just expr)
1155 when (DefaultTotal `elem` opts) $ do i <- getIState
1156 putIState (i { default_total = True })
1157 setColourise $ not quiet && last (True : opt getColour opts)
1158 mapM_ addLangExt (opt getLanguageExt opts)
1159 setREPL runrepl
1160 setQuiet (quiet || isJust script)
1161 setIdeSlave idesl
1162 setVerbose verbose
1163 setCmdLine opts
1164 setOutputTy outty
1165 setCodegen cgn
1166 setTargetTriple trpl
1167 setTargetCPU tcpu
1168 setOptLevel optimize
1169 mapM_ makeOption opts
1170 -- if we have the --bytecode flag, drop into the bytecode assembler
1171 case bcs of
1172 [] -> return ()
1173 xs -> return () -- runIO $ mapM_ bcAsm xs
1174 case ibcsubdir of
1175 [] -> setIBCSubDir ""
1176 (d:_) -> setIBCSubDir d
1177 setImportDirs importdirs
1179 when (not (NoBasePkgs `elem` opts)) $ do
1180 addPkgDir "prelude"
1181 addPkgDir "base"
1182 mapM_ addPkgDir pkgdirs
1183 elabPrims
1184 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"
1185 return ()
1186 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1187 return ()
1188 when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner
1189 ist <- getIState
1191 loadInputs stdout inputs
1193 runIO $ hSetBuffering stdout LineBuffering
1195 ok <- noErrors
1196 when ok $ case output of
1197 [] -> return ()
1198 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1199 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1200 case script of
1201 Nothing -> return ()
1202 Just expr -> execScript expr
1204 -- Create Idris data dir + repl history and config dir
1205 idrisCatch (do dir <- getIdrisUserDataDir
1206 exists <- runIO $ doesDirectoryExist dir
1207 unless exists $ iLOG ("Creating " ++ dir)
1208 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1209 (\e -> return ())
1211 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1213 when (runrepl && not idesl) $ do
1214 initScript
1215 startServer ist inputs
1216 runInputT (replSettings (Just historyFile)) $ repl ist inputs
1217 when (idesl) $ ideslaveStart ist inputs
1218 ok <- noErrors
1219 when (not ok) $ runIO (exitWith (ExitFailure 1))
1220 where
1221 makeOption (OLogging i) = setLogLevel i
1222 makeOption TypeCase = setTypeCase True
1223 makeOption TypeInType = setTypeInType True
1224 makeOption NoCoverage = setCoverage False
1225 makeOption ErrContext = setErrContext True
1226 makeOption _ = return ()
1228 addPkgDir :: String -> Idris ()
1229 addPkgDir p = do ddir <- runIO $ getDataDir
1230 addImportDir (ddir </> p)
1232execScript :: String -> Idris ()
1233execScript expr = do i <- getIState
1234 c <- colourise
1235 case parseExpr i expr of
1236 Failure err -> do iputStrLn $ show (fixColour c err)
1237 runIO $ exitWith (ExitFailure 1)
1238 Success term -> do ctxt <- getContext
1239 (tm, _) <- elabVal toplevel False term
1240 res <- execute tm
1241 runIO $ exitWith ExitSuccess
1243-- | Check if the coloring matches the options and corrects if necessary
1244fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
1245fixColour False doc = ANSI.plain doc
1246fixColour True doc = doc
1248-- | Get the platform-specific, user-specific Idris dir
1249getIdrisUserDataDir :: Idris FilePath
1250getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1252-- | Locate the platform-specific location for the init script
1253getInitScript :: Idris FilePath
1254getInitScript = do idrisDir <- getIdrisUserDataDir
1255 return $ idrisDir </> "repl" </> "init"
1257-- | Run the initialisation script
1258initScript :: Idris ()
1259initScript = do script <- getInitScript
1260 idrisCatch (do go <- runIO $ doesFileExist script
1261 when go $ do
1262 h <- runIO $ openFile script ReadMode
1263 runInit h
1264 runIO $ hClose h)
1265 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1266 where runInit :: Handle -> Idris ()
1267 runInit h = do eof <- lift . lift $ hIsEOF h
1268 ist <- getIState
1269 unless eof $ do
1270 line <- runIO $ hGetLine h
1271 script <- getInitScript
1272 c <- colourise
1273 processLine ist line script c
1274 runInit h
1275 processLine i cmd input clr =
1276 case parseCmd i input cmd of
1277 Failure err -> runIO $ print (fixColour clr err)
1278 Success Reload -> iPrintError "Init scripts cannot reload the file"
1279 Success (Load f) -> iPrintError "Init scripts cannot load files"
1280 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1281 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1282 Success Proofs -> proofs i
1283 Success Quit -> iPrintError "Init scripts cannot quit Idris"
1284 Success cmd -> process stdout [] cmd
1286getFile :: Opt -> Maybe String
1287getFile (Filename str) = Just str
1288getFile _ = Nothing
1290getBC :: Opt -> Maybe String
1291getBC (BCAsm str) = Just str
1292getBC _ = Nothing
1294getOutput :: Opt -> Maybe String
1295getOutput (Output str) = Just str
1296getOutput _ = Nothing
1298getIBCSubDir :: Opt -> Maybe String
1299getIBCSubDir (IBCSubDir str) = Just str
1300getIBCSubDir _ = Nothing
1302getImportDir :: Opt -> Maybe String
1303getImportDir (ImportDir str) = Just str
1304getImportDir _ = Nothing
1306getPkgDir :: Opt -> Maybe String
1307getPkgDir (Pkg str) = Just str
1308getPkgDir _ = Nothing
1310getPkg :: Opt -> Maybe (Bool, String)
1311getPkg (PkgBuild str) = Just (False, str)
1312getPkg (PkgInstall str) = Just (True, str)
1313getPkg _ = Nothing
1315getPkgClean :: Opt -> Maybe String
1316getPkgClean (PkgClean str) = Just str
1317getPkgClean _ = Nothing
1319getCodegen :: Opt -> Maybe Codegen
1320getCodegen (UseCodegen x) = Just x
1321getCodegen _ = Nothing
1323getExecScript :: Opt -> Maybe String
1324getExecScript (InterpretScript expr) = Just expr
1325getExecScript _ = Nothing
1327getOutputTy :: Opt -> Maybe OutputType
1328getOutputTy (OutputTy t) = Just t
1329getOutputTy _ = Nothing
1331getLanguageExt :: Opt -> Maybe LanguageExt
1332getLanguageExt (Extension e) = Just e
1333getLanguageExt _ = Nothing
1335getTriple :: Opt -> Maybe String
1336getTriple (TargetTriple x) = Just x
1337getTriple _ = Nothing
1339getCPU :: Opt -> Maybe String
1340getCPU (TargetCPU x) = Just x
1341getCPU _ = Nothing
1343getOptLevel :: Opt -> Maybe Word
1344getOptLevel (OptLevel x) = Just x
1345getOptLevel _ = Nothing
1347getColour :: Opt -> Maybe Bool
1348getColour (ColourREPL b) = Just b
1349getColour _ = Nothing
1351opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1352opt = mapMaybe
1354ver = showVersion version ++ gitHash
1356banner = " ____ __ _ \n" ++
1357 " / _/___/ /____(_)____ \n" ++
1358 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1359 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1360 " /___/\\__,_/_/ /_/____/ Type :? for help \n"