@@ -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
@@ -29,6 +30,7 @@ import Idris.Inliner
2930import Idris.CaseSplit
3031import Idris.DeepSeq
3132import Idris.Output
33+import Idris.Interactive
3234import Idris.WhoCalls
3335
3436import Paths_idris
@@ -275,9 +277,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
275277 [n] -> Right $ sUN n
276278 (n:ns) -> Right $ sNS (sUN n) ns
277279runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
278− case splitName name of
279− Left err -> iPrintError err
280− Right n -> process stdout "(ideslave)" (DocStr n)
280+ case parseConst orig name of
281+ Success c -> process stdout "(ideslave)" (DocStr (Right c))
282+ Failure _ ->
283+ case splitName name of
284+ Left err -> iPrintError err
285+ Right n -> process stdout "(ideslave)" (DocStr (Left n))
281286runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
282287 process stdout fn (CaseSplitAt False line (sUN name))
283288runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
@@ -312,34 +317,34 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
312317runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
313318 do ist <- getIState
314319 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
315− imp <- impShow
320+ let ppo = ppOptionIst ist
316321 let mvarTys = map (delabTy ist) mvs
317322 let res = (IdeSlave.SymbolAtom "ok",
318323 zipWith (\ n (prems, concl) -> (n, prems, concl))
319324 (map (IdeSlave.StringAtom . show) mvs)
320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
325+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
321326 runIO . putStrLn $ IdeSlave.convSExp "return" res id
322327 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
323328 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
324329 in ((n, t):prems, conc)
325330 getGoal tm = ([], tm)
326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)
331+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
327332 -> ([(String, String, SpanList OutputAnnotation)],
328333 (String, SpanList OutputAnnotation))
329− sexpGoal ist cols imp ns ([], concl) =
334+ sexpGoal ist cols ppo ns ([], concl) =
330335 let infixes = idris_infixes ist
331336 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
332− pprintPTerm imp (zip ns (repeat False)) [] infixes concl
337+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
333338 in ([], concl')
334− sexpGoal ist cols imp ns ((n, t):ps, concl) =
339+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =
335340 let n' = case n of
336341 NS (UN nm) ns -> str nm
337342 UN nm | ('_':'_':_) <- str nm -> "_"
338343 | otherwise -> str nm
339344 _ -> "_"
340345 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t
342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)
346+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
347+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
343348 in ((n', t', spans) : fst rest, snd rest)
344349runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
345350 case splitName n of
@@ -581,21 +586,21 @@ process h fn (ExecVal t)
581586process h fn (Check (PRef _ n))
582587 = do ctxt <- getContext
583588 ist <- getIState
584− imp <- impShow
589+ let ppo = ppOptionIst ist
585590 case lookupNames n ctxt of
586591 ts@(t:_) ->
587592 case lookup t (idris_metavars ist) of
588593 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
589− showMetavarInfo imp ist n i
594+ showMetavarInfo ppo ist n i
590595 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
591596 [] -> ihPrintError h $ "No such variable " ++ show n
592597 where
593− showMetavarInfo imp ist n i
598+ showMetavarInfo ppo ist n i
594599 = case lookupTy n (tt_ctxt ist) of
595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
598− putTy imp ist i bnd (PPi _ n t sc)
600+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
601+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
602+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
603+ putTy ppo ist i bnd (PPi _ n t sc)
599604 = let current = text " " <>
600605 (case n of
601606 MN _ _ -> text "_"
@@ -603,21 +608,21 @@ process h fn (Check (PRef _ n))
603608 _ -> bindingOf n False) <+>
604609 colon <+> align (tPretty bnd ist t) <> line
605610 in
606− current <> putTy imp ist (i-1) ((n,False):bnd) sc
607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
608− putGoal imp ist bnd g
611+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc
612+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
613+ putGoal ppo ist bnd g
609614 = text "--------------------------------------" <$>
610615 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
611616 align (tPretty bnd ist g)
612617
613− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t
618+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
614619
615620
616621process h fn (Check t)
617622 = do (tm, ty) <- elabVal toplevel False t
618623 ctxt <- getContext
619624 ist <- getIState
620− let imp = opt_showimp (idris_options ist)
625+ let ppo = ppOptionIst ist
621626 ty' = normaliseC ctxt [] ty
622627 case tm of
623628 TType _ ->
@@ -625,7 +630,7 @@ process h fn (Check t)
625630 _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
626631 (prettyIst ist (delab ist ty))
627632
628−process h fn (DocStr n)
633+process h fn (DocStr (Left n))
629634 = do ist <- getIState
630635 case lookupCtxtName n (idris_docstrings ist) of
631636 [] -> iPrintError $ "No documentation for " ++ show n
@@ -633,6 +638,11 @@ process h fn (DocStr n)
633638 ihRenderResult h (vsep toShow)
634639 where showDoc ist (n, d) = do doc <- getDocs n
635640 return $ pprintDocs ist doc
641+
642+process h fn (DocStr (Right c))
643+ = do ist <- getIState
644+ ihRenderResult h $ pprintConstDocs ist c (constDocs c)
645+
636646process h fn Universes
637647 = do i <- getIState
638648 let cs = idris_constraints i
@@ -664,8 +674,8 @@ process h fn (TotCheck n)
664674 [] -> ihPrintError h $ "Unknown operator " ++ show n
665675 ts -> do ist <- getIState
666676 c <- colourise
667− imp <- impShow
668− let showN = showName (Just ist) [] imp c
677+ let ppo = ppOptionIst ist
678+ let showN = showName (Just ist) [] ppo c
669679 ihPrintResult h . concat . intersperse "\n" .
670680 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
671681 ts
@@ -689,186 +699,18 @@ process h fn (DebugInfo n)
689699 when (not (null cg')) $ do iputStrLn "Call graph:\n"
690700 iputStrLn (show cg')
691701process h fn (Search t) = iPrintError "Not implemented"
692−-- FIXME: There is far too much repetition in the cases below!
693−process h fn (CaseSplitAt updatefile l n)
694− = do src <- runIO $ readFile fn
695− res <- splitOnLine l n fn
696− iLOG (showSep "\n" (map show res))
697− let (before, (ap : later)) = splitAt (l-1) (lines src)
698− res' <- replaceSplits ap res
699− let new = concat res'
700− if updatefile
701− then do let fb = fn ++ "~" -- make a backup!
702− runIO $ writeFile fb (unlines before ++ new ++ unlines later)
703− runIO $ copyFile fb fn
704− else -- do ihputStrLn h (show res)
705− ihPrintResult h new
702+process h fn (CaseSplitAt updatefile l n)
703+ = caseSplitAt h fn updatefile l n
706704process h fn (AddClauseFrom updatefile l n)
707− = do src <- runIO $ readFile fn
708− let (before, tyline : later) = splitAt (l-1) (lines src)
709− let indent = getIndent 0 (show n) tyline
710− cl <- getClause l n fn
711− -- add clause before first blank line in 'later'
712− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
713− if updatefile
714− then do let fb = fn ++ "~"
715− runIO $ writeFile fb (unlines (before ++ nonblank) ++
716− replicate indent ' ' ++
717− cl ++ "\n" ++
718− unlines rest)
719− runIO $ copyFile fb fn
720− else ihPrintResult h cl
721− where
722− getIndent i n [] = 0
723− getIndent i n xs | take (length n) xs == n = i
724− getIndent i n (x : xs) = getIndent (i + 1) n xs
705+ = addClauseFrom h fn updatefile l n
725706process h fn (AddProofClauseFrom updatefile l n)
726− = do src <- runIO $ readFile fn
727− let (before, tyline : later) = splitAt (l-1) (lines src)
728− let indent = getIndent 0 (show n) tyline
729− cl <- getProofClause l n fn
730− -- add clause before first blank line in 'later'
731− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
732− if updatefile
733− then do let fb = fn ++ "~"
734− runIO $ writeFile fb (unlines (before ++ nonblank) ++
735− replicate indent ' ' ++
736− cl ++ "\n" ++
737− unlines rest)
738− runIO $ copyFile fb fn
739− else ihPrintResult h cl
740− where
741− getIndent i n [] = 0
742− getIndent i n xs | take (length n) xs == n = i
743− getIndent i n (x : xs) = getIndent (i + 1) n xs
707+ = addProofClauseFrom h fn updatefile l n
744708process h fn (AddMissing updatefile l n)
745− = do src <- runIO $ readFile fn
746− let (before, tyline : later) = splitAt (l-1) (lines src)
747− let indent = getIndent 0 (show n) tyline
748− i <- getIState
749− cl <- getInternalApp fn l
750− let n' = getAppName cl
751−
752− extras <- case lookupCtxt n' (idris_patdefs i) of
753− [] -> return ""
754− [(_, tms)] -> do tms' <- nameMissing tms
755− showNew (show n ++ "_rhs") 1 indent tms'
756− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
757− if updatefile
758− then do let fb = fn ++ "~"
759− runIO $ writeFile fb (unlines (before ++ nonblank)
760− ++ extras ++ unlines rest)
761− runIO $ copyFile fb fn
762− else ihPrintResult h extras
763− where showPat = show . stripNS
764− stripNS tm = mapPT dens tm where
765− dens (PRef fc n) = PRef fc (nsroot n)
766− dens t = t
767−
768− nsroot (NS n _) = nsroot n
769− nsroot (SN (WhereN _ _ n)) = nsroot n
770− nsroot n = n
771−
772− getAppName (PApp _ r _) = getAppName r
773− getAppName (PRef _ r) = r
774− getAppName _ = n
775−
776− showNew nm i ind (tm : tms)
777− = do (nm', i') <- getUniq nm i
778− rest <- showNew nm i' ind tms
779− return (replicate ind ' ' ++
780− showPat tm ++ " = ?" ++ nm' ++
781− "\n" ++ rest)
782− showNew nm i _ [] = return ""
783−
784− getIndent i n [] = 0
785− getIndent i n xs | take (length n) xs == n = i
786− getIndent i n (x : xs) = getIndent (i + 1) n xs
787−
709+ = addMissing h fn updatefile l n
788710process h fn (MakeWith updatefile l n)
789− = do src <- runIO $ readFile fn
790− let (before, tyline : later) = splitAt (l-1) (lines src)
791− let ind = getIndent tyline
792− let with = mkWith tyline n
793− -- add clause before first blank line in 'later',
794− -- or (TODO) before first line with same indentation as tyline
795− let (nonblank, rest) = span (\x -> not (all isSpace x) &&
796− not (ind == getIndent x)) later
797− if updatefile then
798− do let fb = fn ++ "~"
799− runIO $ writeFile fb (unlines (before ++ nonblank)
800− ++ with ++ "\n" ++
801− unlines rest)
802− runIO $ copyFile fb fn
803− else ihPrintResult h with
804− where getIndent s = length (takeWhile isSpace s)
805−
711+ = makeWith h fn updatefile l n
806712process h fn (DoProofSearch updatefile rec l n hints)
807− = do src <- runIO $ readFile fn
808− let (before, tyline : later) = splitAt (l-1) (lines src)
809− ctxt <- getContext
810− mn <- case lookupNames n ctxt of
811− [x] -> return x
812− [] -> return n
813− ns -> ierror (CantResolveAlts (map show ns))
814− i <- getIState
815− let (top, envlen, _) = case lookup mn (idris_metavars i) of
816− Just (t, e, False) -> (t, e, False)
817− _ -> (Nothing, 0, True)
818− let fc = fileFC fn
819− let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))
820− (ProofSearch rec t hints)]
821− let def = PClause fc mn (PRef fc mn) [] (body top) []
822− newmv <- idrisCatch
823− (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
824− (tm, ty) <- elabVal toplevel False (PRef fc mn)
825− ctxt <- getContext
826− i <- getIState
827− return . flip displayS "" . renderPretty 1.0 80 $
828− pprintPTerm False [] [] (idris_infixes i)
829− (stripNS
830− (dropCtxt envlen
831− (delab i (specialise ctxt [] [(mn, 1)] tm)))))
832− (\e -> return ("?" ++ show n))
833− if updatefile then
834− do let fb = fn ++ "~"
835− runIO $ writeFile fb (unlines before ++
836− updateMeta False tyline (show n) newmv ++ "\n"
837− ++ unlines later)
838− runIO $ copyFile fb fn
839− else ihPrintResult h newmv
840− where dropCtxt 0 sc = sc
841− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
842− dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
843− dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
844− dropCtxt _ t = t
845−
846− stripNS tm = mapPT dens tm where
847− dens (PRef fc n) = PRef fc (nsroot n)
848− dens t = t
849−
850− nsroot (NS n _) = nsroot n
851− nsroot (SN (WhereN _ _ n)) = nsroot n
852− nsroot n = n
853−
854− updateMeta brack ('?':cs) n new
855− | length cs >= length n
856− = case splitAt (length n) cs of
857− (mv, c:cs) ->
858− if ((isSpace c || c == ')' || c == '}') && mv == n)
859− then addBracket brack new ++ (c : cs)
860− else '?' : mv ++ c : updateMeta True cs n new
861− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
862− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
863− updateMeta brack (c:cs) n new
864− = c : updateMeta (brack || not (isSpace c)) cs n new
865− updateMeta brack [] n new = ""
866−
867− addBracket False new = new
868− addBracket True new@('(':xs) | last xs == ')' = new
869− addBracket True new | any isSpace new = '(' : new ++ ")"
870− | otherwise = new
871−
713+ = doProofSearch h fn updatefile rec l n hints
872714process h fn (Spec t)
873715 = do (tm, ty) <- elabVal toplevel False t
874716 ctxt <- getContext
@@ -946,6 +788,7 @@ process h fn (Prove n')
946788 totcheck (fileFC "(input)", n)
947789 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
948790 mapM_ checkDeclTotality (idris_totcheck i)
791+ warnTotality
949792
950793process h fn (HNF t)
951794 = do (tm, ty) <- elabVal toplevel False t
@@ -958,23 +801,25 @@ process h fn (TestInline t)
958801 ctxt <- getContext
959802 ist <- getIState
960803 let tm' = inlineTerm ist tm
961− imp <- impShow
962804 c <- colourise
963805 iPrintResult (showTm ist (delab ist tm'))
964806process h fn Execute
965− = do ist <- getIState
966− (m, _) <- elabVal toplevel False
967− (PApp fc
968− (PRef fc (sUN "run__IO"))
969− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
970− (tmpn, tmph) <- runIO tempfile
971− runIO $ hClose tmph
972− t <- codegen
973− compile t tmpn m
974− case idris_outputmode ist of
975− RawOutput -> do runIO $ system tmpn
976− return ()
977− IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n
807+ = idrisCatch
808+ (do ist <- getIState
809+ (m, _) <- elabVal toplevel False
810+ (PApp fc
811+ (PRef fc (sUN "run__IO"))
812+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
813+ (tmpn, tmph) <- runIO tempfile
814+ runIO $ hClose tmph
815+ t <- codegen
816+ compile t tmpn m
817+ case idris_outputmode ist of
818+ RawOutput -> do runIO $ system tmpn
819+ return ()
820+ IdeSlave n -> runIO . hPutStrLn h $
821+ IdeSlave.convSExp "run-program" tmpn n)
822+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
978823 where fc = fileFC "main"
979824process h fn (Compile codegen f)
980825 = do (m, _) <- elabVal toplevel False
@@ -1033,6 +878,8 @@ process h fn (SetOpt AutoSolve) = setAutoSolve True
1033878process h fn (UnsetOpt AutoSolve) = setAutoSolve False
1034879process h fn (SetOpt NoBanner) = setNoBanner True
1035880process h fn (UnsetOpt NoBanner) = setNoBanner False
881+process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
882+process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach
1036883
1037884process h fn (SetOpt _) = iPrintError "Not a valid option"
1038885process h fn (UnsetOpt _) = iPrintError "Not a valid option"
@@ -1204,13 +1051,18 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {
12041051 historyFile = hFile
12051052 }
12061053
1207−-- invoke as if from command line
1054+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.
12081055idris :: [Opt] -> IO (Maybe IState)
1209−idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit
1056+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit
12101057 case res of
12111058 Left err -> do putStrLn $ pshow idrisInit err
12121059 return Nothing
12131060 Right ist -> return (Just ist)
1061+ where totalMain = do idrisMain opts
1062+ ist <- getIState
1063+ case idris_totcheckfail ist of
1064+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
1065+ [] -> return ()
12141066
12151067
12161068loadInputs :: Handle -> [FilePath] -> Idris ()
@@ -1256,7 +1108,13 @@ loadInputs h inputs
12561108 _ -> return ()
12571109 ist <- getIState
12581110 putIState (ist { idris_tyinfodata = tidata,
1259− idris_patdefs = patdefs }))
1111+ idris_patdefs = patdefs })
1112+
1113+ case opt getOutput opts of
1114+ [] -> performUsageAnalysis -- interactive
1115+ _ -> return [] -- batch, will be checked by the compiler
1116+
1117+ return ())
12601118 (\e -> do i <- getIState
12611119 case e of
12621120 At f e' -> do setErrSpan f
@@ -1266,8 +1124,8 @@ loadInputs h inputs
12661124 ihWarn stdout emptyFC $ pprintErr i e)
12671125 where -- load all files, stop if any fail
12681126 tryLoad :: Bool -> [IFileType] -> Idris ()
1269− tryLoad keepstate [] = return ()
1270− tryLoad keepstate (f : fs)
1127+ tryLoad keepstate [] = warnTotality >> return ()
1128+ tryLoad keepstate (f : fs)
12711129 = do ist <- getIState
12721130 loadFromIFile h f
12731131 inew <- getIState
@@ -1400,10 +1258,7 @@ idrisMain opts =
14001258
14011259 ok <- noErrors
14021260 when ok $ case output of
1403− -- just do the checks
1404− [] -> performUsageAnalysis >> return ()
1405−
1406− -- the compiler will run usage analysis itself
1261+ [] -> return ()
14071262 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
14081263 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
14091264