579d242 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Cleaner failure for error reflection

579d242David Raymond Christiansen13 years ago

src/Idris/Core/TT.hs+1

compare with master

unifiedsplit

@@ -118,6 +118,7 @@ data Err = Msg String

118 | ProviderError String

119 | LoadingFailed String Err

120 | ReflectionError [[ErrorReportPart]] Err

121+ | ReflectionFailed String Err

121 deriving Eq

122 deriving Eq

122{-!

123{-!

123deriving instance NFData Err

124deriving instance NFData Err

src/Idris/Delaborate.hs+3

@@ -201,6 +201,9 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "

201 showName (Just i) [] False colour n

202 showPart (TermPart tm) = let colour = idris_colourRepl i

203 in showImp (Just i) False colour (delab i tm)

204+pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

205+ indented (pshow i err) ++

206+ "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

204

207

205

208

206showSc i [] = ""

209showSc i [] = ""

src/Idris/ElabTerm.hs+31−8

@@ -1015,7 +1015,7 @@ runTac autoSolve ist tac

1015 runReflected t = do t' <- reify ist t

1016 runTac autoSolve ist t'

1017

1018−-- | Prefix a name with the "Reflection.Language" namespace

1018+-- | Prefix a name with the "Language.Reflection" namespace

1019reflm :: String -> Name

1020reflm n = NS (UN n) ["Reflection", "Language"]

1021

@@ -1354,31 +1354,54 @@ reflectEnv = foldr consToEnvList emptyEnvList

1354 [envTupleType]

1355

1356-- | Reflect an error into the internal datatype of Idris -- TODO

1357+rawBool :: Bool -> Raw

1358+rawBool True = Var (NS (UN "True") ["Bool", "Prelude"])

1359+rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])

1360+

1361+rawNil :: Raw -> Raw

1362+rawNil ty = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"])) [ty]

1363+

1364+rawPairTy :: Raw -> Raw -> Raw

1365+rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

1366+

1357reflectErr :: Err -> Raw

1367reflectErr :: Err -> Raw

1358−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]

1368+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

1359−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]

1369+reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

1370+reflectErr (CantUnify b t1 t2 e ctxt i) =

1371+ raw_apply (Var $ reflErrName "CantUnify")

1372+ [ rawBool b

1373+ , reflect t1

1374+ , reflect t2

1375+ , reflectErr e

1376+ , rawNil $ rawPairTy (Var (reflm "TTName")) (Var (reflm "TT")) --FIXME

1377+ , RConstant (I i)]

1360reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

1378reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

1361

1379

1362withErrorReflection :: Idris a -> Idris a

1380withErrorReflection :: Idris a -> Idris a

1363withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1381withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1364 where handle :: Err -> Idris Err

1382 where handle :: Err -> Idris Err

1383+ handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"

1384+ return e -- Don't do meta-reflection of errors

1385+ handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

1386+ return e

1365 handle e = do ist <- getIState

1387 handle e = do ist <- getIState

1388+ logLvl 2 "Starting error reflection"

1366 let handlers = idris_errorhandlers ist

1389 let handlers = idris_errorhandlers ist

1390+ logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))

1367 let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

1391 let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

1368

1392

1369 -- Typecheck error handlers - if this fails, then something else was wrong earlier!

1393 -- Typecheck error handlers - if this fails, then something else was wrong earlier!

1370 handlers <- case mapM (check (tt_ctxt ist) []) reports of

1394 handlers <- case mapM (check (tt_ctxt ist) []) reports of

1371− Error e -> do formatted <- showErr e

1395+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e

1372− ierror . InternalMsg $

1373− "Type error during error reflection: " ++ formatted

1374 OK hs -> return hs

1396 OK hs -> return hs

1375

1397

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

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

1377 ctxt <- getContext

1399 ctxt <- getContext

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

1400+ let results = map (normalise ctxt []) (map fst handlers)

1401+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

1379

1402

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

1403 -- 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]]

1404+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1382 errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1405 errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1383

1406

1384 return $ case errorparts of

1407 return $ case errorparts of