git.iko.soy/Idris-dev
on de45d29 help sign in
Idris-dev/src/Idris/REPL.hs
1657 lines 73 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards, CPP #-}
4module Idris.REPL where
6import Idris.AbsSyntax
7import Idris.ASTUtils
8import Idris.Apropos (apropos)
9import Idris.REPLParser
10import Idris.ElabDecls
11import Idris.ElabTerm
12import Idris.Erasure
13import Idris.Error
14import Idris.ErrReverse
15import Idris.Delaborate
16import Idris.Docstrings (Docstring, overview, renderDocstring)
17import Idris.IdrisDoc
18import Idris.Prover
19import Idris.Parser hiding (indent)
20import Idris.Primitives
21import Idris.Coverage
22import Idris.Docs hiding (Doc)
23import Idris.Help
24import Idris.Completion
25import qualified Idris.IdeSlave as IdeSlave
26import Idris.Chaser
27import Idris.Imports
28import Idris.Colours hiding (colourise)
29import Idris.Inliner
30import Idris.CaseSplit
31import Idris.DeepSeq
32import Idris.Output
33import Idris.Interactive
34import Idris.WhoCalls
35import Idris.TypeSearch (searchByType)
37import Idris.Elab.Type
38import Idris.Elab.Clause
39import Idris.Elab.Data
40import Idris.Elab.Value
42import Version_idris (gitHash)
43import Util.System
44import Util.DynamicLinker
45import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)
46import Util.Pretty hiding ((</>))
48import Idris.Core.Evaluate
49import Idris.Core.Execute (execute)
50import Idris.Core.TT
51import Idris.Core.Constraints
53import IRTS.Compiler
54import IRTS.CodegenCommon
55import IRTS.System
57import Control.Category
58import Prelude hiding ((.), id)
59import Data.List.Split (splitOn)
60import Data.List (groupBy)
61import qualified Data.Text as T
63import Text.Trifecta.Result(Result(..))
65-- import RTS.SC
66-- import RTS.Bytecode
67-- import RTS.PreC
68-- import RTS.CodegenC
69import System.Console.Haskeline as H
70import System.FilePath
71import System.Exit
72import System.Environment
73import System.Process
74import System.Directory
75import System.IO
76import Control.Monad
77import Control.Monad.Trans.Error (ErrorT(..))
78import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )
79import Control.Monad.Trans ( lift )
80import Control.Concurrent.MVar
81import Network
82import Control.Concurrent
83import Data.Maybe
84import Data.List
85import Data.Char
86import Data.Version
87import Data.Word (Word)
88import Data.Either (partitionEithers)
89import Control.DeepSeq
91import Numeric ( readHex )
93import Debug.Trace
95-- | Run the REPL
96repl :: IState -- ^ The initial state
97 -> [FilePath] -- ^ The loaded modules
98 -> InputT Idris ()
99repl orig mods
100 = -- H.catch
101 do let quiet = opt_quiet (idris_options orig)
102 i <- lift getIState
103 let colour = idris_colourRepl i
104 let theme = idris_colourTheme i
105 let mvs = idris_metavars i
106 let prompt = if quiet
107 then ""
108 else showMVs colour theme mvs ++
109 let str = mkPrompt mods ++ ">" in
110 (if colour then colourisePrompt theme str else str) ++ " "
111 x <- H.catch (getInputLine prompt)
112 (ctrlC (return Nothing))
113 case x of
114 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
115 return ()
116 Just input -> -- H.catch
117 do ms <- H.catch (lift $ processInput input orig mods)
118 (ctrlC (return (Just mods)))
119 case ms of
120 Just mods -> repl orig mods
121 Nothing -> return ()
122-- ctrlC)
123-- ctrlC
124 where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
125 ctrlC act e = do lift $ iputStrLn (show e)
126 act -- repl orig mods
128 showMVs c thm [] = ""
129 showMVs c thm ms = "Metavariables: " ++
130 show' 4 c thm (map fst ms) ++ "\n"
132 show' 0 c thm ms = let l = length ms in
133 "... ( + " ++ show l
134 ++ " other"
135 ++ if l == 1 then ")" else "s)"
136 show' n c thm [m] = showM c thm m
137 show' n c thm (m : ms) = showM c thm m ++ ", " ++
138 show' (n - 1) c thm ms
140 showM c thm n = if c then colouriseFun thm (show n)
141 else show n
143-- | Run the REPL server
144startServer :: IState -> [FilePath] -> Idris ()
145startServer orig fn_in = do tid <- runIO $ forkOS serverLoop
146 return ()
147 where serverLoop :: IO ()
148 -- TODO: option for port number
149 serverLoop = withSocketsDo $
150 do sock <- listenOnLocalhost $ PortNumber 4294
151 loop fn orig { idris_colourRepl = False } sock
153 fn = case fn_in of
154 (f:_) -> f
155 _ -> ""
157 loop fn ist sock
158 = do (h,_,_) <- accept sock
159 hSetEncoding h utf8
160 cmd <- hGetLine h
161 let isth = case idris_outputmode ist of
162 RawOutput _ -> ist {idris_outputmode = RawOutput h}
163 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}
164 (ist', fn) <- processNetCmd orig isth h fn cmd
165 hClose h
166 loop fn ist' sock
168processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->
169 IO (IState, FilePath)
170processNetCmd orig i h fn cmd
171 = do res <- case parseCmd i "(net)" cmd of
172 Failure err -> return (Left (Msg " invalid command"))
173 Success c -> runErrorT $ evalStateT (processNet fn c) i
174 case res of
175 Right x -> return x
176 Left err -> do hPutStrLn h (show err)
177 return (i, fn)
178 where
179 processNet fn Reload = processNet fn (Load fn Nothing)
180 processNet fn (Load f toline) =
181 do let ist = orig { idris_options = idris_options i
182 , idris_colourTheme = idris_colourTheme i
183 , idris_colourRepl = False
184 }
185 putIState ist
186 setErrContext True
187 setOutH h
188 setQuiet True
189 setVerbose False
190 mods <- loadInputs [f] toline
191 ist <- getIState
192 return (ist, f)
193 processNet fn c = do process fn c
194 ist <- getIState
195 return (ist, fn)
196 setOutH :: Handle -> Idris ()
197 setOutH h =
198 do ist <- getIState
199 putIState $ case idris_outputmode ist of
200 RawOutput _ -> ist {idris_outputmode = RawOutput h}
201 IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}
203-- | Run a command on the server on localhost
204runClient :: String -> IO ()
205runClient str = withSocketsDo $ do
206 h <- connectTo "localhost" (PortNumber 4294)
207 hSetEncoding h utf8
208 hPutStrLn h str
209 resp <- hGetResp "" h
210 putStr resp
211 hClose h
212 where hGetResp acc h = do eof <- hIsEOF h
213 if eof then return acc
214 else do l <- hGetLine h
215 hGetResp (acc ++ l ++ "\n") h
217initIdeslaveSocket :: IO Handle
218initIdeslaveSocket = do
219 (sock, port) <- listenOnLocalhostAnyPort
220 putStrLn $ show port
221 (h, _, _) <- accept sock
222 hSetEncoding h utf8
223 return h
225-- | Run the IdeSlave
226ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()
227ideslaveStart s orig mods
228 = do h <- runIO $ if s then initIdeslaveSocket else return stdout
229 setIdeSlave True h
230 i <- getIState
231 case idris_outputmode i of
232 IdeSlave n h ->
233 do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n
234 case mods of
235 a:_ -> runIdeSlaveCommand h n i "" [] (IdeSlave.LoadFile a Nothing)
236 _ -> return ()
237 ideslave h orig mods
239ideslave :: Handle -> IState -> [FilePath] -> Idris ()
240ideslave h orig mods
241 = do idrisCatch
242 (do let inh = if h == stdout then stdin else h
243 len' <- runIO $ IdeSlave.getLen inh
244 len <- case len' of
245 Left err -> ierror err
246 Right n -> return n
247 l <- runIO $ IdeSlave.getNChar inh len ""
248 (sexp, id) <- case IdeSlave.parseMessage l of
249 Left err -> ierror err
250 Right (sexp, id) -> return (sexp, id)
251 i <- getIState
252 putIState $ i { idris_outputmode = (IdeSlave id h) }
253 idrisCatch -- to report correct id back!
254 (do let fn = case mods of
255 (f:_) -> f
256 _ -> ""
257 case IdeSlave.sexpToCommand sexp of
258 Just cmd -> runIdeSlaveCommand h id orig fn mods cmd
259 Nothing -> iPrintError "did not understand" )
260 (\e -> do iPrintError $ show e))
261 (\e -> do iPrintError $ show e)
262 ideslave h orig mods
264-- | Run IDESlave commands
265runIdeSlaveCommand :: Handle -- ^^ The handle for communication
266 -> Integer -- ^^ The continuation ID for the client
267 -> IState -- ^^ The original IState
268 -> FilePath -- ^^ The current open file
269 -> [FilePath] -- ^^ The currently loaded modules
270 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process
271 -> Idris ()
272runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =
273 do c <- colourise
274 i <- getIState
275 case parseCmd i "(input)" cmd of
276 Failure err -> iPrintError $ show (fixColour False err)
277 Success (Prove n') ->
278 idrisCatch
279 (do process fn (Prove n')
280 isetPrompt (mkPrompt mods)
281 case idris_outputmode i of
282 IdeSlave n h -> -- signal completion of proof to ide
283 runIO . hPutStrLn h $
284 IdeSlave.convSExp "return"
285 (IdeSlave.SymbolAtom "ok", "")
286 n
287 _ -> return ())
288 (\e -> do ist <- getIState
289 isetPrompt (mkPrompt mods)
290 case idris_outputmode i of
291 IdeSlave n h ->
292 runIO . hPutStrLn h $
293 IdeSlave.convSExp "abandon-proof" "Abandoned" n
294 _ -> return ()
295 iRenderError $ pprintErr ist e)
296 Success cmd -> idrisCatch
297 (ideslaveProcess fn cmd)
298 (\e -> getIState >>= iRenderError . flip pprintErr e)
299runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =
300 do (unused, compls) <- replCompletion (reverse str, "")
301 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
302 IdeSlave.toSExp (map replacement compls,
303 reverse unused)]
304 runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id
305runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
306 do i <- getIState
307 clearErr
308 putIState (orig { idris_options = idris_options i,
309 idris_outputmode = (IdeSlave id h) })
310 loadInputs [filename] toline
311 isetPrompt (mkPrompt [filename])
312 -- Report either success or failure
313 i <- getIState
314 case (errSpan i) of
315 Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
316 IdeSlave.SexpList []])
317 (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
318 IdeSlave.toSExp fc])
319 (idris_parsedSpan i)
320 in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
321 Just x -> iPrintError $ "didn't load " ++ filename
322 ideslave h orig [filename]
323runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
324 case splitName name of
325 Left err -> iPrintError err
326 Right n -> process "(ideslave)"
327 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
328 where splitName :: String -> Either String Name
329 splitName s = case reverse $ splitOn "." s of
330 [] -> Left ("Didn't understand name '" ++ s ++ "'")
331 [n] -> Right $ sUN n
332 (n:ns) -> Right $ sNS (sUN n) ns
333runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =
334 case parseConst orig name of
335 Success c -> process "(ideslave)" (DocStr (Right c))
336 Failure _ ->
337 case splitName name of
338 Left err -> iPrintError err
339 Right n -> process "(ideslave)" (DocStr (Left n))
340runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =
341 process fn (CaseSplitAt False line (sUN name))
342runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =
343 process fn (AddClauseFrom False line (sUN name))
344runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =
345 process fn (AddProofClauseFrom False line (sUN name))
346runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =
347 process fn (AddMissing False line (sUN name))
348runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =
349 process fn (MakeWith False line (sUN name))
350runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =
351 doProofSearch fn False r line (sUN name) (map sUN hints) depth
352runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =
353 case splitName name of
354 Left err -> iPrintError err
355 Right n -> process fn (MakeLemma False line n)
356runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =
357 process fn (Apropos a)
358runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =
359 do ist <- getIState
360 let opts = idris_options ist
361 let impshow = opt_showimp opts
362 let errCtxt = opt_errContext opts
363 let options = (IdeSlave.SymbolAtom "ok",
364 [(IdeSlave.SymbolAtom "show-implicits", impshow),
365 (IdeSlave.SymbolAtom "error-context", errCtxt)])
366 runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id
367runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =
368 do setImpShow b
369 let msg = (IdeSlave.SymbolAtom "ok", b)
370 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
371runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
372 do setErrContext b
373 let msg = (IdeSlave.SymbolAtom "ok", b)
374 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
375runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =
376 do ist <- getIState
377 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
378 let ppo = ppOptionIst ist
379 -- splitMvs is a list of pairs of names and their split types
380 let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
381 -- mvOutput is the pretty-printed version ready for conversion to SExpr
382 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
383 mapPair show
384 (\(hs, c, pc) ->
385 let bnd = [ n | (n,_,_) <- hs ] in
386 let bnds = inits bnd in
387 (map (\(bnd, h) -> processPremise ist bnd h)
388 (zip bnds hs),
389 render ist bnd c pc))
390 splitMvs
391 runIO . hPutStrLn h $
392 IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
393 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
394 mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
396 -- | Split a function type into a pair of premises, conclusion.
397 -- Each maintains both the original and delaborated versions.
398 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
399 splitPi ist (Bind n (Pi t _) rest) =
400 let (hs, c, pc) = splitPi ist rest in
401 ((n, t, delabTy' ist [] t False False):hs,
402 c, delabTy' ist [] c False False)
403 splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
405 -- | Get the types of a list of metavariable names
406 mvTys :: IState -> [Name] -> [(Name, Type)]
407 mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
409 -- | Show a type and its corresponding PTerm in a format suitable
410 -- for the IDE - that is, pretty-printed and annotated.
411 render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
412 render ist bnd t pt =
413 let prettyT = pprintPTerm (ppOptionIst ist)
414 (zip bnd (repeat False))
415 []
416 (idris_infixes ist)
417 pt
418 in
419 displaySpans .
420 renderPretty 0.9 cols .
421 fmap (fancifyAnnots ist) .
422 annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
423 prettyT
425 -- | Juggle the bits of a premise to prepare for output.
426 processPremise :: IState
427 -> [Name] -- ^ the names to highlight as bound
428 -> (Name, Type, PTerm)
429 -> (String,
430 String,
431 SpanList OutputAnnotation)
432 processPremise ist bnd (n, t, pt) =
433 let (out, spans) = render ist bnd t pt in
434 (show n , out, spans)
436runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =
437 case splitName n of
438 Left err -> iPrintError err
439 Right n -> do calls <- whoCalls n
440 ist <- getIState
441 let msg = (IdeSlave.SymbolAtom "ok",
442 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
443 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
444 where pn ist = displaySpans .
445 renderPretty 0.9 1000 .
446 fmap (fancifyAnnots ist) .
447 prettyName True True []
448runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =
449 case splitName n of
450 Left err -> iPrintError err
451 Right n -> do calls <- callsWho n
452 ist <- getIState
453 let msg = (IdeSlave.SymbolAtom "ok",
454 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
455 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
456 where pn ist = displaySpans .
457 renderPretty 0.9 1000 .
458 fmap (fancifyAnnots ist) .
459 prettyName True True []
461runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =
462 do ctxt <- getContext
463 ist <- getIState
464 let tm' = force (normaliseAll ctxt [] tm)
465 ptm = annotate (AnnTerm bnd tm')
466 (pprintPTerm (ppOptionIst ist)
467 bnd
468 []
469 (idris_infixes ist)
470 (delab ist tm'))
471 msg = (IdeSlave.SymbolAtom "ok",
472 displaySpans .
473 renderPretty 0.9 80 .
474 fmap (fancifyAnnots ist) $ ptm)
475 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
476runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
477 ideSlaveForceTermImplicits h id bnd True tm
478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
479 ideSlaveForceTermImplicits h id bnd False tm
481-- | Show a term for IDESlave with the specified implicitness
482ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
483ideSlaveForceTermImplicits h id bnd impl tm =
484 do ist <- getIState
485 let expl = annotate (AnnTerm bnd tm)
486 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
487 bnd [] (idris_infixes ist)
488 (delab ist tm))
489 msg = (IdeSlave.SymbolAtom "ok",
490 displaySpans .
491 renderPretty 0.9 80 .
492 fmap (fancifyAnnots ist) $ expl)
493 runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
495splitName :: String -> Either String Name
496splitName s = case reverse $ splitOn "." s of
497 [] -> Left ("Didn't understand name '" ++ s ++ "'")
498 [n] -> Right $ sUN n
499 (n:ns) -> Right $ sNS (sUN n) ns
501ideslaveProcess :: FilePath -> Command -> Idris ()
502ideslaveProcess fn Warranty = process fn Warranty
503ideslaveProcess fn Help = process fn Help
504ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
505 iPrintResult "changed directory to"
506ideslaveProcess fn (Eval t) = process fn (Eval t)
507ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)
508 iPrintResult "defined"
509ideslaveProcess fn (Undefine n) = process fn (Undefine n)
510ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
511ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
512ideslaveProcess fn (Check t) = process fn (Check t)
513ideslaveProcess fn (DocStr n) = process fn (DocStr n)
514ideslaveProcess fn Universes = process fn Universes
515ideslaveProcess fn (Defn n) = do process fn (Defn n)
516 iPrintResult ""
517ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
518ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
519 iPrintResult ""
520ideslaveProcess fn (Search t) = process fn (Search t)
521ideslaveProcess fn (Spec t) = process fn (Spec t)
522-- RmProof and AddProof not supported!
523ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
524ideslaveProcess fn (HNF t) = process fn (HNF t)
525--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
526ideslaveProcess fn (TestInline t) = process fn (TestInline t)
528ideslaveProcess fn Execute = do process fn Execute
529 iPrintResult ""
530ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)
531 iPrintResult ""
532ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
533 iPrintResult ""
534ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
535ideslaveProcess fn (Missing n) = process fn (Missing n)
536ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
537 iPrintResult ""
538ideslaveProcess fn ListDynamic = do process fn ListDynamic
539 iPrintResult ""
540ideslaveProcess fn Metavars = process fn Metavars
541ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
542 iPrintResult ""
543ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
544 iPrintResult ""
545ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
546 iPrintResult ""
547ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
548 iPrintResult ""
549ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)
550 iPrintResult ""
551ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)
552 iPrintResult ""
553ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
554ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
555ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)
556ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)
557ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
558ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
559ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
560ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
561ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
562 iPrintResult ""
563ideslaveProcess fn (Apropos a) = do process fn (Apropos a)
564 iPrintResult ""
565ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)
566ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)
567ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)
568ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
571-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
572mkPrompt [] = "Idris"
573mkPrompt [x] = "*" ++ dropExtension x
574mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
576-- | Determine whether a file uses literate syntax
577lit f = case splitExtension f of
578 (_, ".lidr") -> True
579 _ -> False
581processInput :: String ->
582 IState -> [FilePath] -> Idris (Maybe [FilePath])
583processInput cmd orig inputs
584 = do i <- getIState
585 let opts = idris_options i
586 let quiet = opt_quiet opts
587 let fn = case inputs of
588 (f:_) -> f
589 _ -> ""
590 c <- colourise
591 case parseCmd i "(input)" cmd of
592 Failure err -> do runIO $ print (fixColour c err)
593 return (Just inputs)
594 Success Reload ->
595 do putIState $ orig { idris_options = idris_options i
596 , idris_colourTheme = idris_colourTheme i
597 }
598 clearErr
599 mods <- loadInputs inputs Nothing
600 return (Just inputs)
601 Success (Load f toline) ->
602 do putIState orig { idris_options = idris_options i
603 , idris_colourTheme = idris_colourTheme i
604 }
605 clearErr
606 mod <- loadInputs [f] toline
607 return (Just [f])
608 Success (ModImport f) ->
609 do clearErr
610 fmod <- loadModule f
611 return (Just (inputs ++ [fmod]))
612 Success Edit -> do -- takeMVar stvar
613 edit fn orig
614 return (Just inputs)
615 Success Proofs -> do proofs orig
616 return (Just inputs)
617 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")
618 return Nothing
619 Success cmd -> do idrisCatch (process fn cmd)
620 (\e -> do msg <- showErr e ; iputStrLn msg)
621 return (Just inputs)
623resolveProof :: Name -> Idris Name
624resolveProof n'
625 = do i <- getIState
626 ctxt <- getContext
627 n <- case lookupNames n' ctxt of
628 [x] -> return x
629 [] -> return n'
630 ns -> ierror (CantResolveAlts ns)
631 return n
633removeProof :: Name -> Idris ()
634removeProof n =
635 do i <- getIState
636 let proofs = proof_list i
637 let ps = filter ((/= n) . fst) proofs
638 putIState $ i { proof_list = ps }
640edit :: FilePath -> IState -> Idris ()
641edit "" orig = iputStrLn "Nothing to edit"
642edit f orig
643 = do i <- getIState
644 env <- runIO $ getEnvironment
645 let editor = getEditor env
646 let line = case errSpan i of
647 Just l -> " +" ++ show (fst (fc_start l)) ++ " "
648 Nothing -> " "
649 let cmd = editor ++ line ++ fixName f
650 runIO $ system cmd
651 clearErr
652 putIState $ orig { idris_options = idris_options i
653 , idris_colourTheme = idris_colourTheme i
654 }
655 loadInputs [f] Nothing
656-- clearOrigPats
657 iucheck
658 return ()
659 where getEditor env | Just ed <- lookup "EDITOR" env = ed
660 | Just ed <- lookup "VISUAL" env = ed
661 | otherwise = "vi"
662 fixName file | map toLower (takeExtension file) `elem` [".lidr", ".idr"] = file
663 | otherwise = addExtension file "idr"
667proofs :: IState -> Idris ()
668proofs orig
669 = do i <- getIState
670 let ps = proof_list i
671 case ps of
672 [] -> iputStrLn "No proofs available"
673 _ -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)
675insertScript :: String -> [String] -> [String]
676insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
677insertScript prf (p@"---------- Proofs ----------" : "" : xs)
678 = p : "" : prf : xs
679insertScript prf (x : xs) = x : insertScript prf xs
681process :: FilePath -> Command -> Idris ()
682process fn Help = iPrintResult displayHelp
683process fn Warranty = iPrintResult warranty
684process fn (ChangeDirectory f)
685 = do runIO $ setCurrentDirectory f
686 return ()
687process fn (Eval t)
688 = withErrorReflection $ do logLvl 5 $ show t
689 getIState >>= flip warnDisamb t
690 (tm, ty) <- elabVal recinfo ERHS t
691 ctxt <- getContext
692 let tm' = force (normaliseAll ctxt [] tm)
693 let ty' = force (normaliseAll ctxt [] ty)
694 -- Add value to context, call it "it"
695 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))
696 ist <- getIState
697 logLvl 3 $ "Raw: " ++ show (tm', ty')
698 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
699 let tmDoc = pprintDelab ist tm'
700 tyDoc = pprintDelab ist ty'
701 iPrintTermWithType tmDoc tyDoc
704process fn (NewDefn decls) = do
705 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
706 mapM_ defineName namedGroups where
707 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls
708 getName :: PDecl -> Maybe Name
709 getName (PTy docs argdocs syn fc opts name ty) = Just name
710 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
711 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)
712 getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name
713 getName _ = Nothing
714 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
715 getClauseName (PClause fc name whole with rhs whereBlock) = name
716 getClauseName (PWith fc name whole with rhs whereBlock) = name
717 defineName :: [PDecl] -> Idris ()
718 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
719 elabDecl EAll recinfo tyDecl
720 elabClauses recinfo fc opts name (concatMap getClauses decls)
721 setReplDefined (Just name)
722 defineName [PClauses fc opts _ [clause]] = do
723 let pterm = getRHS clause
724 (tm,ty) <- elabVal recinfo ERHS pterm
725 ctxt <- getContext
726 let tm' = force (normaliseAll ctxt [] tm)
727 let ty' = force (normaliseAll ctxt [] ty)
728 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
729 setReplDefined (Just $ getClauseName clause)
730 defineName (PClauses{} : _) = tclift $ tfail (Msg "Only one function body is allowed without a type declaration.")
731 -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way
732 defineName (PFix fc fixity strs : defns) = do
733 fmodifyState idris_fixities (map (Fix fixity) strs ++)
734 unless (null defns) $ defineName defns
735 defineName (PSyntax{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")
736 defineName decls = do
737 elabDecls toplevel (map fixClauses decls)
738 setReplDefined (getName (head decls))
739 getClauses (PClauses fc opts name clauses) = clauses
740 getClauses _ = []
741 getRHS :: PClause -> PTerm
742 getRHS (PClause fc name whole with rhs whereBlock) = rhs
743 getRHS (PWith fc name whole with rhs whereBlock) = rhs
744 getRHS (PClauseR fc with rhs whereBlock) = rhs
745 getRHS (PWithR fc with rhs whereBlock) = rhs
746 setReplDefined :: Maybe Name -> Idris ()
747 setReplDefined Nothing = return ()
748 setReplDefined (Just n) = do
749 oldState <- get
750 fmodifyState repl_definitions (n:)
751 -- the "name" field of PClauses seems to always be MN 2 "__", so we need to
752 -- retrieve the actual name from deeper inside.
753 -- This should really be a full recursive walk through the structure of PDecl, but
754 -- I think it should work this way and I want to test sooner. Also lazy.
755 fixClauses :: PDecl' t -> PDecl' t
756 fixClauses (PClauses fc opts _ css@(clause:cs)) =
757 PClauses fc opts (getClauseName clause) css
758 fixClauses (PInstance syn fc constraints cls parms ty instName decls) =
759 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
760 fixClauses decl = decl
762process fn (Undefine names) = undefine names
763 where
764 undefine :: [Name] -> Idris ()
765 undefine [] = do
766 allDefined <- idris_repl_defs `fmap` get
767 undefine' allDefined []
768 -- Keep track of which names you've removed so you can
769 -- print them out to the user afterward
770 undefine names = undefine' names []
771 undefine' [] list = do iRenderOutput $ printUndefinedNames list
772 return ()
773 undefine' (n:names) already = do
774 allDefined <- idris_repl_defs `fmap` get
775 if n `elem` allDefined
776 then do undefinedJustNow <- undefClosure n
777 undefine' names (undefinedJustNow ++ already)
778 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
779 undefine' names already
780 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
781 -- for now just assume it's a class. Eventually we'll want some kind of
782 -- smart detection of exactly what kind of name we're undefining.
783 fputState (ctxt_lookup n . known_classes) Nothing
784 fmodifyState repl_definitions (delete n)
785 undefClosure n =
786 do replDefs <- idris_repl_defs `fmap` get
787 callGraph <- whoCalls n
788 let users = case lookup n callGraph of
789 Just ns -> nub ns
790 Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
791 undefinedJustNow <- concat `fmap` mapM undefClosure users
792 undefOne n
793 return (nub (n : undefinedJustNow))
797process fn (ExecVal t)
798 = do ctxt <- getContext
799 ist <- getIState
800 (tm, ty) <- elabVal recinfo ERHS t
801-- let tm' = normaliseAll ctxt [] tm
802 let ty' = normaliseAll ctxt [] ty
803 res <- execute tm
804 let (resOut, tyOut) = (prettyIst ist (delab ist res),
805 prettyIst ist (delab ist ty'))
806 iPrintTermWithType resOut tyOut
808process fn (Check (PRef _ n))
809 = do ctxt <- getContext
810 ist <- getIState
811 let ppo = ppOptionIst ist
812 case lookupNames n ctxt of
813 ts@(t:_) ->
814 case lookup t (idris_metavars ist) of
815 Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $
816 showMetavarInfo ppo ist n i
817 Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)
818 [] -> iPrintError $ "No such variable " ++ show n
819 where
820 showMetavarInfo ppo ist n i
821 = case lookupTy n (tt_ctxt ist) of
822 (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
823 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
824 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
825 putTy ppo ist i bnd (PPi _ n t sc)
826 = let current = text " " <>
827 (case n of
828 MN _ _ -> text "_"
829 UN nm | ('_':'_':_) <- str nm -> text "_"
830 _ -> bindingOf n False) <+>
831 colon <+> align (tPretty bnd ist t) <> line
832 in
833 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
834 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
835 putGoal ppo ist bnd g
836 = text "--------------------------------------" <$>
837 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
838 align (tPretty bnd ist g)
840 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
843process fn (Check t)
844 = do (tm, ty) <- elabVal recinfo ERHS t
845 ctxt <- getContext
846 ist <- getIState
847 let ppo = ppOptionIst ist
848 ty' = normaliseC ctxt [] ty
849 case tm of
850 TType _ ->
851 iPrintTermWithType (prettyIst ist PType) type1Doc
852 _ -> iPrintTermWithType (pprintDelab ist tm)
853 (pprintDelab ist ty)
855process fn (DocStr (Left n))
856 = do ist <- getIState
857 case lookupCtxtName n (idris_docstrings ist) of
858 [] -> iPrintError $ "No documentation for " ++ show n
859 ns -> do toShow <- mapM (showDoc ist) ns
860 iRenderResult (vsep toShow)
861 where showDoc ist (n, d) = do doc <- getDocs n
862 return $ pprintDocs ist doc
864process fn (DocStr (Right c))
865 = do ist <- getIState
866 iRenderResult $ pprintConstDocs ist c (constDocs c)
868process fn Universes
869 = do i <- getIState
870 let cs = idris_constraints i
871-- iputStrLn $ showSep "\n" (map show cs)
872 iputStrLn $ show (map fst cs)
873 let n = length cs
874 iputStrLn $ "(" ++ show n ++ " constraints)"
875 case ucheck cs of
876 Error e -> iPrintError $ pshow i e
877 OK _ -> iPrintResult "Universes OK"
878process fn (Defn n)
879 = do i <- getIState
880 iputStrLn "Compiled patterns:\n"
881 iputStrLn $ show (lookupDef n (tt_ctxt i))
882 case lookupCtxt n (idris_patdefs i) of
883 [] -> return ()
884 [(d, _)] -> do iputStrLn "Original definiton:\n"
885 mapM_ (printCase i) d
886 case lookupTotal n (tt_ctxt i) of
887 [t] -> iputStrLn (showTotal t i)
888 _ -> return ()
889 where printCase i (_, lhs, rhs)
890 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
891 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
892 showTm i' (delab i rhs))
893process fn (TotCheck n)
894 = do i <- getIState
895 case lookupNameTotal n (tt_ctxt i) of
896 [] -> iPrintError $ "Unknown operator " ++ show n
897 ts -> do ist <- getIState
898 c <- colourise
899 let ppo = ppOptionIst ist
900 let showN = showName (Just ist) [] ppo c
901 iPrintResult . concat . intersperse "\n" .
902 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
903 ts
906process fn (DebugInfo n)
907 = do i <- getIState
908 let oi = lookupCtxtName n (idris_optimisation i)
909 when (not (null oi)) $ iputStrLn (show oi)
910 let si = lookupCtxt n (idris_statics i)
911 when (not (null si)) $ iputStrLn (show si)
912 let di = lookupCtxt n (idris_datatypes i)
913 when (not (null di)) $ iputStrLn (show di)
914 let d = lookupDef n (tt_ctxt i)
915 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
916 let cg = lookupCtxtName n (idris_callgraph i)
917 i <- getIState
918 let cg' = lookupCtxtName n (idris_callgraph i)
919 sc <- checkSizeChange n
920 iputStrLn $ "Size change: " ++ show sc
921 let fn = lookupCtxtName n (idris_fninfo i)
922 when (not (null cg')) $ do iputStrLn "Call graph:\n"
923 iputStrLn (show cg')
924 when (not (null fn)) $ iputStrLn (show fn)
925process fn (Search t) = searchByType t
926process fn (CaseSplitAt updatefile l n)
927 = caseSplitAt fn updatefile l n
928process fn (AddClauseFrom updatefile l n)
929 = addClauseFrom fn updatefile l n
930process fn (AddProofClauseFrom updatefile l n)
931 = addProofClauseFrom fn updatefile l n
932process fn (AddMissing updatefile l n)
933 = addMissing fn updatefile l n
934process fn (MakeWith updatefile l n)
935 = makeWith fn updatefile l n
936process fn (MakeLemma updatefile l n)
937 = makeLemma fn updatefile l n
938process fn (DoProofSearch updatefile rec l n hints)
939 = doProofSearch fn updatefile rec l n hints Nothing
940process fn (Spec t)
941 = do (tm, ty) <- elabVal recinfo ERHS t
942 ctxt <- getContext
943 ist <- getIState
944 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
945 iPrintResult (show (delab ist tm'))
947process fn (RmProof n')
948 = do i <- getIState
949 n <- resolveProof n'
950 let proofs = proof_list i
951 case lookup n proofs of
952 Nothing -> iputStrLn "No proof to remove"
953 Just _ -> do removeProof n
954 insertMetavar n
955 iputStrLn $ "Removed proof " ++ show n
956 where
957 insertMetavar :: Name -> Idris ()
958 insertMetavar n =
959 do i <- getIState
960 let ms = idris_metavars i
961 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
963process fn' (AddProof prf)
964 = do fn <- do
965 let fn'' = takeWhile (/= ' ') fn'
966 ex <- runIO $ doesFileExist fn''
967 let fnExt = fn'' <.> "idr"
968 exExt <- runIO $ doesFileExist fnExt
969 if ex
970 then return fn''
971 else if exExt
972 then return fnExt
973 else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
974 let fb = fn ++ "~"
975 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
976 prog <- runIO $ readFile fb
977 i <- getIState
978 let proofs = proof_list i
979 n' <- case prf of
980 Nothing -> case proofs of
981 [] -> ifail "No proof to add"
982 ((x, p) : _) -> return x
983 Just nm -> return nm
984 n <- resolveProof n'
985 case lookup n proofs of
986 Nothing -> iputStrLn "No proof to add"
987 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
988 runIO $ writeFile fn (unlines prog')
989 removeProof n
990 iputStrLn $ "Added proof " ++ show n
991 where ls = (lines prog)
993process fn (ShowProof n')
994 = do i <- getIState
995 n <- resolveProof n'
996 let proofs = proof_list i
997 case lookup n proofs of
998 Nothing -> iPrintError "No proof to show"
999 Just p -> iPrintResult $ showProof False n p
1001process fn (Prove n')
1002 = do ctxt <- getContext
1003 ist <- getIState
1004 let ns = lookupNames n' ctxt
1005 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
1006 n <- case metavars of
1007 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
1008 [(n, (_,_,False))] -> return n
1009 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
1010 ns -> ierror (CantResolveAlts (map fst ns))
1011 prover (lit fn) n
1012 -- recheck totality
1013 i <- getIState
1014 totcheck (fileFC "(input)", n)
1015 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
1016 mapM_ checkDeclTotality (idris_totcheck i)
1017 warnTotality
1019process fn (HNF t)
1020 = do (tm, ty) <- elabVal recinfo ERHS t
1021 ctxt <- getContext
1022 ist <- getIState
1023 let tm' = hnf ctxt [] tm
1024 iPrintResult (show (delab ist tm'))
1025process fn (TestInline t)
1026 = do (tm, ty) <- elabVal recinfo ERHS t
1027 ctxt <- getContext
1028 ist <- getIState
1029 let tm' = inlineTerm ist tm
1030 c <- colourise
1031 iPrintResult (showTm ist (delab ist tm'))
1032process fn Execute
1033 = idrisCatch
1034 (do ist <- getIState
1035 (m, _) <- elabVal recinfo ERHS
1036 (PApp fc
1037 (PRef fc (sUN "run__IO"))
1038 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1039 (tmpn, tmph) <- runIO tempfile
1040 runIO $ hClose tmph
1041 t <- codegen
1042 ir <- compile t tmpn m
1043 runIO $ generate t (head (idris_imported ist)) ir
1044 case idris_outputmode ist of
1045 RawOutput h -> do runIO $ system tmpn
1046 return ()
1047 IdeSlave n h -> runIO . hPutStrLn h $
1048 IdeSlave.convSExp "run-program" tmpn n)
1049 (\e -> getIState >>= iRenderError . flip pprintErr e)
1050 where fc = fileFC "main"
1051process fn (Compile codegen f)
1052 = do (m, _) <- elabVal recinfo ERHS
1053 (PApp fc (PRef fc (sUN "run__IO"))
1054 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1055 ir <- compile codegen f m
1056 i <- getIState
1057 runIO $ generate codegen (head (idris_imported i)) ir
1058 where fc = fileFC "main"
1059process fn (LogLvl i) = setLogLevel i
1060-- Elaborate as if LHS of a pattern (debug command)
1061process fn (Pattelab t)
1062 = do (tm, ty) <- elabVal recinfo ELHS t
1063 iPrintResult $ show tm ++ "\n\n : " ++ show ty
1065process fn (Missing n)
1066 = do i <- getIState
1067 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
1068 case lookupCtxt n (idris_patdefs i) of
1069 [] -> iPrintError $ "Unknown operator " ++ show n
1070 [(_, tms)] ->
1071 iPrintResult (showSep "\n" (map (showTm i') tms))
1072 _ -> iPrintError $ "Ambiguous name"
1073process fn (DynamicLink l)
1074 = do i <- getIState
1075 let importdirs = opt_importdirs (idris_options i)
1076 lib = trim l
1077 handle <- lift . lift $ tryLoadLib importdirs lib
1078 case handle of
1079 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
1080 Just x -> do let libs = idris_dynamic_libs i
1081 if x `elem` libs
1082 then do iLOG ("Tried to load duplicate library " ++ lib_name x)
1083 return ()
1084 else putIState $ i { idris_dynamic_libs = x:libs }
1085 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
1086process fn ListDynamic
1087 = do i <- getIState
1088 iputStrLn "Dynamic libraries:"
1089 showLibs $ idris_dynamic_libs i
1090 where showLibs [] = return ()
1091 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls
1092process fn Metavars
1093 = do ist <- getIState
1094 let mvs = map fst (idris_metavars ist) \\ primDefs
1095 case mvs of
1096 [] -> iPrintError "No global metavariables to solve"
1097 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs
1098process fn NOP = return ()
1100process fn (SetOpt ErrContext) = setErrContext True
1101process fn (UnsetOpt ErrContext) = setErrContext False
1102process fn (SetOpt ShowImpl) = setImpShow True
1103process fn (UnsetOpt ShowImpl) = setImpShow False
1104process fn (SetOpt ShowOrigErr) = setShowOrigErr True
1105process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1106process fn (SetOpt AutoSolve) = setAutoSolve True
1107process fn (UnsetOpt AutoSolve) = setAutoSolve False
1108process fn (SetOpt NoBanner) = setNoBanner True
1109process fn (UnsetOpt NoBanner) = setNoBanner False
1110process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
1111process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1113process fn (SetOpt _) = iPrintError "Not a valid option"
1114process fn (UnsetOpt _) = iPrintError "Not a valid option"
1115process fn (SetColour ty c) = setColour ty c
1116process fn ColourOn
1117 = do ist <- getIState
1118 putIState $ ist { idris_colourRepl = True }
1119process fn ColourOff
1120 = do ist <- getIState
1121 putIState $ ist { idris_colourRepl = False }
1122process fn ListErrorHandlers =
1123 do ist <- getIState
1124 iPrintResult $ case idris_errorhandlers ist of
1125 [] -> "No registered error handlers"
1126 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1127process fn (SetConsoleWidth w) = setWidth w
1129process fn (Apropos a) =
1130 do ist <- getIState
1131 let names = apropos ist (T.pack a)
1132 let aproposInfo = [ (n,
1133 delabTy ist n,
1134 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1135 | n <- sort names, isUN n ]
1136 iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)
1137 where isUN (UN _) = True
1138 isUN (NS n _) = isUN n
1139 isUN _ = False
1141process fn (WhoCalls n) =
1142 do calls <- whoCalls n
1143 ist <- getIState
1144 iRenderResult . vsep $
1145 map (\(n, ns) ->
1146 text "Callers of" <+> prettyName True True [] n <$>
1147 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1148 calls
1150process fn (CallsWho n) =
1151 do calls <- callsWho n
1152 ist <- getIState
1153 iRenderResult . vsep $
1154 map (\(n, ns) ->
1155 prettyName True True [] n <+> text "calls:" <$>
1156 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
1157 calls
1158-- IdrisDoc
1159process fn (MakeDoc s) =
1160 do istate <- getIState
1161 let names = words s
1162 parse n | Success x <- runparser name istate fn n = Right x
1163 parse n = Left n
1164 (bad, nss) = partitionEithers $ map parse names
1165 cd <- runIO $ getCurrentDirectory
1166 let outputDir = cd </> "doc"
1167 result <- if null bad then runIO $ generateDocs istate nss outputDir
1168 else return . Left $ "Illegal name: " ++ head bad
1169 case result of Right _ -> iputStrLn "IdrisDoc generated"
1170 Left err -> iPrintError err
1171process fn (PrintDef n) =
1172 do ist <- getIState
1173 let patdefs = idris_patdefs ist
1174 result = map (ppDef ist) (lookupCtxtName n patdefs)
1175 case result of
1176 [] -> iPrintError "Not found"
1177 outs -> iRenderResult . vsep $ outs
1178 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1179 ppDef ist (n, (clauses, missing)) =
1180 prettyName True True [] n <+> colon <+>
1181 pprintPTerm (ppOptionIst ist) [] [] [] (delabTy ist n) <$>
1182 indent 2 (ppClauses ist clauses <> ppMissing missing)
1183 ppClauses ist [] = text "No clauses."
1184 ppClauses ist cs = vsep (map pp cs)
1185 where pp (vars, lhs, rhs) =
1186 let ppTm = pprintPTerm (ppOptionIst ist)
1187 (zip vars (repeat False))
1188 [] [] .
1189 delab ist
1190 in ppTm lhs <+> text "=" <+> ppTm rhs
1191 ppMissing _ = empty
1194showTotal :: Totality -> IState -> String
1195showTotal t@(Partial (Other ns)) i
1196 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
1197showTotal t i = show t
1198showTotalN i n = case lookupTotal n (tt_ctxt i) of
1199 [t] -> showTotal t i
1200 _ -> ""
1202displayHelp = let vstr = showVersion version in
1203 "\nIdris version " ++ vstr ++ "\n" ++
1204 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
1205 concatMap cmdInfo helphead ++
1206 concatMap cmdInfo help
1207 where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text
1208 col c1 c2 l m r =
1209 l ++ take (c1 - length l) (repeat ' ') ++
1210 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1212helphead =
1213 [ (["Command"], SpecialHeaderArg, "Purpose"),
1214 ([""], NoArg, "")
1218replSettings :: Maybe FilePath -> Settings Idris
1219replSettings hFile = setComplete replCompletion $ defaultSettings {
1220 historyFile = hFile
1223-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1224idris :: [Opt] -> IO (Maybe IState)
1225idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
1226 case res of
1227 Left err -> do putStrLn $ pshow idrisInit err
1228 return Nothing
1229 Right ist -> return (Just ist)
1230 where totalMain = do idrisMain opts
1231 ist <- getIState
1232 case idris_totcheckfail ist of
1233 ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1234 [] -> return ()
1237loadInputs :: [FilePath] -> Maybe Int -> Idris ()
1238loadInputs inputs toline -- furthest line to read in input source files
1239 = idrisCatch
1240 (do ist <- getIState
1241 -- if we're in --check and not outputting anything, don't bother
1242 -- loading, as it gets really slow if there's lots of modules in
1243 -- a package (instead, reload all at the end to check for
1244 -- consistency only)
1245 opts <- getCmdLine
1247 let loadCode = case opt getOutput opts of
1248 [] -> not (NoREPL `elem` opts)
1249 _ -> True
1251 -- For each ifile list, check it and build ibcs in the same clean IState
1252 -- so that they don't interfere with each other when checking
1254 let ninputs = zip [1..] inputs
1255 ifiles <- mapWhileOK (\(num, input) ->
1256 do putIState ist
1257 modTree <- buildTree
1258 (map snd (take (num-1) ninputs))
1259 input
1260 let ifiles = getModuleFiles modTree
1261 iLOG ("MODULE TREE : " ++ show modTree)
1262 iLOG ("RELOAD: " ++ show ifiles)
1263 when (not (all ibc ifiles) || loadCode) $
1264 tryLoad False (filter (not . ibc) ifiles)
1265 -- return the files that need rechecking
1266 return ifiles)
1267 ninputs
1268 inew <- getIState
1269 let tidata = idris_tyinfodata inew
1270 let patdefs = idris_patdefs inew
1271 -- If it worked, load the whole thing from all the ibcs together
1272 case errSpan inew of
1273 Nothing ->
1274 do putIState (ist { idris_tyinfodata = tidata })
1275 ibcfiles <- mapM findNewIBC (nub (concat ifiles))
1276 tryLoad True (mapMaybe id ibcfiles)
1277 _ -> return ()
1278 ist <- getIState
1279 putIState (ist { idris_tyinfodata = tidata,
1280 idris_patdefs = patdefs })
1282 case opt getOutput opts of
1283 [] -> performUsageAnalysis -- interactive
1284 _ -> return [] -- batch, will be checked by the compiler
1286 return ())
1287 (\e -> do i <- getIState
1288 case e of
1289 At f e' -> do setErrSpan f
1290 iWarn f $ pprintErr i e'
1291 ProgramLineComment -> return () -- fail elsewhere
1292 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1293 iWarn emptyFC $ pprintErr i e)
1294 where -- load all files, stop if any fail
1295 tryLoad :: Bool -> [IFileType] -> Idris ()
1296 tryLoad keepstate [] = warnTotality >> return ()
1297 tryLoad keepstate (f : fs)
1298 = do ist <- getIState
1299 let maxline
1300 = case toline of
1301 Nothing -> Nothing
1302 Just l -> case f of
1303 IDR fn -> if any (fmatch fn) inputs
1304 then Just l
1305 else Nothing
1306 LIDR fn -> if any (fmatch fn) inputs
1307 then Just l
1308 else Nothing
1309 _ -> Nothing
1310 loadFromIFile f maxline
1311 inew <- getIState
1312 -- FIXME: Save these in IBC to avoid this hack! Need to
1313 -- preserve it all from source inputs
1314 let tidata = idris_tyinfodata inew
1315 let patdefs = idris_patdefs inew
1316 ok <- noErrors
1317 when ok $ do when (not keepstate) $ putIState ist
1318 ist <- getIState
1319 putIState (ist { idris_tyinfodata = tidata,
1320 idris_patdefs = patdefs })
1321 tryLoad keepstate fs
1323 ibc (IBC _ _) = True
1324 ibc _ = False
1326 fmatch ('.':'/':xs) ys = fmatch xs ys
1327 fmatch xs ('.':'/':ys) = fmatch xs ys
1328 fmatch xs ys = xs == ys
1330 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1331 findNewIBC i@(IBC _ _) = return (Just i)
1332 findNewIBC s@(IDR f) = do ist <- get
1333 ibcsd <- valIBCSubDir ist
1334 let ibc = ibcPathNoFallback ibcsd f
1335 ok <- runIO $ doesFileExist ibc
1336 if ok then return (Just (IBC ibc s))
1337 else return Nothing
1338 findNewIBC s@(LIDR f) = do ist <- get
1339 ibcsd <- valIBCSubDir ist
1340 let ibc = ibcPathNoFallback ibcsd f
1341 ok <- runIO $ doesFileExist ibc
1342 if ok then return (Just (IBC ibc s))
1343 else return Nothing
1345 -- Like mapM, but give up when there's an error
1346 mapWhileOK f [] = return []
1347 mapWhileOK f (x : xs) = do x' <- f x
1348 ok <- noErrors
1349 if ok then do xs' <- mapWhileOK f xs
1350 return (x' : xs')
1351 else return [x']
1353idrisMain :: [Opt] -> Idris ()
1354idrisMain opts =
1355 do let inputs = opt getFile opts
1356 let quiet = Quiet `elem` opts
1357 let nobanner = NoBanner `elem` opts
1358 let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts
1359 let runrepl = not (NoREPL `elem` opts)
1360 let verbose = runrepl || Verbose `elem` opts
1361 let output = opt getOutput opts
1362 let ibcsubdir = opt getIBCSubDir opts
1363 let importdirs = opt getImportDir opts
1364 let bcs = opt getBC opts
1365 let pkgdirs = opt getPkgDir opts
1366 let optimize = case opt getOptLevel opts of
1367 [] -> 2
1368 xs -> last xs
1369 let outty = case opt getOutputTy opts of
1370 [] -> Executable
1371 xs -> last xs
1372 let cgn = case opt getCodegen opts of
1373 [] -> Via "c"
1374 xs -> last xs
1375 script <- case opt getExecScript opts of
1376 [] -> return Nothing
1377 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1378 runIO $ exitWith (ExitFailure 1)
1379 [expr] -> return (Just expr)
1380 let immediate = opt getEvalExpr opts
1382 when (DefaultTotal `elem` opts) $ do i <- getIState
1383 putIState (i { default_total = True })
1384 setColourise $ not quiet && last (True : opt getColour opts)
1385 when (not runrepl) $ setWidth InfinitelyWide
1386 mapM_ addLangExt (opt getLanguageExt opts)
1387 setREPL runrepl
1388 setQuiet (quiet || isJust script || not (null immediate))
1389 setVerbose verbose
1390 setCmdLine opts
1391 setOutputTy outty
1392 setNoBanner nobanner
1393 setCodegen cgn
1394 mapM_ makeOption opts
1395 -- if we have the --bytecode flag, drop into the bytecode assembler
1396 case bcs of
1397 [] -> return ()
1398 xs -> return () -- runIO $ mapM_ bcAsm xs
1399 case ibcsubdir of
1400 [] -> setIBCSubDir ""
1401 (d:_) -> setIBCSubDir d
1402 setImportDirs importdirs
1404 setNoBanner nobanner
1406 when (not (NoBasePkgs `elem` opts)) $ do
1407 addPkgDir "prelude"
1408 addPkgDir "base"
1409 mapM_ addPkgDir pkgdirs
1410 elabPrims
1411 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"
1412 addAutoImport "Builtins"
1413 return ()
1414 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
1415 addAutoImport "Prelude"
1416 return ()
1418 when (runrepl && not idesl) initScript
1420 nobanner <- getNoBanner
1422 when (runrepl &&
1423 not quiet &&
1424 not idesl &&
1425 not (isJust script) &&
1426 not nobanner &&
1427 null immediate) $
1428 iputStrLn banner
1430 orig <- getIState
1431 when (not idesl) $ loadInputs inputs Nothing
1433 runIO $ hSetBuffering stdout LineBuffering
1435 ok <- noErrors
1436 when ok $ case output of
1437 [] -> return ()
1438 (o:_) -> idrisCatch (process "" (Compile cgn o))
1439 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1441 case immediate of
1442 [] -> return ()
1443 exprs -> do setWidth InfinitelyWide
1444 mapM_ (\str -> do ist <- getIState
1445 c <- colourise
1446 case parseExpr ist str of
1447 Failure err -> do iputStrLn $ show (fixColour c err)
1448 runIO $ exitWith (ExitFailure 1)
1449 Success e -> process "" (Eval e))
1450 exprs
1451 runIO $ exitWith ExitSuccess
1454 case script of
1455 Nothing -> return ()
1456 Just expr -> execScript expr
1458 -- Create Idris data dir + repl history and config dir
1459 idrisCatch (do dir <- getIdrisUserDataDir
1460 exists <- runIO $ doesDirectoryExist dir
1461 unless exists $ iLOG ("Creating " ++ dir)
1462 runIO $ createDirectoryIfMissing True (dir </> "repl"))
1463 (\e -> return ())
1465 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir
1467 when (runrepl && not idesl) $ do
1468-- clearOrigPats
1469 startServer orig inputs
1470 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1471 let idesock = IdeslaveSocket `elem` opts
1472 when (idesl) $ ideslaveStart idesock orig inputs
1473 ok <- noErrors
1474 when (not ok) $ runIO (exitWith (ExitFailure 1))
1475 where
1476 makeOption (OLogging i) = setLogLevel i
1477 makeOption TypeCase = setTypeCase True
1478 makeOption TypeInType = setTypeInType True
1479 makeOption NoCoverage = setCoverage False
1480 makeOption ErrContext = setErrContext True
1481 makeOption _ = return ()
1483 addPkgDir :: String -> Idris ()
1484 addPkgDir p = do ddir <- runIO $ getDataDir
1485 addImportDir (ddir </> p)
1486 addIBC (IBCImportDir (ddir </> p))
1488runMain :: Idris () -> IO ()
1489runMain prog = do res <- runErrorT $ execStateT prog idrisInit
1490 case res of
1491 Left err -> putStrLn $ "Uncaught error: " ++ show err
1492 Right _ -> return ()
1494execScript :: String -> Idris ()
1495execScript expr = do i <- getIState
1496 c <- colourise
1497 case parseExpr i expr of
1498 Failure err -> do iputStrLn $ show (fixColour c err)
1499 runIO $ exitWith (ExitFailure 1)
1500 Success term -> do ctxt <- getContext
1501 (tm, _) <- elabVal recinfo ERHS term
1502 res <- execute tm
1503 runIO $ exitWith ExitSuccess
1505-- | Get the platform-specific, user-specific Idris dir
1506getIdrisUserDataDir :: Idris FilePath
1507getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
1509-- | Locate the platform-specific location for the init script
1510getInitScript :: Idris FilePath
1511getInitScript = do idrisDir <- getIdrisUserDataDir
1512 return $ idrisDir </> "repl" </> "init"
1514-- | Run the initialisation script
1515initScript :: Idris ()
1516initScript = do script <- getInitScript
1517 idrisCatch (do go <- runIO $ doesFileExist script
1518 when go $ do
1519 h <- runIO $ openFile script ReadMode
1520 runInit h
1521 runIO $ hClose h)
1522 (\e -> iPrintError $ "Error reading init file: " ++ show e)
1523 where runInit :: Handle -> Idris ()
1524 runInit h = do eof <- lift . lift $ hIsEOF h
1525 ist <- getIState
1526 unless eof $ do
1527 line <- runIO $ hGetLine h
1528 script <- getInitScript
1529 c <- colourise
1530 processLine ist line script c
1531 runInit h
1532 processLine i cmd input clr =
1533 case parseCmd i input cmd of
1534 Failure err -> runIO $ print (fixColour clr err)
1535 Success Reload -> iPrintError "Init scripts cannot reload the file"
1536 Success (Load f _) -> iPrintError "Init scripts cannot load files"
1537 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1538 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1539 Success Proofs -> proofs i
1540 Success Quit -> iPrintError "Init scripts cannot quit Idris"
1541 Success cmd -> process [] cmd
1543getFile :: Opt -> Maybe String
1544getFile (Filename str) = Just str
1545getFile _ = Nothing
1547getBC :: Opt -> Maybe String
1548getBC (BCAsm str) = Just str
1549getBC _ = Nothing
1551getOutput :: Opt -> Maybe String
1552getOutput (Output str) = Just str
1553getOutput _ = Nothing
1555getIBCSubDir :: Opt -> Maybe String
1556getIBCSubDir (IBCSubDir str) = Just str
1557getIBCSubDir _ = Nothing
1559getImportDir :: Opt -> Maybe String
1560getImportDir (ImportDir str) = Just str
1561getImportDir _ = Nothing
1563getPkgDir :: Opt -> Maybe String
1564getPkgDir (Pkg str) = Just str
1565getPkgDir _ = Nothing
1567getPkg :: Opt -> Maybe (Bool, String)
1568getPkg (PkgBuild str) = Just (False, str)
1569getPkg (PkgInstall str) = Just (True, str)
1570getPkg _ = Nothing
1572getPkgClean :: Opt -> Maybe String
1573getPkgClean (PkgClean str) = Just str
1574getPkgClean _ = Nothing
1576getPkgREPL :: Opt -> Maybe String
1577getPkgREPL (PkgREPL str) = Just str
1578getPkgREPL _ = Nothing
1580getPkgCheck :: Opt -> Maybe String
1581getPkgCheck (PkgCheck str) = Just str
1582getPkgCheck _ = Nothing
1584-- | Returns None if given an Opt which is not PkgMkDoc
1585-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1586getPkgMkDoc :: Opt -- ^ Opt to extract
1587 -> Maybe String -- ^ Result
1588getPkgMkDoc (PkgMkDoc str) = Just str
1589getPkgMkDoc _ = Nothing
1591getPkgTest :: Opt -- ^ the option to extract
1592 -> Maybe String -- ^ the package file to test
1593getPkgTest (PkgTest f) = Just f
1594getPkgTest _ = Nothing
1596getCodegen :: Opt -> Maybe Codegen
1597getCodegen (UseCodegen x) = Just x
1598getCodegen _ = Nothing
1600getExecScript :: Opt -> Maybe String
1601getExecScript (InterpretScript expr) = Just expr
1602getExecScript _ = Nothing
1604getEvalExpr :: Opt -> Maybe String
1605getEvalExpr (EvalExpr expr) = Just expr
1606getEvalExpr _ = Nothing
1608getOutputTy :: Opt -> Maybe OutputType
1609getOutputTy (OutputTy t) = Just t
1610getOutputTy _ = Nothing
1612getLanguageExt :: Opt -> Maybe LanguageExt
1613getLanguageExt (Extension e) = Just e
1614getLanguageExt _ = Nothing
1616getTriple :: Opt -> Maybe String
1617getTriple (TargetTriple x) = Just x
1618getTriple _ = Nothing
1620getCPU :: Opt -> Maybe String
1621getCPU (TargetCPU x) = Just x
1622getCPU _ = Nothing
1624getOptLevel :: Opt -> Maybe Word
1625getOptLevel (OptLevel x) = Just x
1626getOptLevel _ = Nothing
1628getColour :: Opt -> Maybe Bool
1629getColour (ColourREPL b) = Just b
1630getColour _ = Nothing
1632opt :: (Opt -> Maybe a) -> [Opt] -> [a]
1633opt = mapMaybe
1635ver = showVersion version ++ gitHash
1637banner = " ____ __ _ \n" ++
1638 " / _/___/ /____(_)____ \n" ++
1639 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1640 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1641 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1642 "\n" ++
1643 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1644 "For details type :warranty."
1646warranty = "\n" ++
1647 "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1648 "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1649 "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1650 "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1651 "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1652 "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1653 "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1654 "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1655 "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1656 "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1657 "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"