@@ -20,7 +20,7 @@ import Control.Monad
20import Control.Monad.State.Strict
20import Control.Monad.State.Strict
21import Data.List
21import Data.List
22import qualified Data.Map as M
22import qualified Data.Map as M
23−import Data.Maybe (mapMaybe)
23+import Data.Maybe (mapMaybe, fromMaybe)
24import qualified Data.Set as S
24import qualified Data.Set as S
25import qualified Data.Text as T
25import qualified Data.Text as T
@@ -191,7 +191,7 @@ elab ist info pattern opts fn tm
191 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
191 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
192 ht == txt "Lazy'" = True
192 ht == txt "Lazy'" = True
193 forceErr env (Elaborating _ _ t) = forceErr env t
193 forceErr env (Elaborating _ _ t) = forceErr env t
194− forceErr env (ElaboratingArg _ _ t) = forceErr env t
194+ forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
195 forceErr env (At _ t) = forceErr env t
195 forceErr env (At _ t) = forceErr env t
196 forceErr env t = False
196 forceErr env t = False
@@ -727,10 +727,7 @@ elab ist info pattern opts fn tm
727 -> Bool -- ^ under a 'force'
727 -> Bool -- ^ under a 'force'
728 -> [(Bool, PTerm)] -- ^ (Laziness, argument)
728 -> [(Bool, PTerm)] -- ^ (Laziness, argument)
729 -> ElabD ()
729 -> ElabD ()
730− elabArgs ist ina failed fc retry f [] force _
730+ elabArgs ist ina failed fc retry f [] force _ = return ()
731−-- | retry = let (ns, ts) = unzip (reverse failed) in
732−-- elabArgs ina [] False ns ts
733− | otherwise = return ()
734 elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
731 elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
735 = elabArgs ist ina failed fc r f ns force args
732 = elabArgs ist ina failed fc r f ns force args
736 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
733 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
741 | otherwise = elabArg argName holeName t
738 | otherwise = elabArg argName holeName t
742 where elabArg argName holeName t =
739 where elabArg argName holeName t =
743 do now_elaborating fc f argName
740 do now_elaborating fc f argName
741+ wrapErr f argName $ do
744− hs <- get_holes
742+ hs <- get_holes
745− tm <- get_term
743+ tm <- get_term
746− -- No coercing under an explicit Force (or it can Force/Delay
744+ -- No coercing under an explicit Force (or it can Force/Delay
747− -- recursively!)
745+ -- recursively!)
748− let elab = if force then elab' else elabE
746+ let elab = if force then elab' else elabE
749− failed' <- -- trace (show (n, t, hs, tm)) $
747+ failed' <- -- trace (show (n, t, hs, tm)) $
750− -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
748+ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
751− case holeName `elem` hs of
749+ case holeName `elem` hs of
752− True -> do focus holeName; elab ina t; return failed
750+ True -> do focus holeName; elab ina t; return failed
753− False -> return failed
751+ False -> return failed
754− done_elaborating_arg f argName
752+ done_elaborating_arg f argName
755− elabArgs ist ina failed fc r f ns force args
753+ elabArgs ist ina failed fc r f ns force args
756−
754+ wrapErr f argName action =
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
755+ do elabState <- get
756+ while <- elaborating_app
757+ let while' = map (\(x, y, z)-> (y, z)) while
761− (result, newState) <- case runStateT action elabState of
758+ (result, newState) <- case runStateT action elabState of
762− OK (res, newState) -> return (res, newState)
759+ OK (res, newState) -> return (res, newState)
763− Error e@(ReflectionError _ _) -> (lift . tfail) e
760+ Error e -> do done_elaborating_arg f argName
764− Error e@(ReflectionFailed _ _) -> (lift . tfail) e
761+ lift (tfail (elaboratingArgErr while' e))
765− Error e -> handle e >>= lift . tfail
766− put newState
762+ put newState
767− return result
763+ return result
768− where handle :: Err -> ElabD Err
764+
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
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
780− -- Normalize error handler terms to produce the new messages
781− let ctxt = tt_ctxt ist
782− results = map (normalise ctxt []) (map fst handlers)
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
791− parts -> ReflectionError errorparts e
793-- 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
794-- any nested alternatives where that function is also at the head
767-- any nested alternatives where that function is also at the head
@@ -1631,6 +1604,14 @@ reflectErr (LoadingFailed str err) =
1631 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
1604 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
1632reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
1605reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
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)
1635withErrorReflection :: Idris a -> Idris a
1616withErrorReflection :: Idris a -> Idris a
1636withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1617withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
@@ -1646,35 +1627,50 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1646 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
1627 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
1647 err' <- handle err
1628 err' <- handle err
1648 return (Elaborating what n err')
1629 return (Elaborating what n err')
1649− handle e@(ElaboratingArg f a 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
1650− err' <- handle err
1633+ then handle err
1634+ else applyHandlers err hs
1651− return (ElaboratingArg f a err')
1635+ return (ElaboratingArg f a prev err')
1652 -- TODO: argument-specific error handlers go here for ElaboratingArg
1636 -- TODO: argument-specific error handlers go here for ElaboratingArg
1653 handle e = do ist <- getIState
1637 handle e = do ist <- getIState
1654− let err = fmap (errReverse ist) e
1655 logLvl 2 "Starting error reflection"
1638 logLvl 2 "Starting error reflection"
1656 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 " ++
1657− logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
1653+ concat (intersperse ", " (map show handlers))
1658− let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1654+ let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
1660− -- 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!
1661− handlers <- case mapM (check (tt_ctxt ist) []) reports of
1657+ handlers <- case mapM (check (tt_ctxt ist) []) reports of
1662− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1658+ Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
1663− OK hs -> return hs
1659+ OK hs -> return hs
1665− -- Normalize error handler terms to produce the new messages
1661+ -- Normalize error handler terms to produce the new messages
1666− ctxt <- getContext
1662+ ctxt <- getContext
1667− let results = map (normalise ctxt []) (map fst handlers)
1663+ let results = map (normalise ctxt []) (map fst handlers)
1668− 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))
1670− -- 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
1671− let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1667+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
1672− errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1668+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
1673− Left err -> ierror err
1669+ Left err -> ierror err
1674− Right ok -> return ok
1670+ Right ok -> return ok
1675− return $ case errorparts of
1671+ return $ case errorparts of
1676− [] -> e
1672+ [] -> e
1677− parts -> ReflectionError errorparts e
1673+ parts -> ReflectionError errorparts e
1679fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1675fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
1680fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
1676fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)