57c3ffc · Idris-dev · git.iko.soy

src/Idris/Core/Elaborate.hs+4

compare with master

unifiedsplit

@@ -167,6 +167,10 @@ done_elaborating_app :: Name -> Elab' aux ()

167done_elaborating_app f = updatePS (doneElaboratingAppPS f)

168done_elaborating_arg :: Name -> Name -> Elab' aux ()

169done_elaborating_arg f a = updatePS (doneElaboratingArgPS f a)

170+elaborating_app :: Elab' aux [(FC, Name, Name)]

171+elaborating_app = do ES (ps, _) _ _ <- get

172+ return $ map (\ (FailContext x y z) -> (x, y, z))

173+ (while_elaborating ps)

170

174

171-- Some handy gadgets for pulling out bits of state

175-- Some handy gadgets for pulling out bits of state

172

176

src/Idris/Core/TT.hs+1

@@ -198,6 +198,7 @@ instance Show Err where

198 show (At f e) = show f ++ ":" ++ show e

199 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

200 show x ++ ": " ++ show e

201+ show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

201 show _ = "Error"

202 show _ = "Error"

202

203

203instance Pretty Err OutputAnnotation where

204instance Pretty Err OutputAnnotation where

src/Idris/Delaborate.hs+10−2

@@ -221,11 +221,19 @@ pprintErr' i (ElaboratingArg f x _ e)

221 | isUN x =

222 text "When elaborating argument" <+>

223 annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity

224− text "to function" <+> annName f <> colon <>

224+ text "to" <+> whatIsName <> annName f <> colon <>

225 indented (pprintErr' i e)

226 | otherwise =

227− text "When elaborating an application of function" <+>

227+ text "When elaborating an application of" <+> whatIsName <>

228 annName f <> colon <> indented (pprintErr' i e)

229+ where whatIsName = let ctxt = tt_ctxt i

230+ in if isTConName f ctxt

231+ then text "type constructor" <> space

232+ else if isConName f ctxt

233+ then text "constructor" <> space

234+ else if isFnName f ctxt

235+ then text "function" <> space

236+ else empty

229pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

237pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

230pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

238pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

231pprintErr' i (ReflectionError parts orig) =

239pprintErr' i (ReflectionError parts orig) =

test/basic009/expected+2−1

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

1MAIN-PASS

2Faulty.idr:6:7:When elaborating type of Faulty.fault:

3+When elaborating an application of type constructor =:

3−Can't disambiguate name: A.num, B.C.num

4+ Can't disambiguate name: A.num, B.C.num

4Multiple.idr:3:1:import alias not unique: "X"

5Multiple.idr:3:1:import alias not unique: "X"

test/error004/expected+4−2

@@ -1,4 +1,6 @@

1FunErrTest.idr:33:10:When elaborating right hand side of badCadr1:

2+When elaborating argument cons1 to function FunErrTest.cadr:

2−Could not prove that [] has at least two elements.

3+ Could not prove that [] has at least two elements.

3FunErrTest.idr:36:10:When elaborating right hand side of badCadr2:

4FunErrTest.idr:36:10:When elaborating right hand side of badCadr2:

5+When elaborating argument cons2 to function FunErrTest.cadr:

4−Could not prove that tail [(fromInteger 1)] refl has at least two elements.

6+ Could not prove that tail [(fromInteger 1)] refl has at least two elements.

test/reg034/expected+2−2

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

1reg034.idr:6:5:When elaborating left hand side of bar:

2−When elaborating an application of function main.bar:

2+When elaborating an application of main.bar:

3 Can't unify

4 [95mx[0m [94m=[0m [95mx[0m

5 with

@@ -11,7 +11,7 @@ When elaborating an application of function main.bar:

11 with

12 [92mlength[0m [95mxs[0m

13reg034.idr:9:5:When elaborating left hand side of foo:

14−When elaborating an application of function main.foo:

14+When elaborating an application of main.foo:

15 Can't unify

16 [95mx[0m [94m=[0m [95mx[0m

17 with