@@ -4,6 +4,7 @@
4module Idris.REPL where
4module Idris.REPL where
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7import Idris.Apropos (apropos)
8import Idris.Apropos (apropos)
8import Idris.REPLParser
9import Idris.REPLParser
9import Idris.ElabDecls
10import Idris.ElabDecls
@@ -13,6 +14,7 @@ import Idris.Error
13import Idris.ErrReverse
14import Idris.ErrReverse
14import Idris.Delaborate
15import Idris.Delaborate
15import Idris.Docstrings (Docstring, overview, renderDocstring)
16import Idris.Docstrings (Docstring, overview, renderDocstring)
16import Idris.Prover
18import Idris.Prover
17import Idris.Parser hiding (indent)
19import Idris.Parser hiding (indent)
18import Idris.Primitives
20import Idris.Primitives
@@ -28,6 +30,9 @@ import Idris.Inliner
28import Idris.CaseSplit
30import Idris.CaseSplit
29import Idris.DeepSeq
31import Idris.DeepSeq
30import Idris.Output
32import Idris.Output
33+import Idris.Interactive
35+import Idris.TypeSearch (searchByType)
32import Paths_idris
37import Paths_idris
33import Version_idris (gitHash)
38import Version_idris (gitHash)
@@ -77,6 +82,7 @@ import Data.List
77import Data.Char
82import Data.Char
78import Data.Version
83import Data.Version
79import Data.Word (Word)
84import Data.Word (Word)
85+import Data.Either (partitionEithers)
80import Control.DeepSeq
86import Control.DeepSeq
82import Debug.Trace
88import Debug.Trace
@@ -104,7 +110,7 @@ repl orig mods
104 return ()
110 return ()
105 Just input -> -- H.catch
111 Just input -> -- H.catch
106 do ms <- H.catch (lift $ processInput input orig mods)
112 do ms <- H.catch (lift $ processInput input orig mods)
107− (ctrlC (return (Just mods)))
113+ (ctrlC (return (Just mods)))
108 case ms of
114 case ms of
109 Just mods -> repl orig mods
115 Just mods -> repl orig mods
110 Nothing -> return ()
116 Nothing -> return ()
@@ -115,7 +121,7 @@ repl orig mods
115 act -- repl orig mods
121 act -- repl orig mods
117 showMVs c thm [] = ""
123 showMVs c thm [] = ""
118− showMVs c thm ms = "Metavariables: " ++
124+ showMVs c thm ms = "Metavariables: " ++
119 show' 4 c thm (map fst ms) ++ "\n"
125 show' 4 c thm (map fst ms) ++ "\n"
121 show' 0 c thm ms = let l = length ms in
127 show' 0 c thm ms = let l = length ms in
@@ -123,7 +129,7 @@ repl orig mods
123 ++ " other"
129 ++ " other"
124 ++ if l == 1 then ")" else "s)"
130 ++ if l == 1 then ")" else "s)"
125 show' n c thm [m] = showM c thm m
131 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 ++ ", " ++
127 show' (n - 1) c thm ms
133 show' (n - 1) c thm ms
129 showM c thm n = if c then colouriseFun thm (show n)
135 showM c thm n = if c then colouriseFun thm (show n)
@@ -161,8 +167,8 @@ processNetCmd orig i h fn cmd
161 Left err -> do hPutStrLn h (show err)
167 Left err -> do hPutStrLn h (show err)
162 return (i, fn)
168 return (i, fn)
164− processNet fn Reload = processNet fn (Load fn)
170+ processNet fn Reload = processNet fn (Load fn Nothing)
165− processNet fn (Load f) =
171+ processNet fn (Load f toline) =
166 do let ist = orig { idris_options = idris_options i
172 do let ist = orig { idris_options = idris_options i
167 , idris_colourTheme = idris_colourTheme i
173 , idris_colourTheme = idris_colourTheme i
168 , idris_colourRepl = False
174 , idris_colourRepl = False
@@ -172,7 +178,7 @@ processNetCmd orig i h fn cmd
172 setOutH h
178 setOutH h
173 setQuiet True
179 setQuiet True
174 setVerbose False
180 setVerbose False
175− mods <- loadInputs h [f]
181+ mods <- loadInputs h [f] toline
176 ist <- getIState
182 ist <- getIState
177 return (ist, f)
183 return (ist, f)
178 processNet fn c = do process h fn c
184 processNet fn c = do process h fn c
@@ -248,17 +254,22 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =
248 IdeSlave.toSExp (map replacement compls,
254 IdeSlave.toSExp (map replacement compls,
249 reverse unused)]
255 reverse unused)]
250 runIO $ putStrLn $ IdeSlave.convSExp "return" good id
256 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) =
252 do i <- getIState
258 do i <- getIState
254 putIState (orig { idris_options = idris_options i,
260 putIState (orig { idris_options = idris_options i,
255 idris_outputmode = (IdeSlave id) })
261 idris_outputmode = (IdeSlave id) })
256− loadInputs stdout [filename]
262+ loadInputs stdout [filename] toline
257 isetPrompt (mkPrompt [filename])
263 isetPrompt (mkPrompt [filename])
258 -- Report either success or failure
264 -- Report either success or failure
259 i <- getIState
265 i <- getIState
260 case (errSpan i) of
266 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
262 Just x -> iPrintError $ "didn't load " ++ filename
273 Just x -> iPrintError $ "didn't load " ++ filename
263 ideslave orig [filename]
274 ideslave orig [filename]
264runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
275runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
@@ -272,14 +283,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
272 [n] -> Right $ sUN n
283 [n] -> Right $ sUN n
273 (n:ns) -> Right $ sNS (sUN n) ns
284 (n:ns) -> Right $ sNS (sUN n) ns
274runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
285runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
275− case splitName name of
286+ case parseConst orig name of
287+ Success c -> process stdout "(ideslave)" (DocStr (Right c))
289+ case splitName name of
276− Left err -> iPrintError err
290+ Left err -> iPrintError err
277− Right n -> process stdout "(ideslave)" (DocStr n)
291+ Right n -> process stdout "(ideslave)" (DocStr (Left n))
278− where splitName :: String -> Either String Name
279− splitName s = case reverse $ splitOn "." s of
280− [] -> Left ("Didn't understand name '" ++ s ++ "'")
281− [n] -> Right $ sUN n
282− (n:ns) -> Right $ sNS (sUN n) ns
283runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
292runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
284 process stdout fn (CaseSplitAt False line (sUN name))
293 process stdout fn (CaseSplitAt False line (sUN name))
285runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
294runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
@@ -290,8 +299,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =
290 process stdout fn (AddMissing False line (sUN name))
299 process stdout fn (AddMissing False line (sUN name))
291runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
300runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
292 process stdout fn (MakeWith False line (sUN name))
301 process stdout fn (MakeWith False line (sUN name))
293−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =
302+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =
294− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
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)
295runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
308runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
296 process stdout fn (Apropos a)
309 process stdout fn (Apropos a)
297runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
310runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
@@ -314,37 +327,68 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
314runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
327runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
315 do ist <- getIState
328 do ist <- getIState
316 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
329 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
317− imp <- impShow
330+ let ppo = ppOptionIst ist
318 let mvarTys = map (delabTy ist) mvs
331 let mvarTys = map (delabTy ist) mvs
319 let res = (IdeSlave.SymbolAtom "ok",
332 let res = (IdeSlave.SymbolAtom "ok",
320 zipWith (\ n (prems, concl) -> (n, prems, concl))
333 zipWith (\ n (prems, concl) -> (n, prems, concl))
321 (map (IdeSlave.StringAtom . show) mvs)
334 (map (IdeSlave.StringAtom . show) mvs)
322− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
335+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
323 runIO . putStrLn $ IdeSlave.convSExp "return" res id
336 runIO . putStrLn $ IdeSlave.convSExp "return" res id
324 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
337 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
325 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
338 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
326 in ((n, t):prems, conc)
339 in ((n, t):prems, conc)
327 getGoal tm = ([], tm)
340 getGoal tm = ([], tm)
328− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)
341+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
329 -> ([(String, String, SpanList OutputAnnotation)],
342 -> ([(String, String, SpanList OutputAnnotation)],
330 (String, SpanList OutputAnnotation))
343 (String, SpanList OutputAnnotation))
331− sexpGoal ist cols imp ns ([], concl) =
344+ sexpGoal ist cols ppo ns ([], concl) =
345+ let infixes = idris_infixes ist
332− let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
346+ concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
333− pprintPTerm imp (zip ns (repeat False)) [] concl
347+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
334 in ([], concl')
348 in ([], concl')
335− sexpGoal ist cols imp ns ((n, t):ps, concl) =
349+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =
336 let n' = case n of
350 let n' = case n of
337 NS (UN nm) ns -> str nm
351 NS (UN nm) ns -> str nm
338 UN nm | ('_':'_':_) <- str nm -> "_"
352 UN nm | ('_':'_':_) <- str nm -> "_"
339 | otherwise -> str nm
353 | otherwise -> str nm
341 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
355 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
342− pprintPTerm imp (zip ns (repeat False)) [] t
356+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
343− rest = sexpGoal ist cols imp (n:ns) (ps, concl)
357+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
344 in ((n', t', spans) : fst rest, snd rest)
358 in ((n', t', spans) : fst rest, snd rest)
345−
359+runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
361+ Left err -> iPrintError err
362+ Right n -> do calls <- whoCalls n
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) .
371+runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
373+ Left err -> iPrintError err
374+ Right n -> do calls <- callsWho n
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) .
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
347ideslaveProcess :: FilePath -> Command -> Idris ()
390ideslaveProcess :: FilePath -> Command -> Idris ()
391+ideslaveProcess fn Warranty = process stdout fn Warranty
348ideslaveProcess fn Help = process stdout fn Help
392ideslaveProcess fn Help = process stdout fn Help
349ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
393ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)
350 iPrintResult "changed directory to"
394 iPrintResult "changed directory to"
@@ -359,7 +403,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
359ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
403ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
360ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
404ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
361 iPrintResult ""
405 iPrintResult ""
362−ideslaveProcess fn (Info n) = process stdout fn (Info n)
363ideslaveProcess fn (Search t) = process stdout fn (Search t)
406ideslaveProcess fn (Search t) = process stdout fn (Search t)
364ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
407ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
365-- RmProof and AddProof not supported!
408-- RmProof and AddProof not supported!
@@ -400,11 +443,13 @@ ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddPr
400ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
443ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)
401ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
444ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)
402ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)
445ideslaveProcess 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)
404ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
447ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)
405 iPrintResult ""
448 iPrintResult ""
406ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
449ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)
407 iPrintResult ""
450 iPrintResult ""
451+ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)
452+ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)
408ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
453ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
@@ -436,14 +481,14 @@ processInput cmd orig inputs
436 , idris_colourTheme = idris_colourTheme i
481 , idris_colourTheme = idris_colourTheme i
439− mods <- loadInputs stdout inputs
484+ mods <- loadInputs stdout inputs Nothing
440 return (Just inputs)
485 return (Just inputs)
441− Success (Load f) ->
486+ Success (Load f toline) ->
442 do putIState orig { idris_options = idris_options i
487 do putIState orig { idris_options = idris_options i
443 , idris_colourTheme = idris_colourTheme i
488 , idris_colourTheme = idris_colourTheme i
446− mod <- loadInputs stdout [f]
491+ mod <- loadInputs stdout [f] toline
447 return (Just [f])
492 return (Just [f])
448 Success (ModImport f) ->
493 Success (ModImport f) ->
449 do clearErr
494 do clearErr
@@ -467,7 +512,7 @@ resolveProof n'
467 n <- case lookupNames n' ctxt of
512 n <- case lookupNames n' ctxt of
468 [x] -> return x
513 [x] -> return x
469 [] -> return n'
514 [] -> return n'
470− ns -> ierror (CantResolveAlts (map show ns))
515+ ns -> ierror (CantResolveAlts ns)
473removeProof :: Name -> Idris ()
518removeProof :: Name -> Idris ()
@@ -492,7 +537,7 @@ edit f orig
492 putIState $ orig { idris_options = idris_options i
537 putIState $ orig { idris_options = idris_options i
493 , idris_colourTheme = idris_colourTheme i
538 , idris_colourTheme = idris_colourTheme i
495− loadInputs stdout [f]
540+ loadInputs stdout [f] Nothing
496-- clearOrigPats
541-- clearOrigPats
498 return ()
543 return ()
@@ -520,11 +565,13 @@ insertScript prf (x : xs) = x : insertScript prf xs
521process :: Handle -> FilePath -> Command -> Idris ()
566process :: Handle -> FilePath -> Command -> Idris ()
522process h fn Help = iPrintResult displayHelp
567process h fn Help = iPrintResult displayHelp
568+process h fn Warranty = iPrintResult warranty
523process h fn (ChangeDirectory f)
569process h fn (ChangeDirectory f)
524 = do runIO $ setCurrentDirectory f
570 = do runIO $ setCurrentDirectory f
525 return ()
571 return ()
526process h fn (Eval t)
572process h fn (Eval t)
573+ = withErrorReflection $ do logLvl 5 $ show t
527− = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
574+ (tm, ty) <- elabVal toplevel False t
528 ctxt <- getContext
575 ctxt <- getContext
529 let tm' = force (normaliseAll ctxt [] tm)
576 let tm' = force (normaliseAll ctxt [] tm)
530 let ty' = force (normaliseAll ctxt [] ty)
577 let ty' = force (normaliseAll ctxt [] ty)
@@ -533,41 +580,39 @@ process h fn (Eval t)
533 ist <- getIState
580 ist <- getIState
534 logLvl 3 $ "Raw: " ++ show (tm', ty')
581 logLvl 3 $ "Raw: " ++ show (tm', ty')
535 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
582 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
536− let imp = opt_showimp (idris_options ist)
537− tmDoc = prettyImp imp (delab ist tm')
583+ let tmDoc = prettyIst ist (delab ist tm')
538− tyDoc = prettyImp imp (delab ist ty')
584+ tyDoc = prettyIst ist (delab ist ty')
539 ihPrintTermWithType h tmDoc tyDoc
585 ihPrintTermWithType h tmDoc tyDoc
541process h fn (ExecVal t)
587process h fn (ExecVal t)
542 = do ctxt <- getContext
588 = do ctxt <- getContext
543 ist <- getIState
589 ist <- getIState
544− let imp = opt_showimp (idris_options ist)
545 (tm, ty) <- elabVal toplevel False t
590 (tm, ty) <- elabVal toplevel False t
546-- let tm' = normaliseAll ctxt [] tm
591-- let tm' = normaliseAll ctxt [] tm
547 let ty' = normaliseAll ctxt [] ty
592 let ty' = normaliseAll ctxt [] ty
548 res <- execute tm
593 res <- execute tm
549− let (resOut, tyOut) = (prettyImp imp (delab ist res),
594+ let (resOut, tyOut) = (prettyIst ist (delab ist res),
550− prettyImp imp (delab ist ty'))
595+ prettyIst ist (delab ist ty'))
551 ihPrintTermWithType h resOut tyOut
596 ihPrintTermWithType h resOut tyOut
553process h fn (Check (PRef _ n))
598process h fn (Check (PRef _ n))
554 = do ctxt <- getContext
599 = do ctxt <- getContext
555 ist <- getIState
600 ist <- getIState
556− imp <- impShow
601+ let ppo = ppOptionIst ist
557 case lookupNames n ctxt of
602 case lookupNames n ctxt of
558 ts@(t:_) ->
603 ts@(t:_) ->
559 case lookup t (idris_metavars ist) of
604 case lookup t (idris_metavars ist) of
560 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
605 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
561− showMetavarInfo imp ist n i
606+ showMetavarInfo ppo ist n i
562 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
607 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
563 [] -> ihPrintError h $ "No such variable " ++ show n
608 [] -> ihPrintError h $ "No such variable " ++ show n
565− showMetavarInfo imp ist n i
610+ showMetavarInfo ppo ist n i
566 = case lookupTy n (tt_ctxt ist) of
611 = case lookupTy n (tt_ctxt ist) of
567− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
612+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
568− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
613+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
569− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
614+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
570− putTy imp ist i bnd (PPi _ n t sc)
615+ putTy ppo ist i bnd (PPi _ n t sc)
571 = let current = text " " <>
616 = let current = text " " <>
572 (case n of
617 (case n of
573 MN _ _ -> text "_"
618 MN _ _ -> text "_"
@@ -575,37 +620,41 @@ process h fn (Check (PRef _ n))
575 _ -> bindingOf n False) <+>
620 _ -> bindingOf n False) <+>
576 colon <+> align (tPretty bnd ist t) <> line
621 colon <+> align (tPretty bnd ist t) <> line
578− current <> putTy imp ist (i-1) ((n,False):bnd) sc
623+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc
579− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
624+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
580− putGoal imp ist bnd g
625+ putGoal ppo ist bnd g
581 = text "--------------------------------------" <$>
626 = text "--------------------------------------" <$>
582 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
627 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
583 align (tPretty bnd ist g)
628 align (tPretty bnd ist g)
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
588process h fn (Check t)
633process h fn (Check t)
589 = do (tm, ty) <- elabVal toplevel False t
634 = do (tm, ty) <- elabVal toplevel False t
590 ctxt <- getContext
635 ctxt <- getContext
591 ist <- getIState
636 ist <- getIState
592− let imp = opt_showimp (idris_options ist)
637+ let ppo = ppOptionIst ist
593 ty' = normaliseC ctxt [] ty
638 ty' = normaliseC ctxt [] ty
594 case tm of
639 case tm of
595 TType _ ->
640 TType _ ->
596− ihPrintTermWithType h (prettyImp imp PType) type1Doc
641+ ihPrintTermWithType h (prettyIst ist PType) type1Doc
597− _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
642+ _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
598− (prettyImp imp (delab ist ty))
643+ (prettyIst ist (delab ist ty))
600−process h fn (DocStr n)
645+process h fn (DocStr (Left n))
601− = do i <- getIState
646+ = do ist <- getIState
602− let imp = opt_showimp (idris_options i)
603− case lookupCtxtName n (idris_docstrings i) of
647+ case lookupCtxtName n (idris_docstrings ist) of
604 [] -> iPrintError $ "No documentation for " ++ show n
648 [] -> iPrintError $ "No documentation for " ++ show n
605− ns -> do toShow <- mapM (showDoc imp) ns
649+ ns -> do toShow <- mapM (showDoc ist) ns
606 ihRenderResult h (vsep toShow)
650 ihRenderResult h (vsep toShow)
607− where showDoc imp (n, d) = do doc <- getDocs n
651+ where showDoc ist (n, d) = do doc <- getDocs n
608− return $ pprintDocs imp doc
652+ return $ pprintDocs ist doc
654+process h fn (DocStr (Right c))
655+ = do ist <- getIState
656+ ihRenderResult h $ pprintConstDocs ist c (constDocs c)
609process h fn Universes
658process h fn Universes
610 = do i <- getIState
659 = do i <- getIState
611 let cs = idris_constraints i
660 let cs = idris_constraints i
@@ -637,8 +686,8 @@ process h fn (TotCheck n)
637 [] -> ihPrintError h $ "Unknown operator " ++ show n
686 [] -> ihPrintError h $ "Unknown operator " ++ show n
638 ts -> do ist <- getIState
687 ts -> do ist <- getIState
639 c <- colourise
688 c <- colourise
640− imp <- impShow
689+ let ppo = ppOptionIst ist
641− let showN = showName (Just ist) [] imp c
690+ let showN = showName (Just ist) [] ppo c
642 ihPrintResult h . concat . intersperse "\n" .
691 ihPrintResult h . concat . intersperse "\n" .
643 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
692 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
@@ -661,191 +710,21 @@ process h fn (DebugInfo n)
661 iputStrLn $ "Size change: " ++ show sc
710 iputStrLn $ "Size change: " ++ show sc
662 when (not (null cg')) $ do iputStrLn "Call graph:\n"
711 when (not (null cg')) $ do iputStrLn "Call graph:\n"
663 iputStrLn (show cg')
712 iputStrLn (show cg')
664−process h fn (Info n)
713+process h fn (Search t) = searchByType h t
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!
672process h fn (CaseSplitAt updatefile l n)
714process 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
715+ = caseSplitAt h fn updatefile l n
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)
685process h fn (AddClauseFrom updatefile l n)
716process 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
717+ = addClauseFrom h fn updatefile l n
693− then do let fb = fn ++ "~"
694− runIO $ writeFile fb (unlines (before ++ nonblank) ++
695− replicate indent ' ' ++
698− runIO $ copyFile fb fn
699− else ihPrintResult h cl
701− getIndent i n [] = 0
702− getIndent i n xs | take (length n) xs == n = i
703− getIndent i n (x : xs) = getIndent (i + 1) n xs
704process h fn (AddProofClauseFrom updatefile l n)
718process 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
719+ = addProofClauseFrom h fn updatefile l n
712− then do let fb = fn ++ "~"
713− runIO $ writeFile fb (unlines (before ++ nonblank) ++
714− replicate indent ' ' ++
717− runIO $ copyFile fb fn
718− else ihPrintResult h cl
720− getIndent i n [] = 0
721− getIndent i n xs | take (length n) xs == n = i
722− getIndent i n (x : xs) = getIndent (i + 1) n xs
723process h fn (AddMissing updatefile l n)
720process h fn (AddMissing updatefile l n)
724− = do src <- runIO $ readFile fn
721+ = addMissing h fn updatefile l n
725− let (before, tyline : later) = splitAt (l-1) (lines src)
726− let indent = getIndent 0 (show n) tyline
728− cl <- getInternalApp fn l
729− let n' = getAppName cl
731− extras <- case lookupCtxt n' (idris_patdefs i) of
733− [(_, tms)] -> do tms' <- nameMissing tms
734− showNew (show n ++ "_rhs") 1 indent tms'
735− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
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)
747− nsroot (NS n _) = nsroot n
748− nsroot (SN (WhereN _ _ n)) = nsroot n
751− getAppName (PApp _ r _) = getAppName r
752− getAppName (PRef _ r) = r
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' ++
761− showNew nm i _ [] = return ""
763− getIndent i n [] = 0
764− getIndent i n xs | take (length n) xs == n = i
765− getIndent i n (x : xs) = getIndent (i + 1) n xs
767process h fn (MakeWith updatefile l n)
722process h fn (MakeWith updatefile l n)
768− = do src <- runIO $ readFile fn
723+ = makeWith h fn updatefile l n
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
724+process h fn (MakeLemma updatefile l n)
777− do let fb = fn ++ "~"
725+ = makeLemma h fn updatefile l n
778− runIO $ writeFile fb (unlines (before ++ nonblank)
781− runIO $ copyFile fb fn
782− else ihPrintResult h with
783− where getIndent s = length (takeWhile isSpace s)
785−process h fn (DoProofSearch updatefile l n hints)
726+process h fn (DoProofSearch updatefile rec l n hints)
786− = do src <- runIO $ readFile fn
727+ = doProofSearch h fn updatefile rec l n hints Nothing
787− let (before, tyline : later) = splitAt (l-1) (lines src)
789− mn <- case lookupNames n ctxt of
792− ns -> ierror (CantResolveAlts (map show ns))
794− let (top, envlen, _) = case lookup mn (idris_metavars i) of
795− Just (t, e, False) -> (t, e, False)
796− _ -> (Nothing, 0, True)
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) []
802− (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
803− (tm, ty) <- elabVal toplevel False (PRef fc mn)
806− return $ show (stripNS
808− (delab i (specialise ctxt [] [(mn, 1)] tm)))))
809− (\e -> return ("?" ++ show n))
811− do let fb = fn ++ "~"
812− runIO $ writeFile fb (unlines before ++
813− updateMeta False tyline (show n) newmv ++ "\n"
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
823− stripNS tm = mapPT dens tm where
824− dens (PRef fc n) = PRef fc (nsroot n)
827− nsroot (NS n _) = nsroot n
828− nsroot (SN (WhereN _ _ n)) = nsroot n
831− updateMeta brack ('?':cs) n new
832− | length cs >= length n
833− = case splitAt (length n) cs of
835− if ((isSpace c || c == ')' || c == '}') && mv == n)
836− then addBracket brack new ++ (c : cs)
837− else '?' : mv ++ c : updateMeta True cs n new
838− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
839− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
840− updateMeta brack (c:cs) n new
841− = c : updateMeta (brack || not (isSpace c)) cs n new
842− updateMeta brack [] n new = ""
844− addBracket False new = new
845− addBracket True new@('(':xs) | last xs == ')' = new
846− addBracket True new | any isSpace new = '(' : new ++ ")"
849process h fn (Spec t)
728process h fn (Spec t)
850 = do (tm, ty) <- elabVal toplevel False t
729 = do (tm, ty) <- elabVal toplevel False t
851 ctxt <- getContext
730 ctxt <- getContext
@@ -871,14 +750,15 @@ process h fn (RmProof n')
872process h fn' (AddProof prf)
751process h fn' (AddProof prf)
873 = do fn <- do
752 = do fn <- do
753+ let fn'' = takeWhile (/= ' ') fn'
874− ex <- runIO $ doesFileExist fn'
754+ ex <- runIO $ doesFileExist fn''
875− let fnExt = fn' <.> "idr"
755+ let fnExt = fn'' <.> "idr"
876 exExt <- runIO $ doesFileExist fnExt
756 exExt <- runIO $ doesFileExist fnExt
878− then return fn'
758+ then return fn''
879 else if exExt
759 else if exExt
880 then return fnExt
760 then return fnExt
881− else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
761+ else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
882 let fb = fn ++ "~"
762 let fb = fn ++ "~"
883 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
763 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
884 prog <- runIO $ readFile fb
764 prog <- runIO $ readFile fb
@@ -915,13 +795,14 @@ process h fn (Prove n')
915 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
795 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
916 [(n, (_,_,False))] -> return n
796 [(n, (_,_,False))] -> return n
917 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
797 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
918− ns -> ierror (CantResolveAlts (map show ns))
798+ ns -> ierror (CantResolveAlts (map fst ns))
919 prover (lit fn) n
799 prover (lit fn) n
920 -- recheck totality
800 -- recheck totality
921 i <- getIState
801 i <- getIState
922 totcheck (fileFC "(input)", n)
802 totcheck (fileFC "(input)", n)
923 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
803 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
924 mapM_ checkDeclTotality (idris_totcheck i)
804 mapM_ checkDeclTotality (idris_totcheck i)
926process h fn (HNF t)
807process h fn (HNF t)
927 = do (tm, ty) <- elabVal toplevel False t
808 = do (tm, ty) <- elabVal toplevel False t
@@ -934,23 +815,25 @@ process h fn (TestInline t)
934 ctxt <- getContext
815 ctxt <- getContext
935 ist <- getIState
816 ist <- getIState
936 let tm' = inlineTerm ist tm
817 let tm' = inlineTerm ist tm
938 c <- colourise
818 c <- colourise
939 iPrintResult (showTm ist (delab ist tm'))
819 iPrintResult (showTm ist (delab ist tm'))
940process h fn Execute
820process h fn Execute
941− = do ist <- getIState
822+ (do ist <- getIState
942− (m, _) <- elabVal toplevel False
823+ (m, _) <- elabVal toplevel False
943− (PApp fc
824+ (PApp fc
944− (PRef fc (sUN "run__IO"))
825+ (PRef fc (sUN "run__IO"))
945− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
826+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
946− (tmpn, tmph) <- runIO tempfile
827+ (tmpn, tmph) <- runIO tempfile
947− runIO $ hClose tmph
828+ runIO $ hClose tmph
948− t <- codegen
829+ t <- codegen
949− compile t tmpn m
830+ compile t tmpn m
950− case idris_outputmode ist of
831+ case idris_outputmode ist of
951− RawOutput -> do runIO $ system tmpn
832+ RawOutput -> do runIO $ system tmpn
952− return ()
833+ return ()
834+ IdeSlave n -> runIO . hPutStrLn h $
953− IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n
835+ IdeSlave.convSExp "run-program" tmpn n)
836+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
954 where fc = fileFC "main"
837 where fc = fileFC "main"
955process h fn (Compile codegen f)
838process h fn (Compile codegen f)
956 = do (m, _) <- elabVal toplevel False
839 = do (m, _) <- elabVal toplevel False
@@ -968,7 +851,7 @@ process h fn (Missing n)
968 = do i <- getIState
851 = do i <- getIState
969 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
852 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
970 case lookupCtxt n (idris_patdefs i) of
853 case lookupCtxt n (idris_patdefs i) of
971− [] -> return ()
854+ [] -> ihPrintError h $ "Unknown operator " ++ show n
972 [(_, tms)] ->
855 [(_, tms)] ->
973 iPrintResult (showSep "\n" (map (showTm i') tms))
856 iPrintResult (showSep "\n" (map (showTm i') tms))
974 _ -> iPrintError $ "Ambiguous name"
857 _ -> iPrintError $ "Ambiguous name"
@@ -1007,6 +890,10 @@ process h fn (SetOpt ShowOrigErr) = setShowOrigErr True
1007process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
890process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False
1008process h fn (SetOpt AutoSolve) = setAutoSolve True
891process h fn (SetOpt AutoSolve) = setAutoSolve True
1009process h fn (UnsetOpt AutoSolve) = setAutoSolve False
892process 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
1011process h fn (SetOpt _) = iPrintError "Not a valid option"
898process h fn (SetOpt _) = iPrintError "Not a valid option"
1012process h fn (UnsetOpt _) = iPrintError "Not a valid option"
899process h fn (UnsetOpt _) = iPrintError "Not a valid option"
@@ -1019,52 +906,54 @@ process h fn ColourOff
1019 putIState $ ist { idris_colourRepl = False }
906 putIState $ ist { idris_colourRepl = False }
1020process h fn ListErrorHandlers =
907process h fn ListErrorHandlers =
1021 do ist <- getIState
908 do ist <- getIState
1022− case idris_errorhandlers ist of
909+ iPrintResult $ case idris_errorhandlers ist of
1023− [] -> iPrintResult "No registered error handlers"
910+ [] -> "No registered error handlers"
1025− iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
911+ handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
1026process h fn (SetConsoleWidth w) = setWidth w
912process h fn (SetConsoleWidth w) = setWidth w
1028process h fn (Apropos a) =
914process h fn (Apropos a) =
1029 do ist <- getIState
915 do ist <- getIState
1030− let impl = opt_showimp (idris_options ist)
1031 let names = apropos ist (T.pack a)
916 let names = apropos ist (T.pack a)
1032 let aproposInfo = [ (n,
917 let aproposInfo = [ (n,
1033 delabTy ist n,
918 delabTy ist n,
1034 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
919 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))
1035 | n <- sort names, isUN n ]
920 | n <- sort names, isUN n ]
1036− ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)
921+ ihRenderResult h $ vsep (map (prettyDocumentedIst ist) 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
922+ where isUN (UN _) = True
1041 isUN (NS n _) = isUN n
923 isUN (NS n _) = isUN n
1042 isUN _ = False
924 isUN _ = False
1044−classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
926+process h fn (WhoCalls n) =
927+ do calls <- whoCalls n
929+ ihRenderResult h . vsep $
931+ text "Callers of" <+> prettyName True [] n <$>
932+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
935+process h fn (CallsWho n) =
936+ do calls <- callsWho n
1045−classInfo ci = do ist <- getIState
937+ ist <- getIState
1046− ctxt <- getContext
938+ ihRenderResult h . vsep $
1047− return $
939+ map (\(n, ns) ->
1048− text "Parameters:" <+>
940+ prettyName True [] n <+> text "calls:" <$>
1049− hsep (punctuate comma (map (prettyName False params') params)) <>
941+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))
1050− line <> line <>
942+ calls
1051− text "Methods:" <> line <>
943+-- IdrisDoc
1052− indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>
944+process h fn (MakeDoc s) =
1053− text "Default superclass instances:" <>
945+ do istate <- getIState
1054− line <>
946+ let names = words s
1055− indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>
947+ parse n | Success x <- runparser name istate fn n = Right x
1056− line <>
948+ parse n = Left n
1057− text "Instances:" <> line <>
949+ (bad, nss) = partitionEithers $ map parse names
1058− indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))
950+ cd <- runIO $ getCurrentDirectory
1059− where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
951+ let outputDir = cd </> "doc"
1060− dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
952+ result <- if null bad then runIO $ generateDocs istate nss outputDir
1061− dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
953+ else return . Left $ "Illegal name: " ++ head bad
1062− dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
954+ case result of Right _ -> iputStrLn "IdrisDoc generated"
1063− dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
955+ Left err -> iPrintError err
1064− dumpInstance ist ctxt n = pp ist $ delabTy ist n
956+
1065− params = class_params ci
1066− params' = zip params (repeat False)
1067− pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []
1069showTotal :: Totality -> IState -> String
958showTotal :: Totality -> IState -> String
1070showTotal t@(Partial (Other ns)) i
959showTotal t@(Partial (Other ns)) i
@@ -1084,80 +973,6 @@ displayHelp = let vstr = showVersion version in
1084 l ++ take (c1 - length l) (repeat ' ') ++
973 l ++ take (c1 - length l) (repeat ' ') ++
1085 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
974 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
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
1096−parseArgs :: [String] -> [Opt]
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)
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)
1161helphead =
976helphead =
1162 [ (["Command"], SpecialHeaderArg, "Purpose"),
977 [ (["Command"], SpecialHeaderArg, "Purpose"),
1163 ([""], NoArg, "")
978 ([""], NoArg, "")
@@ -1169,17 +984,22 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
1169 historyFile = hFile
984 historyFile = hFile
1172−-- invoke as if from command line
987+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
1173idris :: [Opt] -> IO (Maybe IState)
988idris :: [Opt] -> IO (Maybe IState)
1174−idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
989+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
1175 case res of
990 case res of
1176 Left err -> do putStrLn $ pshow idrisInit err
991 Left err -> do putStrLn $ pshow idrisInit err
1177 return Nothing
992 return Nothing
1178 Right ist -> return (Just ist)
993 Right ist -> return (Just ist)
994+ where totalMain = do idrisMain opts
996+ case idris_totcheckfail ist of
997+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1181−loadInputs :: Handle -> [FilePath] -> Idris ()
1001+loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()
1182−loadInputs h inputs
1002+loadInputs h inputs toline -- furthest line to read in input source files
1183 = idrisCatch
1003 = idrisCatch
1184 (do ist <- getIState
1004 (do ist <- getIState
1185 -- if we're in --check and not outputting anything, don't bother
1005 -- if we're in --check and not outputting anything, don't bother
@@ -1204,14 +1024,13 @@ loadInputs h inputs
1204 let ifiles = getModuleFiles modTree
1024 let ifiles = getModuleFiles modTree
1205 iLOG ("MODULE TREE : " ++ show modTree)
1025 iLOG ("MODULE TREE : " ++ show modTree)
1206 iLOG ("RELOAD: " ++ show ifiles)
1026 iLOG ("RELOAD: " ++ show ifiles)
1207− when (not (all ibc ifiles) || loadCode) $
1027+ when (not (all ibc ifiles) || loadCode) $
1208 tryLoad False (filter (not . ibc) ifiles)
1028 tryLoad False (filter (not . ibc) ifiles)
1209 -- return the files that need rechecking
1029 -- return the files that need rechecking
1210− return ifiles)
1030+ return ifiles)
1212 inew <- getIState
1032 inew <- getIState
1213 let tidata = idris_tyinfodata inew
1033 let tidata = idris_tyinfodata inew
1214− let lineapps = idris_lineapps inew
1215 let patdefs = idris_patdefs inew
1034 let patdefs = idris_patdefs inew
1216 -- If it worked, load the whole thing from all the ibcs together
1035 -- If it worked, load the whole thing from all the ibcs together
1217 case errSpan inew of
1036 case errSpan inew of
@@ -1222,38 +1041,56 @@ loadInputs h inputs
1222 _ -> return ()
1041 _ -> return ()
1223 ist <- getIState
1042 ist <- getIState
1224 putIState (ist { idris_tyinfodata = tidata,
1043 putIState (ist { idris_tyinfodata = tidata,
1225− idris_lineapps = lineapps,
1226− idris_patdefs = patdefs }))
1044+ idris_patdefs = patdefs })
1046+ case opt getOutput opts of
1047+ [] -> performUsageAnalysis -- interactive
1048+ _ -> return [] -- batch, will be checked by the compiler
1227 (\e -> do i <- getIState
1051 (\e -> do i <- getIState
1228 case e of
1052 case e of
1229− At f _ -> do setErrSpan f
1053+ At f e' -> do setErrSpan f
1230− ihRenderError stdout $ pprintErr i e
1054+ ihWarn stdout f $ pprintErr i e'
1231 ProgramLineComment -> return () -- fail elsewhere
1055 ProgramLineComment -> return () -- fail elsewhere
1232 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1056 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1233− iputStrLn (pshow i e))
1057+ ihWarn stdout emptyFC $ pprintErr i e)
1234 where -- load all files, stop if any fail
1058 where -- load all files, stop if any fail
1235 tryLoad :: Bool -> [IFileType] -> Idris ()
1059 tryLoad :: Bool -> [IFileType] -> Idris ()
1236− tryLoad keepstate [] = return ()
1060+ tryLoad keepstate [] = warnTotality >> return ()
1237− tryLoad keepstate (f : fs)
1061+ tryLoad keepstate (f : fs)
1238 = do ist <- getIState
1062 = do ist <- getIState
1066+ Just l -> case f of
1067+ IDR fn -> if any (fmatch fn) inputs
1070+ LIDR fn -> if any (fmatch fn) inputs
1239− loadFromIFile h f
1074+ loadFromIFile h f maxline
1240 inew <- getIState
1075 inew <- getIState
1241 -- FIXME: Save these in IBC to avoid this hack! Need to
1076 -- FIXME: Save these in IBC to avoid this hack! Need to
1242 -- preserve it all from source inputs
1077 -- preserve it all from source inputs
1243 let tidata = idris_tyinfodata inew
1078 let tidata = idris_tyinfodata inew
1244− let lineapps = idris_lineapps inew
1245 let patdefs = idris_patdefs inew
1079 let patdefs = idris_patdefs inew
1246 ok <- noErrors
1080 ok <- noErrors
1247 when ok $ do when (not keepstate) $ putIState ist
1081 when ok $ do when (not keepstate) $ putIState ist
1248 ist <- getIState
1082 ist <- getIState
1249 putIState (ist { idris_tyinfodata = tidata,
1083 putIState (ist { idris_tyinfodata = tidata,
1250− idris_lineapps = lineapps,
1251 idris_patdefs = patdefs })
1084 idris_patdefs = patdefs })
1252 tryLoad keepstate fs
1085 tryLoad keepstate fs
1254 ibc (IBC _ _) = True
1087 ibc (IBC _ _) = True
1255 ibc _ = False
1088 ibc _ = False
1090+ fmatch ('.':'/':xs) ys = fmatch xs ys
1091+ fmatch xs ('.':'/':ys) = fmatch xs ys
1092+ fmatch xs ys = xs == ys
1257 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1094 findNewIBC :: IFileType -> Idris (Maybe IFileType)
1258 findNewIBC i@(IBC _ _) = return (Just i)
1095 findNewIBC i@(IBC _ _) = return (Just i)
1259 findNewIBC s@(IDR f) = do ist <- get
1096 findNewIBC s@(IDR f) = do ist <- get
@@ -1310,17 +1147,20 @@ idrisMain opts =
1310 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1147 x:y:xs -> do iputStrLn "More than one interpreter expression found."
1311 runIO $ exitWith (ExitFailure 1)
1148 runIO $ exitWith (ExitFailure 1)
1312 [expr] -> return (Just expr)
1149 [expr] -> return (Just expr)
1150+ let immediate = opt getEvalExpr opts
1313 when (DefaultTotal `elem` opts) $ do i <- getIState
1152 when (DefaultTotal `elem` opts) $ do i <- getIState
1314 putIState (i { default_total = True })
1153 putIState (i { default_total = True })
1315 setColourise $ not quiet && last (True : opt getColour opts)
1154 setColourise $ not quiet && last (True : opt getColour opts)
1316 when (not runrepl) $ setWidth InfinitelyWide
1155 when (not runrepl) $ setWidth InfinitelyWide
1317 mapM_ addLangExt (opt getLanguageExt opts)
1156 mapM_ addLangExt (opt getLanguageExt opts)
1318 setREPL runrepl
1157 setREPL runrepl
1319− setQuiet (quiet || isJust script)
1158+ setQuiet (quiet || isJust script || not (null immediate))
1320 setIdeSlave idesl
1159 setIdeSlave idesl
1321 setVerbose verbose
1160 setVerbose verbose
1322 setCmdLine opts
1161 setCmdLine opts
1323 setOutputTy outty
1162 setOutputTy outty
1163+ setNoBanner nobanner
1324 setCodegen cgn
1164 setCodegen cgn
1325 setTargetTriple trpl
1165 setTargetTriple trpl
1326 setTargetCPU tcpu
1166 setTargetCPU tcpu
@@ -1335,6 +1175,8 @@ idrisMain opts =
1335 (d:_) -> setIBCSubDir d
1175 (d:_) -> setIBCSubDir d
1336 setImportDirs importdirs
1176 setImportDirs importdirs
1178+ setNoBanner nobanner
1338 when (not (NoBasePkgs `elem` opts)) $ do
1180 when (not (NoBasePkgs `elem` opts)) $ do
1339 addPkgDir "prelude"
1181 addPkgDir "prelude"
1340 addPkgDir "base"
1182 addPkgDir "base"
@@ -1344,22 +1186,43 @@ idrisMain opts =
1344 return ()
1186 return ()
1345 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1187 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1346 return ()
1188 return ()
1347− when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner
1189+
1190+ when (runrepl && not idesl) initScript
1192+ nobanner <- getNoBanner
1197+ not (isJust script) &&
1349 orig <- getIState
1202 orig <- getIState
1350− loadInputs stdout inputs
1203+ loadInputs stdout inputs Nothing
1352 runIO $ hSetBuffering stdout LineBuffering
1205 runIO $ hSetBuffering stdout LineBuffering
1354 ok <- noErrors
1207 ok <- noErrors
1355 when ok $ case output of
1208 when ok $ case output of
1356− -- just do the checks
1209+ [] -> return ()
1357− [] -> performUsageAnalysis >> return ()
1359− -- the compiler will run usage analysis itself
1360 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1210 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
1361 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1211 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1215+ exprs -> do setWidth InfinitelyWide
1216+ mapM_ (\str -> do ist <- getIState
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))
1223+ runIO $ exitWith ExitSuccess
1363 case script of
1226 case script of
1364 Nothing -> return ()
1227 Nothing -> return ()
1365 Just expr -> execScript expr
1228 Just expr -> execScript expr
@@ -1375,7 +1238,6 @@ idrisMain opts =
1376 when (runrepl && not idesl) $ do
1239 when (runrepl && not idesl) $ do
1377-- clearOrigPats
1240-- clearOrigPats
1379 startServer orig inputs
1241 startServer orig inputs
1380 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1242 runInputT (replSettings (Just historyFile)) $ repl orig inputs
1381 when (idesl) $ ideslaveStart orig inputs
1243 when (idesl) $ ideslaveStart orig inputs
@@ -1435,7 +1297,7 @@ initScript = do script <- getInitScript
1435 case parseCmd i input cmd of
1297 case parseCmd i input cmd of
1436 Failure err -> runIO $ print (fixColour clr err)
1298 Failure err -> runIO $ print (fixColour clr err)
1437 Success Reload -> iPrintError "Init scripts cannot reload the file"
1299 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"
1439 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1301 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
1440 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1302 Success Edit -> iPrintError "Init scripts cannot invoke the editor"
1441 Success Proofs -> proofs i
1303 Success Proofs -> proofs i
@@ -1483,6 +1345,18 @@ getPkgCheck :: Opt -> Maybe String
1483getPkgCheck (PkgCheck str) = Just str
1345getPkgCheck (PkgCheck str) = Just str
1484getPkgCheck _ = Nothing
1346getPkgCheck _ = Nothing
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
1355+getPkgTest :: Opt -- ^ the option to extract
1356+ -> Maybe String -- ^ the package file to test
1357+getPkgTest (PkgTest f) = Just f
1358+getPkgTest _ = Nothing
1486getCodegen :: Opt -> Maybe Codegen
1360getCodegen :: Opt -> Maybe Codegen
1487getCodegen (UseCodegen x) = Just x
1361getCodegen (UseCodegen x) = Just x
1488getCodegen _ = Nothing
1362getCodegen _ = Nothing
@@ -1491,6 +1365,10 @@ getExecScript :: Opt -> Maybe String
1491getExecScript (InterpretScript expr) = Just expr
1365getExecScript (InterpretScript expr) = Just expr
1492getExecScript _ = Nothing
1366getExecScript _ = Nothing
1368+getEvalExpr :: Opt -> Maybe String
1369+getEvalExpr (EvalExpr expr) = Just expr
1370+getEvalExpr _ = Nothing
1494getOutputTy :: Opt -> Maybe OutputType
1372getOutputTy :: Opt -> Maybe OutputType
1495getOutputTy (OutputTy t) = Just t
1373getOutputTy (OutputTy t) = Just t
1496getOutputTy _ = Nothing
1374getOutputTy _ = Nothing
@@ -1524,6 +1402,20 @@ banner = " ____ __ _ \n" ++
1524 " / _/___/ /____(_)____ \n" ++
1402 " / _/___/ /____(_)____ \n" ++
1525 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1403 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
1526 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1404 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
1527− " /___/\\__,_/_/ /_/____/ Type :? for help \n"
1405+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
1529−
1407+ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
1408+ "For details type :warranty."
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"