f01873f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add stack of elaboration context to ElaboratingArg

This is for argument-specific error reflection.

commitf01873f27d8718982e2234f2649e2354819f74dd authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 21 Mar 2014, 16:06 (13 years ago) parent7f3d436

6 files changed+15−13

compare with master

unifiedsplit

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

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

@@ -687,7 +687,7 @@ 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

691691 recoverableErr (At _ e) = recoverableErr e

692692 recoverableErr _ = True

693693

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 Name Name (Err' t)

143+ | ElaboratingArg Name Name [(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 f x e) = "Elaborating " ++ show f ++ " arg " ++

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

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

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

201201 show _ = "Error"

202202

203203instance Pretty Err OutputAnnotation where

src/Idris/Core/Unify.hs+4−2

@@ -40,8 +40,10 @@ data UResult a = UOK a

4040-- | Smart constructor for unification errors that takes into account the FailContext

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

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

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

43+cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

44+ At fc (ElaboratingArg f x

45+ (map (\(FailContext _ f' x') -> (f', x')) prev)

46+ (CantUnify r t1 t2 e ctxt i))

4547

4648-- Solve metavariables by matching terms against each other

4749-- Not really unification, of course!

src/Idris/Delaborate.hs+1−1

@@ -217,7 +217,7 @@ 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 f x e)

220+pprintErr' i (ElaboratingArg f x _ e)

221221 | isUN x =

222222 text "When elaborating argument" <+>

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

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+4−4

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

@@ -1643,9 +1643,9 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

16431643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

16441644 err' <- handle err

16451645 return (Elaborating what n err')

1646− handle e@(ElaboratingArg f a err) = do logLvl 3 "Reflecting body of ElaboratingArg"

1647− err' <- handle err

1648− return (ElaboratingArg f a err')

1646+ handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

1647+ err' <- handle err

1648+ return (ElaboratingArg f a prev err')

16491649 -- TODO: argument-specific error handlers go here for ElaboratingArg

16501650 handle e = do ist <- getIState

16511651 let err = fmap (errReverse ist) e