git.iko.soy/Idris-dev
on master help sign in
Enable pretty printing of CantResolveAlts errors.

I undid the creation of the CantResolveTactics constructor, and instead ensured all CantResolveAlts errors provide Names in some way.

commit282abc8ff989fbdbe139866719a22b5fe283ecbb authorbmsherman <bmsherman@users.noreply.github.com> dateFri 30 May 2014, 23:18 (12 years ago) parent9907240
5 files changed+35−40
compare with master
unifiedsplit
src/Idris/Core/Elaborate.hs+3−3 src/Idris/Core/TT.hs−1 src/Idris/Delaborate.hs+26−4 src/Idris/ElabTerm.hs+6−9 src/Idris/Output.hs−23
src/Idris/Core/Elaborate.hs+3−3
@@ -706,16 +706,16 @@ tryWhen False a b = a
706706
707707
708708-- Try a selection of tactics. Exactly one must work, all others must fail
709−tryAll :: [(Elab' aux a, String)] -> Elab' aux a
709+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
710710tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs
711711 where
712712 cantResolve :: Elab' aux a
713− cantResolve = lift $ tfail $ CantResolveTactics (map snd xs)
713+ cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
714714
715715 tryAll' :: [Elab' aux a] -> -- successes
716716 Int -> -- most problems
717717 (Elab' aux a, Int) -> -- smallest failure
718− [(Elab' aux a, String)] -> -- still to try
718+ [(Elab' aux a, Name)] -> -- still to try
719719 Elab' aux a
720720 tryAll' [res] pmax _ [] = res
721721 tryAll' (_:_) pmax _ [] = cantResolve
src/Idris/Core/TT.hs−1
@@ -134,7 +134,6 @@ data Err' t
134134 | NotInjective t t t
135135 | CantResolve t
136136 | CantResolveAlts [Name]
137− | CantResolveTactics [String]
138137 | IncompleteTerm t
139138 | UniverseError
140139 | ProgramLineComment
src/Idris/Delaborate.hs+26−4
@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where
2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintErr) where
33
44-- Convert core TT back into high level syntax, primarily for display
55-- purposes.
@@ -9,6 +9,7 @@ import Util.Pretty
99import Idris.AbsSyntax
1010import Idris.Core.TT
1111import Idris.Core.Evaluate
12+import Idris.Docstrings (overview, renderDocstring)
1213import Idris.ErrReverse
1314
1415import Data.List (intersperse)
@@ -195,9 +196,7 @@ pprintErr' i (NotInjective p x y) =
195196 pprintTerm i (delab i y)
196197pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
197198pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
198− align (cat (punctuate (comma <> space) (map annName as)))
199−pprintErr' i (CantResolveTactics ts) = text "Can't resolve tactics:" <+>
200− align (cat (punctuate (comma <> space) (map text ts)))
199+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
201200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
202201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
203202pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
@@ -260,6 +259,29 @@ annName n = annName' n (showbasic n)
260259annName' :: Name -> String -> Doc OutputAnnotation
261260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
262261
262+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
263+fancifyAnnots ist annot@(AnnName n _ _ _) =
264+ do let ctxt = tt_ctxt ist
265+ docs = docOverview ist n
266+ ty = Just (getTy ist n)
267+ case () of
268+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
269+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
270+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
271+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
272+ _ | otherwise -> annot
273+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
274+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
275+ let o = overview (fst docs)
276+ -- TODO make width configurable
277+ out = displayS . renderPretty 1.0 50 $ renderDocstring o
278+ return (out "")
279+ getTy :: IState -> Name -> String -- fails if name not already extant!
280+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
281+ delabTy ist n
282+ in (displayS . renderPretty 1.0 50 $ theTy) ""
283+fancifyAnnots _ annot = annot
284+
263285showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
264286showSc i [] = empty
265287showSc i xs = line <> line <> text "In context:" <>
src/Idris/ElabTerm.hs+6−9
@@ -266,10 +266,10 @@ elab ist info pattern opts fn tm
266266 let as' = pruneByType tc ctxt as
267267-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
268268 tryAll (zip (map (elab' ina) as') (map showHd as'))
269− where showHd (PApp _ (PRef _ n) _) = show n
270− showHd (PRef _ n) = show n
271− showHd (PApp _ h _) = show h
272− showHd x = show x
269+ where showHd (PApp _ (PRef _ n) _) = n
270+ showHd (PRef _ n) = n
271+ showHd (PApp _ h _) = showHd h
272+ showHd x = NErased -- We probably should do something better than this here
273273 elab' ina (PAlternative False as)
274274 = trySeq as
275275 where -- if none work, take the error from the first
@@ -969,7 +969,7 @@ runTac autoSolve ist fn tac
969969 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
970970 let tacs = map (\ (fn', imps) ->
971971 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
972− show fn')) fnimps
972+ fn')) fnimps
973973 tryAll tacs
974974 when autoSolve solveAll
975975 where envArgs n = do e <- get_env
@@ -985,7 +985,7 @@ runTac autoSolve ist fn tac
985985 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
986986 let tacs = map (\ (fn', imps) ->
987987 (apply (Var fn') (map (\x -> (x, 0)) imps),
988− show fn')) fnimps
988+ fn')) fnimps
989989 tryAll tacs
990990 when autoSolve solveAll
991991 where isImp (PImp _ _ _ _ _) = True
@@ -1589,9 +1589,6 @@ reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflec
15891589reflectErr (CantResolveAlts ss) =
15901590 raw_apply (Var $ reflErrName "CantResolveAlts")
15911591 [rawList (Var $ (sUN "String")) (map Var ss)]
1592−reflectErr (CantResolveTactics ss) =
1593− raw_apply (Var $ reflErrName "CantResolveTactics")
1594− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
15951592reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
15961593reflectErr UniverseError = Var $ reflErrName "UniverseError"
15971594reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
src/Idris/Output.hs−23
@@ -109,29 +109,6 @@ ihRenderResult h d = do ist <- getIState
109109 RawOutput -> consoleDisplayAnnotated h d
110110 IdeSlave n -> ideSlaveReturnAnnotated n h d
111111
112−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
113−fancifyAnnots ist annot@(AnnName n _ _ _) =
114− do let ctxt = tt_ctxt ist
115− docs = docOverview ist n
116− ty = Just (getTy ist n)
117− case () of
118− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
119− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
120− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
121− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
122− _ | otherwise -> annot
123− where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
124− docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
125− let o = overview (fst docs)
126− -- TODO make width configurable
127− out = displayS . renderPretty 1.0 50 $ renderDocstring o
128− return (out "")
129− getTy :: IState -> Name -> String -- fails if name not already extant!
130− getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
131− delabTy ist n
132− in (displayS . renderPretty 1.0 50 $ theTy) ""
133−fancifyAnnots _ annot = annot
134−
135112-- | Show an error with semantic highlighting
136113ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
137114ihRenderError h e = do ist <- getIState