@@ -20,7 +20,7 @@ import Control.Monad
2020import Control.Monad.State.Strict
2121import Data.List
2222import qualified Data.Map as M
23−import Data.Maybe (mapMaybe)
23+import Data.Maybe (mapMaybe, fromMaybe)
2424import qualified Data.Set as S
2525import qualified Data.Text as T
2626
@@ -191,7 +191,7 @@ elab ist info pattern opts fn tm
191191 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
192192 ht == txt "Lazy'" = True
193193 forceErr env (Elaborating _ _ t) = forceErr env t
194− forceErr env (ElaboratingArg _ _ t) = forceErr env t
194+ forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
195195 forceErr env (At _ t) = forceErr env t
196196 forceErr env t = False
197197
@@ -727,10 +727,7 @@ elab ist info pattern opts fn tm
727727 -> Bool -- ^ under a 'force'
728728 -> [(Bool, PTerm)] -- ^ (Laziness, argument)
729729 -> ElabD ()
730− elabArgs ist ina failed fc retry f [] force _
731−-- | retry = let (ns, ts) = unzip (reverse failed) in
732−-- elabArgs ina [] False ns ts
733− | otherwise = return ()
730+ elabArgs ist ina failed fc retry f [] force _ = return ()
734731 elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
735732 = elabArgs ist ina failed fc r f ns force args
736733 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
@@ -741,54 +738,30 @@ elab ist info pattern opts fn tm
741738 | otherwise = elabArg argName holeName t
742739 where elabArg argName holeName t =
743740 do now_elaborating fc f argName
744− hs <- get_holes
745− tm <- get_term
746− -- No coercing under an explicit Force (or it can Force/Delay
747− -- recursively!)
748− let elab = if force then elab' else elabE
749− failed' <- -- trace (show (n, t, hs, tm)) $
750− -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
751− case holeName `elem` hs of
752− True -> do focus holeName; elab ina t; return failed
753− False -> return failed
754− done_elaborating_arg f argName
755− elabArgs ist ina failed fc r f ns force args
756−
757−-- | Perform error reflection for function applicaitons with specific error handlers
758−reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a
759−reflectFunctionErrors ist f arg action =
760− do elabState <- get
761− (result, newState) <- case runStateT action elabState of
762− OK (res, newState) -> return (res, newState)
763− Error e@(ReflectionError _ _) -> (lift . tfail) e
764− Error e@(ReflectionFailed _ _) -> (lift . tfail) e
765− Error e -> handle e >>= lift . tfail
766− put newState
767− return result
768− where handle :: Err -> ElabD Err
769− handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist
770− handlers = (maybe [] S.toList . M.lookup arg) funhandlers
771− reports = map (\n -> RApp (Var n) (reflectErr e)) handlers
772−
773−
774− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
775− handlers <- case mapM (check (tt_ctxt ist) []) reports of
776− Error e -> lift . tfail $
777− ReflectionFailed "Type error while constructing reflected error" e
778− OK hs -> return hs
779−
780− -- Normalize error handler terms to produce the new messages
781− let ctxt = tt_ctxt ist
782− results = map (normalise ctxt []) (map fst handlers)
783−
784− -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
785− let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
786− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
787− Left err -> lift (tfail err)
788− Right ok -> return ok
789− return $ case errorparts of
790− [] -> e
791− parts -> ReflectionError errorparts e
741+ wrapErr f argName $ do
742+ hs <- get_holes
743+ tm <- get_term
744+ -- No coercing under an explicit Force (or it can Force/Delay
745+ -- recursively!)
746+ let elab = if force then elab' else elabE
747+ failed' <- -- trace (show (n, t, hs, tm)) $
748+ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
749+ case holeName `elem` hs of
750+ True -> do focus holeName; elab ina t; return failed
751+ False -> return failed
752+ done_elaborating_arg f argName
753+ elabArgs ist ina failed fc r f ns force args
754+ wrapErr f argName action =
755+ do elabState <- get
756+ while <- elaborating_app
757+ let while' = map (\(x, y, z)-> (y, z)) while
758+ (result, newState) <- case runStateT action elabState of
759+ OK (res, newState) -> return (res, newState)
760+ Error e -> do done_elaborating_arg f argName
761+ lift (tfail (elaboratingArgErr while' e))
762+ put newState
763+ return result
764+
792765
793766-- For every alternative, look at the function at the head. Automatically resolve
794767-- any nested alternatives where that function is also at the head
@@ -1631,6 +1604,14 @@ reflectErr (LoadingFailed str err) =
16311604 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
16321605reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
16331606
1607+elaboratingArgErr :: [(Name, Name)] -> Err -> Err
1608+elaboratingArgErr [] err = err
1609+elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
1610+ where rewrite (ElaboratingArg _ _ _ _) = Nothing
1611+ rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
1612+ rewrite (At fc e) = fmap (At fc) (rewrite e)
1613+ rewrite err = Just (ElaboratingArg f x during err)
1614+
16341615
16351616withErrorReflection :: Idris a -> Idris a
16361617withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
@@ -1646,35 +1627,50 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
16461627 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
16471628 err' <- handle err
16481629 return (Elaborating what n err')
1649− handle e@(ElaboratingArg f a err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1650− err' <- handle err
1651− return (ElaboratingArg f a err')
1630+ handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
1631+ hs <- getFnHandlers f a
1632+ err' <- if null hs
1633+ then handle err
1634+ else applyHandlers err hs
1635+ return (ElaboratingArg f a prev err')
16521636 -- TODO: argument-specific error handlers go here for ElaboratingArg
16531637 handle e = do ist <- getIState
1654− let err = fmap (errReverse ist) e
16551638 logLvl 2 "Starting error reflection"
16561639 let handlers = idris_errorhandlers ist
1657− logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1658− let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1659−
1660− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
1661− handlers <- case mapM (check (tt_ctxt ist) []) reports of
1662− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1663− OK hs -> return hs
1664−
1665− -- Normalize error handler terms to produce the new messages
1666− ctxt <- getContext
1667− let results = map (normalise ctxt []) (map fst handlers)
1668− logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
1669−
1670− -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
1671− let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1672− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1673− Left err -> ierror err
1674− Right ok -> return ok
1675− return $ case errorparts of
1676− [] -> e
1677− 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
16781674
16791675fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
16801676fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)