git.iko.soy/Idris-dev
on 08ddbaa help sign in
Idris-dev/src/Idris/REPL.hs
1529 lines 68 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards, CPP #-}
4module Idris.REPL where
6import Idris.AbsSyntax
7import Idris.Apropos (apropos)
8import Idris.REPLParser
9import Idris.ElabDecls
10import Idris.ElabTerm
11import Idris.Erasure
12import Idris.Error
13import Idris.ErrReverse
14import Idris.Delaborate
15import Idris.Docstrings (Docstring, overview, renderDocstring)
16import Idris.Prover
17import Idris.Parser hiding (indent)
18import Idris.Primitives
19import Idris.Coverage
20import Idris.Docs hiding (Doc)
21import Idris.Help
22import Idris.Completion
23import qualified Idris.IdeSlave as IdeSlave
24import Idris.Chaser
25import Idris.Imports
26import Idris.Colours hiding (colourise)
27import Idris.Inliner
28import Idris.CaseSplit
29import Idris.DeepSeq
30import Idris.Output
32import Paths_idris
33import Version_idris (gitHash)
34import Util.System
35import Util.DynamicLinker
36import Util.Net (listenOnLocalhost)
37import Util.Pretty hiding ((</>))
39import Idris.Core.Evaluate
40import Idris.Core.Execute (execute)
41import Idris.Core.TT
42import Idris.Core.Constraints
44import IRTS.Compiler
45import IRTS.CodegenCommon
47import Data.List.Split (splitOn)
48import qualified Data.Text as T
50import Text.Trifecta.Result(Result(..))
52-- import RTS.SC
53-- import RTS.Bytecode
54-- import RTS.PreC
55-- import RTS.CodegenC
56#ifdef IDRIS_LLVM
57import LLVM.General.Target
58#else
59import Util.LLVMStubs
60#endif
61import System.Console.Haskeline as H
62import System.FilePath
63import System.Exit
64import System.Environment
65import System.Process
66import System.Directory
67import System.IO
68import Control.Monad
69import Control.Monad.Trans.Error (ErrorT(..))
70import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
71import Control.Monad.Trans ( lift )
72import Control.Concurrent.MVar
73import Network
74import Control.Concurrent
75import Data.Maybe
76import Data.List
77import Data.Char
78import Data.Version
79import Data.Word (Word)
80import Control.DeepSeq
82import Debug.Trace
84-- | Run the REPL
85repl :: IState -- ^ The initial state
86 -> [FilePath] -- ^ The loaded modules
87 -> InputT Idris ()
88repl orig mods
89 = -- H.catch
90 do let quiet = opt_quiet (idris_options orig)
91 i <- lift getIState
92 let colour = idris_colourRepl i
93 let theme = idris_colourTheme i
94 let mvs = idris_metavars i
95 let prompt = if quiet
96 then ""
97 else showMVs colour theme mvs ++
98 let str = mkPrompt mods ++ ">" in
99 (if colour then colourisePrompt theme str else str) ++ " "
100 x <- H.catch (getInputLine prompt)
101 (ctrlC (return Nothing))
102 case x of
103 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
104 return ()
105 Just input -> -- H.catch
106 do ms <- H.catch (lift $ processInput input orig mods)
107 (ctrlC (return (Just mods)))
108 case ms of
109 Just mods -> repl orig mods
110 Nothing -> return ()
111-- ctrlC)
112-- ctrlC
113 where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
114 ctrlC act e = do lift $ iputStrLn (show e)
115 act -- repl orig mods
117 showMVs c thm [] = ""
118 showMVs c thm ms = "Metavariables: " ++
119 show' 4 c thm (map fst ms) ++ "\n"
121 show' 0 c thm ms = let l = length ms in
122 "... ( + " ++ show l
123 ++ " other"
124 ++ if l == 1 then ")" else "s)"
125 show' n c thm [m] = showM c thm m
126 show' n c thm (m : ms) = showM c thm m ++ ", " ++
127 show' (n - 1) c thm ms
129 showM c thm n = if c then colouriseFun thm (show n)
130 else show n
132-- | Run the REPL server
133startServer :: IState -> [FilePath] -> Idris ()
134startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
135 return ()
136 where serverLoop :: IO ()
137 -- TODO: option for port number
138 serverLoop = withSocketsDo $
139 do sock <- listenOnLocalhost $ PortNumber 4294
140 loop fn orig sock
142 fn = case fn_in of
143 (f:_) -> f
144 _ -> ""
146 loop fn ist sock
147 = do (h,_,_) <- accept sock
148 cmd <- hGetLine h
149 (ist', fn) <- processNetCmd orig ist h fn cmd
150 hClose h
151 loop fn ist' sock
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 cmd -> runIdeSlaveCommand id orig fn mods cmd
220 Nothing -> iPrintError "did not understand" )
221 (\e -> do iPrintError $ show e))
222 (\e -> do iPrintError $ show e)
223 ideslave orig mods
225-- | Run IDESlave commands
226runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client
227 -> IState -- ^^ The original IState
228 -> FilePath -- ^^ The current open file
229 -> [FilePath] -- ^^ The currently loaded modules
230 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process
231 -> Idris ()
232runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
233 do c <- colourise
234 i <- getIState
235 case parseCmd i "(input)" cmd of
236 Failure err -> iPrintError $ show (fixColour c err)
237 Success (Prove n') -> do iPrintResult ""
238 idrisCatch
239 (process stdout fn (Prove n'))
240 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
241 isetPrompt (mkPrompt mods)
242 Success cmd -> idrisCatch
243 (ideslaveProcess fn cmd)
244 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
245runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =
246 do (unused, compls) <- replCompletion (reverse str, "")
247 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
248 IdeSlave.toSExp (map replacement compls,
249 reverse unused)]
250 runIO $ putStrLn $ IdeSlave.convSExp "return" good id
251runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =
252 do i <- getIState
253 clearErr
254 putIState (orig { idris_options = idris_options i,
255 idris_outputmode = (IdeSlave id) })
256 loadInputs stdout [filename]
257 isetPrompt (mkPrompt [filename])
258 -- Report either success or failure
259 i <- getIState
260 case (errSpan i) of
261 Nothing -> iPrintResult $ "loaded " ++ filename
262 Just x -> iPrintError $ "didn't load " ++ filename
263 ideslave orig [filename]
264runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
265 case splitName name of
266 Left err -> iPrintError err
267 Right n -> process stdout "(ideslave)"
268 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
269 where splitName :: String -> Either String Name
270 splitName s = case reverse $ splitOn "." s of
271 [] -> Left ("Didn't understand name '" ++ s ++ "'")
272 [n] -> Right $ sUN n
273 (n:ns) -> Right $ sNS (sUN n) ns
274runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
275 case splitName name of
276 Left err -> iPrintError err
277 Right n -> process stdout "(ideslave)" (DocStr n)
278 where splitName :: String -> Either String Name
279 splitName s = case reverse $ splitOn "." s of
280 [] -> Left ("Didn't understand name '" ++ s ++ "'")
281 [n] -> Right $ sUN n
282 (n:ns) -> Right $ sNS (sUN n) ns
283runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
284 process stdout fn (CaseSplitAt False line (sUN name))
285runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
286 process stdout fn (AddClauseFrom False line (sUN name))
287runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =
288 process stdout fn (AddProofClauseFrom False line (sUN name))
289runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =
290 process stdout fn (AddMissing False line (sUN name))
291runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
292 process stdout fn (MakeWith False line (sUN name))
293runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =
294 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
295runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
296 process stdout fn (Apropos a)
297runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
298 do ist <- getIState
299 let opts = idris_options ist
300 let impshow = opt_showimp opts
301 let errCtxt = opt_errContext opts
302 let options = (IdeSlave.SymbolAtom "ok",
303 [(IdeSlave.SymbolAtom "show-implicits", impshow),
304 (IdeSlave.SymbolAtom "error-context", errCtxt)])
305 runIO . putStrLn $ IdeSlave.convSExp "return" options id
306runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =
307 do setImpShow b
308 let msg = (IdeSlave.SymbolAtom "ok", b)
309 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
310runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
311 do setErrContext b
312 let msg = (IdeSlave.SymbolAtom "ok", b)
313 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
314runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
315 do ist <- getIState
316 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
317 imp <- impShow
318 let mvarTys = map (delabTy ist) mvs
319 let res = (IdeSlave.SymbolAtom "ok",
320 zipWith (\ n (prems, concl) -> (n, prems, concl))
321 (map (IdeSlave.StringAtom . show) mvs)
322 (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
323 runIO . putStrLn $ IdeSlave.convSExp "return" res id
324 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
325 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
326 in ((n, t):prems, conc)
327 getGoal tm = ([], tm)
328 sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)
329 -> ([(String, String, SpanList OutputAnnotation)],
330 (String, SpanList OutputAnnotation))
331 sexpGoal ist cols imp ns ([], concl) =
332 let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
333 pprintPTerm imp (zip ns (repeat False)) [] concl
334 in ([], concl')
335 sexpGoal ist cols imp ns ((n, t):ps, concl) =
336 let n' = case n of
337 NS (UN nm) ns -> str nm
338 UN nm | ('_':'_':_) <- str nm -> "_"
339 | otherwise -> str nm
340 _ -> "_"
341 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
342 pprintPTerm imp (zip ns (repeat False)) [] t
343 rest = sexpGoal ist cols imp (n:ns) (ps, concl)
344 in ((n', t', spans) : fst rest, snd rest)
347ideslaveProcess :: FilePath -> Command -> Idris ()
348ideslaveProcess fn Help = process stdout fn Help
349ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
350 iPrintResult "changed directory to"
351ideslaveProcess fn (Eval t) = process stdout fn (Eval t)
352ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)
353ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))
354ideslaveProcess fn (Check t) = process stdout fn (Check t)
355ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)
356ideslaveProcess fn Universes = process stdout fn Universes
357ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
358 iPrintResult ""
359ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
360ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
361 iPrintResult ""
362ideslaveProcess fn (Info n) = process stdout fn (Info n)
363ideslaveProcess fn (Search t) = process stdout fn (Search t)
364ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
365-- RmProof and AddProof not supported!
366ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')
367ideslaveProcess fn (HNF t) = process stdout fn (HNF t)
368--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!
369ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)
371ideslaveProcess fn Execute = do process stdout fn Execute
372 iPrintResult ""
373ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)
374 iPrintResult ""
375ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)
376 iPrintResult ""
377ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)
378ideslaveProcess fn (Missing n) = process stdout fn (Missing n)
379ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)
380 iPrintResult ""
381ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic
382 iPrintResult ""
383ideslaveProcess fn Metavars = process stdout fn Metavars
384ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)
385 iPrintResult ""
386ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)
387 iPrintResult ""
388ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)
389 iPrintResult ""
390ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)
391 iPrintResult ""
392ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)
393 iPrintResult ""
394ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)
395 iPrintResult ""
396ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)
397ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)
398ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)
399ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)
400ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
401ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
402ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
403ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)
404ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
405 iPrintResult ""
406ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
407 iPrintResult ""
408ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
411-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
412mkPrompt [] = "Idris"
413mkPrompt [x] = "*" ++ dropExtension x
414mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
416-- | Determine whether a file uses literate syntax
417lit f = case splitExtension f of
418 (_, ".lidr") -> True
419 _ -> False
421processInput :: String ->
422 IState -> [FilePath] -> Idris (Maybe [FilePath])
423processInput cmd orig inputs
424 = do i <- getIState
425 let opts = idris_options i
426 let quiet = opt_quiet opts
427 let fn = case inputs of
428 (f:_) -> f
429 _ -> ""
430 c <- colourise
431 case parseCmd i "(input)" cmd of
432 Failure err -> do runIO $ print (fixColour c err)
433 return (Just inputs)
434 Success Reload ->
435 do putIState $ orig { idris_options = idris_options i
436 , idris_colourTheme = idris_colourTheme i
437 }
438 clearErr
439 mods <- loadInputs stdout inputs
440 return (Just inputs)
441 Success (Load f) ->
442 do putIState orig { idris_options = idris_options i
443 , idris_colourTheme = idris_colourTheme i
444 }
445 clearErr
446 mod <- loadInputs stdout [f]
447 return (Just [f])
448 Success (ModImport f) ->
449 do clearErr
450 fmod <- loadModule stdout f
451 return (Just (inputs ++ [fmod]))
452 Success Edit -> do -- takeMVar stvar
453 edit fn orig
454 return (Just inputs)
455 Success Proofs -> do proofs orig
456 return (Just inputs)
457 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
458 return Nothing
459 Success cmd -> do idrisCatch (process stdout fn cmd)
460 (\e -> do msg <- showErr e ; iputStrLn msg)
461 return (Just inputs)
463resolveProof :: Name -> Idris Name
464resolveProof n'
465 = do i <- getIState
466 ctxt <- getContext
467 n <- case lookupNames n' ctxt of
468 [x] -> return x
469 [] -> return n'
470 ns -> ierror (CantResolveAlts (map show ns))
471 return n
473removeProof :: Name -> Idris ()
474removeProof n =
475 do i <- getIState
476 let proofs = proof_list i
477 let ps = filter ((/= n) . fst) proofs
478 putIState $ i { proof_list = ps }
480edit :: FilePath -> IState -> Idris ()
481edit "" orig = iputStrLn "Nothing to edit"
482edit f orig
483 = do i <- getIState
484 env <- runIO $ getEnvironment
485 let editor = getEditor env
486 let line = case errSpan i of
487 Just l -> " +" ++ show (fst (fc_start l)) ++ " "
488 Nothing -> " "
489 let cmd = editor ++ line ++ fixName f
490 runIO $ system cmd
491 clearErr
492 putIState $ orig { idris_options = idris_options i
493 , idris_colourTheme = idris_colourTheme i
494 }
495 loadInputs stdout [f]
496-- clearOrigPats
497 iucheck
498 return ()
499 where getEditor env | Just ed <- lookup "EDITOR" env = ed
500 | Just ed <- lookup "VISUAL" env = ed
501 | otherwise = "vi"
502 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file
503 | otherwise = addExtension file "idr"
507proofs :: IState -> Idris ()
508proofs orig
509 = do i <- getIState
510 let ps = proof_list i
511 case ps of
512 [] -> iputStrLn "No proofs available"
513 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
515insertScript :: String -> [String] -> [String]
516insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
517insertScript prf (p@"---------- Proofs ----------" : "" : xs)
518 = p : "" : prf : xs
519insertScript prf (x : xs) = x : insertScript prf xs
521process :: Handle -> FilePath -> Command -> Idris ()
522process h fn Help = iPrintResult displayHelp
523process h fn (ChangeDirectory f)
524 = do runIO $ setCurrentDirectory f
525 return ()
526process h fn (Eval t)
527 = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
528 ctxt <- getContext
529 let tm' = force (normaliseAll ctxt [] tm)
530 let ty' = force (normaliseAll ctxt [] ty)
531 -- Add value to context, call it "it"
532 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
533 ist <- getIState
534 logLvl 3 $ "Raw: " ++ show (tm', ty')
535 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
536 let imp = opt_showimp (idris_options ist)
537 tmDoc = prettyImp imp (delab ist tm')
538 tyDoc = prettyImp imp (delab ist ty')
539 ihPrintTermWithType h tmDoc tyDoc
541process h fn (ExecVal t)
542 = do ctxt <- getContext
543 ist <- getIState
544 let imp = opt_showimp (idris_options ist)
545 (tm, ty) <- elabVal toplevel False t
546-- let tm' = normaliseAll ctxt [] tm
547 let ty' = normaliseAll ctxt [] ty
548 res <- execute tm
549 let (resOut, tyOut) = (prettyImp imp (delab ist res),
550 prettyImp imp (delab ist ty'))
551 ihPrintTermWithType h resOut tyOut
553process h fn (Check (PRef _ n))
554 = do ctxt <- getContext
555 ist <- getIState
556 imp <- impShow
557 case lookupNames n ctxt of
558 ts@(t:_) ->
559 case lookup t (idris_metavars ist) of
560 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
561 showMetavarInfo imp ist n i
562 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
563 [] -> ihPrintError h $ "No such variable " ++ show n
564 where
565 showMetavarInfo imp ist n i
566 = case lookupTy n (tt_ctxt ist) of
567 (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
568 putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
569 putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
570 putTy imp ist i bnd (PPi _ n t sc)
571 = let current = text " " <>
572 (case n of
573 MN _ _ -> text "_"
574 UN nm | ('_':'_':_) <- str nm -> text "_"
575 _ -> bindingOf n False) <+>
576 colon <+> align (tPretty bnd ist t) <> line
577 in
578 current <> putTy imp ist (i-1) ((n,False):bnd) sc
579 putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
580 putGoal imp ist bnd g
581 = text "--------------------------------------" <$>
582 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
583 align (tPretty bnd ist g)
585 tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t
588process h fn (Check t)
589 = do (tm, ty) <- elabVal toplevel False t
590 ctxt <- getContext
591 ist <- getIState
592 let imp = opt_showimp (idris_options ist)
593 ty' = normaliseC ctxt [] ty
594 case tm of
595 TType _ ->
596 ihPrintTermWithType h (prettyImp imp PType) type1Doc
597 _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
598 (prettyImp imp (delab ist ty))
600process h fn (DocStr n)
601 = do i <- getIState
602 let imp = opt_showimp (idris_options i)
603 case lookupCtxtName n (idris_docstrings i) of
604 [] -> iPrintError $ "No documentation for " ++ show n
605 ns -> do toShow <- mapM (showDoc imp) ns
606 ihRenderResult h (vsep toShow)
607 where showDoc imp (n, d) = do doc <- getDocs n
608 return $ pprintDocs imp doc
609process h fn Universes
610 = do i <- getIState
611 let cs = idris_constraints i
612-- iputStrLn $ showSep "\n" (map show cs)
613 iputStrLn $ show (map fst cs)
614 let n = length cs
615 iputStrLn $ "(" ++ show n ++ " constraints)"
616 case ucheck cs of
617 Error e -> iPrintError $ pshow i e
618 OK _ -> iPrintResult "Universes OK"
619process h fn (Defn n)
620 = do i <- getIState
621 iputStrLn "Compiled patterns:\n"
622 iputStrLn $ show (lookupDef n (tt_ctxt i))
623 case lookupCtxt n (idris_patdefs i) of
624 [] -> return ()
625 [(d, _)] -> do iputStrLn "Original definiton:\n"
626 mapM_ (printCase i) d
627 case lookupTotal n (tt_ctxt i) of
628 [t] -> iputStrLn (showTotal t i)
629 _ -> return ()
630 where printCase i (_, lhs, rhs)
631 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
632 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
633 showTm i' (delab i rhs))
634process h fn (TotCheck n)
635 = do i <- getIState
636 case lookupNameTotal n (tt_ctxt i) of
637 [] -> ihPrintError h $ "Unknown operator " ++ show n
638 ts -> do ist <- getIState
639 c <- colourise
640 imp <- impShow
641 let showN = showName (Just ist) [] imp c
642 ihPrintResult h . concat . intersperse "\n" .
643 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
644 ts
647process h fn (DebugInfo n)
648 = do i <- getIState
649 let oi = lookupCtxtName n (idris_optimisation i)
650 when (not (null oi)) $ iputStrLn (show oi)
651 let si = lookupCtxt n (idris_statics i)
652 when (not (null si)) $ iputStrLn (show si)
653 let di = lookupCtxt n (idris_datatypes i)
654 when (not (null di)) $ iputStrLn (show di)
655 let d = lookupDef n (tt_ctxt i)
656 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
657 let cg = lookupCtxtName n (idris_callgraph i)
658 i <- getIState
659 let cg' = lookupCtxtName n (idris_callgraph i)
660 sc <- checkSizeChange n
661 iputStrLn $ "Size change: " ++ show sc
662 when (not (null cg')) $ do iputStrLn "Call graph:\n"
663 iputStrLn (show cg')
664process h fn (Info n)
665 = do i <- getIState
666 case lookupCtxt n (idris_classes i) of
667 [c] -> do info <- classInfo c
668 ihRenderResult h info
669 _ -> iPrintError "Not a class"
670process h fn (Search t) = iPrintError "Not implemented"
671-- FIXME: There is far too much repetition in the cases below!
672process h fn (CaseSplitAt updatefile l n)
673 = do src <- runIO $ readFile fn
674 res <- splitOnLine l n fn
675 iLOG (showSep "\n" (map show res))
676 let (before, (ap : later)) = splitAt (l-1) (lines src)
677 res' <- replaceSplits ap res
678 let new = concat res'
679 if updatefile
680 then do let fb = fn ++ "~" -- make a backup!
681 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
682 runIO $ copyFile fb fn
683 else -- do ihputStrLn h (show res)
684 ihPrintResult h new
685process h fn (AddClauseFrom updatefile l n)
686 = do src <- runIO $ readFile fn
687 let (before, tyline : later) = splitAt (l-1) (lines src)
688 let indent = getIndent 0 (show n) tyline
689 cl <- getClause l n fn
690 -- add clause before first blank line in 'later'
691 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
692 if updatefile
693 then do let fb = fn ++ "~"
694 runIO $ writeFile fb (unlines (before ++ nonblank) ++
695 replicate indent ' ' ++
696 cl ++ "\n" ++
697 unlines rest)
698 runIO $ copyFile fb fn
699 else ihPrintResult h cl
700 where
701 getIndent i n [] = 0
702 getIndent i n xs | take (length n) xs == n = i
703 getIndent i n (x : xs) = getIndent (i + 1) n xs
704process h fn (AddProofClauseFrom updatefile l n)
705 = do src <- runIO $ readFile fn
706 let (before, tyline : later) = splitAt (l-1) (lines src)
707 let indent = getIndent 0 (show n) tyline
708 cl <- getProofClause l n fn
709 -- add clause before first blank line in 'later'
710 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
711 if updatefile
712 then do let fb = fn ++ "~"
713 runIO $ writeFile fb (unlines (before ++ nonblank) ++
714 replicate indent ' ' ++
715 cl ++ "\n" ++
716 unlines rest)
717 runIO $ copyFile fb fn
718 else ihPrintResult h cl
719 where
720 getIndent i n [] = 0
721 getIndent i n xs | take (length n) xs == n = i
722 getIndent i n (x : xs) = getIndent (i + 1) n xs
723process h fn (AddMissing updatefile l n)
724 = do src <- runIO $ readFile fn
725 let (before, tyline : later) = splitAt (l-1) (lines src)
726 let indent = getIndent 0 (show n) tyline
727 i <- getIState
728 cl <- getInternalApp fn l
729 let n' = getAppName cl
731 extras <- case lookupCtxt n' (idris_patdefs i) of
732 [] -> return ""
733 [(_, tms)] -> do tms' <- nameMissing tms
734 showNew (show n ++ "_rhs") 1 indent tms'
735 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
736 if updatefile
737 then do let fb = fn ++ "~"
738 runIO $ writeFile fb (unlines (before ++ nonblank)
739 ++ extras ++ unlines rest)
740 runIO $ copyFile fb fn
741 else ihPrintResult h extras
742 where showPat = show . stripNS
743 stripNS tm = mapPT dens tm where
744 dens (PRef fc n) = PRef fc (nsroot n)
745 dens t = t
747 nsroot (NS n _) = nsroot n
748 nsroot (SN (WhereN _ _ n)) = nsroot n
749 nsroot n = n
751 getAppName (PApp _ r _) = getAppName r
752 getAppName (PRef _ r) = r
753 getAppName _ = n
755 showNew nm i ind (tm : tms)
756 = do (nm', i') <- getUniq nm i
757 rest <- showNew nm i' ind tms
758 return (replicate ind ' ' ++
759 showPat tm ++ " = ?" ++ nm' ++
760 "\n" ++ rest)
761 showNew nm i _ [] = return ""
763 getIndent i n [] = 0
764 getIndent i n xs | take (length n) xs == n = i
765 getIndent i n (x : xs) = getIndent (i + 1) n xs
767process h fn (MakeWith updatefile l n)
768 = do src <- runIO $ readFile fn
769 let (before, tyline : later) = splitAt (l-1) (lines src)
770 let ind = getIndent tyline
771 let with = mkWith tyline n
772 -- add clause before first blank line in 'later',
773 -- or (TODO) before first line with same indentation as tyline
774 let (nonblank, rest) = span (\x -> not (all isSpace x) &&
775 not (ind == getIndent x)) later
776 if updatefile then
777 do let fb = fn ++ "~"
778 runIO $ writeFile fb (unlines (before ++ nonblank)
779 ++ with ++ "\n" ++
780 unlines rest)
781 runIO $ copyFile fb fn
782 else ihPrintResult h with
783 where getIndent s = length (takeWhile isSpace s)
785process h fn (DoProofSearch updatefile l n hints)
786 = do src <- runIO $ readFile fn
787 let (before, tyline : later) = splitAt (l-1) (lines src)
788 ctxt <- getContext
789 mn <- case lookupNames n ctxt of
790 [x] -> return x
791 [] -> return n
792 ns -> ierror (CantResolveAlts (map show ns))
793 i <- getIState
794 let (top, envlen, _) = case lookup mn (idris_metavars i) of
795 Just (t, e, False) -> (t, e, False)
796 _ -> (Nothing, 0, True)
797 let fc = fileFC fn
798 let body t = PProof [Try (TSeq Intros (ProofSearch t hints))
799 (ProofSearch t hints)]
800 let def = PClause fc mn (PRef fc mn) [] (body top) []
801 newmv <- idrisCatch
802 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
803 (tm, ty) <- elabVal toplevel False (PRef fc mn)
804 ctxt <- getContext
805 i <- getIState
806 return $ show (stripNS
807 (dropCtxt envlen
808 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
809 (\e -> return ("?" ++ show n))
810 if updatefile then
811 do let fb = fn ++ "~"
812 runIO $ writeFile fb (unlines before ++
813 updateMeta False tyline (show n) newmv ++ "\n"
814 ++ unlines later)
815 runIO $ copyFile fb fn
816 else ihPrintResult h newmv
817 where dropCtxt 0 sc = sc
818 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
819 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
820 dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
821 dropCtxt _ t = t
823 stripNS tm = mapPT dens tm where
824 dens (PRef fc n) = PRef fc (nsroot n)
825 dens t = t
827 nsroot (NS n _) = nsroot n
828 nsroot (SN (WhereN _ _ n)) = nsroot n
829 nsroot n = n
831 updateMeta brack ('?':cs) n new
832 | length cs >= length n
833 = case splitAt (length n) cs of
834 (mv, c:cs) ->
835 if ((isSpace c || c == ')' || c == '}') && mv == n)
836 then addBracket brack new ++ (c : cs)
837 else '?' : mv ++ c : updateMeta True cs n new
838 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
839 updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
840 updateMeta brack (c:cs) n new
841 = c : updateMeta (brack || not (isSpace c)) cs n new
842 updateMeta brack [] n new = ""
844 addBracket False new = new
845 addBracket True new@('(':xs) | last xs == ')' = new
846 addBracket True new | any isSpace new = '(' : new ++ ")"
847 | otherwise = new
849process h fn (Spec t)
850 = do (tm, ty) <- elabVal toplevel False t
851 ctxt <- getContext
852 ist <- getIState
853 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
854 iPrintResult (show (delab ist tm'))
856process h fn (RmProof n')
857 = do i <- getIState
858 n <- resolveProof n'
859 let proofs = proof_list i
860 case lookup n proofs of
861 Nothing -> iputStrLn "No proof to remove"
862 Just _ -> do removeProof n
863 insertMetavar n
864 iputStrLn $ "Removed proof " ++ show n
865 where
866 insertMetavar :: Name -> Idris ()
867 insertMetavar n =
868 do i <- getIState
869 let ms = idris_metavars i
870 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
872process h fn' (AddProof prf)
873 = do fn <- do
874 ex <- runIO $ doesFileExist fn'
875 let fnExt = fn' <.> "idr"
876 exExt <- runIO $ doesFileExist fnExt
877 if ex
878 then return fn'
879 else if exExt
880 then return fnExt
881 else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
882 let fb = fn ++ "~"
883 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
884 prog <- runIO $ readFile fb
885 i <- getIState
886 let proofs = proof_list i
887 n' <- case prf of
888 Nothing -> case proofs of
889 [] -> ifail "No proof to add"
890 ((x, p) : _) -> return x
891 Just nm -> return nm
892 n <- resolveProof n'
893 case lookup n proofs of
894 Nothing -> iputStrLn "No proof to add"
895 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
896 runIO $ writeFile fn (unlines prog')
897 removeProof n
898 iputStrLn $ "Added proof " ++ show n
899 where ls = (lines prog)
901process h fn (ShowProof n')
902 = do i <- getIState
903 n <- resolveProof n'
904 let proofs = proof_list i
905 case lookup n proofs of
906 Nothing -> iPrintError "No proof to show"
907 Just p -> iPrintResult $ showProof False n p
909process h fn (Prove n')
910 = do ctxt <- getContext
911 ist <- getIState
912 let ns = lookupNames n' ctxt
913 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
914 n <- case metavars of
915 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
916 [(n, (_,_,False))] -> return n
917 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
918 ns -> ierror (CantResolveAlts (map show ns))
919 prover (lit fn) n
920 -- recheck totality
921 i <- getIState
922 totcheck (fileFC "(input)", n)
923 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
924 mapM_ checkDeclTotality (idris_totcheck i)
926process h fn (HNF t)
927 = do (tm, ty) <- elabVal toplevel False t
928 ctxt <- getContext
929 ist <- getIState
930 let tm' = hnf ctxt [] tm
931 iPrintResult (show (delab ist tm'))
932process h fn (TestInline t)
933 = do (tm, ty) <- elabVal toplevel False t
934 ctxt <- getContext
935 ist <- getIState
936 let tm' = inlineTerm ist tm
937 imp <- impShow
938 c <- colourise
939 iPrintResult (showTm ist (delab ist tm'))
940process h fn Execute
941 = do ist <- getIState
942 (m, _) <- elabVal toplevel False
943 (PApp fc
944 (PRef fc (sUN "run__IO"))
945 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
946 (tmpn, tmph) <- runIO tempfile
947 runIO $ hClose tmph
948 t <- codegen
949 compile t tmpn m
950 case idris_outputmode ist of
951 RawOutput -> do runIO $ system tmpn
952 return ()
953 IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n
954 where fc = fileFC "main"
955process h fn (Compile codegen f)
956 = do (m, _) <- elabVal toplevel False
957 (PApp fc (PRef fc (sUN "run__IO"))
958 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
959 compile codegen f m
960 where fc = fileFC "main"
961process h fn (LogLvl i) = setLogLevel i
962-- Elaborate as if LHS of a pattern (debug command)
963process h fn (Pattelab t)
964 = do (tm, ty) <- elabVal toplevel True t
965 iPrintResult $ show tm ++ "\n\n : " ++ show ty
967process h fn (Missing n)
968 = do i <- getIState
969 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
970 case lookupCtxt n (idris_patdefs i) of
971 [] -> return ()
972 [(_, tms)] ->
973 iPrintResult (showSep "\n" (map (showTm i') tms))
974 _ -> iPrintError $ "Ambiguous name"
975process h fn (DynamicLink l)
976 = do i <- getIState
977 let importdirs = opt_importdirs (idris_options i)
978 lib = trim l
979 handle <- lift . lift $ tryLoadLib importdirs lib
980 case handle of
981 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
982 Just x -> do let libs = idris_dynamic_libs i
983 if x `elem` libs
984 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
985 return ()
986 else putIState $ i { idris_dynamic_libs = x:libs }
987 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
988process h fn ListDynamic
989 = do i <- getIState
990 iputStrLn "Dynamic libraries:"
991 showLibs $ idris_dynamic_libs i
992 where showLibs [] = return ()
993 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
994process h fn Metavars
995 = do ist <- getIState
996 let mvs = map fst (idris_metavars ist) \\ primDefs
997 case mvs of
998 [] -> iPrintError "No global metavariables to solve"
999 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
1000process h fn NOP = return ()
1002process h fn (SetOpt ErrContext) = setErrContext True
1003process h fn (UnsetOpt ErrContext) = setErrContext False
1004process h fn (SetOpt ShowImpl) = setImpShow True
1005process h fn (UnsetOpt ShowImpl) = setImpShow False
1006process h fn (SetOpt ShowOrigErr) = setShowOrigErr True
1007process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1008process h fn (SetOpt AutoSolve) = setAutoSolve True
1009process h fn (UnsetOpt AutoSolve) = setAutoSolve False
1011process h fn (SetOpt _) = iPrintError "Not a valid option"
1012process h fn (UnsetOpt _) = iPrintError "Not a valid option"
1013process h fn (SetColour ty c) = setColour ty c
1014process h fn ColourOn
1015 = do ist <- getIState
1016 putIState $ ist { idris_colourRepl = True }
1017process h fn ColourOff
1018 = do ist <- getIState
1019 putIState $ ist { idris_colourRepl = False }
1020process h fn ListErrorHandlers =
1021 do ist <- getIState
1022 case idris_errorhandlers ist of
1023 [] -> iPrintResult "No registered error handlers"
1024 handlers ->
1025 iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1026process h fn (SetConsoleWidth w) = setWidth w
1028process h fn (Apropos a) =
1029 do ist <- getIState
1030 let impl = opt_showimp (idris_options ist)
1031 let names = apropos ist (T.pack a)
1032 let aproposInfo = [ (n,
1033 delabTy ist n,
1034 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1035 | n <- sort names, isUN n ]
1036 ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)
1037 where renderApropos impl (name, ty, docs) =
1038 prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>
1039 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1040 isUN (UN _) = True
1041 isUN (NS n _) = isUN n
1042 isUN _ = False
1044classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
1045classInfo ci = do ist <- getIState
1046 ctxt <- getContext
1047 return $
1048 text "Parameters:" <+>
1049 hsep (punctuate comma (map (prettyName False params') params)) <>
1050 line <> line <>
1051 text "Methods:" <> line <>
1052 indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>
1053 text "Default superclass instances:" <>
1054 line <>
1055 indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>
1056 line <>
1057 text "Instances:" <> line <>
1058 indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))
1059 where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
1060 dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
1061 dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
1062 dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
1063 dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
1064 dumpInstance ist ctxt n = pp ist $ delabTy ist n
1065 params = class_params ci
1066 params' = zip params (repeat False)
1067 pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []
1069showTotal :: Totality -> IState -> String
1070showTotal t@(Partial (Other ns)) i
1071 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
1072showTotal t i = show t
1073showTotalN i n = case lookupTotal n (tt_ctxt i) of
1074 [t] -> showTotal t i
1075 _ -> ""
1077displayHelp = let vstr = showVersion version in
1078 "\nIdris version " ++ vstr ++ "\n" ++
1079 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
1080 concatMap cmdInfo helphead ++
1081 concatMap cmdInfo help
1082 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
1083 col c1 c2 l m r =
1084 l ++ take (c1 - length l) (repeat ' ') ++
1085 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1087parseCodegen :: String -> Codegen
1088parseCodegen "C" = ViaC
1089parseCodegen "Java" = ViaJava
1090parseCodegen "bytecode" = Bytecode
1091parseCodegen "javascript" = ViaJavaScript
1092parseCodegen "node" = ViaNode
1093parseCodegen "llvm" = ViaLLVM
1094parseCodegen _ = error "unknown codegen" -- FIXME: partial function
1096parseArgs :: [String] -> [Opt]
1097parseArgs [] = []
1098parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)
1099parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
1100parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
1101parseArgs ("--client":ns) = [Client (showSep " " ns)]
1102parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
1103parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)
1104parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
1105parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)
1106parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
1107parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
1108parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
1109parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
1110parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
1111parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
1112parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
1113parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)
1114parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
1115parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
1116parseArgs ("--help":ns) = Usage : (parseArgs ns)
1117parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
1118parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
1119parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
1120parseArgs ("--version":ns) = Ver : (parseArgs ns)
1121parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
1122parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
1123parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
1124parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
1125-- Package Related options
1126parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
1127parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1128parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1129parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1130parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)
1131parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1132parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)
1133-- Misc Options
1134parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
1135parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
1136parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
1137parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)
1138parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
1139parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
1140parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
1141parseArgs ["--exec"] = InterpretScript "Main.main" : []
1142parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
1143parseArgs (('-':'X':extName):ns) = case maybeRead extName of
1144 Just ext -> Extension ext : parseArgs ns
1145 -- Not sure what to do for the Nothing case
1146 Nothing -> error ("Unknown extension " ++ extName)
1147 where maybeRead = fmap fst . listToMaybe . reads
1148parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns
1149parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns
1150parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns
1151parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns
1152parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns
1153parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns
1154parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns
1155parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns
1156parseArgs ("--color":ns) = ColourREPL True : parseArgs ns
1157parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns
1158parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns
1159parseArgs (n:ns) = Filename n : (parseArgs ns)
1161helphead =
1162 [ (["Command"], SpecialHeaderArg, "Purpose"),
1163 ([""], NoArg, "")
1167replSettings :: Maybe FilePath -> Settings Idris
1168replSettings hFile = setComplete replCompletion $ defaultSettings {
1169 historyFile = hFile
1172-- invoke as if from command line
1173idris :: [Opt] -> IO (Maybe IState)
1174idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
1175 case res of
1176 Left err -> do putStrLn $ pshow idrisInit err
1177 return Nothing
1178 Right ist -> return (Just ist)
1181loadInputs :: Handle -> [FilePath] -> Idris ()
1182loadInputs h inputs
1183 = idrisCatch
1184 (do ist <- getIState
1185 -- if we're in --check and not outputting anything, don't bother
1186 -- loading, as it gets really slow if there's lots of modules in
1187 -- a package (instead, reload all at the end to check for
1188 -- consistency only)
1189 opts <- getCmdLine
1191 let loadCode = case opt getOutput opts of
1192 [] -> not (NoREPL `elem` opts)
1193 _ -> True
1195 -- For each ifile list, check it and build ibcs in the same clean IState
1196 -- so that they don't interfere with each other when checking
1198 let ninputs = zip [1..] inputs
1199 ifiles <- mapWhileOK (\(num, input) ->
1200 do putIState ist
1201 modTree <- buildTree
1202 (map snd (take (num-1) ninputs))
1203 input
1204 let ifiles = getModuleFiles modTree
1205 iLOG ("MODULE TREE : " ++ show modTree)
1206 iLOG ("RELOAD: " ++ show ifiles)
1207 when (not (all ibc ifiles) || loadCode) $
1208 tryLoad False (filter (not . ibc) ifiles)
1209 -- return the files that need rechecking
1210 return ifiles)
1211 ninputs
1212 inew <- getIState
1213 let tidata = idris_tyinfodata inew
1214 let lineapps = idris_lineapps inew
1215 let patdefs = idris_patdefs inew
1216 -- If it worked, load the whole thing from all the ibcs together
1217 case errSpan inew of
1218 Nothing ->
1219 do putIState (ist { idris_tyinfodata = tidata })
1220 ibcfiles <- mapM findNewIBC (nub (concat ifiles))
1221 tryLoad True (mapMaybe id ibcfiles)
1222 _ -> return ()
1223 ist <- getIState
1224 putIState (ist { idris_tyinfodata = tidata,
1225 idris_lineapps = lineapps,
1226 idris_patdefs = patdefs }))
1227 (\e -> do i <- getIState
1228 case e of
1229 At f _ -> do setErrSpan f
1230 ihRenderError stdout $ pprintErr i e
1231 ProgramLineComment -> return () -- fail elsewhere
1232 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1233 iputStrLn (pshow i e))
1234 where -- load all files, stop if any fail
1235 tryLoad :: Bool -> [IFileType] -> Idris ()
1236 tryLoad keepstate [] = return ()
1237 tryLoad keepstate (f : fs)
1238 = do ist <- getIState
1239 loadFromIFile h f
1240 inew <- getIState
1241 -- FIXME: Save these in IBC to avoid this hack! Need to
1242 -- preserve it all from source inputs
1243 let tidata = idris_tyinfodata inew
1244 let lineapps = idris_lineapps inew
1245 let patdefs = idris_patdefs inew
1246 ok <- noErrors
1247 when ok $ do when (not keepstate) $ putIState ist
1248 ist <- getIState
1249 putIState (ist { idris_tyinfodata = tidata,
1250 idris_lineapps = lineapps,
1251 idris_patdefs = patdefs })
1252 tryLoad keepstate fs
1254 ibc (IBC _ _) = True
1255 ibc _ = False
1257 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1258 findNewIBC i@(IBC _ _) = return (Just i)
1259 findNewIBC s@(IDR f) = do ist <- get
1260 ibcsd <- valIBCSubDir ist
1261 let ibc = ibcPathNoFallback ibcsd f
1262 ok <- runIO $ doesFileExist ibc
1263 if ok then return (Just (IBC ibc s))
1264 else return Nothing
1265 findNewIBC s@(LIDR f) = do ist <- get
1266 ibcsd <- valIBCSubDir ist
1267 let ibc = ibcPathNoFallback ibcsd f
1268 ok <- runIO $ doesFileExist ibc
1269 if ok then return (Just (IBC ibc s))
1270 else return Nothing
1272 -- Like mapM, but give up when there's an error
1273 mapWhileOK f [] = return []
1274 mapWhileOK f (x : xs) = do x' <- f x
1275 ok <- noErrors
1276 if ok then do xs' <- mapWhileOK f xs
1277 return (x' : xs')
1278 else return [x']
1280idrisMain :: [Opt] -> Idris ()
1281idrisMain opts =
1282 do let inputs = opt getFile opts
1283 let quiet = Quiet `elem` opts
1284 let nobanner = NoBanner `elem` opts
1285 let idesl = Ideslave `elem` opts
1286 let runrepl = not (NoREPL `elem` opts)
1287 let verbose = runrepl || Verbose `elem` opts
1288 let output = opt getOutput opts
1289 let ibcsubdir = opt getIBCSubDir opts
1290 let importdirs = opt getImportDir opts
1291 let bcs = opt getBC opts
1292 let pkgdirs = opt getPkgDir opts
1293 let optimize = case opt getOptLevel opts of
1294 [] -> 2
1295 xs -> last xs
1296 trpl <- case opt getTriple opts of
1297 [] -> runIO $ getDefaultTargetTriple
1298 xs -> return (last xs)
1299 tcpu <- case opt getCPU opts of
1300 [] -> runIO $ getHostCPUName
1301 xs -> return (last xs)
1302 let outty = case opt getOutputTy opts of
1303 [] -> Executable
1304 xs -> last xs
1305 let cgn = case opt getCodegen opts of
1306 [] -> ViaC
1307 xs -> last xs
1308 script <- case opt getExecScript opts of
1309 [] -> return Nothing
1310 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1311 runIO $ exitWith (ExitFailure 1)
1312 [expr] -> return (Just expr)
1313 when (DefaultTotal `elem` opts) $ do i <- getIState
1314 putIState (i { default_total = True })
1315 setColourise $ not quiet && last (True : opt getColour opts)
1316 when (not runrepl) $ setWidth InfinitelyWide
1317 mapM_ addLangExt (opt getLanguageExt opts)
1318 setREPL runrepl
1319 setQuiet (quiet || isJust script)
1320 setIdeSlave idesl
1321 setVerbose verbose
1322 setCmdLine opts
1323 setOutputTy outty
1324 setCodegen cgn
1325 setTargetTriple trpl
1326 setTargetCPU tcpu
1327 setOptLevel optimize
1328 mapM_ makeOption opts
1329 -- if we have the --bytecode flag, drop into the bytecode assembler
1330 case bcs of
1331 [] -> return ()
1332 xs -> return () -- runIO $ mapM_ bcAsm xs
1333 case ibcsubdir of
1334 [] -> setIBCSubDir ""
1335 (d:_) -> setIBCSubDir d
1336 setImportDirs importdirs
1338 when (not (NoBasePkgs `elem` opts)) $ do
1339 addPkgDir "prelude"
1340 addPkgDir "base"
1341 mapM_ addPkgDir pkgdirs
1342 elabPrims
1343 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"
1344 return ()
1345 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1346 return ()
1347 when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner
1349 orig <- getIState
1350 loadInputs stdout inputs
1352 runIO $ hSetBuffering stdout LineBuffering
1354 ok <- noErrors
1355 when ok $ case output of
1356 -- just do the checks
1357 [] -> performUsageAnalysis >> return ()
1359 -- the compiler will run usage analysis itself
1360 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1361 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1363 case script of
1364 Nothing -> return ()
1365 Just expr -> execScript expr
1367 -- Create Idris data dir + repl history and config dir
1368 idrisCatch (do dir <- getIdrisUserDataDir
1369 exists <- runIO $ doesDirectoryExist dir
1370 unless exists $ iLOG ("Creating " ++ dir)
1371 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1372 (\e -> return ())
1374 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1376 when (runrepl && not idesl) $ do
1377-- clearOrigPats
1378 initScript
1379 startServer orig inputs
1380 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1381 when (idesl) $ ideslaveStart orig inputs
1382 ok <- noErrors
1383 when (not ok) $ runIO (exitWith (ExitFailure 1))
1384 where
1385 makeOption (OLogging i) = setLogLevel i
1386 makeOption TypeCase = setTypeCase True
1387 makeOption TypeInType = setTypeInType True
1388 makeOption NoCoverage = setCoverage False
1389 makeOption ErrContext = setErrContext True
1390 makeOption _ = return ()
1392 addPkgDir :: String -> Idris ()
1393 addPkgDir p = do ddir <- runIO $ getDataDir
1394 addImportDir (ddir </> p)
1396execScript :: String -> Idris ()
1397execScript expr = do i <- getIState
1398 c <- colourise
1399 case parseExpr i expr of
1400 Failure err -> do iputStrLn $ show (fixColour c err)
1401 runIO $ exitWith (ExitFailure 1)
1402 Success term -> do ctxt <- getContext
1403 (tm, _) <- elabVal toplevel False term
1404 res <- execute tm
1405 runIO $ exitWith ExitSuccess
1407-- | Get the platform-specific, user-specific Idris dir
1408getIdrisUserDataDir :: Idris FilePath
1409getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1411-- | Locate the platform-specific location for the init script
1412getInitScript :: Idris FilePath
1413getInitScript = do idrisDir <- getIdrisUserDataDir
1414 return $ idrisDir </> "repl" </> "init"
1416-- | Run the initialisation script
1417initScript :: Idris ()
1418initScript = do script <- getInitScript
1419 idrisCatch (do go <- runIO $ doesFileExist script
1420 when go $ do
1421 h <- runIO $ openFile script ReadMode
1422 runInit h
1423 runIO $ hClose h)
1424 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1425 where runInit :: Handle -> Idris ()
1426 runInit h = do eof <- lift . lift $ hIsEOF h
1427 ist <- getIState
1428 unless eof $ do
1429 line <- runIO $ hGetLine h
1430 script <- getInitScript
1431 c <- colourise
1432 processLine ist line script c
1433 runInit h
1434 processLine i cmd input clr =
1435 case parseCmd i input cmd of
1436 Failure err -> runIO $ print (fixColour clr err)
1437 Success Reload -> iPrintError "Init scripts cannot reload the file"
1438 Success (Load f) -> iPrintError "Init scripts cannot load files"
1439 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1440 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1441 Success Proofs -> proofs i
1442 Success Quit -> iPrintError "Init scripts cannot quit Idris"
1443 Success cmd -> process stdout [] cmd
1445getFile :: Opt -> Maybe String
1446getFile (Filename str) = Just str
1447getFile _ = Nothing
1449getBC :: Opt -> Maybe String
1450getBC (BCAsm str) = Just str
1451getBC _ = Nothing
1453getOutput :: Opt -> Maybe String
1454getOutput (Output str) = Just str
1455getOutput _ = Nothing
1457getIBCSubDir :: Opt -> Maybe String
1458getIBCSubDir (IBCSubDir str) = Just str
1459getIBCSubDir _ = Nothing
1461getImportDir :: Opt -> Maybe String
1462getImportDir (ImportDir str) = Just str
1463getImportDir _ = Nothing
1465getPkgDir :: Opt -> Maybe String
1466getPkgDir (Pkg str) = Just str
1467getPkgDir _ = Nothing
1469getPkg :: Opt -> Maybe (Bool, String)
1470getPkg (PkgBuild str) = Just (False, str)
1471getPkg (PkgInstall str) = Just (True, str)
1472getPkg _ = Nothing
1474getPkgClean :: Opt -> Maybe String
1475getPkgClean (PkgClean str) = Just str
1476getPkgClean _ = Nothing
1478getPkgREPL :: Opt -> Maybe String
1479getPkgREPL (PkgREPL str) = Just str
1480getPkgREPL _ = Nothing
1482getPkgCheck :: Opt -> Maybe String
1483getPkgCheck (PkgCheck str) = Just str
1484getPkgCheck _ = Nothing
1486getCodegen :: Opt -> Maybe Codegen
1487getCodegen (UseCodegen x) = Just x
1488getCodegen _ = Nothing
1490getExecScript :: Opt -> Maybe String
1491getExecScript (InterpretScript expr) = Just expr
1492getExecScript _ = Nothing
1494getOutputTy :: Opt -> Maybe OutputType
1495getOutputTy (OutputTy t) = Just t
1496getOutputTy _ = Nothing
1498getLanguageExt :: Opt -> Maybe LanguageExt
1499getLanguageExt (Extension e) = Just e
1500getLanguageExt _ = Nothing
1502getTriple :: Opt -> Maybe String
1503getTriple (TargetTriple x) = Just x
1504getTriple _ = Nothing
1506getCPU :: Opt -> Maybe String
1507getCPU (TargetCPU x) = Just x
1508getCPU _ = Nothing
1510getOptLevel :: Opt -> Maybe Word
1511getOptLevel (OptLevel x) = Just x
1512getOptLevel _ = Nothing
1514getColour :: Opt -> Maybe Bool
1515getColour (ColourREPL b) = Just b
1516getColour _ = Nothing
1518opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1519opt = mapMaybe
1521ver = showVersion version ++ gitHash
1523banner = " ____ __ _ \n" ++
1524 " / _/___/ /____(_)____ \n" ++
1525 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1526 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1527 " /___/\\__,_/_/ /_/____/ Type :? for help \n"