f1e36be · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -278,7 +278,7 @@ addNameHint ty n

278 ty' <- case lookupCtxtName ty (idris_implicits i) of

279 [(tyn, _)] -> return tyn

280 [] -> throwError (NoSuchVariable ty)

281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

281+ tyns -> throwError (CantResolveAlts (map fst tyns))

282 let ns' = case lookupCtxt ty' (idris_namehints i) of

283 [ns] -> ns ++ [n]

284 _ -> [n]

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

@@ -709,7 +709,7 @@ tryWhen False a b = a

709

710

711-- Try a selection of tactics. Exactly one must work, all others must fail

712−tryAll :: [(Elab' aux a, String)] -> Elab' aux a

712+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

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

714 where

715 cantResolve :: Elab' aux a

@@ -718,7 +718,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

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

719 Int -> -- most problems

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

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

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

722 Elab' aux a

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

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

src/Idris/Core/Evaluate.hs+10−5

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

@@ -868,14 +868,19 @@ lookupNames n ctxt

868 = let ns = lookupCtxtName n (definitions ctxt) in

869 map fst ns

870

871−lookupTy :: Name -> Context -> [Type]

871+lookupTyName :: Name -> Context -> [(Name, Type)]

872−lookupTy n ctxt

872+lookupTyName n ctxt = do

873− = do def <- lookupCtxt n (definitions ctxt)

873+ (name, def) <- lookupCtxtName n (definitions ctxt)

874− case tfst def of

874+ ty <- case tfst def of

875 (Function ty _) -> return ty

876 (TyDecl _ ty) -> return ty

877 (Operator ty _ _) -> return ty

878 (CaseOp _ ty _ _ _ _) -> return ty

879+ return (name, ty)

880+

881+

882+lookupTy :: Name -> Context -> [Type]

883+lookupTy n ctxt = map snd (lookupTyName n ctxt)

879

884

880isConName :: Name -> Context -> Bool

885isConName :: Name -> Context -> Bool

881isConName n ctxt = isTConName n ctxt || isDConName n ctxt

886isConName n ctxt = isTConName n ctxt || isDConName n ctxt

src/Idris/Core/TT.hs+1−1

@@ -133,7 +133,7 @@ data Err' t

133 | NoTypeDecl Name

134 | NotInjective t t t

135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137 | IncompleteTerm t

138 | UniverseError

139 | ProgramLineComment

src/Idris/Delaborate.hs+26−2

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

3

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

13

14

14import Data.List (intersperse)

15import Data.List (intersperse)

@@ -195,7 +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 text as)))

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

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

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

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

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

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

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

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

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

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

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

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

260

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+

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

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

262showSc i [] = empty

286showSc i [] = empty

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

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

src/Idris/ElabDecls.hs+1−1

@@ -2042,7 +2042,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2042 [c] -> return c

2043 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

2044 cs -> tclift $ tfail $ At fc

2045− (CantResolveAlts (map (show . fst) cs))

2045+ (CantResolveAlts (map fst cs))

2046 let constraint = PApp fc (PRef fc n) (map pexp ps)

2047 let iname = mkiname n ps expn

2048 let emptyclass = null (class_methods ci)

src/Idris/ElabTerm.hs+8−8

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

271 let as' = pruneByType (map fst env) tc ctxt as

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

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

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

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

275− showHd (PRef _ n) = show n

275+ showHd (PRef _ n) = n

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

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

277− showHd x = show x

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

278 elab' ina (PAlternative False as)

279 = trySeq as

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

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

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

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

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

994− show fn')) fnimps

994+ fn')) fnimps

995 tryAll tacs

996 when autoSolve solveAll

997 where envArgs n = do e <- get_env

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

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

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

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

1010− show fn')) fnimps

1010+ fn')) fnimps

1011 tryAll tacs

1012 when autoSolve solveAll

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

@@ -1609,8 +1609,8 @@ reflectErr (NotInjective t1 t2 t3) =

1609 ]

1610reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

1611reflectErr (CantResolveAlts ss) =

1612− raw_apply (Var $ reflErrName "CantResolve")

1612+ raw_apply (Var $ reflErrName "CantResolveAlts")

1613− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

1613+ [rawList (Var $ (sUN "String")) (map Var ss)]

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

1615reflectErr UniverseError = Var $ reflErrName "UniverseError"

1616reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/Erasure.hs+1−1

@@ -109,7 +109,7 @@ performUsageAnalysis = do

109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of

110 [(n', _)] -> Right n'

111 [] -> Left (NoSuchVariable n)

112− more -> Left (CantResolveAlts (map (show . fst) more))

112+ more -> Left (CantResolveAlts (map fst more))

113 where

114 n = sNS (sUN "main") ["Main"]

115

src/Idris/Interactive.hs+4−4

@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

162 mn <- case lookupNames n ctxt of

163 [x] -> return x

164 [] -> return n

165− ns -> ierror (CantResolveAlts (map show ns))

165+ ns -> ierror (CantResolveAlts ns)

166 i <- getIState

167 let (top, envlen, _) = case lookup mn (idris_metavars i) of

168 Just (t, e, False) -> (t, e, False)

@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n

242 let isProv = checkProv tyline (show n)

243

244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

245+ mty <- case lookupTyName n ctxt of

246− [t] -> return t

246+ [(_,t)] -> return t

247 [] -> ierror (NoSuchVariable n)

248− ns -> ierror (CantResolveAlts (map show ns))

248+ ns -> ierror (CantResolveAlts (map fst ns))

249 i <- getIState

250

251 if (not isProv) then do

src/Idris/Output.hs−32

@@ -83,38 +83,6 @@ ihRenderResult h d = do ist <- getIState

83 RawOutput -> consoleDisplayAnnotated h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

85

86−makeAnnName :: IState -> Name -> Maybe OutputAnnotation

87−makeAnnName ist n

88− | isDConName n ctxt = annName DataOutput

89− | isFnName n ctxt = annName FunOutput

90− | isTConName n ctxt = annName TypeOutput

91− | isMetavarName n ist = annName MetavarOutput

92− | otherwise = Nothing

93− where ctxt = tt_ctxt ist

94− docs = docOverview ist n

95− ty = Just (getTy ist n)

96−

97− annName :: NameOutput -> Maybe OutputAnnotation

98− annName nameType = Just (AnnName n (Just nameType) docs ty)

99− docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

100− docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

101− let o = overview (fst docs)

102− -- TODO make width configurable

103− out = displayS . renderPretty 1.0 50 $ renderDocstring o

104− return (out "")

105− getTy :: IState -> Name -> String -- fails if name not already extant!

106− getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

107− delabTy ist n

108− in (displayS . renderPretty 1.0 50 $ theTy) ""

109−

110−

111−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

112−fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of

113− Just fancyAnnot -> fancyAnnot

114− Nothing -> annot

115−fancifyAnnots _ annot = annot

116−

117−

118ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

86ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

119ideSlaveReturnWithStatus status n h out = do

87ideSlaveReturnWithStatus status n h out = do

120 ist <- getIState

88 ist <- getIState

src/Idris/Parser.hs+1−1

@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1034 case lookupCtxtName n (idris_implicits i) of

1035 [(n', _)] -> return n'

1036 [] -> throwError (NoSuchVariable n)

1037− more -> throwError (CantResolveAlts (map (show . fst) more))

1037+ more -> throwError (CantResolveAlts (map fst more))

1038

1039pLangExt :: IdrisParser LanguageExt

1040pLangExt = (reserved "TypeProviders" >> return TypeProviders)

src/Idris/REPL.hs+2−2

@@ -512,7 +512,7 @@ resolveProof n'

512 n <- case lookupNames n' ctxt of

513 [x] -> return x

514 [] -> return n'

515− ns -> ierror (CantResolveAlts (map show ns))

515+ ns -> ierror (CantResolveAlts ns)

516 return n

517

518removeProof :: Name -> Idris ()

@@ -795,7 +795,7 @@ process h fn (Prove n')

795 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

796 [(n, (_,_,False))] -> return n

797 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

798− ns -> ierror (CantResolveAlts (map show ns))

798+ ns -> ierror (CantResolveAlts (map fst ns))

799 prover (lit fn) n

800 -- recheck totality

801 i <- getIState