282abc8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Enable pretty printing of CantResolveAlts errors.

282abc8bmsherman12 years ago

src/Idris/Core/Elaborate.hs+3−3

compare with master

unifiedsplit

@@ -706,16 +706,16 @@ tryWhen False a b = a

706

707

708-- 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

710tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

711 where

712 cantResolve :: Elab' aux a

713− cantResolve = lift $ tfail $ CantResolveTactics (map snd xs)

713+ cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

714

715 tryAll' :: [Elab' aux a] -> -- successes

716 Int -> -- most problems

717 (Elab' aux a, Int) -> -- smallest failure

718− [(Elab' aux a, String)] -> -- still to try

718+ [(Elab' aux a, Name)] -> -- still to try

719 Elab' aux a

720 tryAll' [res] pmax _ [] = res

721 tryAll' (_:_) pmax _ [] = cantResolve

src/Idris/Core/TT.hs−1

@@ -134,7 +134,6 @@ data Err' t

134 | NotInjective t t t

135 | CantResolve t

136 | CantResolveAlts [Name]

137− | CantResolveTactics [String]

138 | IncompleteTerm t

137 | IncompleteTerm t

139 | UniverseError

138 | UniverseError

140 | ProgramLineComment

139 | ProgramLineComment

src/Idris/Delaborate.hs+26−4

@@ -1,5 +1,5 @@

1{-# 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

4-- Convert core TT back into high level syntax, primarily for display

5-- purposes.

@@ -9,6 +9,7 @@ import Util.Pretty

9import Idris.AbsSyntax

10import Idris.Core.TT

11import Idris.Core.Evaluate

12+import Idris.Docstrings (overview, renderDocstring)

12import Idris.ErrReverse

13import Idris.ErrReverse

14import Data.List (intersperse)

15import Data.List (intersperse)

@@ -195,9 +196,7 @@ pprintErr' i (NotInjective p x y) =

195 pprintTerm i (delab i y)

196 pprintTerm i (delab i y)

196pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

197pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

197pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

198pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

198− align (cat (punctuate (comma <> space) (map annName as)))

199+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

199−pprintErr' i (CantResolveTactics ts) = text "Can't resolve tactics:" <+>

200− align (cat (punctuate (comma <> space) (map text ts)))

201pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

202pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

203pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

202pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

@@ -260,6 +259,29 @@ annName n = annName' n (showbasic n)

260annName' :: Name -> String -> Doc OutputAnnotation

259annName' :: Name -> String -> Doc OutputAnnotation

261annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

262

261

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+

263showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

285showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

264showSc i [] = empty

286showSc i [] = empty

265showSc i xs = line <> line <> text "In context:" <>

287showSc i xs = line <> line <> text "In context:" <>

src/Idris/ElabTerm.hs+6−9

@@ -266,10 +266,10 @@ elab ist info pattern opts fn tm

266 let as' = pruneByType tc ctxt as

267-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

268 tryAll (zip (map (elab' ina) as') (map showHd as'))

269− where showHd (PApp _ (PRef _ n) _) = show n

269+ where showHd (PApp _ (PRef _ n) _) = n

270− showHd (PRef _ n) = show n

270+ showHd (PRef _ n) = n

271− showHd (PApp _ h _) = show h

271+ showHd (PApp _ h _) = showHd h

272− showHd x = show x

272+ showHd x = NErased -- We probably should do something better than this here

273 elab' ina (PAlternative False as)

274 = trySeq as

275 where -- if none work, take the error from the first

@@ -969,7 +969,7 @@ runTac autoSolve ist fn tac

969 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

970 let tacs = map (\ (fn', imps) ->

971 (match_apply (Var fn') (map (\x -> (x, 0)) imps),

972− show fn')) fnimps

972+ fn')) fnimps

973 tryAll tacs

974 when autoSolve solveAll

975 where envArgs n = do e <- get_env

@@ -985,7 +985,7 @@ runTac autoSolve ist fn tac

985 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

986 let tacs = map (\ (fn', imps) ->

987 (apply (Var fn') (map (\x -> (x, 0)) imps),

988− show fn')) fnimps

988+ fn')) fnimps

989 tryAll tacs

990 when autoSolve solveAll

991 where isImp (PImp _ _ _ _ _) = True

@@ -1589,9 +1589,6 @@ reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflec

1589reflectErr (CantResolveAlts ss) =

1590 raw_apply (Var $ reflErrName "CantResolveAlts")

1591 [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)]

1595reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1592reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1596reflectErr UniverseError = Var $ reflErrName "UniverseError"

1593reflectErr UniverseError = Var $ reflErrName "UniverseError"

1597reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

1594reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/Output.hs−23

@@ -109,29 +109,6 @@ ihRenderResult h d = do ist <- getIState

109 RawOutput -> consoleDisplayAnnotated h d

110 IdeSlave n -> ideSlaveReturnAnnotated n h d

111

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−

135-- | Show an error with semantic highlighting

112-- | Show an error with semantic highlighting

136ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

113ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

137ihRenderError h e = do ist <- getIState

114ihRenderError h e = do ist <- getIState