95960ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Separate reflected errors from multiple handlers

commit95960cebf1ed73eff49bf3017afe541a340429c2 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 10 Jan 2014, 09:52 (13 years ago) parent40da42f

4 files changed+12−7

compare with master

unifiedsplit

src/Idris/Core/TT.hs+1−1 src/Idris/Delaborate.hs+3−2 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+7−3

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

@@ -117,7 +117,7 @@ data Err = Msg String

117117 | Elaborating String Name Err

118118 | ProviderError String

119119 | LoadingFailed String Err

120− | ReflectionError [ErrorReportPart]

120+ | ReflectionError [[ErrorReportPart]] Err

121121 deriving Eq

122122{-!

123123deriving instance NFData Err

src/Idris/Delaborate.hs+3−2

@@ -192,8 +192,9 @@ pshow i (Elaborating s n e) = "When elaborating " ++ s ++

192192 showqual i n ++ ":\n" ++ pshow i e

193193pshow i (ProviderError msg) = "Type provider error: " ++ msg

194194pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e

195−pshow i (ReflectionError parts) = let parts' = map showPart parts in

196− concat (intersperse " " parts')

195+pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

196+ concat (intersperse "\n" parts') ++

197+ "\nOriginal error:\n" ++ indented (pshow i orig)

197198 where showPart :: ErrorReportPart -> String

198199 showPart (TextPart str) = str

199200 showPart (NamePart n) = let colour = idris_colourRepl i in

src/Idris/ElabDecls.hs+1−1

@@ -122,7 +122,7 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122122 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt

123123 if tyIsHandler nty'

124124 then do i <- getIState

125− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }

125+ putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }

126126 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

127127 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

128128 when corec $ do setAccessibility n Frozen

src/Idris/ElabTerm.hs+7−3

@@ -1375,11 +1375,15 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

13751375

13761376 -- Normalize error handler terms to produce the new messages

13771377 ctxt <- getContext

1378− let results = map (normalise ctxt []) (map fst handlers)

1378+ let results = map (normalise ctxt []) (map fst handlers) :: [Term]

13791379

1380+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

1381+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results) :: [[Term]]

1382+ errorparts <- mapM (mapM reifyReportPart) errorpartsTT

13801383

1381− errorparts <- mapM reifyReportPart (concat (mapMaybe unList (mapMaybe fromTTMaybe results)))

1382− return $ ReflectionError errorparts

1384+ return $ case errorparts of

1385+ [] -> e

1386+ parts -> ReflectionError errorparts e

13831387

13841388 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

13851389 fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm