git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1273 from bmsherman/cantResolveAlts

Change the type of the CantResolveAlts constructor.

commitf1e36be5401c07f597224ea80e54ef5f473f413f authorEdwin Brady <edwin.brady@gmail.com> dateWed 4 Jun 2014, 20:52 (12 years ago) parent34d6f3921124c3
12 files changed+57−60
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/Evaluate.hs+10−5 src/Idris/Core/TT.hs+1−1 src/Idris/Delaborate.hs+26−2 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+8−8 src/Idris/Erasure.hs+1−1 src/Idris/Interactive.hs+4−4 src/Idris/Output.hs−32 src/Idris/Parser.hs+1−1 src/Idris/REPL.hs+2−2
src/Idris/AbsSyntax.hs+1−1
@@ -278,7 +278,7 @@ addNameHint ty n
278278 ty' <- case lookupCtxtName ty (idris_implicits i) of
279279 [(tyn, _)] -> return tyn
280280 [] -> throwError (NoSuchVariable ty)
281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
281+ tyns -> throwError (CantResolveAlts (map fst tyns))
282282 let ns' = case lookupCtxt ty' (idris_namehints i) of
283283 [ns] -> ns ++ [n]
284284 _ -> [n]
src/Idris/Core/Elaborate.hs+2−2
@@ -709,7 +709,7 @@ tryWhen False a b = a
709709
710710
711711-- 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
713713tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs
714714 where
715715 cantResolve :: Elab' aux a
@@ -718,7 +718,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs
718718 tryAll' :: [Elab' aux a] -> -- successes
719719 Int -> -- most problems
720720 (Elab' aux a, Int) -> -- smallest failure
721− [(Elab' aux a, String)] -> -- still to try
721+ [(Elab' aux a, Name)] -> -- still to try
722722 Elab' aux a
723723 tryAll' [res] pmax _ [] = res
724724 tryAll' (_:_) pmax _ [] = cantResolve
src/Idris/Core/Evaluate.hs+10−5
@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1414 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where
@@ -868,14 +868,19 @@ lookupNames n ctxt
868868 = let ns = lookupCtxtName n (definitions ctxt) in
869869 map fst ns
870870
871−lookupTy :: Name -> Context -> [Type]
872−lookupTy n ctxt
873− = do def <- lookupCtxt n (definitions ctxt)
874− case tfst def of
871+lookupTyName :: Name -> Context -> [(Name, Type)]
872+lookupTyName n ctxt = do
873+ (name, def) <- lookupCtxtName n (definitions ctxt)
874+ ty <- case tfst def of
875875 (Function ty _) -> return ty
876876 (TyDecl _ ty) -> return ty
877877 (Operator ty _ _) -> return ty
878878 (CaseOp _ ty _ _ _ _) -> return ty
879+ return (name, ty)
880+
881+
882+lookupTy :: Name -> Context -> [Type]
883+lookupTy n ctxt = map snd (lookupTyName n ctxt)
879884
880885isConName :: Name -> Context -> Bool
881886isConName n ctxt = isTConName n ctxt || isDConName n ctxt
src/Idris/Core/TT.hs+1−1
@@ -133,7 +133,7 @@ data Err' t
133133 | NoTypeDecl Name
134134 | NotInjective t t t
135135 | CantResolve t
136− | CantResolveAlts [String]
136+ | CantResolveAlts [Name]
137137 | IncompleteTerm t
138138 | UniverseError
139139 | ProgramLineComment
src/Idris/Delaborate.hs+26−2
@@ -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,7 +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 text as)))
199+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
199200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
200201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
201202pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
@@ -258,6 +259,29 @@ annName n = annName' n (showbasic n)
258259annName' :: Name -> String -> Doc OutputAnnotation
259260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
260261
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+
261285showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
262286showSc i [] = empty
263287showSc 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
20422042 [c] -> return c
20432043 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
20442044 cs -> tclift $ tfail $ At fc
2045− (CantResolveAlts (map (show . fst) cs))
2045+ (CantResolveAlts (map fst cs))
20462046 let constraint = PApp fc (PRef fc n) (map pexp ps)
20472047 let iname = mkiname n ps expn
20482048 let emptyclass = null (class_methods ci)
src/Idris/ElabTerm.hs+8−8
@@ -271,10 +271,10 @@ elab ist info pattern opts fn tm
271271 let as' = pruneByType (map fst env) tc ctxt as
272272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
273273 tryAll (zip (map (elab' ina) as') (map showHd as'))
274− where showHd (PApp _ (PRef _ n) _) = show n
275− showHd (PRef _ n) = show n
276− showHd (PApp _ h _) = show h
277− showHd x = show x
274+ where showHd (PApp _ (PRef _ n) _) = n
275+ showHd (PRef _ n) = n
276+ showHd (PApp _ h _) = showHd h
277+ showHd x = NErased -- We probably should do something better than this here
278278 elab' ina (PAlternative False as)
279279 = trySeq as
280280 where -- if none work, take the error from the first
@@ -991,7 +991,7 @@ runTac autoSolve ist fn tac
991991 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
992992 let tacs = map (\ (fn', imps) ->
993993 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
994− show fn')) fnimps
994+ fn')) fnimps
995995 tryAll tacs
996996 when autoSolve solveAll
997997 where envArgs n = do e <- get_env
@@ -1007,7 +1007,7 @@ runTac autoSolve ist fn tac
10071007 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
10081008 let tacs = map (\ (fn', imps) ->
10091009 (apply (Var fn') (map (\x -> (x, 0)) imps),
1010− show fn')) fnimps
1010+ fn')) fnimps
10111011 tryAll tacs
10121012 when autoSolve solveAll
10131013 where isImp (PImp _ _ _ _ _) = True
@@ -1609,8 +1609,8 @@ reflectErr (NotInjective t1 t2 t3) =
16091609 ]
16101610reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
16111611reflectErr (CantResolveAlts ss) =
1612− raw_apply (Var $ reflErrName "CantResolve")
1613− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
1612+ raw_apply (Var $ reflErrName "CantResolveAlts")
1613+ [rawList (Var $ (sUN "String")) (map Var ss)]
16141614reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
16151615reflectErr UniverseError = Var $ reflErrName "UniverseError"
16161616reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
src/Idris/Erasure.hs+1−1
@@ -109,7 +109,7 @@ performUsageAnalysis = do
109109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of
110110 [(n', _)] -> Right n'
111111 [] -> Left (NoSuchVariable n)
112− more -> Left (CantResolveAlts (map (show . fst) more))
112+ more -> Left (CantResolveAlts (map fst more))
113113 where
114114 n = sNS (sUN "main") ["Main"]
115115
src/Idris/Interactive.hs+4−4
@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)
162162 mn <- case lookupNames n ctxt of
163163 [x] -> return x
164164 [] -> return n
165− ns -> ierror (CantResolveAlts (map show ns))
165+ ns -> ierror (CantResolveAlts ns)
166166 i <- getIState
167167 let (top, envlen, _) = case lookup mn (idris_metavars i) of
168168 Just (t, e, False) -> (t, e, False)
@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n
242242 let isProv = checkProv tyline (show n)
243243
244244 ctxt <- getContext
245− mty <- case lookupTy n ctxt of
246− [t] -> return t
245+ mty <- case lookupTyName n ctxt of
246+ [(_,t)] -> return t
247247 [] -> ierror (NoSuchVariable n)
248− ns -> ierror (CantResolveAlts (map show ns))
248+ ns -> ierror (CantResolveAlts (map fst ns))
249249 i <- getIState
250250
251251 if (not isProv) then do
src/Idris/Output.hs−32
@@ -83,38 +83,6 @@ ihRenderResult h d = do ist <- getIState
8383 RawOutput -> consoleDisplayAnnotated h d
8484 IdeSlave n -> ideSlaveReturnAnnotated n h d
8585
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−
11886ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
11987ideSlaveReturnWithStatus status n h out = do
12088 ist <- getIState
src/Idris/Parser.hs+1−1
@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
10341034 case lookupCtxtName n (idris_implicits i) of
10351035 [(n', _)] -> return n'
10361036 [] -> throwError (NoSuchVariable n)
1037− more -> throwError (CantResolveAlts (map (show . fst) more))
1037+ more -> throwError (CantResolveAlts (map fst more))
10381038
10391039pLangExt :: IdrisParser LanguageExt
10401040pLangExt = (reserved "TypeProviders" >> return TypeProviders)
src/Idris/REPL.hs+2−2
@@ -512,7 +512,7 @@ resolveProof n'
512512 n <- case lookupNames n' ctxt of
513513 [x] -> return x
514514 [] -> return n'
515− ns -> ierror (CantResolveAlts (map show ns))
515+ ns -> ierror (CantResolveAlts ns)
516516 return n
517517
518518removeProof :: Name -> Idris ()
@@ -795,7 +795,7 @@ process h fn (Prove n')
795795 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
796796 [(n, (_,_,False))] -> return n
797797 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
798− ns -> ierror (CantResolveAlts (map show ns))
798+ ns -> ierror (CantResolveAlts (map fst ns))
799799 prover (lit fn) n
800800 -- recheck totality
801801 i <- getIState