@@ -1015,7 +1015,7 @@ runTac autoSolve ist tac
10151015 runReflected t = do t' <- reify ist t
10161016 runTac autoSolve ist t'
10171017
1018−-- | Prefix a name with the "Reflection.Language" namespace
1018+-- | Prefix a name with the "Language.Reflection" namespace
10191019reflm :: String -> Name
10201020reflm n = NS (UN n) ["Reflection", "Language"]
10211021
@@ -1354,31 +1354,54 @@ reflectEnv = foldr consToEnvList emptyEnvList
13541354 [envTupleType]
13551355
13561356-- | 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+
13571367reflectErr :: Err -> Raw
1358−reflectErr (Msg msg) = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]
1359−reflectErr (InternalMsg msg) = raw_apply (Var (NS (UN "InternalMsg") ["Errors", "Reflection", "Language"])) [RConstant (Str msg)]
1368+reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [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)]
13601378reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
13611379
13621380withErrorReflection :: Idris a -> Idris a
13631381withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
13641382 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
13651387 handle e = do ist <- getIState
1388+ logLvl 2 "Starting error reflection"
13661389 let handlers = idris_errorhandlers ist
1390+ logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
13671391 let reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
13681392
13691393 -- Typecheck error handlers - if this fails, then something else was wrong earlier!
13701394 handlers <- case mapM (check (tt_ctxt ist) []) reports of
1371− Error e -> do formatted <- showErr e
1372− ierror . InternalMsg $
1373− "Type error during error reflection: " ++ formatted
1395+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
13741396 OK hs -> return hs
13751397
13761398 -- Normalize error handler terms to produce the new messages
13771399 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))
13791402
13801403 -- 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)
13821405 errorparts <- mapM (mapM reifyReportPart) errorpartsTT
13831406
13841407 return $ case errorparts of