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