fb3f7f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use At to hold FCs

commitfb3f7f09745b62eec37cfe4ace7c50da946b4b68 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 17:23 (13 years ago) parent5cee305

7 files changed+10−14

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+2−1 src/Idris/Core/TT.hs+4−4 src/Idris/Core/Unify.hs+1−1 src/Idris/Delaborate.hs+1−3 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+1−1 src/Idris/Error.hs−3

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

@@ -687,7 +687,8 @@ try' t1 t2 proofSearch

687687 r || proofSearch

688688 recoverableErr (CantSolveGoal _ _) = False

689689 recoverableErr (ProofSearchFail _) = False

690− recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

690+ recoverableErr (ElaboratingArg _ _ e) = recoverableErr e

691+ recoverableErr (At _ e) = recoverableErr e

691692 recoverableErr _ = True

692693

693694tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

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

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

140140 | NoRewriting t

141141 | At FC (Err' t)

142142 | Elaborating String Name (Err' t)

143− | ElaboratingArg FC Name Name (Err' t)

143+ | ElaboratingArg Name Name (Err' t)

144144 | ProviderError String

145145 | LoadingFailed String (Err' t)

146146 | ReflectionError [[ErrorReportPart]] (Err' t)

@@ -171,7 +171,7 @@ instance Sized Err where

171171 size ProgramLineComment = 1

172172 size (At fc err) = size fc + size err

173173 size (Elaborating _ n err) = size err

174− size (ElaboratingArg _ _ _ err) = size err

174+ size (ElaboratingArg _ _ err) = size err

175175 size (ProviderError msg) = length msg

176176 size (LoadingFailed fn e) = 1 + length fn + size e

177177 size _ = 1

@@ -196,8 +196,8 @@ instance Show Err where

196196 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

197197 show ProgramLineComment = "Program line next to comment"

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

199− show (ElaboratingArg fc f x e) = show fc ++ ": Elaborating " ++ show f ++ " arg " ++

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

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

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

201201 show _ = "Error"

202202

203203instance Pretty Err OutputAnnotation where

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

@@ -41,7 +41,7 @@ data UResult a = UOK a

4141cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t

4242cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

4343cantUnify (FailContext fc f x : _) r t1 t2 e ctxt i =

44− ElaboratingArg fc f x (CantUnify r t1 t2 e ctxt i)

44+ At fc (ElaboratingArg f x (CantUnify r t1 t2 e ctxt i))

4545

4646-- Solve metavariables by matching terms against each other

4747-- Not really unification, of course!

src/Idris/Delaborate.hs+1−3

@@ -217,15 +217,13 @@ pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr

217217pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

218218 annName' n (showqual i n) <> colon <$>

219219 pprintErr' i e

220−pprintErr' i (ElaboratingArg fc f x e)

220+pprintErr' i (ElaboratingArg f x e)

221221 | isUN x =

222− annotate (AnnFC fc) (text (show fc)) <> colon <+>

223222 text "When elaborating argument" <+>

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

225224 text "to function" <+> annName f <> colon <>

226225 indented (pprintErr' i e)

227226 | otherwise =

228− annotate (AnnFC fc) (text (show fc)) <> colon <+>

229227 text "When elaborating an application of function" <+>

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

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

src/Idris/ElabDecls.hs+1−1

@@ -1279,7 +1279,7 @@ checkPossible info fc tcgen fname lhs_in

12791279 impossibleError (CantConvert _ _ _) = False

12801280 impossibleError (At _ e) = impossibleError e

12811281 impossibleError (Elaborating _ _ e) = impossibleError e

1282− impossibleError (ElaboratingArg _ _ _ e) = impossibleError e

1282+ impossibleError (ElaboratingArg _ _ e) = impossibleError e

12831283 impossibleError _ = True

12841284

12851285 sameFam topx topy

src/Idris/ElabTerm.hs+1−1

@@ -189,7 +189,7 @@ elab ist info pattern opts fn tm

189189 | (P _ (UN ht) _, _) <- unApply t,

190190 ht == txt "Lazy" = True

191191 forceErr (Elaborating _ _ t) = forceErr t

192− forceErr (ElaboratingArg _ _ _ t) = forceErr t

192+ forceErr (ElaboratingArg _ _ t) = forceErr t

193193 forceErr (At _ t) = forceErr t

194194 forceErr t = False

195195

src/Idris/Error.hs−3

@@ -57,8 +57,6 @@ ierror = throwError

5757tclift :: TC a -> Idris a

5858tclift (OK v) = return v

5959tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

60−tclift (Error err@(ElaboratingArg fc _ _ e)) = do setErrSpan fc

61− throwError err

6260tclift (Error err) = throwError err

6361

6462tctry :: TC a -> TC a -> Idris a

@@ -69,5 +67,4 @@ tctry tc1 tc2

6967

7068getErrSpan :: Err -> FC

7169getErrSpan (At fc _) = fc

72−getErrSpan (ElaboratingArg fc _ _ e) = fc

7370getErrSpan _ = emptyFC