@@ -4,6 +4,7 @@
44module Idris.REPL where
55
66import Idris.AbsSyntax
7+import Idris.ASTUtils
78import Idris.Apropos (apropos)
89import Idris.REPLParser
910import Idris.ElabDecls
@@ -13,6 +14,7 @@ import Idris.Error
1314import Idris.ErrReverse
1415import Idris.Delaborate
1516import Idris.Docstrings (Docstring, overview, renderDocstring)
17+import Idris.IdrisDoc
1618import Idris.Prover
1719import Idris.Parser hiding (indent)
1820import Idris.Primitives
@@ -28,6 +30,9 @@ import Idris.Inliner
2830import Idris.CaseSplit
2931import Idris.DeepSeq
3032import Idris.Output
33+import Idris.Interactive
34+import Idris.WhoCalls
35+import Idris.TypeSearch (searchByType)
3136
3237import Paths_idris
3338import Version_idris (gitHash)
@@ -77,6 +82,7 @@ import Data.List
7782import Data.Char
7883import Data.Version
7984import Data.Word (Word)
85+import Data.Either (partitionEithers)
8086import Control.DeepSeq
8187
8288import Debug.Trace
@@ -104,7 +110,7 @@ repl orig mods
104110 return ()
105111 Just input -> -- H.catch
106112 do ms <- H.catch (lift $ processInput input orig mods)
107− (ctrlC (return (Just mods)))
113+ (ctrlC (return (Just mods)))
108114 case ms of
109115 Just mods -> repl orig mods
110116 Nothing -> return ()
@@ -115,7 +121,7 @@ repl orig mods
115121 act -- repl orig mods
116122
117123 showMVs c thm [] = ""
118− showMVs c thm ms = "Metavariables: " ++
124+ showMVs c thm ms = "Metavariables: " ++
119125 show' 4 c thm (map fst ms) ++ "\n"
120126
121127 show' 0 c thm ms = let l = length ms in
@@ -123,7 +129,7 @@ repl orig mods
123129 ++ " other"
124130 ++ if l == 1 then ")" else "s)"
125131 show' n c thm [m] = showM c thm m
126− show' n c thm (m : ms) = showM c thm m ++ ", " ++
132+ show' n c thm (m : ms) = showM c thm m ++ ", " ++
127133 show' (n - 1) c thm ms
128134
129135 showM c thm n = if c then colouriseFun thm (show n)
@@ -161,8 +167,8 @@ processNetCmd orig i h fn cmd
161167 Left err -> do hPutStrLn h (show err)
162168 return (i, fn)
163169 where
164− processNet fn Reload = processNet fn (Load fn)
165− processNet fn (Load f) =
170+ processNet fn Reload = processNet fn (Load fn Nothing)
171+ processNet fn (Load f toline) =
166172 do let ist = orig { idris_options = idris_options i
167173 , idris_colourTheme = idris_colourTheme i
168174 , idris_colourRepl = False
@@ -172,7 +178,7 @@ processNetCmd orig i h fn cmd
172178 setOutH h
173179 setQuiet True
174180 setVerbose False
175− mods <- loadInputs h [f]
181+ mods <- loadInputs h [f] toline
176182 ist <- getIState
177183 return (ist, f)
178184 processNet fn c = do process h fn c
@@ -248,17 +254,22 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =
248254 IdeSlave.toSExp (map replacement compls,
249255 reverse unused)]
250256 runIO $ putStrLn $ IdeSlave.convSExp "return" good id
251−runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =
257+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =
252258 do i <- getIState
253259 clearErr
254260 putIState (orig { idris_options = idris_options i,
255261 idris_outputmode = (IdeSlave id) })
256− loadInputs stdout [filename]
262+ loadInputs stdout [filename] toline
257263 isetPrompt (mkPrompt [filename])
258264 -- Report either success or failure
259265 i <- getIState
260266 case (errSpan i) of
261− Nothing -> iPrintResult $ "loaded " ++ filename
267+ Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
268+ IdeSlave.SexpList []])
269+ (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
270+ IdeSlave.toSExp fc])
271+ (idris_parsedSpan i)
272+ in runIO . putStrLn $ IdeSlave.convSExp "return" msg id
262273 Just x -> iPrintError $ "didn't load " ++ filename
263274 ideslave orig [filename]
264275runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
@@ -272,14 +283,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
272283 [n] -> Right $ sUN n
273284 (n:ns) -> Right $ sNS (sUN n) ns
274285runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
275− case splitName name of
276− Left err -> iPrintError err
277− Right n -> process stdout "(ideslave)" (DocStr n)
278− where splitName :: String -> Either String Name
279− splitName s = case reverse $ splitOn "." s of
280− [] -> Left ("Didn't understand name '" ++ s ++ "'")
281− [n] -> Right $ sUN n
282− (n:ns) -> Right $ sNS (sUN n) ns
286+ case parseConst orig name of
287+ Success c -> process stdout "(ideslave)" (DocStr (Right c))
288+ Failure _ ->
289+ case splitName name of
290+ Left err -> iPrintError err
291+ Right n -> process stdout "(ideslave)" (DocStr (Left n))
283292runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
284293 process stdout fn (CaseSplitAt False line (sUN name))
285294runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
@@ -290,8 +299,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =
290299 process stdout fn (AddMissing False line (sUN name))
291300runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
292301 process stdout fn (MakeWith False line (sUN name))
293−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =
294− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
302+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =
303+ doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth
304+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =
305+ case splitName name of
306+ Left err -> iPrintError err
307+ Right n -> process stdout fn (MakeLemma False line n)
295308runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
296309 process stdout fn (Apropos a)
297310runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
@@ -314,37 +327,68 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
314327runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
315328 do ist <- getIState
316329 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
317− imp <- impShow
330+ let ppo = ppOptionIst ist
318331 let mvarTys = map (delabTy ist) mvs
319332 let res = (IdeSlave.SymbolAtom "ok",
320333 zipWith (\ n (prems, concl) -> (n, prems, concl))
321334 (map (IdeSlave.StringAtom . show) mvs)
322− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
335+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
323336 runIO . putStrLn $ IdeSlave.convSExp "return" res id
324337 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
325338 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
326339 in ((n, t):prems, conc)
327340 getGoal tm = ([], tm)
328− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)
341+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
329342 -> ([(String, String, SpanList OutputAnnotation)],
330343 (String, SpanList OutputAnnotation))
331− sexpGoal ist cols imp ns ([], concl) =
332− let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
333− pprintPTerm imp (zip ns (repeat False)) [] concl
344+ sexpGoal ist cols ppo ns ([], concl) =
345+ let infixes = idris_infixes ist
346+ concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
347+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
334348 in ([], concl')
335− sexpGoal ist cols imp ns ((n, t):ps, concl) =
349+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =
336350 let n' = case n of
337351 NS (UN nm) ns -> str nm
338352 UN nm | ('_':'_':_) <- str nm -> "_"
339353 | otherwise -> str nm
340354 _ -> "_"
341355 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
342− pprintPTerm imp (zip ns (repeat False)) [] t
343− rest = sexpGoal ist cols imp (n:ns) (ps, concl)
356+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
357+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
344358 in ((n', t', spans) : fst rest, snd rest)
345−
359+runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
360+ case splitName n of
361+ Left err -> iPrintError err
362+ Right n -> do calls <- whoCalls n
363+ ist <- getIState
364+ let msg = (IdeSlave.SymbolAtom "ok",
365+ map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
366+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
367+ where pn ist = displaySpans .
368+ renderPretty 0.9 1000 .
369+ fmap (fancifyAnnots ist) .
370+ prettyName True []
371+runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
372+ case splitName n of
373+ Left err -> iPrintError err
374+ Right n -> do calls <- callsWho n
375+ ist <- getIState
376+ let msg = (IdeSlave.SymbolAtom "ok",
377+ map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)
378+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
379+ where pn ist = displaySpans .
380+ renderPretty 0.9 1000 .
381+ fmap (fancifyAnnots ist) .
382+ prettyName True []
383+
384+splitName :: String -> Either String Name
385+splitName s = case reverse $ splitOn "." s of
386+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
387+ [n] -> Right $ sUN n
388+ (n:ns) -> Right $ sNS (sUN n) ns
346389
347390ideslaveProcess :: FilePath -> Command -> Idris ()
391+ideslaveProcess fn Warranty = process stdout fn Warranty
348392ideslaveProcess fn Help = process stdout fn Help
349393ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
350394 iPrintResult "changed directory to"
@@ -359,7 +403,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
359403ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
360404ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
361405 iPrintResult ""
362−ideslaveProcess fn (Info n) = process stdout fn (Info n)
363406ideslaveProcess fn (Search t) = process stdout fn (Search t)
364407ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
365408-- RmProof and AddProof not supported!
@@ -400,11 +443,13 @@ ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddPr
400443ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
401444ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
402445ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
403−ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)
446+ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)
404447ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
405448 iPrintResult ""
406449ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
407450 iPrintResult ""
451+ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)
452+ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)
408453ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
409454
410455
@@ -436,14 +481,14 @@ processInput cmd orig inputs
436481 , idris_colourTheme = idris_colourTheme i
437482 }
438483 clearErr
439− mods <- loadInputs stdout inputs
484+ mods <- loadInputs stdout inputs Nothing
440485 return (Just inputs)
441− Success (Load f) ->
486+ Success (Load f toline) ->
442487 do putIState orig { idris_options = idris_options i
443488 , idris_colourTheme = idris_colourTheme i
444489 }
445490 clearErr
446− mod <- loadInputs stdout [f]
491+ mod <- loadInputs stdout [f] toline
447492 return (Just [f])
448493 Success (ModImport f) ->
449494 do clearErr
@@ -467,7 +512,7 @@ resolveProof n'
467512 n <- case lookupNames n' ctxt of
468513 [x] -> return x
469514 [] -> return n'
470− ns -> ierror (CantResolveAlts (map show ns))
515+ ns -> ierror (CantResolveAlts ns)
471516 return n
472517
473518removeProof :: Name -> Idris ()
@@ -492,7 +537,7 @@ edit f orig
492537 putIState $ orig { idris_options = idris_options i
493538 , idris_colourTheme = idris_colourTheme i
494539 }
495− loadInputs stdout [f]
540+ loadInputs stdout [f] Nothing
496541-- clearOrigPats
497542 iucheck
498543 return ()
@@ -520,11 +565,13 @@ insertScript prf (x : xs) = x : insertScript prf xs
520565
521566process :: Handle -> FilePath -> Command -> Idris ()
522567process h fn Help = iPrintResult displayHelp
568+process h fn Warranty = iPrintResult warranty
523569process h fn (ChangeDirectory f)
524570 = do runIO $ setCurrentDirectory f
525571 return ()
526572process h fn (Eval t)
527− = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
573+ = withErrorReflection $ do logLvl 5 $ show t
574+ (tm, ty) <- elabVal toplevel False t
528575 ctxt <- getContext
529576 let tm' = force (normaliseAll ctxt [] tm)
530577 let ty' = force (normaliseAll ctxt [] ty)
@@ -533,41 +580,39 @@ process h fn (Eval t)
533580 ist <- getIState
534581 logLvl 3 $ "Raw: " ++ show (tm', ty')
535582 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
536− let imp = opt_showimp (idris_options ist)
537− tmDoc = prettyImp imp (delab ist tm')
538− tyDoc = prettyImp imp (delab ist ty')
583+ let tmDoc = prettyIst ist (delab ist tm')
584+ tyDoc = prettyIst ist (delab ist ty')
539585 ihPrintTermWithType h tmDoc tyDoc
540586
541587process h fn (ExecVal t)
542588 = do ctxt <- getContext
543589 ist <- getIState
544− let imp = opt_showimp (idris_options ist)
545590 (tm, ty) <- elabVal toplevel False t
546591-- let tm' = normaliseAll ctxt [] tm
547592 let ty' = normaliseAll ctxt [] ty
548593 res <- execute tm
549− let (resOut, tyOut) = (prettyImp imp (delab ist res),
550− prettyImp imp (delab ist ty'))
594+ let (resOut, tyOut) = (prettyIst ist (delab ist res),
595+ prettyIst ist (delab ist ty'))
551596 ihPrintTermWithType h resOut tyOut
552597
553598process h fn (Check (PRef _ n))
554599 = do ctxt <- getContext
555600 ist <- getIState
556− imp <- impShow
601+ let ppo = ppOptionIst ist
557602 case lookupNames n ctxt of
558603 ts@(t:_) ->
559604 case lookup t (idris_metavars ist) of
560605 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
561− showMetavarInfo imp ist n i
606+ showMetavarInfo ppo ist n i
562607 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
563608 [] -> ihPrintError h $ "No such variable " ++ show n
564609 where
565− showMetavarInfo imp ist n i
610+ showMetavarInfo ppo ist n i
566611 = case lookupTy n (tt_ctxt ist) of
567− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
568− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
569− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
570− putTy imp ist i bnd (PPi _ n t sc)
612+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
613+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
614+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
615+ putTy ppo ist i bnd (PPi _ n t sc)
571616 = let current = text " " <>
572617 (case n of
573618 MN _ _ -> text "_"
@@ -575,37 +620,41 @@ process h fn (Check (PRef _ n))
575620 _ -> bindingOf n False) <+>
576621 colon <+> align (tPretty bnd ist t) <> line
577622 in
578− current <> putTy imp ist (i-1) ((n,False):bnd) sc
579− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
580− putGoal imp ist bnd g
623+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc
624+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
625+ putGoal ppo ist bnd g
581626 = text "--------------------------------------" <$>
582627 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
583628 align (tPretty bnd ist g)
584629
585− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t
630+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
586631
587632
588633process h fn (Check t)
589634 = do (tm, ty) <- elabVal toplevel False t
590635 ctxt <- getContext
591636 ist <- getIState
592− let imp = opt_showimp (idris_options ist)
637+ let ppo = ppOptionIst ist
593638 ty' = normaliseC ctxt [] ty
594639 case tm of
595640 TType _ ->
596− ihPrintTermWithType h (prettyImp imp PType) type1Doc
597− _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
598− (prettyImp imp (delab ist ty))
641+ ihPrintTermWithType h (prettyIst ist PType) type1Doc
642+ _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
643+ (prettyIst ist (delab ist ty))
599644
600−process h fn (DocStr n)
601− = do i <- getIState
602− let imp = opt_showimp (idris_options i)
603− case lookupCtxtName n (idris_docstrings i) of
645+process h fn (DocStr (Left n))
646+ = do ist <- getIState
647+ case lookupCtxtName n (idris_docstrings ist) of
604648 [] -> iPrintError $ "No documentation for " ++ show n
605− ns -> do toShow <- mapM (showDoc imp) ns
649+ ns -> do toShow <- mapM (showDoc ist) ns
606650 ihRenderResult h (vsep toShow)
607− where showDoc imp (n, d) = do doc <- getDocs n
608− return $ pprintDocs imp doc
651+ where showDoc ist (n, d) = do doc <- getDocs n
652+ return $ pprintDocs ist doc
653+
654+process h fn (DocStr (Right c))
655+ = do ist <- getIState
656+ ihRenderResult h $ pprintConstDocs ist c (constDocs c)
657+
609658process h fn Universes
610659 = do i <- getIState
611660 let cs = idris_constraints i
@@ -637,8 +686,8 @@ process h fn (TotCheck n)
637686 [] -> ihPrintError h $ "Unknown operator " ++ show n
638687 ts -> do ist <- getIState
639688 c <- colourise
640− imp <- impShow
641− let showN = showName (Just ist) [] imp c
689+ let ppo = ppOptionIst ist
690+ let showN = showName (Just ist) [] ppo c
642691 ihPrintResult h . concat . intersperse "\n" .
643692 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
644693 ts
@@ -661,191 +710,21 @@ process h fn (DebugInfo n)
661710 iputStrLn $ "Size change: " ++ show sc
662711 when (not (null cg')) $ do iputStrLn "Call graph:\n"
663712 iputStrLn (show cg')
664−process h fn (Info n)
665− = do i <- getIState
666− case lookupCtxt n (idris_classes i) of
667− [c] -> do info <- classInfo c
668− ihRenderResult h info
669− _ -> iPrintError "Not a class"
670−process h fn (Search t) = iPrintError "Not implemented"
671−-- FIXME: There is far too much repetition in the cases below!
713+process h fn (Search t) = searchByType h t
672714process h fn (CaseSplitAt updatefile l n)
673− = do src <- runIO $ readFile fn
674− res <- splitOnLine l n fn
675− iLOG (showSep "\n" (map show res))
676− let (before, (ap : later)) = splitAt (l-1) (lines src)
677− res' <- replaceSplits ap res
678− let new = concat res'
679− if updatefile
680− then do let fb = fn ++ "~" -- make a backup!
681− runIO $ writeFile fb (unlines before ++ new ++ unlines later)
682− runIO $ copyFile fb fn
683− else -- do ihputStrLn h (show res)
684− ihPrintResult h new
715+ = caseSplitAt h fn updatefile l n
685716process h fn (AddClauseFrom updatefile l n)
686− = do src <- runIO $ readFile fn
687− let (before, tyline : later) = splitAt (l-1) (lines src)
688− let indent = getIndent 0 (show n) tyline
689− cl <- getClause l n fn
690− -- add clause before first blank line in 'later'
691− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
692− if updatefile
693− then do let fb = fn ++ "~"
694− runIO $ writeFile fb (unlines (before ++ nonblank) ++
695− replicate indent ' ' ++
696− cl ++ "\n" ++
697− unlines rest)
698− runIO $ copyFile fb fn
699− else ihPrintResult h cl
700− where
701− getIndent i n [] = 0
702− getIndent i n xs | take (length n) xs == n = i
703− getIndent i n (x : xs) = getIndent (i + 1) n xs
717+ = addClauseFrom h fn updatefile l n
704718process h fn (AddProofClauseFrom updatefile l n)
705− = do src <- runIO $ readFile fn
706− let (before, tyline : later) = splitAt (l-1) (lines src)
707− let indent = getIndent 0 (show n) tyline
708− cl <- getProofClause l n fn
709− -- add clause before first blank line in 'later'
710− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
711− if updatefile
712− then do let fb = fn ++ "~"
713− runIO $ writeFile fb (unlines (before ++ nonblank) ++
714− replicate indent ' ' ++
715− cl ++ "\n" ++
716− unlines rest)
717− runIO $ copyFile fb fn
718− else ihPrintResult h cl
719− where
720− getIndent i n [] = 0
721− getIndent i n xs | take (length n) xs == n = i
722− getIndent i n (x : xs) = getIndent (i + 1) n xs
719+ = addProofClauseFrom h fn updatefile l n
723720process h fn (AddMissing updatefile l n)
724− = do src <- runIO $ readFile fn
725− let (before, tyline : later) = splitAt (l-1) (lines src)
726− let indent = getIndent 0 (show n) tyline
727− i <- getIState
728− cl <- getInternalApp fn l
729− let n' = getAppName cl
730−
731− extras <- case lookupCtxt n' (idris_patdefs i) of
732− [] -> return ""
733− [(_, tms)] -> do tms' <- nameMissing tms
734− showNew (show n ++ "_rhs") 1 indent tms'
735− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
736− if updatefile
737− then do let fb = fn ++ "~"
738− runIO $ writeFile fb (unlines (before ++ nonblank)
739− ++ extras ++ unlines rest)
740− runIO $ copyFile fb fn
741− else ihPrintResult h extras
742− where showPat = show . stripNS
743− stripNS tm = mapPT dens tm where
744− dens (PRef fc n) = PRef fc (nsroot n)
745− dens t = t
746−
747− nsroot (NS n _) = nsroot n
748− nsroot (SN (WhereN _ _ n)) = nsroot n
749− nsroot n = n
750−
751− getAppName (PApp _ r _) = getAppName r
752− getAppName (PRef _ r) = r
753− getAppName _ = n
754−
755− showNew nm i ind (tm : tms)
756− = do (nm', i') <- getUniq nm i
757− rest <- showNew nm i' ind tms
758− return (replicate ind ' ' ++
759− showPat tm ++ " = ?" ++ nm' ++
760− "\n" ++ rest)
761− showNew nm i _ [] = return ""
762−
763− getIndent i n [] = 0
764− getIndent i n xs | take (length n) xs == n = i
765− getIndent i n (x : xs) = getIndent (i + 1) n xs
766−
721+ = addMissing h fn updatefile l n
767722process h fn (MakeWith updatefile l n)
768− = do src <- runIO $ readFile fn
769− let (before, tyline : later) = splitAt (l-1) (lines src)
770− let ind = getIndent tyline
771− let with = mkWith tyline n
772− -- add clause before first blank line in 'later',
773− -- or (TODO) before first line with same indentation as tyline
774− let (nonblank, rest) = span (\x -> not (all isSpace x) &&
775− not (ind == getIndent x)) later
776− if updatefile then
777− do let fb = fn ++ "~"
778− runIO $ writeFile fb (unlines (before ++ nonblank)
779− ++ with ++ "\n" ++
780− unlines rest)
781− runIO $ copyFile fb fn
782− else ihPrintResult h with
783− where getIndent s = length (takeWhile isSpace s)
784−
785−process h fn (DoProofSearch updatefile l n hints)
786− = do src <- runIO $ readFile fn
787− let (before, tyline : later) = splitAt (l-1) (lines src)
788− ctxt <- getContext
789− mn <- case lookupNames n ctxt of
790− [x] -> return x
791− [] -> return n
792− ns -> ierror (CantResolveAlts (map show ns))
793− i <- getIState
794− let (top, envlen, _) = case lookup mn (idris_metavars i) of
795− Just (t, e, False) -> (t, e, False)
796− _ -> (Nothing, 0, True)
797− let fc = fileFC fn
798− let body t = PProof [Try (TSeq Intros (ProofSearch t hints))
799− (ProofSearch t hints)]
800− let def = PClause fc mn (PRef fc mn) [] (body top) []
801− newmv <- idrisCatch
802− (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
803− (tm, ty) <- elabVal toplevel False (PRef fc mn)
804− ctxt <- getContext
805− i <- getIState
806− return $ show (stripNS
807− (dropCtxt envlen
808− (delab i (specialise ctxt [] [(mn, 1)] tm)))))
809− (\e -> return ("?" ++ show n))
810− if updatefile then
811− do let fb = fn ++ "~"
812− runIO $ writeFile fb (unlines before ++
813− updateMeta False tyline (show n) newmv ++ "\n"
814− ++ unlines later)
815− runIO $ copyFile fb fn
816− else ihPrintResult h newmv
817− where dropCtxt 0 sc = sc
818− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
819− dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
820− dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
821− dropCtxt _ t = t
822−
823− stripNS tm = mapPT dens tm where
824− dens (PRef fc n) = PRef fc (nsroot n)
825− dens t = t
826−
827− nsroot (NS n _) = nsroot n
828− nsroot (SN (WhereN _ _ n)) = nsroot n
829− nsroot n = n
830−
831− updateMeta brack ('?':cs) n new
832− | length cs >= length n
833− = case splitAt (length n) cs of
834− (mv, c:cs) ->
835− if ((isSpace c || c == ')' || c == '}') && mv == n)
836− then addBracket brack new ++ (c : cs)
837− else '?' : mv ++ c : updateMeta True cs n new
838− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
839− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
840− updateMeta brack (c:cs) n new
841− = c : updateMeta (brack || not (isSpace c)) cs n new
842− updateMeta brack [] n new = ""
843−
844− addBracket False new = new
845− addBracket True new@('(':xs) | last xs == ')' = new
846− addBracket True new | any isSpace new = '(' : new ++ ")"
847− | otherwise = new
848−
723+ = makeWith h fn updatefile l n
724+process h fn (MakeLemma updatefile l n)
725+ = makeLemma h fn updatefile l n
726+process h fn (DoProofSearch updatefile rec l n hints)
727+ = doProofSearch h fn updatefile rec l n hints Nothing
849728process h fn (Spec t)
850729 = do (tm, ty) <- elabVal toplevel False t
851730 ctxt <- getContext
@@ -871,14 +750,15 @@ process h fn (RmProof n')
871750
872751process h fn' (AddProof prf)
873752 = do fn <- do
874− ex <- runIO $ doesFileExist fn'
875− let fnExt = fn' <.> "idr"
753+ let fn'' = takeWhile (/= ' ') fn'
754+ ex <- runIO $ doesFileExist fn''
755+ let fnExt = fn'' <.> "idr"
876756 exExt <- runIO $ doesFileExist fnExt
877757 if ex
878− then return fn'
758+ then return fn''
879759 else if exExt
880760 then return fnExt
881− else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
761+ else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
882762 let fb = fn ++ "~"
883763 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
884764 prog <- runIO $ readFile fb
@@ -915,13 +795,14 @@ process h fn (Prove n')
915795 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
916796 [(n, (_,_,False))] -> return n
917797 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
918− ns -> ierror (CantResolveAlts (map show ns))
798+ ns -> ierror (CantResolveAlts (map fst ns))
919799 prover (lit fn) n
920800 -- recheck totality
921801 i <- getIState
922802 totcheck (fileFC "(input)", n)
923803 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
924804 mapM_ checkDeclTotality (idris_totcheck i)
805+ warnTotality
925806
926807process h fn (HNF t)
927808 = do (tm, ty) <- elabVal toplevel False t
@@ -934,23 +815,25 @@ process h fn (TestInline t)
934815 ctxt <- getContext
935816 ist <- getIState
936817 let tm' = inlineTerm ist tm
937− imp <- impShow
938818 c <- colourise
939819 iPrintResult (showTm ist (delab ist tm'))
940820process h fn Execute
941− = do ist <- getIState
942− (m, _) <- elabVal toplevel False
943− (PApp fc
944− (PRef fc (sUN "run__IO"))
945− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
946− (tmpn, tmph) <- runIO tempfile
947− runIO $ hClose tmph
948− t <- codegen
949− compile t tmpn m
950− case idris_outputmode ist of
951− RawOutput -> do runIO $ system tmpn
952− return ()
953− IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n
821+ = idrisCatch
822+ (do ist <- getIState
823+ (m, _) <- elabVal toplevel False
824+ (PApp fc
825+ (PRef fc (sUN "run__IO"))
826+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
827+ (tmpn, tmph) <- runIO tempfile
828+ runIO $ hClose tmph
829+ t <- codegen
830+ compile t tmpn m
831+ case idris_outputmode ist of
832+ RawOutput -> do runIO $ system tmpn
833+ return ()
834+ IdeSlave n -> runIO . hPutStrLn h $
835+ IdeSlave.convSExp "run-program" tmpn n)
836+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
954837 where fc = fileFC "main"
955838process h fn (Compile codegen f)
956839 = do (m, _) <- elabVal toplevel False
@@ -968,7 +851,7 @@ process h fn (Missing n)
968851 = do i <- getIState
969852 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
970853 case lookupCtxt n (idris_patdefs i) of
971− [] -> return ()
854+ [] -> ihPrintError h $ "Unknown operator " ++ show n
972855 [(_, tms)] ->
973856 iPrintResult (showSep "\n" (map (showTm i') tms))
974857 _ -> iPrintError $ "Ambiguous name"
@@ -1007,6 +890,10 @@ process h fn (SetOpt ShowOrigErr) = setShowOrigErr True
1007890process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1008891process h fn (SetOpt AutoSolve) = setAutoSolve True
1009892process h fn (UnsetOpt AutoSolve) = setAutoSolve False
893+process h fn (SetOpt NoBanner) = setNoBanner True
894+process h fn (UnsetOpt NoBanner) = setNoBanner False
895+process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
896+process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1010897
1011898process h fn (SetOpt _) = iPrintError "Not a valid option"
1012899process h fn (UnsetOpt _) = iPrintError "Not a valid option"
@@ -1019,52 +906,54 @@ process h fn ColourOff
1019906 putIState $ ist { idris_colourRepl = False }
1020907process h fn ListErrorHandlers =
1021908 do ist <- getIState
1022− case idris_errorhandlers ist of
1023− [] -> iPrintResult "No registered error handlers"
1024− handlers ->
1025− iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
909+ iPrintResult $ case idris_errorhandlers ist of
910+ [] -> "No registered error handlers"
911+ handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1026912process h fn (SetConsoleWidth w) = setWidth w
1027913
1028914process h fn (Apropos a) =
1029915 do ist <- getIState
1030− let impl = opt_showimp (idris_options ist)
1031916 let names = apropos ist (T.pack a)
1032917 let aproposInfo = [ (n,
1033918 delabTy ist n,
1034919 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1035920 | n <- sort names, isUN n ]
1036− ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)
1037− where renderApropos impl (name, ty, docs) =
1038− prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>
1039− fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1040− isUN (UN _) = True
921+ ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)
922+ where isUN (UN _) = True
1041923 isUN (NS n _) = isUN n
1042924 isUN _ = False
1043925
1044−classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
1045−classInfo ci = do ist <- getIState
1046− ctxt <- getContext
1047− return $
1048− text "Parameters:" <+>
1049− hsep (punctuate comma (map (prettyName False params') params)) <>
1050− line <> line <>
1051− text "Methods:" <> line <>
1052− indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>
1053− text "Default superclass instances:" <>
1054− line <>
1055− indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>
1056− line <>
1057− text "Instances:" <> line <>
1058− indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))
1059− where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
1060− dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
1061− dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
1062− dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
1063− dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
1064− dumpInstance ist ctxt n = pp ist $ delabTy ist n
1065− params = class_params ci
1066− params' = zip params (repeat False)
1067− pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []
926+process h fn (WhoCalls n) =
927+ do calls <- whoCalls n
928+ ist <- getIState
929+ ihRenderResult h . vsep $
930+ map (\(n, ns) ->
931+ text "Callers of" <+> prettyName True [] n <$>
932+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
933+ calls
934+
935+process h fn (CallsWho n) =
936+ do calls <- callsWho n
937+ ist <- getIState
938+ ihRenderResult h . vsep $
939+ map (\(n, ns) ->
940+ prettyName True [] n <+> text "calls:" <$>
941+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
942+ calls
943+-- IdrisDoc
944+process h fn (MakeDoc s) =
945+ do istate <- getIState
946+ let names = words s
947+ parse n | Success x <- runparser name istate fn n = Right x
948+ parse n = Left n
949+ (bad, nss) = partitionEithers $ map parse names
950+ cd <- runIO $ getCurrentDirectory
951+ let outputDir = cd </> "doc"
952+ result <- if null bad then runIO $ generateDocs istate nss outputDir
953+ else return . Left $ "Illegal name: " ++ head bad
954+ case result of Right _ -> iputStrLn "IdrisDoc generated"
955+ Left err -> iPrintError err
956+
1068957
1069958showTotal :: Totality -> IState -> String
1070959showTotal t@(Partial (Other ns)) i
@@ -1084,80 +973,6 @@ displayHelp = let vstr = showVersion version in
1084973 l ++ take (c1 - length l) (repeat ' ') ++
1085974 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
1086975
1087−parseCodegen :: String -> Codegen
1088−parseCodegen "C" = ViaC
1089−parseCodegen "Java" = ViaJava
1090−parseCodegen "bytecode" = Bytecode
1091−parseCodegen "javascript" = ViaJavaScript
1092−parseCodegen "node" = ViaNode
1093−parseCodegen "llvm" = ViaLLVM
1094−parseCodegen _ = error "unknown codegen" -- FIXME: partial function
1095−
1096−parseArgs :: [String] -> [Opt]
1097−parseArgs [] = []
1098−parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)
1099−parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
1100−parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
1101−parseArgs ("--client":ns) = [Client (showSep " " ns)]
1102−parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
1103−parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)
1104−parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
1105−parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)
1106−parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
1107−parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
1108−parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
1109−parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
1110−parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
1111−parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
1112−parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
1113−parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)
1114−parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
1115−parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
1116−parseArgs ("--help":ns) = Usage : (parseArgs ns)
1117−parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)
1118−parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)
1119−parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)
1120−parseArgs ("--version":ns) = Ver : (parseArgs ns)
1121−parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)
1122−parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)
1123−parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)
1124−parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)
1125−-- Package Related options
1126−parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
1127−parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1128−parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1129−parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1130−parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)
1131−parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1132−parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)
1133−-- Misc Options
1134−parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)
1135−parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)
1136−parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)
1137−parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)
1138−parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)
1139−parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
1140−parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)
1141−parseArgs ["--exec"] = InterpretScript "Main.main" : []
1142−parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns
1143−parseArgs (('-':'X':extName):ns) = case maybeRead extName of
1144− Just ext -> Extension ext : parseArgs ns
1145− -- Not sure what to do for the Nothing case
1146− Nothing -> error ("Unknown extension " ++ extName)
1147− where maybeRead = fmap fst . listToMaybe . reads
1148−parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns
1149−parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns
1150−parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns
1151−parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns
1152−parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns
1153−parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns
1154−parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns
1155−parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns
1156−parseArgs ("--color":ns) = ColourREPL True : parseArgs ns
1157−parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns
1158−parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns
1159−parseArgs (n:ns) = Filename n : (parseArgs ns)
1160−
1161976helphead =
1162977 [ (["Command"], SpecialHeaderArg, "Purpose"),
1163978 ([""], NoArg, "")
@@ -1169,17 +984,22 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
1169984 historyFile = hFile
1170985 }
1171986
1172−-- invoke as if from command line
987+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1173988idris :: [Opt] -> IO (Maybe IState)
1174−idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
989+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
1175990 case res of
1176991 Left err -> do putStrLn $ pshow idrisInit err
1177992 return Nothing
1178993 Right ist -> return (Just ist)
994+ where totalMain = do idrisMain opts
995+ ist <- getIState
996+ case idris_totcheckfail ist of
997+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
998+ [] -> return ()
1179999
11801000
1181−loadInputs :: Handle -> [FilePath] -> Idris ()
1182−loadInputs h inputs
1001+loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()
1002+loadInputs h inputs toline -- furthest line to read in input source files
11831003 = idrisCatch
11841004 (do ist <- getIState
11851005 -- if we're in --check and not outputting anything, don't bother
@@ -1204,14 +1024,13 @@ loadInputs h inputs
12041024 let ifiles = getModuleFiles modTree
12051025 iLOG ("MODULE TREE : " ++ show modTree)
12061026 iLOG ("RELOAD: " ++ show ifiles)
1207− when (not (all ibc ifiles) || loadCode) $
1027+ when (not (all ibc ifiles) || loadCode) $
12081028 tryLoad False (filter (not . ibc) ifiles)
12091029 -- return the files that need rechecking
1210− return ifiles)
1030+ return ifiles)
12111031 ninputs
12121032 inew <- getIState
12131033 let tidata = idris_tyinfodata inew
1214− let lineapps = idris_lineapps inew
12151034 let patdefs = idris_patdefs inew
12161035 -- If it worked, load the whole thing from all the ibcs together
12171036 case errSpan inew of
@@ -1222,38 +1041,56 @@ loadInputs h inputs
12221041 _ -> return ()
12231042 ist <- getIState
12241043 putIState (ist { idris_tyinfodata = tidata,
1225− idris_lineapps = lineapps,
1226− idris_patdefs = patdefs }))
1044+ idris_patdefs = patdefs })
1045+
1046+ case opt getOutput opts of
1047+ [] -> performUsageAnalysis -- interactive
1048+ _ -> return [] -- batch, will be checked by the compiler
1049+
1050+ return ())
12271051 (\e -> do i <- getIState
12281052 case e of
1229− At f _ -> do setErrSpan f
1230− ihRenderError stdout $ pprintErr i e
1053+ At f e' -> do setErrSpan f
1054+ ihWarn stdout f $ pprintErr i e'
12311055 ProgramLineComment -> return () -- fail elsewhere
12321056 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1233− iputStrLn (pshow i e))
1057+ ihWarn stdout emptyFC $ pprintErr i e)
12341058 where -- load all files, stop if any fail
12351059 tryLoad :: Bool -> [IFileType] -> Idris ()
1236− tryLoad keepstate [] = return ()
1237− tryLoad keepstate (f : fs)
1060+ tryLoad keepstate [] = warnTotality >> return ()
1061+ tryLoad keepstate (f : fs)
12381062 = do ist <- getIState
1239− loadFromIFile h f
1063+ let maxline
1064+ = case toline of
1065+ Nothing -> Nothing
1066+ Just l -> case f of
1067+ IDR fn -> if any (fmatch fn) inputs
1068+ then Just l
1069+ else Nothing
1070+ LIDR fn -> if any (fmatch fn) inputs
1071+ then Just l
1072+ else Nothing
1073+ _ -> Nothing
1074+ loadFromIFile h f maxline
12401075 inew <- getIState
12411076 -- FIXME: Save these in IBC to avoid this hack! Need to
12421077 -- preserve it all from source inputs
12431078 let tidata = idris_tyinfodata inew
1244− let lineapps = idris_lineapps inew
12451079 let patdefs = idris_patdefs inew
12461080 ok <- noErrors
12471081 when ok $ do when (not keepstate) $ putIState ist
12481082 ist <- getIState
12491083 putIState (ist { idris_tyinfodata = tidata,
1250− idris_lineapps = lineapps,
12511084 idris_patdefs = patdefs })
12521085 tryLoad keepstate fs
12531086
12541087 ibc (IBC _ _) = True
12551088 ibc _ = False
12561089
1090+ fmatch ('.':'/':xs) ys = fmatch xs ys
1091+ fmatch xs ('.':'/':ys) = fmatch xs ys
1092+ fmatch xs ys = xs == ys
1093+
12571094 findNewIBC :: IFileType -> Idris (Maybe IFileType)
12581095 findNewIBC i@(IBC _ _) = return (Just i)
12591096 findNewIBC s@(IDR f) = do ist <- get
@@ -1310,17 +1147,20 @@ idrisMain opts =
13101147 x:y:xs -> do iputStrLn "More than one interpreter expression found."
13111148 runIO $ exitWith (ExitFailure 1)
13121149 [expr] -> return (Just expr)
1150+ let immediate = opt getEvalExpr opts
1151+
13131152 when (DefaultTotal `elem` opts) $ do i <- getIState
13141153 putIState (i { default_total = True })
13151154 setColourise $ not quiet && last (True : opt getColour opts)
13161155 when (not runrepl) $ setWidth InfinitelyWide
13171156 mapM_ addLangExt (opt getLanguageExt opts)
13181157 setREPL runrepl
1319− setQuiet (quiet || isJust script)
1158+ setQuiet (quiet || isJust script || not (null immediate))
13201159 setIdeSlave idesl
13211160 setVerbose verbose
13221161 setCmdLine opts
13231162 setOutputTy outty
1163+ setNoBanner nobanner
13241164 setCodegen cgn
13251165 setTargetTriple trpl
13261166 setTargetCPU tcpu
@@ -1335,6 +1175,8 @@ idrisMain opts =
13351175 (d:_) -> setIBCSubDir d
13361176 setImportDirs importdirs
13371177
1178+ setNoBanner nobanner
1179+
13381180 when (not (NoBasePkgs `elem` opts)) $ do
13391181 addPkgDir "prelude"
13401182 addPkgDir "base"
@@ -1344,22 +1186,43 @@ idrisMain opts =
13441186 return ()
13451187 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
13461188 return ()
1347− when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner
1189+
1190+ when (runrepl && not idesl) initScript
1191+
1192+ nobanner <- getNoBanner
1193+
1194+ when (runrepl &&
1195+ not quiet &&
1196+ not idesl &&
1197+ not (isJust script) &&
1198+ not nobanner &&
1199+ null immediate) $
1200+ iputStrLn banner
13481201
13491202 orig <- getIState
1350− loadInputs stdout inputs
1203+ loadInputs stdout inputs Nothing
13511204
13521205 runIO $ hSetBuffering stdout LineBuffering
13531206
13541207 ok <- noErrors
13551208 when ok $ case output of
1356− -- just do the checks
1357− [] -> performUsageAnalysis >> return ()
1358−
1359− -- the compiler will run usage analysis itself
1209+ [] -> return ()
13601210 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
13611211 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
13621212
1213+ case immediate of
1214+ [] -> return ()
1215+ exprs -> do setWidth InfinitelyWide
1216+ mapM_ (\str -> do ist <- getIState
1217+ c <- colourise
1218+ case parseExpr ist str of
1219+ Failure err -> do iputStrLn $ show (fixColour c err)
1220+ runIO $ exitWith (ExitFailure 1)
1221+ Success e -> process stdout "" (Eval e))
1222+ exprs
1223+ runIO $ exitWith ExitSuccess
1224+
1225+
13631226 case script of
13641227 Nothing -> return ()
13651228 Just expr -> execScript expr
@@ -1375,7 +1238,6 @@ idrisMain opts =
13751238
13761239 when (runrepl && not idesl) $ do
13771240-- clearOrigPats
1378− initScript
13791241 startServer orig inputs
13801242 runInputT (replSettings (Just historyFile)) $ repl orig inputs
13811243 when (idesl) $ ideslaveStart orig inputs
@@ -1435,7 +1297,7 @@ initScript = do script <- getInitScript
14351297 case parseCmd i input cmd of
14361298 Failure err -> runIO $ print (fixColour clr err)
14371299 Success Reload -> iPrintError "Init scripts cannot reload the file"
1438− Success (Load f) -> iPrintError "Init scripts cannot load files"
1300+ Success (Load f _) -> iPrintError "Init scripts cannot load files"
14391301 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
14401302 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
14411303 Success Proofs -> proofs i
@@ -1483,6 +1345,18 @@ getPkgCheck :: Opt -> Maybe String
14831345getPkgCheck (PkgCheck str) = Just str
14841346getPkgCheck _ = Nothing
14851347
1348+-- | Returns None if given an Opt which is not PkgMkDoc
1349+-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1350+getPkgMkDoc :: Opt -- ^ Opt to extract
1351+ -> Maybe String -- ^ Result
1352+getPkgMkDoc (PkgMkDoc str) = Just str
1353+getPkgMkDoc _ = Nothing
1354+
1355+getPkgTest :: Opt -- ^ the option to extract
1356+ -> Maybe String -- ^ the package file to test
1357+getPkgTest (PkgTest f) = Just f
1358+getPkgTest _ = Nothing
1359+
14861360getCodegen :: Opt -> Maybe Codegen
14871361getCodegen (UseCodegen x) = Just x
14881362getCodegen _ = Nothing
@@ -1491,6 +1365,10 @@ getExecScript :: Opt -> Maybe String
14911365getExecScript (InterpretScript expr) = Just expr
14921366getExecScript _ = Nothing
14931367
1368+getEvalExpr :: Opt -> Maybe String
1369+getEvalExpr (EvalExpr expr) = Just expr
1370+getEvalExpr _ = Nothing
1371+
14941372getOutputTy :: Opt -> Maybe OutputType
14951373getOutputTy (OutputTy t) = Just t
14961374getOutputTy _ = Nothing
@@ -1524,6 +1402,20 @@ banner = " ____ __ _ \n" ++
15241402 " / _/___/ /____(_)____ \n" ++
15251403 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
15261404 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1527− " /___/\\__,_/_/ /_/____/ Type :? for help \n"
1528−
1529−
1405+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1406+ "\n" ++
1407+ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1408+ "For details type :warranty."
1409+
1410+warranty = "\n" ++
1411+ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
1412+ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
1413+ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
1414+ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
1415+ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
1416+ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
1417+ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
1418+ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
1419+ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
1420+ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
1421+ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"