@@ -763,42 +763,6 @@ elab ist info pattern opts fn tm
763 return result
763 return result
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 =
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
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
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
789− -- Normalize error handler terms to produce the new messages
790− let ctxt = tt_ctxt ist
791− results = map (normalise ctxt []) (map fst handlers)
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
800− parts -> ReflectionError errorparts e
802-- For every alternative, look at the function at the head. Automatically resolve
766-- For every alternative, look at the function at the head. Automatically resolve
803-- any nested alternatives where that function is also at the head
767-- any nested alternatives where that function is also at the head
@@ -1664,34 +1628,49 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1664 err' <- handle err
1628 err' <- handle err
1665 return (Elaborating what n err')
1629 return (Elaborating what n err')
1666 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1630 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1631+ hs <- getFnHandlers f a
1667− err' <- handle err
1633+ then handle err
1634+ else applyHandlers err hs
1668 return (ElaboratingArg f a prev err')
1635 return (ElaboratingArg f a prev err')
1669 -- TODO: argument-specific error handlers go here for ElaboratingArg
1636 -- TODO: argument-specific error handlers go here for ElaboratingArg
1670 handle e = do ist <- getIState
1637 handle e = do ist <- getIState
1671− let err = fmap (errReverse ist) e
1672 logLvl 2 "Starting error reflection"
1638 logLvl 2 "Starting error reflection"
1673 let handlers = idris_errorhandlers ist
1639 let handlers = idris_errorhandlers ist
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
1649+ applyHandlers e handlers =
1650+ do ist <- getIState
1651+ let err = fmap (errReverse ist) e
1652+ logLvl 3 $ "Using reflection handlers " ++
1674− logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1653+ concat (intersperse ", " (map show handlers))
1675− let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1654+ let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1677− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1656+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1678− handlers <- case mapM (check (tt_ctxt ist) []) reports of
1657+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1679− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1658+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1680− OK hs -> return hs
1659+ OK hs -> return hs
1682− -- Normalize error handler terms to produce the new messages
1661+ -- Normalize error handler terms to produce the new messages
1683− ctxt <- getContext
1662+ ctxt <- getContext
1684− let results = map (normalise ctxt []) (map fst handlers)
1663+ let results = map (normalise ctxt []) (map fst handlers)
1685− logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1664+ logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1687− -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1666+ -- 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)
1667+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1689− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1668+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1690− Left err -> ierror err
1669+ Left err -> ierror err
1691− Right ok -> return ok
1670+ Right ok -> return ok
1692− return $ case errorparts of
1671+ return $ case errorparts of
1693− [] -> e
1672+ [] -> e
1694− parts -> ReflectionError errorparts e
1673+ parts -> ReflectionError errorparts e
1696fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1675fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1697fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
1676fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)