git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/REPL.hs
1566 lines 71 kB history raw
1{-|
2Module : Idris.REPL
3Description : Entry Point for the Idris REPL and CLI.
4License : BSD3
5Maintainer : The Idris Community.
6-}
8{-# LANGUAGE PatternGuards #-}
10module Idris.REPL
11 ( idemodeStart
12 , startServer
13 , runClient
14 , process
15 , replSettings
16 , repl
17 , proofs
18 ) where
20import Control.Category
21import Control.Concurrent
22import Control.Concurrent.Async (race)
23import Control.DeepSeq
24import qualified Control.Exception as X
25import Control.Monad
26import Control.Monad.Trans (lift)
27import Control.Monad.Trans.Except (runExceptT)
28import Control.Monad.Trans.State.Strict (evalStateT, get, put)
29import qualified Data.Binary as Binary
30import qualified Data.ByteString.Base64 as Base64
31import qualified Data.ByteString.Lazy as Lazy
32import qualified Data.ByteString.UTF8 as UTF8
33import Data.Char
34import Data.Either (partitionEithers)
35import Data.List hiding (group)
36import Data.List.Split (splitOn)
37import Data.Maybe
38import qualified Data.Set as S
39import qualified Data.Text as T
40import Data.Version
41import Idris.AbsSyntax
42import Idris.Apropos (apropos, aproposModules)
43import Idris.ASTUtils
44import Idris.Colours hiding (colourise)
45import Idris.Completion
46import Idris.Core.Constraints
47import Idris.Core.Evaluate
48import Idris.Core.Execute (execute)
49import Idris.Core.TT
50import Idris.Core.Unify
51import Idris.Core.WHNF
52import Idris.Coverage
53import Idris.DataOpts
54import Idris.Delaborate
55import Idris.Docs
56import Idris.Docstrings (overview, renderDocTerm, renderDocstring)
57import Idris.Elab.Clause
58import Idris.Elab.Term
59import Idris.Elab.Value
60import Idris.ElabDecls
61import Idris.Error
62import Idris.ErrReverse
63import Idris.Help
64import Idris.IBC
65import qualified Idris.IdeMode as IdeMode
66import Idris.IdrisDoc
67import Idris.Info
68import Idris.Inliner
69import Idris.Interactive
70import Idris.ModeCommon
71import Idris.Options
72import Idris.Output
73import Idris.Parser hiding (indent)
74import Idris.Prover
75import Idris.REPL.Browse (namesInNS, namespacesInNS)
76import Idris.REPL.Commands
77import Idris.REPL.Parser
78import Idris.Termination
79import Idris.TypeSearch (searchByType)
80import Idris.WhoCalls
81import IRTS.Compiler
82import Network
83import Prelude hiding (id, (.), (<$>))
84import System.Console.Haskeline as H
85import System.Directory
86import System.Environment
87import System.Exit
88import System.FilePath (addExtension, dropExtension, splitExtension,
89 takeDirectory, takeExtension, (<.>), (</>))
90import System.FSNotify (watchDir, withManager)
91import System.FSNotify.Devel (allEvents, doAllEvents)
92import System.IO
93import System.Process
94import Text.Trifecta.Result (ErrInfo(..), Result(..))
95import Util.DynamicLinker
96import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)
97import Util.Pretty hiding ((</>))
98import Util.System
99import Version_idris (gitHash)
101import Debug.Trace
103-- | Run the REPL
104repl :: IState -- ^ The initial state
105 -> [FilePath] -- ^ The loaded modules
106 -> FilePath -- ^ The file to edit (with :e)
107 -> InputT Idris ()
108repl orig mods efile
109 = -- H.catch
110 do let quiet = opt_quiet (idris_options orig)
111 i <- lift getIState
112 let colour = idris_colourRepl i
113 let theme = idris_colourTheme i
114 let mvs = idris_metavars i
115 let prompt = if quiet
116 then ""
117 else showMVs colour theme mvs ++
118 let str = mkPrompt mods ++ ">" in
119 (if colour && not isWindows
120 then colourisePrompt theme str
121 else str) ++ " "
122 x <- H.catch (H.withInterrupt $ getInputLine prompt)
123 (ctrlC (return $ Just ""))
124 case x of
125 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
126 return ()
127 Just input -> -- H.catch
128 do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)
129 (ctrlC (return (Just mods)))
130 case ms of
131 Just mods -> let efile' = fromMaybe efile (listToMaybe mods)
132 in repl orig mods efile'
133 Nothing -> return ()
134-- ctrlC)
135-- ctrlC
136 where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
137 ctrlC act e = do lift $ iputStrLn (show e)
138 act -- repl orig mods
140 showMVs c thm [] = ""
141 showMVs c thm ms = "Holes: " ++
142 show' 4 c thm (map fst ms) ++ "\n"
144 show' 0 c thm ms = let l = length ms in
145 "... ( + " ++ show l
146 ++ " other"
147 ++ if l == 1 then ")" else "s)"
148 show' n c thm [m] = showM c thm m
149 show' n c thm (m : ms) = showM c thm m ++ ", " ++
150 show' (n - 1) c thm ms
152 showM c thm n = if c then colouriseFun thm (show n)
153 else show n
155-- | Run the REPL server
156startServer :: PortNumber -> IState -> [FilePath] -> Idris ()
157startServer port orig fn_in = do tid <- runIO $ forkIO (serverLoop port)
158 return ()
159 where serverLoop port = withSocketsDo $
160 do sock <- listenOnLocalhost port
161 loop fn orig { idris_colourRepl = False } sock
163 fn = fromMaybe "" (listToMaybe fn_in)
165 loop fn ist sock
166 = do (h,_,_) <- accept sock
167 hSetEncoding h utf8
168 cmd <- hGetLine h
169 let isth = case idris_outputmode ist of
170 RawOutput _ -> ist {idris_outputmode = RawOutput h}
171 IdeMode n _ -> ist {idris_outputmode = IdeMode n h}
172 (ist', fn) <- processNetCmd orig isth h fn cmd
173 hClose h
174 loop fn ist' sock
176processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
177 IO (IState, FilePath)
178processNetCmd orig i h fn cmd
179 = do res <- case parseCmd i "(net)" cmd of
180 Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))
181 Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i
182 Success (Left err) -> return (Left (Msg err))
183 case res of
184 Right x -> return x
185 Left err -> do hPutStrLn h (show err)
186 return (i, fn)
187 where
188 processNet fn Reload = processNet fn (Load fn Nothing)
189 processNet fn (Load f toline) =
190 -- The $!! here prevents a space leak on reloading.
191 -- This isn't a solution - but it's a temporary stopgap.
192 -- See issue #2386
193 do putIState $!! orig { idris_options = idris_options i
194 , idris_colourTheme = idris_colourTheme i
195 , idris_colourRepl = False
196 }
197 setErrContext True
198 setOutH h
199 setQuiet True
200 setVerbose 0
201 mods <- loadInputs [f] toline
202 ist <- getIState
203 return (ist, f)
204 processNet fn c = do process fn c
205 ist <- getIState
206 return (ist, fn)
207 setOutH :: Handle -> Idris ()
208 setOutH h =
209 do ist <- getIState
210 putIState $ case idris_outputmode ist of
211 RawOutput _ -> ist {idris_outputmode = RawOutput h}
212 IdeMode n _ -> ist {idris_outputmode = IdeMode n h}
214-- | Run a command on the server on localhost
215runClient :: Maybe PortNumber -> String -> IO ()
216runClient port str = withSocketsDo $ do
217 let port' = fromMaybe defaultPort port
218 res <- X.try (connectTo "localhost" $ PortNumber port')
219 case res of
220 Right h -> do
221 hSetEncoding h utf8
222 hPutStrLn h str
223 resp <- hGetResp "" h
224 putStr resp
225 hClose h
227 Left err -> do
228 connectionError err
229 exitWith (ExitFailure 1)
231 where hGetResp acc h = do eof <- hIsEOF h
232 if eof then return acc
233 else do l <- hGetLine h
234 hGetResp (acc ++ l ++ "\n") h
236 connectionError :: X.SomeException -> IO ()
237 connectionError _ =
238 putStrLn "Unable to connect to a running Idris repl"
241initIdemodeSocket :: IO Handle
242initIdemodeSocket = do
243 (sock, port) <- listenOnLocalhostAnyPort
244 putStrLn $ show port
245 (h, _, _) <- accept sock
246 hSetEncoding h utf8
247 return h
249-- | Run the IdeMode
250idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()
251idemodeStart s orig mods
252 = do h <- runIO $ if s then initIdemodeSocket else return stdout
253 setIdeMode True h
254 i <- getIState
255 case idris_outputmode i of
256 IdeMode n h ->
257 do runIO $ hPutStrLn h $ IdeMode.convSExp "protocol-version" IdeMode.ideModeEpoch n
258 case mods of
259 a:_ -> runIdeModeCommand h n i "" [] (IdeMode.LoadFile a Nothing)
260 _ -> return ()
261 idemode h orig mods
263idemode :: Handle -> IState -> [FilePath] -> Idris ()
264idemode h orig mods
265 = do idrisCatch
266 (do let inh = if h == stdout then stdin else h
267 len' <- runIO $ IdeMode.getLen inh
268 len <- case len' of
269 Left err -> ierror err
270 Right n -> return n
271 l <- runIO $ IdeMode.getNChar inh len ""
272 (sexp, id) <- case IdeMode.parseMessage l of
273 Left err -> ierror err
274 Right (sexp, id) -> return (sexp, id)
275 i <- getIState
276 putIState $ i { idris_outputmode = (IdeMode id h) }
277 idrisCatch -- to report correct id back!
278 (do let fn = fromMaybe "" (listToMaybe mods)
279 case IdeMode.sexpToCommand sexp of
280 Just cmd -> runIdeModeCommand h id orig fn mods cmd
281 Nothing -> iPrintError "did not understand" )
282 (\e -> do iPrintError $ show e))
283 (\e -> do iPrintError $ show e)
284 idemode h orig mods
286-- | Run IDEMode commands
287runIdeModeCommand :: Handle -- ^^ The handle for communication
288 -> Integer -- ^^ The continuation ID for the client
289 -> IState -- ^^ The original IState
290 -> FilePath -- ^^ The current open file
291 -> [FilePath] -- ^^ The currently loaded modules
292 -> IdeMode.IdeModeCommand -- ^^ The command to process
293 -> Idris ()
294runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =
295 do c <- colourise
296 i <- getIState
297 case parseCmd i "(input)" cmd of
298 Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)
299 Success (Right (Prove mode n')) ->
300 idrisCatch
301 (do process fn (Prove mode n')
302 isetPrompt (mkPrompt mods)
303 case idris_outputmode i of
304 IdeMode n h -> -- signal completion of proof to ide
305 runIO . hPutStrLn h $
306 IdeMode.convSExp "return"
307 (IdeMode.SymbolAtom "ok", "")
308 n
309 _ -> return ())
310 (\e -> do ist <- getIState
311 isetPrompt (mkPrompt mods)
312 case idris_outputmode i of
313 IdeMode n h ->
314 runIO . hPutStrLn h $
315 IdeMode.convSExp "abandon-proof" "Abandoned" n
316 _ -> return ()
317 iRenderError $ pprintErr ist e)
318 Success (Right cmd) -> idrisCatch
319 (idemodeProcess fn cmd)
320 (\e -> getIState >>= iRenderError . flip pprintErr e)
321 Success (Left err) -> iPrintError err
322runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =
323 do (unused, compls) <- replCompletion (reverse str, "")
324 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",
325 IdeMode.toSExp (map replacement compls,
326 reverse unused)]
327 runIO . hPutStrLn h $ IdeMode.convSExp "return" good id
328runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename toline) =
329 -- The $!! here prevents a space leak on reloading.
330 -- This isn't a solution - but it's a temporary stopgap.
331 -- See issue #2386
332 do i <- getIState
333 clearErr
334 putIState $!! orig { idris_options = idris_options i,
335 idris_outputmode = (IdeMode id h) }
336 mods <- loadInputs [filename] toline
337 isetPrompt (mkPrompt mods)
338 -- Report either success or failure
339 i <- getIState
340 case (errSpan i) of
341 Nothing -> let msg = maybe (IdeMode.SexpList [IdeMode.SymbolAtom "ok",
342 IdeMode.SexpList []])
343 (\fc -> IdeMode.SexpList [IdeMode.SymbolAtom "ok",
344 IdeMode.toSExp fc])
345 (idris_parsedSpan i)
346 in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
347 Just x -> iPrintError $ "didn't load " ++ filename
348 idemode h orig mods
349runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =
350 case splitName name of
351 Left err -> iPrintError err
352 Right n -> process "(idemode)"
353 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))
354runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =
355 case parseConst orig name of
356 Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))
357 Failure _ ->
358 case splitName name of
359 Left err -> iPrintError err
360 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))
361 where howMuch IdeMode.Overview = OverviewDocs
362 howMuch IdeMode.Full = FullDocs
363runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =
364 process fn (CaseSplitAt False line (sUN name))
365runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =
366 process fn (AddClauseFrom False line (sUN name))
367runIdeModeCommand h id orig fn mods (IdeMode.AddProofClause line name) =
368 process fn (AddProofClauseFrom False line (sUN name))
369runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =
370 process fn (AddMissing False line (sUN name))
371runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =
372 process fn (MakeWith False line (sUN name))
373runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) =
374 process fn (MakeCase False line (sUN name))
375runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =
376 doProofSearch fn False r line (sUN name) (map sUN hints) depth
377runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =
378 case splitName name of
379 Left err -> iPrintError err
380 Right n -> process fn (MakeLemma False line n)
381runIdeModeCommand h id orig fn mods (IdeMode.Apropos a) =
382 process fn (Apropos [] a)
383runIdeModeCommand h id orig fn mods (IdeMode.GetOpts) =
384 do ist <- getIState
385 let opts = idris_options ist
386 let impshow = opt_showimp opts
387 let errCtxt = opt_errContext opts
388 let options = (IdeMode.SymbolAtom "ok",
389 [(IdeMode.SymbolAtom "show-implicits", impshow),
390 (IdeMode.SymbolAtom "error-context", errCtxt)])
391 runIO . hPutStrLn h $ IdeMode.convSExp "return" options id
392runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ShowImpl b) =
393 do setImpShow b
394 let msg = (IdeMode.SymbolAtom "ok", b)
395 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
396runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) =
397 do setErrContext b
398 let msg = (IdeMode.SymbolAtom "ok", b)
399 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
400runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
401 do ist <- getIState
402 let mvs = reverse $ [ (n, i)
403 | (n, (_, i, _, _, _)) <- idris_metavars ist
404 , not (n `elem` primDefs)
405 ]
406 let ppo = ppOptionIst ist
407 -- splitMvs is a list of pairs of names and their split types
408 let splitMvs = [ (n, (premises, concl, tm))
409 | (n, i, ty) <- mvTys ist mvs
410 , let (premises, concl, tm) = splitPi ist i ty]
411 -- mvOutput is the pretty-printed version ready for conversion to SExpr
412 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
413 mapPair show
414 (\(hs, c, pc) ->
415 let bnd = [ n | (n,_,_) <- hs ] in
416 let bnds = inits bnd in
417 (map (\(bnd, h) -> processPremise ist bnd h)
418 (zip bnds hs),
419 render ist bnd c pc))
420 splitMvs
421 runIO . hPutStrLn h $
422 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
423 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
424 firstOfThree (x, y, z) = x
425 mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs
427 -- | Split a function type into a pair of premises, conclusion.
428 -- Each maintains both the original and delaborated versions.
429 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
430 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =
431 let (hs, c, pc) = splitPi ist (i - 1) rest in
432 ((n, t, delabTy' ist [] [] t False False True):hs,
433 c, delabTy' ist [] [] c False False True)
434 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)
436 -- | Get the types of a list of metavariable names
437 mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
438 mvTys ist mvs = [ (n, i, ty)
439 | (n, i) <- mvs
440 , ty <- maybeToList (fmap (vToP . snd) (lookupTyNameExact n (tt_ctxt ist)))
441 ]
443 -- | Show a type and its corresponding PTerm in a format suitable
444 -- for the IDE - that is, pretty-printed and annotated.
445 render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
446 render ist bnd t pt =
447 let prettyT = pprintPTerm (ppOptionIst ist)
448 (zip bnd (repeat False))
449 []
450 (idris_infixes ist)
451 pt
452 in
453 displaySpans .
454 renderPretty 0.9 cols .
455 fmap (fancifyAnnots ist True) .
456 annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
457 prettyT
459 -- | Juggle the bits of a premise to prepare for output.
460 processPremise :: IState
461 -> [Name] -- ^ the names to highlight as bound
462 -> (Name, Type, PTerm)
463 -> (String,
464 String,
465 SpanList OutputAnnotation)
466 processPremise ist bnd (n, t, pt) =
467 let (out, spans) = render ist bnd t pt in
468 (show n , out, spans)
470runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =
471 case splitName n of
472 Left err -> iPrintError err
473 Right n -> do calls <- whoCalls n
474 ist <- getIState
475 let msg = (IdeMode.SymbolAtom "ok",
476 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
477 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
478 where pn ist = displaySpans .
479 renderPretty 0.9 1000 .
480 fmap (fancifyAnnots ist True) .
481 prettyName True True []
483runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =
484 case splitName n of
485 Left err -> iPrintError err
486 Right n -> do calls <- callsWho n
487 ist <- getIState
488 let msg = (IdeMode.SymbolAtom "ok",
489 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
490 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
491 where pn ist = displaySpans .
492 renderPretty 0.9 1000 .
493 fmap (fancifyAnnots ist True) .
494 prettyName True True []
496runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =
497 case splitOn "." ns of
498 [] -> iPrintError "No namespace provided"
499 ns -> do underNSs <- fmap (map $ concat . intersperse ".") $ namespacesInNS ns
500 names <- namesInNS ns
501 if null underNSs && null names
502 then iPrintError "Invalid or empty namespace"
503 else do ist <- getIState
504 underNs <- mapM pn names
505 let msg = (IdeMode.SymbolAtom "ok", (underNSs, underNs))
506 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
507 where pn n =
508 do ctxt <- getContext
509 ist <- getIState
510 return $
511 displaySpans .
512 renderPretty 0.9 1000 .
513 fmap (fancifyAnnots ist True) $
514 prettyName True False [] n <>
515 case lookupTyExact n ctxt of
516 Just t ->
517 space <> colon <> space <> align (group (pprintDelab ist t))
518 Nothing ->
519 empty
521runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =
522 do ctxt <- getContext
523 ist <- getIState
524 let tm' = normaliseAll ctxt [] tm
525 ptm = annotate (AnnTerm bnd tm')
526 (pprintPTerm (ppOptionIst ist)
527 bnd
528 []
529 (idris_infixes ist)
530 (delab ist tm'))
531 msg = (IdeMode.SymbolAtom "ok",
532 displaySpans .
533 renderPretty 0.9 80 .
534 fmap (fancifyAnnots ist True) $ ptm)
535 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
536runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =
537 ideModeForceTermImplicits h id bnd True tm
538runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =
539 ideModeForceTermImplicits h id bnd False tm
540runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) =
541 do ist <- getIState
542 let ptm = annotate (AnnTerm bnd tm)
543 (pprintTT (map fst bnd) tm)
544 msg = (IdeMode.SymbolAtom "ok",
545 displaySpans .
546 renderPretty 0.9 70 .
547 fmap (fancifyAnnots ist True) $ ptm)
548 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
549runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =
550 case splitName name of
551 Left err -> iPrintError err
552 Right n -> process "(idemode)" (PrintDef n)
553runIdeModeCommand h id orig fn modes (IdeMode.ErrString e) =
554 do ist <- getIState
555 let out = displayS . renderPretty 1.0 60 $ pprintErr ist e
556 msg = (IdeMode.SymbolAtom "ok", IdeMode.StringAtom $ out "")
557 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
558runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =
559 do ist <- getIState
560 let (out, spans) =
561 displaySpans .
562 renderPretty 0.9 80 .
563 fmap (fancifyAnnots ist True) $ pprintErr ist e
564 msg = (IdeMode.SymbolAtom "ok", out, spans)
565 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
566runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion =
567 let idrisVersion = (versionBranch getIdrisVersionNoGit,
568 if not (null gitHash)
569 then [gitHash]
570 else [])
571 msg = (IdeMode.SymbolAtom "ok", idrisVersion)
572 in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
575-- | Show a term for IDEMode with the specified implicitness
576ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
577ideModeForceTermImplicits h id bnd impl tm =
578 do ist <- getIState
579 let expl = annotate (AnnTerm bnd tm)
580 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
581 bnd [] (idris_infixes ist)
582 (delab ist tm))
583 msg = (IdeMode.SymbolAtom "ok",
584 displaySpans .
585 renderPretty 0.9 80 .
586 fmap (fancifyAnnots ist True) $ expl)
587 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
589splitName :: String -> Either String Name
590splitName s | "{{{{{" `isPrefixOf` s =
591 decode $ drop 5 $ reverse $ drop 5 $ reverse s
592 where decode x =
593 case Base64.decode (UTF8.fromString x) of
594 Left err -> Left err
595 Right ok ->
596 case Binary.decodeOrFail (Lazy.fromStrict ok) of
597 Left _ -> Left "Bad binary instance for Name"
598 Right (_, _, n) -> Right n
600splitName s = case reverse $ splitOn "." s of
601 [] -> Left ("Didn't understand name '" ++ s ++ "'")
602 [n] -> Right . sUN $ unparen n
603 (n:ns) -> Right $ sNS (sUN (unparen n)) ns
604 where unparen "" = ""
605 unparen ('(':x:xs) | last xs == ')' = init (x:xs)
606 unparen str = str
608idemodeProcess :: FilePath -> Command -> Idris ()
609idemodeProcess fn Warranty = process fn Warranty
610idemodeProcess fn Help = process fn Help
611idemodeProcess fn (RunShellCommand cmd) =
612 iPrintError ":! is not currently supported in IDE mode."
613idemodeProcess fn (ChangeDirectory f) =
614 do process fn (ChangeDirectory f)
615 dir <- runIO $ getCurrentDirectory
616 iPrintResult $ "changed directory to " ++ dir
617idemodeProcess fn (ModImport f) = process fn (ModImport f)
618idemodeProcess fn (Eval t) = process fn (Eval t)
619idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)
620 iPrintResult "defined"
621idemodeProcess fn (Undefine n) = process fn (Undefine n)
622idemodeProcess fn (ExecVal t) = process fn (ExecVal t)
623idemodeProcess fn (Check (PRef x hls n)) = process fn (Check (PRef x hls n))
624idemodeProcess fn (Check t) = process fn (Check t)
625idemodeProcess fn (Core t) = process fn (Core t)
626idemodeProcess fn (DocStr n w) = process fn (DocStr n w)
627idemodeProcess fn Universes = process fn Universes
628idemodeProcess fn (Defn n) = do process fn (Defn n)
629 iPrintResult ""
630idemodeProcess fn (TotCheck n) = process fn (TotCheck n)
631idemodeProcess fn (DebugInfo n) = do process fn (DebugInfo n)
632 iPrintResult ""
633idemodeProcess fn (Search ps t) = process fn (Search ps t)
634idemodeProcess fn (Spec t) = process fn (Spec t)
635-- RmProof and AddProof not supported!
636idemodeProcess fn (ShowProof n') = process fn (ShowProof n')
637idemodeProcess fn (WHNF t) = process fn (WHNF t)
638--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!
639idemodeProcess fn (TestInline t) = process fn (TestInline t)
641idemodeProcess fn (Execute t) = do process fn (Execute t)
642 iPrintResult ""
643idemodeProcess fn (Compile codegen f) = do process fn (Compile codegen f)
644 iPrintResult ""
645idemodeProcess fn (LogLvl i) = do process fn (LogLvl i)
646 iPrintResult ""
647idemodeProcess fn (Pattelab t) = process fn (Pattelab t)
648idemodeProcess fn (Missing n) = process fn (Missing n)
649idemodeProcess fn (DynamicLink l) = do process fn (DynamicLink l)
650 iPrintResult ""
651idemodeProcess fn ListDynamic = do process fn ListDynamic
652 iPrintResult ""
653idemodeProcess fn Metavars = process fn Metavars
654idemodeProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
655 iPrintResult ""
656idemodeProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
657 iPrintResult ""
658idemodeProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
659 iPrintResult ""
660idemodeProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
661 iPrintResult ""
662idemodeProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)
663 iPrintResult ""
664idemodeProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)
665 iPrintResult ""
666idemodeProcess fn (SetOpt x) = process fn (SetOpt x)
667idemodeProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
668idemodeProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)
669idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)
670idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
671idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
672idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
673idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)
674idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
675idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
676 iPrintResult ""
677idemodeProcess fn (SetPrinterDepth d) = do process fn (SetPrinterDepth d)
678 iPrintResult ""
679idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)
680 iPrintResult ""
681idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n)
682idemodeProcess fn (CallsWho n) = process fn (CallsWho n)
683idemodeProcess fn (PrintDef n) = process fn (PrintDef n)
684idemodeProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm)
685idemodeProcess fn _ = iPrintError "command not recognized or not supported"
688-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
689mkPrompt [] = "Idris"
690mkPrompt [x] = "*" ++ dropExtension x
691mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
693-- | Determine whether a file uses literate syntax
694lit f = case splitExtension f of
695 (_, ".lidr") -> True
696 _ -> False
698reload :: IState -> [FilePath] -> Idris (Maybe [FilePath])
699reload orig inputs = do
700 i <- getIState
701 -- The $!! here prevents a space leak on reloading.
702 -- This isn't a solution - but it's a temporary stopgap.
703 -- See issue #2386
704 putIState $!! orig { idris_options = idris_options i
705 , idris_colourTheme = idris_colourTheme i
706 , imported = imported i
707 }
708 clearErr
709 fmap Just $ loadInputs inputs Nothing
711watch :: IState -> [FilePath] -> Idris (Maybe [FilePath])
712watch orig inputs = do
713 resp <- runIO $ do
714 let dirs = nub $ map takeDirectory inputs
715 inputSet <- fmap S.fromList $ mapM canonicalizePath inputs
716 signal <- newEmptyMVar
717 withManager $ \mgr -> do
718 forM_ dirs $ \dir ->
719 watchDir mgr dir (allEvents $ flip S.member inputSet) (doAllEvents $ putMVar signal)
720 race getLine (takeMVar signal)
721 case resp of
722 Left _ -> return (Just inputs) -- canceled, so nop
723 Right _ -> reload orig inputs >> watch orig inputs
725processInput :: String ->
726 IState -> [FilePath] -> FilePath -> Idris (Maybe [FilePath])
727processInput cmd orig inputs efile
728 = do i <- getIState
729 let opts = idris_options i
730 let quiet = opt_quiet opts
731 let fn = fromMaybe "" (listToMaybe inputs)
732 c <- colourise
733 case parseCmd i "(input)" cmd of
734 Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
735 return (Just inputs)
736 Success (Right Reload) ->
737 reload orig inputs
738 Success (Right Watch) ->
739 if null inputs then
740 do iputStrLn "No loaded files to watch."
741 return (Just inputs)
742 else
743 do iputStrLn efile
744 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."
745 watch orig inputs
746 Success (Right (Load f toline)) ->
747 -- The $!! here prevents a space leak on reloading.
748 -- This isn't a solution - but it's a temporary stopgap.
749 -- See issue #2386
750 do putIState $!! orig { idris_options = idris_options i
751 , idris_colourTheme = idris_colourTheme i
752 }
753 clearErr
754 mod <- loadInputs [f] toline
755 return (Just mod)
756 Success (Right (ModImport f)) ->
757 do clearErr
758 fmod <- loadModule f (IBC_REPL True)
759 return (Just (inputs ++ maybe [] (:[]) fmod))
760 Success (Right Edit) -> do -- takeMVar stvar
761 edit efile orig
762 return (Just inputs)
763 Success (Right Proofs) -> do proofs orig
764 return (Just inputs)
765 Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")
766 return Nothing
767 Success (Right cmd ) -> do idrisCatch (process fn cmd)
768 (\e -> do msg <- showErr e ; iputStrLn msg)
769 return (Just inputs)
770 Success (Left err) -> do runIO $ putStrLn err
771 return (Just inputs)
773resolveProof :: Name -> Idris Name
774resolveProof n'
775 = do i <- getIState
776 ctxt <- getContext
777 n <- case lookupNames n' ctxt of
778 [x] -> return x
779 [] -> return n'
780 ns -> ierror (CantResolveAlts ns)
781 return n
783removeProof :: Name -> Idris ()
784removeProof n =
785 do i <- getIState
786 let proofs = proof_list i
787 let ps = filter ((/= n) . fst) proofs
788 putIState $ i { proof_list = ps }
790edit :: FilePath -> IState -> Idris ()
791edit "" orig = iputStrLn "Nothing to edit"
792edit f orig
793 = do i <- getIState
794 env <- runIO getEnvironment
795 let editor = getEditor env
796 let line = case errSpan i of
797 Just l -> '+' : show (fst (fc_start l))
798 Nothing -> ""
799 let cmdLine = intercalate " " [editor, line, fixName f]
800 runIO $ system cmdLine
801 clearErr
802 -- The $!! here prevents a space leak on reloading.
803 -- This isn't a solution - but it's a temporary stopgap.
804 -- See issue #2386
805 putIState $!! orig { idris_options = idris_options i
806 , idris_colourTheme = idris_colourTheme i
807 }
808 loadInputs [f] Nothing
809-- clearOrigPats
810 iucheck
811 return ()
812 where getEditor env | Just ed <- lookup "EDITOR" env = ed
813 | Just ed <- lookup "VISUAL" env = ed
814 | otherwise = "vi"
815 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = quote file
816 | otherwise = quote $ addExtension file "idr"
817 where
818 quoteChar = if isWindows then '"' else '\''
819 quote s = [quoteChar] ++ s ++ [quoteChar]
823proofs :: IState -> Idris ()
824proofs orig
825 = do i <- getIState
826 let ps = proof_list i
827 case ps of
828 [] -> iputStrLn "No proofs available"
829 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
831insertScript :: String -> [String] -> [String]
832insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
833insertScript prf (p@"---------- Proofs ----------" : "" : xs)
834 = p : "" : prf : xs
835insertScript prf (x : xs) = x : insertScript prf xs
837process :: FilePath -> Command -> Idris ()
838process fn Help = iPrintResult displayHelp
839process fn Warranty = iPrintResult warranty
840process fn (RunShellCommand cmd) = runIO $ system cmd >> return ()
841process fn (ChangeDirectory f)
842 = do runIO $ setCurrentDirectory f
843 return ()
844process fn (ModImport f) = do fmod <- loadModule f (IBC_REPL True)
845 case fmod of
846 Just pr -> isetPrompt pr
847 Nothing -> iPrintError $ "Can't find import " ++ f
848process fn (Eval t)
849 = withErrorReflection $
850 do logParser 5 $ show t
851 getIState >>= flip warnDisamb t
852 (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
853 ctxt <- getContext
854 let tm' = perhapsForce $ normaliseBlocking ctxt []
855 [sUN "foreign",
856 sUN "prim_read",
857 sUN "prim_write"]
858 tm
859 let ty' = perhapsForce $ normaliseAll ctxt [] ty
860 -- Add value to context, call it "it"
861 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
862 ist <- getIState
863 logParser 3 $ "Raw: " ++ show (tm', ty')
864 logParser 10 $ "Debug: " ++ showEnvDbg [] tm'
865 let tmDoc = pprintDelab ist tm'
866 -- errReverse to make type more readable
867 tyDoc = pprintDelab ist (errReverse ist ty')
868 iPrintTermWithType tmDoc tyDoc
869 where perhapsForce tm | termSmallerThan 100 tm = force tm
870 | otherwise = tm
872process fn (NewDefn decls) = do
873 logParser 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
874 mapM_ defineName namedGroups where
875 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls
876 getName :: PDecl -> Maybe Name
877 getName (PTy docs argdocs syn fc opts name _ ty) = Just name
878 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
879 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)
880 getName (PInterface doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name
881 getName _ = Nothing
882 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
883 getClauseName (PClause fc name whole with rhs whereBlock) = name
884 getClauseName (PWith fc name whole with rhs pn whereBlock) = name
885 defineName :: [PDecl] -> Idris ()
886 defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do
887 elabDecl EAll info tyDecl
888 elabClauses info fc opts name (concatMap getClauses decls)
889 setReplDefined (Just name)
890 defineName [PClauses fc opts _ [clause]] = do
891 let pterm = getRHS clause
892 (tm,ty) <- elabVal info ERHS pterm
893 ctxt <- getContext
894 let tm' = force (normaliseAll ctxt [] tm)
895 let ty' = force (normaliseAll ctxt [] ty)
896 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
897 setReplDefined (Just $ getClauseName clause)
898 defineName (PClauses{} : _) = tclift $ tfail (Msg "Only one function body is allowed without a type declaration.")
899 -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
900 defineName (PFix fc fixity strs : defns) = do
901 fmodifyState idris_fixities (map (Fix fixity) strs ++)
902 unless (null defns) $ defineName defns
903 defineName (PSyntax _ syntax:_) = do
904 i <- get
905 put (addReplSyntax i syntax)
906 defineName decls = do
907 elabDecls (toplevelWith fn) (map fixClauses decls)
908 setReplDefined (getName (head decls))
909 getClauses (PClauses fc opts name clauses) = clauses
910 getClauses _ = []
911 getRHS :: PClause -> PTerm
912 getRHS (PClause fc name whole with rhs whereBlock) = rhs
913 getRHS (PWith fc name whole with rhs pn whereBlock) = rhs
914 getRHS (PClauseR fc with rhs whereBlock) = rhs
915 getRHS (PWithR fc with rhs pn whereBlock) = rhs
916 setReplDefined :: Maybe Name -> Idris ()
917 setReplDefined Nothing = return ()
918 setReplDefined (Just n) = do
919 oldState <- get
920 fmodifyState repl_definitions (n:)
921 -- the "name" field of PClauses seems to always be MN 2 "__", so we need to
922 -- retrieve the actual name from deeper inside.
923 -- This should really be a full recursive walk through the structure of PDecl, but
924 -- I think it should work this way and I want to test sooner. Also lazy.
925 fixClauses :: PDecl' t -> PDecl' t
926 fixClauses (PClauses fc opts _ css@(clause:cs)) =
927 PClauses fc opts (getClauseName clause) css
928 fixClauses (PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName decls) =
929 PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName (map fixClauses decls)
930 fixClauses decl = decl
932 info = recinfo (fileFC "toplevel")
934process fn (Undefine names) = undefine names
935 where
936 undefine :: [Name] -> Idris ()
937 undefine [] = do
938 allDefined <- idris_repl_defs `fmap` get
939 undefine' allDefined []
940 -- Keep track of which names you've removed so you can
941 -- print them out to the user afterward
942 undefine names = undefine' names []
943 undefine' [] list = do iRenderResult $ printUndefinedNames list
944 return ()
945 undefine' (n:names) already = do
946 allDefined <- idris_repl_defs `fmap` get
947 if n `elem` allDefined
948 then do undefinedJustNow <- undefClosure n
949 undefine' names (undefinedJustNow ++ already)
950 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
951 undefine' names already
952 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
953 -- for now just assume it's an interface. Eventually we'll want some kind of
954 -- smart detection of exactly what kind of name we're undefining.
955 fputState (ctxt_lookup n . known_interfaces) Nothing
956 fmodifyState repl_definitions (delete n)
957 undefClosure n =
958 do replDefs <- idris_repl_defs `fmap` get
959 callGraph <- whoCalls n
960 let users = case lookup n callGraph of
961 Just ns -> nub ns
962 Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
963 undefinedJustNow <- concat `fmap` mapM undefClosure users
964 undefOne n
965 return (nub (n : undefinedJustNow))
969process fn (ExecVal t)
970 = do ctxt <- getContext
971 ist <- getIState
972 (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
973-- let tm' = normaliseAll ctxt [] tm
974 let ty' = normaliseAll ctxt [] ty
975 res <- execute tm
976 let (resOut, tyOut) = (prettyIst ist (delab ist res),
977 prettyIst ist (delab ist ty'))
978 iPrintTermWithType resOut tyOut
980process fn (Check (PRef _ _ n))
981 = do ctxt <- getContext
982 ist <- getIState
983 let ppo = ppOptionIst ist
984 case lookupNames n ctxt of
985 ts@(t:_) ->
986 case lookup t (idris_metavars ist) of
987 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
988 showMetavarInfo ppo ist n i
989 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
990 [] -> iPrintError $ "No such variable " ++ show n
991 where
992 showMetavarInfo ppo ist n i
993 = case lookupTy n (tt_ctxt ist) of
994 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in
995 putTy ppo ist i [] (delab ist (errReverse ist ty'))
996 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
997 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
998 putTy ppo ist i bnd (PPi _ n _ t sc)
999 = let current = case n of
1000 MN _ _ -> text ""
1001 UN nm | ('_':'_':_) <- str nm -> text ""
1002 _ -> text " " <>
1003 bindingOf n False
1004 <+> colon
1005 <+> align (tPretty bnd ist t)
1006 <> line
1007 in
1008 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
1009 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
1010 putGoal ppo ist bnd g
1011 = text "--------------------------------------" <$>
1012 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
1013 align (tPretty bnd ist g)
1015 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
1018process fn (Check t)
1019 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
1020 ctxt <- getContext
1021 ist <- getIState
1022 let ppo = ppOptionIst ist
1023 ty' = if opt_evaltypes (idris_options ist)
1024 then normaliseC ctxt [] ty
1025 else ty
1026 case tm of
1027 TType _ ->
1028 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc
1029 _ -> iPrintTermWithType (pprintDelab ist tm)
1030 (pprintDelab ist ty')
1032process fn (Core t)
1033 = case t of
1034 PRef _ _ n ->
1035 do ist <- getIState
1036 case lookupDef n (tt_ctxt ist) of
1037 [CaseOp _ _ _ _ _ _] -> pprintDef True n >>= iRenderResult . vsep
1038 _ -> coreTerm t
1039 t -> coreTerm t
1040 where coreTerm t =
1041 do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
1042 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
1044process fn (DocStr (Left n) w)
1045 | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc
1046 | otherwise = do
1047 ist <- getIState
1048 let docs = lookupCtxtName n (idris_docstrings ist) ++
1049 map (\(n,d)-> (n, (d, [])))
1050 (lookupCtxtName (modDocN n) (idris_moduledocs ist))
1051 case docs of
1052 [] -> iPrintError $ "No documentation for " ++ show n
1053 ns -> do toShow <- mapM (showDoc ist) ns
1054 iRenderResult (vsep toShow)
1055 where showDoc ist (n, d) = do doc <- getDocs n w
1056 return $ pprintDocs ist doc
1058 modDocN (NS (UN n) ns) = NS modDocName (n:ns)
1059 modDocN (UN n) = NS modDocName [n]
1060 modDocN _ = sMN 1 "NotFoundForSure"
1062process fn (DocStr (Right c) _) -- constants only have overviews
1063 = do ist <- getIState
1064 iRenderResult $ pprintConstDocs ist c (constDocs c)
1066process fn Universes
1067 = do i <- getIState
1068 let cs = idris_constraints i
1069 let cslist = S.toAscList cs
1070-- iputStrLn $ showSep "\n" (map show cs)
1071 iputStrLn $ showSep "\n" (map show cslist)
1072 let n = length cslist
1073 iputStrLn $ "(" ++ show n ++ " constraints)"
1074 case ucheck cs of
1075 Error e -> iPrintError $ pshow i e
1076 OK _ -> iPrintResult "Universes OK"
1077process fn (Defn n)
1078 = do i <- getIState
1079 let head = text "Compiled patterns:" <$>
1080 text (show (lookupDef n (tt_ctxt i)))
1081 let defs =
1082 case lookupCtxt n (idris_patdefs i) of
1083 [] -> empty
1084 [(d, _)] -> text "Original definiton:" <$>
1085 vsep (map (printCase i) d)
1086 let tot =
1087 case lookupTotal n (tt_ctxt i) of
1088 [t] -> showTotal t i
1089 _ -> empty
1090 iRenderResult $ vsep [head, defs, tot]
1091 where printCase i (_, lhs, rhs)
1092 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
1093 in text (showTm i' (delab i lhs)) <+> text "=" <+>
1094 text (showTm i' (delab i rhs))
1095process fn (TotCheck n)
1096 = do i <- getIState
1097 case lookupNameTotal n (tt_ctxt i) of
1098 [] -> iPrintError $ "Unknown operator " ++ show n
1099 ts -> do ist <- getIState
1100 c <- colourise
1101 let ppo = ppOptionIst ist
1102 let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
1103 showName (Just ist) [] ppo False n
1104 iRenderResult . vsep .
1105 map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
1106 ts
1108process fn (DebugUnify l r)
1109 = do (ltm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS l
1110 (rtm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS r
1111 ctxt <- getContext
1112 case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of
1113 OK ans -> iputStrLn (show ans)
1114 Error e -> iputStrLn (show e)
1116process fn (DebugInfo n)
1117 = do i <- getIState
1118 let oi = lookupCtxtName n (idris_optimisation i)
1119 when (not (null oi)) $ iputStrLn (show oi)
1120 let si = lookupCtxt n (idris_statics i)
1121 when (not (null si)) $ iputStrLn (show si)
1122 let di = lookupCtxt n (idris_datatypes i)
1123 when (not (null di)) $ iputStrLn (show di)
1124 let imps = lookupCtxt n (idris_implicits i)
1125 when (not (null imps)) $ iputStrLn (show imps)
1126 let d = lookupDefAcc n False (tt_ctxt i)
1127 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
1128 let cg = lookupCtxtName n (idris_callgraph i)
1129 i <- getIState
1130 let cg' = lookupCtxtName n (idris_callgraph i)
1131 sc <- checkSizeChange n
1132 iputStrLn $ "Size change: " ++ show sc
1133 let fn = lookupCtxtName n (idris_fninfo i)
1134 when (not (null cg')) $ do iputStrLn "Call graph:\n"
1135 iputStrLn (show cg')
1136 when (not (null fn)) $ iputStrLn (show fn)
1137process fn (Search pkgs t) = searchByType pkgs t
1138process fn (CaseSplitAt updatefile l n)
1139 = caseSplitAt fn updatefile l n
1140process fn (AddClauseFrom updatefile l n)
1141 = addClauseFrom fn updatefile l n
1142process fn (AddProofClauseFrom updatefile l n)
1143 = addProofClauseFrom fn updatefile l n
1144process fn (AddMissing updatefile l n)
1145 = addMissing fn updatefile l n
1146process fn (MakeWith updatefile l n)
1147 = makeWith fn updatefile l n
1148process fn (MakeCase updatefile l n)
1149 = makeCase fn updatefile l n
1150process fn (MakeLemma updatefile l n)
1151 = makeLemma fn updatefile l n
1152process fn (DoProofSearch updatefile rec l n hints)
1153 = doProofSearch fn updatefile rec l n hints Nothing
1154process fn (Spec t)
1155 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1156 ctxt <- getContext
1157 ist <- getIState
1158 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
1159 iPrintResult (show (delab ist tm'))
1161process fn (RmProof n')
1162 = do i <- getIState
1163 n <- resolveProof n'
1164 let proofs = proof_list i
1165 case lookup n proofs of
1166 Nothing -> iputStrLn "No proof to remove"
1167 Just _ -> do removeProof n
1168 insertMetavar n
1169 iputStrLn $ "Removed proof " ++ show n
1170 where
1171 insertMetavar :: Name -> Idris ()
1172 insertMetavar n =
1173 do i <- getIState
1174 let ms = idris_metavars i
1175 putIState $ i { idris_metavars = (n, (Nothing, 0, [], False, False)) : ms }
1177process fn' (AddProof prf)
1178 = do fn <- do
1179 let fn'' = takeWhile (/= ' ') fn'
1180 ex <- runIO $ doesFileExist fn''
1181 let fnExt = fn'' <.> "idr"
1182 exExt <- runIO $ doesFileExist fnExt
1183 if ex
1184 then return fn''
1185 else if exExt
1186 then return fnExt
1187 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
1188 let fb = fn ++ "~"
1189 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
1190 prog <- runIO $ readSource fb
1191 i <- getIState
1192 let proofs = proof_list i
1193 n' <- case prf of
1194 Nothing -> case proofs of
1195 [] -> ifail "No proof to add"
1196 ((x, _) : _) -> return x
1197 Just nm -> return nm
1198 n <- resolveProof n'
1199 case lookup n proofs of
1200 Nothing -> iputStrLn "No proof to add"
1201 Just (mode, prf) ->
1202 do let script = if mode
1203 then showRunElab (lit fn) n prf
1204 else showProof (lit fn) n prf
1205 let prog' = insertScript script ls
1206 runIO $ writeSource fn (unlines prog')
1207 removeProof n
1208 iputStrLn $ "Added proof " ++ show n
1209 where ls = (lines prog)
1211process fn (ShowProof n')
1212 = do i <- getIState
1213 n <- resolveProof n'
1214 let proofs = proof_list i
1215 case lookup n proofs of
1216 Nothing -> iPrintError "No proof to show"
1217 Just (m, p) -> iPrintResult $ if m
1218 then showRunElab False n p
1219 else showProof False n p
1221process fn (Prove mode n')
1222 = do ctxt <- getContext
1223 ist <- getIState
1224 let ns = lookupNames n' ctxt
1225 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
1226 n <- case metavars of
1227 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
1228 [(n, (_,_,_,False,_))] -> return n
1229 [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes")
1230 [(_, (_,_,_,True,_))] -> ierror (Msg "Declarations not solvable using prover")
1231 ns -> ierror (CantResolveAlts (map fst ns))
1232 prover (toplevelWith fn) mode (lit fn) n
1233 -- recheck totality
1234 i <- getIState
1235 totcheck (fileFC "(input)", n)
1236 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
1237 mapM_ checkDeclTotality (idris_totcheck i)
1238 warnTotality
1239process fn (WHNF t)
1240 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1241 ctxt <- getContext
1242 ist <- getIState
1243 let tm' = whnf ctxt [] tm
1244 let tmArgs' = whnfArgs ctxt [] tm
1245 iPrintResult $ "WHNF: " ++ (show (delab ist tm'))
1246 iPrintResult $ "WHNF args: " ++ (show (delab ist tmArgs'))
1247process fn (TestInline t)
1248 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1249 ctxt <- getContext
1250 ist <- getIState
1251 let tm' = inlineTerm ist tm
1252 c <- colourise
1253 iPrintResult (showTm ist (delab ist tm'))
1254process fn (Execute tm)
1255 = idrisCatch
1256 (do ist <- getIState
1257 (m_in, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)
1258 m <- applyOpts m_in
1259 (tmpn, tmph) <- runIO $ tempfile ""
1260 runIO $ hClose tmph
1261 t <- codegen
1262 -- gcc adds .exe when it builds windows programs
1263 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
1264 ir <- compile t tmpn (Just m)
1265 runIO $ generate t (fst (head (idris_imported ist))) ir
1266 case idris_outputmode ist of
1267 RawOutput h -> do runIO $ rawSystem progName []
1268 return ()
1269 IdeMode n h -> runIO . hPutStrLn h $
1270 IdeMode.convSExp "run-program" tmpn n)
1271 (\e -> getIState >>= iRenderError . flip pprintErr e)
1272 where fc = fileFC "main"
1273process fn (Compile codegen f)
1274 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =
1275 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""
1276 | otherwise = do opts <- getCmdLine
1277 let iface = Interface `elem` opts
1278 let mainname = sNS (sUN "main") ["Main"]
1280 m <- if iface then return Nothing else
1281 do (m', _) <- elabVal (recinfo (fileFC "compiler")) ERHS
1282 (PApp fc (PRef fc [] (sUN "run__IO"))
1283 [pexp $ PRef fc [] mainname])
1284 return (Just m')
1285 ir <- compile codegen f m
1286 i <- getIState
1287 runIO $ generate codegen (fst (head (idris_imported i))) ir
1288 where fc = fileFC "main"
1289process fn (LogLvl i) = setLogLevel i
1290process fn (LogCategory cs) = setLogCats cs
1291-- Elaborate as if LHS of a pattern (debug command)
1292process fn (Pattelab t)
1293 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ELHS t
1294 iPrintResult $ show tm ++ "\n\n : " ++ show ty
1296process fn (Missing n)
1297 = do i <- getIState
1298 ppOpts <- fmap ppOptionIst getIState
1299 case lookupCtxt n (idris_patdefs i) of
1300 [] -> iPrintError $ "Unknown name " ++ show n
1301 [(_, tms)] ->
1302 iRenderResult (vsep (map (pprintPTerm ppOpts
1303 []
1304 []
1305 (idris_infixes i))
1306 tms))
1307 _ -> iPrintError "Ambiguous name"
1308process fn (DynamicLink l)
1309 = do i <- getIState
1310 let importdirs = opt_importdirs (idris_options i)
1311 lib = trim l
1312 handle <- lift . lift $ tryLoadLib importdirs lib
1313 case handle of
1314 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
1315 Just x -> do let libs = idris_dynamic_libs i
1316 if x `elem` libs
1317 then do logParser 1 ("Tried to load duplicate library " ++ lib_name x)
1318 return ()
1319 else putIState $ i { idris_dynamic_libs = x:libs }
1320 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
1321process fn ListDynamic
1322 = do i <- getIState
1323 iputStrLn "Dynamic libraries:"
1324 showLibs $ idris_dynamic_libs i
1325 where showLibs [] = return ()
1326 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
1327process fn Metavars
1328 = do ist <- getIState
1329 let mvs = map fst (idris_metavars ist) \\ primDefs
1330 case mvs of
1331 [] -> iPrintError "No global holes to solve"
1332 _ -> iPrintResult $ "Global holes:\n\t" ++ show mvs
1333process fn NOP = return ()
1335process fn (SetOpt ErrContext) = setErrContext True
1336process fn (UnsetOpt ErrContext) = setErrContext False
1337process fn (SetOpt ShowImpl) = setImpShow True
1338process fn (UnsetOpt ShowImpl) = setImpShow False
1339process fn (SetOpt ShowOrigErr) = setShowOrigErr True
1340process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1341process fn (SetOpt AutoSolve) = setAutoSolve True
1342process fn (UnsetOpt AutoSolve) = setAutoSolve False
1343process fn (SetOpt NoBanner) = setNoBanner True
1344process fn (UnsetOpt NoBanner) = setNoBanner False
1345process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1346process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1347process fn (SetOpt EvalTypes) = setEvalTypes True
1348process fn (UnsetOpt EvalTypes) = setEvalTypes False
1350process fn (SetOpt DesugarNats) = setDesugarNats True
1351process fn (UnsetOpt DesugarNats) = setDesugarNats False
1353process fn (SetOpt _) = iPrintError "Not a valid option"
1354process fn (UnsetOpt _) = iPrintError "Not a valid option"
1355process fn (SetColour ty c) = setColour ty c
1356process fn ColourOn
1357 = do ist <- getIState
1358 putIState $ ist { idris_colourRepl = True }
1359process fn ColourOff
1360 = do ist <- getIState
1361 putIState $ ist { idris_colourRepl = False }
1362process fn ListErrorHandlers =
1363 do ist <- getIState
1364 iPrintResult $ case idris_errorhandlers ist of
1365 [] -> "No registered error handlers"
1366 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1367process fn (SetConsoleWidth w) = setWidth w
1368process fn (SetPrinterDepth d) = setDepth d
1369process fn (Apropos pkgs a) =
1370 do orig <- getIState
1371 when (not (null pkgs)) $
1372 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
1373 mapM_ loadPkgIndex pkgs
1374 ist <- getIState
1375 let mods = aproposModules ist (T.pack a)
1376 let names = apropos ist (T.pack a)
1377 let aproposInfo = [ (n,
1378 delabTy ist n,
1379 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1380 | n <- sort names, isUN n ]
1381 if (not (null mods)) || (not (null aproposInfo))
1382 then iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$>
1383 ppD ist d <> line) mods) <$>
1384 vsep (map (prettyDocumentedIst ist) aproposInfo)
1385 else iRenderError $ text "No results found"
1386 where isUN (UN _) = True
1387 isUN (NS n _) = isUN n
1388 isUN _ = False
1389 ppD ist = renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) []))
1392process fn (WhoCalls n) =
1393 do calls <- whoCalls n
1394 ist <- getIState
1395 iRenderResult . vsep $
1396 map (\(n, ns) ->
1397 text "Callers of" <+> prettyName True True [] n <$>
1398 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1399 calls
1401process fn (CallsWho n) =
1402 do calls <- callsWho n
1403 ist <- getIState
1404 iRenderResult . vsep $
1405 map (\(n, ns) ->
1406 prettyName True True [] n <+> text "calls:" <$>
1407 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1408 calls
1410process fn (Browse ns) =
1411 do underNSs <- namespacesInNS ns
1412 names <- namesInNS ns
1413 if null underNSs && null names
1414 then iPrintError "Invalid or empty namespace"
1415 else do ist <- getIState
1416 iRenderResult $
1417 text "Namespaces:" <$>
1418 indent 2 (vsep (map (text . showSep ".") underNSs)) <$>
1419 text "Names:" <$>
1420 indent 2 (vsep (map (\n -> prettyName True False [] n <+> colon <+>
1421 (group . align $ pprintDelabTy ist n))
1422 names))
1424-- IdrisDoc
1425process fn (MakeDoc s) =
1426 do istate <- getIState
1427 let names = words s
1428 parse n | Success x <- runparser (fmap fst name) istate fn n = Right x
1429 parse n = Left n
1430 (bad, nss) = partitionEithers $ map parse names
1431 cd <- runIO getCurrentDirectory
1432 let outputDir = cd </> "doc"
1433 result <- if null bad then runIO $ generateDocs istate nss outputDir
1434 else return . Left $ "Illegal name: " ++ head bad
1435 case result of Right _ -> iputStrLn "IdrisDoc generated"
1436 Left err -> iPrintError err
1437process fn (PrintDef n) =
1438 do result <- pprintDef False n
1439 case result of
1440 [] -> iPrintError "Not found"
1441 outs -> iRenderResult . vsep $ outs
1443-- Show relevant transformation rules for the name 'n'
1444process fn (TransformInfo n)
1445 = do i <- getIState
1446 let ts = lookupCtxt n (idris_transforms i)
1447 let res = map (showTrans i) ts
1448 iRenderResult . vsep $ concat res
1449 where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]
1450 showTrans i [] = []
1451 showTrans i ((lhs, rhs) : ts)
1452 = let ppTm tm = annotate (AnnTerm [] tm) .
1453 pprintPTerm (ppOptionIst i) [] [] [] .
1454 delab i $ tm
1455 ts' = showTrans i ts in
1456 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'
1458-- iRenderOutput (pretty lhs)
1459-- iputStrLn " ==> "
1460-- iPrintTermWithType (pprintDelab i rhs)
1461-- iputStrLn "---------------"
1462-- showTrans i ts
1464process fn (PPrint fmt width (PRef _ _ n))
1465 = do outs <- pprintDef False n
1466 iPrintResult =<< renderExternal fmt width (vsep outs)
1469process fn (PPrint fmt width t)
1470 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
1471 ctxt <- getContext
1472 ist <- getIState
1473 let ppo = ppOptionIst ist
1474 ty' = normaliseC ctxt [] ty
1475 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
1477showTotal :: Totality -> IState -> Doc OutputAnnotation
1478showTotal t@(Partial (Other ns)) i
1479 = text "possibly not total due to:" <$>
1480 vsep (map (showTotalN i) ns)
1481showTotal t@(Partial (Mutual ns)) i
1482 = text "possibly not total due to recursive path:" <$>
1483 align (group (vsep (punctuate comma
1484 (map (\n -> annotate (AnnName n Nothing Nothing Nothing) $
1485 text (show n))
1486 ns))))
1487showTotal t i = text (show t)
1489showTotalN :: IState -> Name -> Doc OutputAnnotation
1490showTotalN ist n = case lookupTotal n (tt_ctxt ist) of
1491 [t] -> showN n <> text ", which is" <+> showTotal t ist
1492 _ -> empty
1493 where
1494 ppo = ppOptionIst ist
1495 showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
1496 showName (Just ist) [] ppo False n
1498displayHelp = let vstr = showVersion getIdrisVersionNoGit in
1499 "\nIdris version " ++ vstr ++ "\n" ++
1500 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
1501 concatMap cmdInfo helphead ++
1502 concatMap cmdInfo help
1503 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
1504 col c1 c2 l m r =
1505 l ++ take (c1 - length l) (repeat ' ') ++
1506 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1508pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
1509pprintDef asCore n =
1510 do ist <- getIState
1511 ctxt <- getContext
1512 let ambiguous = length (lookupNames n ctxt) > 1
1513 patdefs = idris_patdefs ist
1514 tyinfo = idris_datatypes ist
1515 if asCore
1516 then return $ map (ppCoreDef ist) (lookupCtxtName n patdefs)
1517 else return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1518 map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1519 map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1520 where ppCoreDef :: IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1521 ppCoreDef ist (n, (clauses, missing)) =
1522 case lookupTy n (tt_ctxt ist) of
1523 [] -> error "Attempted pprintDef of TT of thing that doesn't exist"
1524 (ty:_) -> prettyName True True [] n <+> colon <+>
1525 align (annotate (AnnTerm [] ty) (pprintTT [] ty)) <$>
1526 vsep (map (\(vars, lhs, rhs) -> pprintTTClause vars lhs rhs) clauses)
1527 ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1528 ppDef amb ist (n, (clauses, missing)) =
1529 prettyName True amb [] n <+> colon <+>
1530 align (pprintDelabTy ist n) <$>
1531 ppClauses ist clauses <> ppMissing missing
1532 ppClauses ist [] = text "No clauses."
1533 ppClauses ist cs = vsep (map pp cs)
1534 where pp (varTys, lhs, rhs) =
1535 let vars = map fst varTys
1536 ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1537 pprintPTerm (ppOptionIst ist)
1538 (zip vars (repeat False))
1539 [] (idris_infixes ist) .
1540 delabWithEnv ist varTys $
1542 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1543 ppMissing _ = empty
1545 ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1546 ppTy amb ist (n, TI constructors isCodata _ _ _ _)
1547 = kwd key <+> prettyName True amb [] n <+> colon <+>
1548 align (pprintDelabTy ist n) <+> kwd "where" <$>
1549 indent 2 (vsep (map (ppCon False ist) constructors))
1550 where
1551 key | isCodata = "codata"
1552 | otherwise = "data"
1553 kwd = annotate AnnKeyword . text
1554 ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n)
1557helphead =
1558 [ (["Command"], SpecialHeaderArg, "Purpose"),
1559 ([""], NoArg, "")
1563replSettings :: Maybe FilePath -> Settings Idris
1564replSettings hFile = setComplete replCompletion $ defaultSettings {
1565 historyFile = hFile