@@ -763,42 +763,6 @@ elab ist info pattern opts fn tm
763763 return result
764764
765765
766−-- | Perform error reflection for function applicaitons with specific error handlers
767−reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a
768−reflectFunctionErrors ist f arg action =
769− do elabState <- get
770− (result, newState) <- case runStateT action elabState of
771− OK (res, newState) -> return (res, newState)
772− Error e@(ReflectionError _ _) -> (lift . tfail) e
773− Error e@(ReflectionFailed _ _) -> (lift . tfail) e
774− Error e -> handle e >>= lift . tfail
775− put newState
776− return result
777− where handle :: Err -> ElabD Err
778− handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist
779− handlers = (maybe [] S.toList . M.lookup arg) funhandlers
780− reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
781−
782−
783− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
784− handlers <- case mapM (check (tt_ctxt ist) []) reports of
785− Error e -> lift . tfail $
786− ReflectionFailed "Type error while constructing reflected error" e
787− OK hs -> return hs
788−
789− -- Normalize error handler terms to produce the new messages
790− let ctxt = tt_ctxt ist
791− results = map (normalise ctxt []) (map fst handlers)
792−
793− -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
794− let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
795− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
796− Left err -> lift (tfail err)
797− Right ok -> return ok
798− return $ case errorparts of
799− [] -> e
800− parts -> ReflectionError errorparts e
801−
802766-- For every alternative, look at the function at the head. Automatically resolve
803767-- any nested alternatives where that function is also at the head
804768
@@ -1664,34 +1628,49 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
16641628 err' <- handle err
16651629 return (Elaborating what n err')
16661630 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1667− err' <- handle err
1631+ hs <- getFnHandlers f a
1632+ err' <- if null hs
1633+ then handle err
1634+ else applyHandlers err hs
16681635 return (ElaboratingArg f a prev err')
16691636 -- TODO: argument-specific error handlers go here for ElaboratingArg
16701637 handle e = do ist <- getIState
1671− let err = fmap (errReverse ist) e
16721638 logLvl 2 "Starting error reflection"
16731639 let handlers = idris_errorhandlers ist
1674− logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1675− let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1676−
1677− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1678− handlers <- case mapM (check (tt_ctxt ist) []) reports of
1679− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1680− OK hs -> return hs
1681−
1682− -- Normalize error handler terms to produce the new messages
1683− ctxt <- getContext
1684− let results = map (normalise ctxt []) (map fst handlers)
1685− logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1686−
1687− -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1688− let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1689− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1690− Left err -> ierror err
1691− Right ok -> return ok
1692− return $ case errorparts of
1693− [] -> e
1694− parts -> ReflectionError errorparts e
1640+ applyHandlers e handlers
1641+ getFnHandlers :: Name -> Name -> Idris [Name]
1642+ getFnHandlers f arg = do ist <- getIState
1643+ let funHandlers = maybe M.empty id .
1644+ lookupCtxtExact f .
1645+ idris_function_errorhandlers $ ist
1646+ return . maybe [] S.toList . M.lookup arg $ funHandlers
1647+
1648+
1649+ applyHandlers e handlers =
1650+ do ist <- getIState
1651+ let err = fmap (errReverse ist) e
1652+ logLvl 3 $ "Using reflection handlers " ++
1653+ concat (intersperse ", " (map show handlers))
1654+ let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1655+
1656+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1657+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1658+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1659+ OK hs -> return hs
1660+
1661+ -- Normalize error handler terms to produce the new messages
1662+ ctxt <- getContext
1663+ let results = map (normalise ctxt []) (map fst handlers)
1664+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1665+
1666+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1667+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1668+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1669+ Left err -> ierror err
1670+ Right ok -> return ok
1671+ return $ case errorparts of
1672+ [] -> e
1673+ parts -> ReflectionError errorparts e
16951674
16961675fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
16971676fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)