0ab30e7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Restrict error reflection scope to one argument

0ab30e7David Raymond Christiansen13 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -309,6 +309,9 @@ Extra-source-files:

309 test/test037/run

310 test/test037/expected

311 test/test037/*.idr

312+ test/test038/run

313+ test/test038/expected

314+ test/test038/*.idr

312

315

313source-repository head

316source-repository head

314 type: git

317 type: git

src/Idris/AbsSyntax.hs+18−8

@@ -25,6 +25,7 @@ import Data.List

25import Data.Char

26import qualified Data.Text as T

27import Data.Either

28+import qualified Data.Map as M

28import Data.Maybe

29import Data.Maybe

29import qualified Data.Set as S

30import qualified Data.Set as S

30import Data.Word (Word)

31import Data.Word (Word)

@@ -149,14 +150,23 @@ addToCG n cg

149 = do i <- getIState

150 = do i <- getIState

150 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

151 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

151

152

152−-- | Adds hs as error handlers for n. If n is ambiguous, all matching ns are updated.

153+-- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.

153−addFunctionErrorHandlers :: Name -> [Name] -> Idris ()

154+addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

154−addFunctionErrorHandlers n hs = do i <- getIState

155+addFunctionErrorHandlers f arg hs =

156+ do i <- getIState

155− let currentHandlers = idris_function_errorhandlers i

157+ let oldHandlers = idris_function_errorhandlers i

156− let newHandlers = updateDef n

158+ let newHandlers = flip (addDef f) oldHandlers $

157− (\handlers -> handlers `S.union` S.fromList hs)

159+ case lookupCtxtExact f oldHandlers of

158− currentHandlers

160+ Nothing -> M.singleton arg (S.fromList hs)

161+ Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers

162+ -- will always be one of those two, thus no extra case

159− putIState $ i { idris_function_errorhandlers = newHandlers }

163+ putIState $ i { idris_function_errorhandlers = newHandlers }

164+

165+getFunctionErrorHandlers :: Name -> Name -> Idris [Name]

166+getFunctionErrorHandlers f arg = do i <- getIState

167+ return . maybe [] S.toList $

168+ undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)

169+

160

170

161-- Trace all the names in a call graph starting at the given name

171-- Trace all the names in a call graph starting at the given name

162getAllNames :: Name -> Idris [Name]

172getAllNames :: Name -> Idris [Name]

src/Idris/AbsSyntaxTree.hs+2−1

@@ -24,6 +24,7 @@ import Control.Monad.Trans.Error

25import Data.List

26import Data.Char

27+import qualified Data.Map as M

27import qualified Data.Text as T

28import qualified Data.Text as T

28import Data.Either

29import Data.Either

29import qualified Data.Set as S

30import qualified Data.Set as S

@@ -136,7 +137,7 @@ data IState = IState {

136 idris_outh :: Handle,

137 idris_outh :: Handle,

137 idris_errorhandlers :: [Name], -- ^ Global error handlers

138 idris_errorhandlers :: [Name], -- ^ Global error handlers

138 idris_nameIdx :: (Int, Ctxt (Int, Name)),

139 idris_nameIdx :: (Int, Ctxt (Int, Name)),

139− idris_function_errorhandlers :: Ctxt (S.Set Name) -- ^ Specific error handlers

140+ idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers

140 }

141 }

141

142

142data SizeChange = Smaller | Same | Bigger | Unknown

143data SizeChange = Smaller | Same | Bigger | Unknown

src/Idris/Core/Elaborate.hs+18−13

@@ -401,8 +401,11 @@ qed = do processTactic' QED

401undo :: Elab' aux ()

402undo = processTactic' Undo

403

404+-- | Prepare to apply a function by creating holes to be filled by the arguments

404−prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]

405+prepare_apply :: Raw -- ^ The operation being applied

406+ -> [Bool] -- ^ Whether arguments are implicit

407+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes to be filled with elaborated argument values

405−prepare_apply fn imps =

408+prepare_apply fn imps =

406 do ty <- get_type fn

409 do ty <- get_type fn

407 ctxt <- get_context

410 ctxt <- get_context

408 env <- get_env

411 env <- get_env

@@ -414,11 +417,13 @@ prepare_apply fn imps =

414 let n = length (filter not imps)

417 let n = length (filter not imps)

415 let (h : hs) = holes p

418 let (h : hs) = holes p

416 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

419 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

417−-- case claims of

418−-- [] -> return ()

419−-- (h : _) -> reorder_claims h

420 return $! claims

421 where

422+ mkClaims :: Type -- ^ The type of the operation being applied

423+ -> [Bool] -- ^ Whether the arguments are implicit

424+ -> [(Name, Name)] -- ^ Accumulator for produced claims

425+ -> [Name] -- ^ Hypotheses

426+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

422 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

427 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

423 do let t = rebind hs t_in

428 do let t = rebind hs t_in

424 n <- getNameFrom (mkMN n')

429 n <- getNameFrom (mkMN n')

@@ -427,7 +432,7 @@ prepare_apply fn imps =

427-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

432-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

428 claim n (forget t)

433 claim n (forget t)

429 when i (movelast n)

434 when i (movelast n)

430− mkClaims sc' is (n : claims) hs

435+ mkClaims sc' is ((n', n) : claims) hs

431 mkClaims t [] claims _ = return $! (reverse claims)

436 mkClaims t [] claims _ = return $! (reverse claims)

432 mkClaims _ _ _ _

437 mkClaims _ _ _ _

433 | Var n <- fn

438 | Var n <- fn

@@ -452,11 +457,11 @@ prepare_apply fn imps =

452 rebind hs (App f a) = App (rebind hs f) (rebind hs a)

457 rebind hs (App f a) = App (rebind hs f) (rebind hs a)

453 rebind hs t = t

458 rebind hs t = t

454

459

455−apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

460+apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

456apply = apply' fill

461apply = apply' fill

457match_apply = apply' match_fill

462match_apply = apply' match_fill

458

463

459−apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

464+apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

460apply' fillt fn imps =

465apply' fillt fn imps =

461 do args <- prepare_apply fn (map fst imps)

466 do args <- prepare_apply fn (map fst imps)

462 -- _Don't_ solve the arguments we're specifying by hand.

467 -- _Don't_ solve the arguments we're specifying by hand.

@@ -468,7 +473,7 @@ apply' fillt fn imps =

468 let dont = head hs : dontunify p ++

473 let dont = head hs : dontunify p ++

469 if null imps then [] -- do all we can

474 if null imps then [] -- do all we can

470 else

475 else

471− map fst (filter (not.snd) (zip args (map fst imps)))

476+ map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

472 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

477 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

473 unified p

478 unified p

474 let unify = -- trace ("Not done " ++ show hs) $

479 let unify = -- trace ("Not done " ++ show hs) $

@@ -477,10 +482,10 @@ apply' fillt fn imps =

477 keepGiven dont hunis hs

482 keepGiven dont hunis hs

478 put (ES (p { dontunify = dont, unified = (n, unify),

483 put (ES (p { dontunify = dont, unified = (n, unify),

479 notunified = notunify ++ notunified p }, a) s prev)

484 notunified = notunify ++ notunified p }, a) s prev)

480− fillt (raw_apply fn (map Var args))

485+ fillt (raw_apply fn (map (Var . snd) args))

481-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

486-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

482 end_unify

487 end_unify

483− return $! (map (updateUnify unify) args)

488+ return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

484 where updateUnify us n = case lookup n us of

489 where updateUnify us n = case lookup n us of

485 Just (P _ t _) -> t

490 Just (P _ t _) -> t

486 _ -> n

491 _ -> n

@@ -488,8 +493,8 @@ apply' fillt fn imps =

488apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

493apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

489apply2 fn elabs =

494apply2 fn elabs =

490 do args <- prepare_apply fn (map isJust elabs)

495 do args <- prepare_apply fn (map isJust elabs)

491− fill (raw_apply fn (map Var args))

496+ fill (raw_apply fn (map (Var . snd) args))

492− elabArgs args elabs

497+ elabArgs (map snd args) elabs

493 ES (p, a) s prev <- get

498 ES (p, a) s prev <- get

494 let (n, hs) = unified p

499 let (n, hs) = unified p

495 end_unify

500 end_unify

src/Idris/ElabTerm.hs+90−52

@@ -13,10 +13,14 @@ import Idris.Core.TT

13import Idris.Core.Evaluate

14import Idris.Core.Typecheck (check)

16+import Control.Applicative ((<$>))

16import Control.Monad

17import Control.Monad

17import Control.Monad.State.Strict

18import Control.Monad.State.Strict

18import Data.List

19import Data.List

20+import qualified Data.Map as M

19import Data.Maybe (mapMaybe)

21import Data.Maybe (mapMaybe)

22+import qualified Data.Set as S

23+import qualified Data.Text as T

21import Debug.Trace

25import Debug.Trace

@@ -396,7 +400,7 @@ elab ist info pattern opts fn tm

396 solve

400 solve

397 elab' (_, _, inty) (PApp fc (PRef _ f) args')

401 elab' (_, _, inty) (PApp fc (PRef _ f) args')

398 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

402 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

399− = lift $ tfail (Msg "Typecase is not allowed")

403+ = lift $ tfail (Msg "Typecase is not allowed")

400 -- if f is local, just do a simple_app

404 -- if f is local, just do a simple_app

401 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

405 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

402 = do env <- get_env

406 = do env <- get_env

@@ -419,12 +423,14 @@ elab ist info pattern opts fn tm

419 _ -> mapM_ setInjective (map getTm args)

423 _ -> mapM_ setInjective (map getTm args)

420 ctxt <- get_context

424 ctxt <- get_context

421 let guarded = isConName f ctxt

425 let guarded = isConName f ctxt

426+-- trace ("args is " ++ show args) $ return ()

422 ns <- apply (Var f) (map isph args)

427 ns <- apply (Var f) (map isph args)

428+-- trace ("ns is " ++ show ns) $ return ()

423 -- Sort so that the implicit tactics and alternatives go last

429 -- Sort so that the implicit tactics and alternatives go last

424 let (ns', eargs) = unzip $

430 let (ns', eargs) = unzip $

425 sortBy cmpArg (zip ns args)

431 sortBy cmpArg (zip ns args)

426− elabArgs (ina || not isinf, guarded, inty)

432+ elabArgs ist (ina || not isinf, guarded, inty)

427− [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

433+ [] fc False f ns' (map (\x -> (lazyarg x, getTm x)) eargs)

428 solve

434 solve

429 ivs' <- get_instances

435 ivs' <- get_instances

430 -- Attempt to resolve any type classes which have 'complete' types,

436 -- Attempt to resolve any type classes which have 'complete' types,

@@ -613,45 +619,73 @@ elab ist info pattern opts fn tm

613 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

619 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

614

620

615 -- | Elaborate the arguments to a function

621 -- | Elaborate the arguments to a function

622+ elabArgs :: IState -- ^ The current Idris state

616− elabArgs :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

623+ -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

617 -> [Bool]

624 -> [Bool]

618 -> FC -- ^ Source location

625 -> FC -- ^ Source location

619 -> Bool

626 -> Bool

620− -> [Name] -- ^ Names of arguments - these identify the holes to be filled

627+ -> Name -- ^ Name of the function being applied

628+ -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

621 -> [(Bool, PTerm)] -- ^ (Laziness, argument)

629 -> [(Bool, PTerm)] -- ^ (Laziness, argument)

622 -> ElabD ()

630 -> ElabD ()

623− elabArgs ina failed fc retry [] _

631+ elabArgs ist ina failed fc retry f [] _

624-- | retry = let (ns, ts) = unzip (reverse failed) in

632-- | retry = let (ns, ts) = unzip (reverse failed) in

625-- elabArgs ina [] False ns ts

633-- elabArgs ina [] False ns ts

626 | otherwise = return ()

634 | otherwise = return ()

627− elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args)

635+ elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args)

628− = elabArgs ina failed fc r ns args

636+ = elabArgs ist ina failed fc r f ns args

629− elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

637+ elabArgs ist ina failed fc r f ((argName, holeName):ns) ((lazy, t) : args)

630 | lazy && not pattern

638 | lazy && not pattern

631− = do elabArg n (PApp bi (PRef bi (sUN "lazy"))

639+ = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

632− [pimp (sUN "a") Placeholder True,

640+ [pimp (sUN "a") Placeholder True,

633− pexp t]);

641+ pexp t])

634− | otherwise = elabArg n t

642+ | otherwise = elabArg argName holeName t

635− where elabArg n t

643+ where elabArg argName holeName t =

644+ reflectFunctionErrors ist f argName $

636− = do hs <- get_holes

645+ do hs <- get_holes

637− tm <- get_term

646+ tm <- get_term

638− failed' <- -- trace (show (n, t, hs, tm)) $

647+ failed' <- -- trace (show (n, t, hs, tm)) $

639− -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

648+ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

640− case n `elem` hs of

649+ case holeName `elem` hs of

641− True -> do focus n; elabE ina t; return failed

650+ True -> do focus holeName; elabE ina t; return failed

642− False -> return failed

651+ False -> return failed

643− elabArgs ina failed fc r ns args

652+ elabArgs ist ina failed fc r f ns args

644−

653+

645−-- | Perform error reflection for functions with specific error handlers

654+-- | Perform error reflection for function applicaitons with specific error handlers

646−reflectFunctionErrors :: IState -> Name -> ElabD a -> ElabD a

655+reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a

647−reflectFunctionErrors ist f action =

656+reflectFunctionErrors ist f arg action =

648 do elabState <- get

657 do elabState <- get

649 (result, newState) <- case runStateT action elabState of

658 (result, newState) <- case runStateT action elabState of

650 OK (res, newState) -> return (res, newState)

659 OK (res, newState) -> return (res, newState)

651− Error e -> lift (tfail e) -- TODO: actual error reflection!

660+ Error e@(ReflectionError _ _) -> (lift . tfail) e

661+ Error e@(ReflectionFailed _ _) -> (lift . tfail) e

662+ Error e -> handle e >>= lift . tfail

652 put newState

663 put newState

653 return result

664 return result

665+ where handle :: Err -> ElabD Err

666+ handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist

667+ handlers = (maybe [] S.toList . M.lookup arg) funhandlers

668+ reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

669+

670+

671+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!

672+ handlers <- case mapM (check (tt_ctxt ist) []) reports of

673+ Error e -> lift . tfail $

674+ ReflectionFailed "Type error while constructing reflected error" e

675+ OK hs -> return hs

654

676

677+ -- Normalize error handler terms to produce the new messages

678+ let ctxt = tt_ctxt ist

679+ results = map (normalise ctxt []) (map fst handlers)

680+

681+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

682+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

683+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

684+ Left err -> lift (tfail err)

685+ Right ok -> return ok

686+ return $ case errorparts of

687+ [] -> e

688+ parts -> ReflectionError errorparts e

655

689

656-- For every alternative, look at the function at the head. Automatically resolve

690-- For every alternative, look at the function at the head. Automatically resolve

657-- any nested alternatives where that function is also at the head

691-- any nested alternatives where that function is also at the head

@@ -788,8 +822,8 @@ resolveTC depth topg fn ist

788 [args] -> map isImp (snd args) -- won't be overloaded!

822 [args] -> map isImp (snd args) -- won't be overloaded!

789 ps <- get_probs

823 ps <- get_probs

790 tm <- get_term

824 tm <- get_term

791− args <- try' (apply (Var n) imps)

825+ args <- map snd <$> try' (apply (Var n) imps)

792− (match_apply (Var n) imps) True

826+ (match_apply (Var n) imps) True

793 ps' <- get_probs

827 ps' <- get_probs

794 when (length ps < length ps') $ fail "Can't apply type class"

828 when (length ps < length ps') $ fail "Can't apply type class"

795-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

829-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

@@ -802,7 +836,7 @@ resolveTC depth topg fn ist

802 -- if there's any arguments left, we've failed to resolve

836 -- if there's any arguments left, we've failed to resolve

803 hs <- get_holes

837 hs <- get_holes

804 ulog <- getUnifyLog

838 ulog <- getUnifyLog

805− solve

839+ solve

806 traceWhen ulog ("Got " ++ show n) $ return ()

840 traceWhen ulog ("Got " ++ show n) $ return ()

807 where isImp (PImp p _ _ _ _ _) = (True, p)

841 where isImp (PImp p _ _ _ _ _) = (True, p)

808 isImp arg = (False, priority arg)

842 isImp arg = (False, priority arg)

@@ -1487,6 +1521,7 @@ reflectErr (LoadingFailed str err) =

1487 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

1521 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

1488reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

1522reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

1489

1523

1524+

1490withErrorReflection :: Idris a -> Idris a

1525withErrorReflection :: Idris a -> Idris a

1491withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1526withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1492 where handle :: Err -> Idris Err

1527 where handle :: Err -> Idris Err

@@ -1512,47 +1547,50 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1512

1547

1513 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

1548 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

1514 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1549 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1515− errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1550+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

1516−

1551+ Left err -> ierror err

1552+ Right ok -> return ok

1517 return $ case errorparts of

1553 return $ case errorparts of

1518 [] -> e

1554 [] -> e

1519 parts -> ReflectionError errorparts e

1555 parts -> ReflectionError errorparts e

1520

1556

1521− fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1557+fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1522− fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1558+fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1523− | just == txt "Just" = Just tm

1559+ | just == txt "Just" = Just tm

1524− fromTTMaybe x = Nothing

1560+fromTTMaybe x = Nothing

1525

1561

1526reflErrName :: String -> Name

1562reflErrName :: String -> Name

1527reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

1563reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

1528

1564

1565+-- | Attempt to reify a report part from TT to the internal

1566+-- representation. Not in Idris or ElabD monads because it should be usable

1567+-- from either.

1529−reifyReportPart :: Term -> Idris ErrorReportPart

1568+reifyReportPart :: Term -> Either Err ErrorReportPart

1530reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

1569reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

1531− return (TextPart msg)

1570+ Right (TextPart msg)

1532reifyReportPart (App (P (DCon _ _) n _) ttn)

1571reifyReportPart (App (P (DCon _ _) n _) ttn)

1533 | n == reflErrName "NamePart" =

1572 | n == reflErrName "NamePart" =

1534 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

1573 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

1535− Error e -> ierror . InternalMsg $

1574+ Error e -> Left . InternalMsg $

1536 "could not reify name term " ++

1575 "could not reify name term " ++

1537 show ttn ++

1576 show ttn ++

1538 " when reflecting an error"

1577 " when reflecting an error"

1539− OK (n', _)-> return $ NamePart n'

1578+ OK (n', _)-> Right $ NamePart n'

1540reifyReportPart (App (P (DCon _ _) n _) tm)

1579reifyReportPart (App (P (DCon _ _) n _) tm)

1541 | n == reflErrName "TermPart" =

1580 | n == reflErrName "TermPart" =

1542− do ist <- getIState

1543− case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1581+ case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1544− Error e -> ierror . InternalMsg $

1582+ Error e -> Left . InternalMsg $

1545− "could not reify reflected term " ++

1583+ "could not reify reflected term " ++

1546− show tm ++

1584+ show tm ++

1547− " when reflecting an error"

1585+ " when reflecting an error"

1548− OK (tm', _) -> return $ TermPart tm'

1586+ OK (tm', _) -> Right $ TermPart tm'

1549reifyReportPart (App (P (DCon _ _) n _) tm)

1587reifyReportPart (App (P (DCon _ _) n _) tm)

1550 | n == reflErrName "SubReport" =

1588 | n == reflErrName "SubReport" =

1551− case unList tm of

1589+ case unList tm of

1552− Just xs -> do subParts <- mapM reifyReportPart xs

1590+ Just xs -> do subParts <- mapM reifyReportPart xs

1553− return (SubReport subParts)

1591+ Right (SubReport subParts)

1554− Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm

1592+ Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

1555−reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x

1593+reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

1556

1594

1557envTupleType :: Raw

1595envTupleType :: Raw

1558envTupleType

1596envTupleType

src/Idris/Parser.hs+8−6

@@ -55,6 +55,7 @@ import Data.Char

55import qualified Data.HashSet as HS

56import qualified Data.Text as T

57import qualified Data.ByteString.UTF8 as UTF8

58+import qualified Data.Set as S

59import Debug.Trace

60import Debug.Trace

@@ -870,15 +871,16 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

870 <|> do try (lchar '%' *> reserved "name")

871 <|> do try (lchar '%' *> reserved "name")

871 ty <- iName []

872 ty <- iName []

872 ns <- sepBy1 name (lchar ',')

873 ns <- sepBy1 name (lchar ',')

873− return [PDirective

874− (do ty' <- disambiguate ty

874+ return [PDirective (do ty' <- disambiguate ty

875− mapM_ (addNameHint ty') ns

875+ mapM_ (addNameHint ty') ns

876− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

876+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

877 <|> do try (lchar '%' *> reserved "error_handlers")

878 fn <- iName []

879+ arg <- iName []

879 ns <- sepBy1 name (lchar ',')

880 ns <- sepBy1 name (lchar ',')

880− return [PDirective $ do n' <- disambiguate fn

881+ return [PDirective (do fn' <- disambiguate fn

882+ ns' <- mapM disambiguate ns

881− addFunctionErrorHandlers fn ns]

883+ addFunctionErrorHandlers fn' arg ns')]

882 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

884 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

883 return [PDirective (addLangExt ext)]

885 return [PDirective (addLangExt ext)]

884 <?> "directive"

886 <?> "directive"

src/Idris/ProofSearch.hs+2−1

@@ -10,6 +10,7 @@ import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

13+import Control.Applicative ((<$>))

13import Control.Monad

14import Control.Monad

14import Debug.Trace

15import Debug.Trace

@@ -86,7 +87,7 @@ proofSearch elab fn nroot hints ist = psRec maxDepth

86 [args] -> map isImp (snd args)

87 [args] -> map isImp (snd args)

87 _ -> fail "Ambiguous name"

88 _ -> fail "Ambiguous name"

88 ps <- get_probs

89 ps <- get_probs

89− args <- apply (Var n) imps

90+ args <- map snd <$> apply (Var n) imps

90 ps' <- get_probs

91 ps' <- get_probs

91 when (length ps < length ps') $ fail "Can't apply constructor"

92 when (length ps < length ps') $ fail "Can't apply constructor"

92 mapM_ (\ (_, h) -> do focus h

93 mapM_ (\ (_, h) -> do focus h

test/test038/FunErrTest.idrnew file+49

@@ -0,0 +1,49 @@

1+module FunErrTest

3+import Language.Reflection

4+import Language.Reflection.Errors

5+import Language.Reflection.Utils

7+%language ErrorReflection

9+total

10+cadr : (xs : List a)

11+ -> {auto cons1 : isCons xs = True}

12+ -> {auto cons2 : isCons (tail xs cons1) = True}

13+ -> a

14+cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

15+cadr (x :: []) {cons1=refl} {cons2=refl} impossible

16+

17+total

18+eltsErr : TT -> TT -> Maybe (List ErrorReportPart)

19+eltsErr (P (DCon _ _) (NS (UN "False") _) _) (P (DCon _ _) (NS (UN "True") _) _) =

20+ Just [ NamePart (NS (UN "cadr") ["FunErrTest"])

21+ , TextPart "requires that its argument contain at least two elements."

22+ ]

23+eltsErr (P (DCon _ _) (NS (UN "True") _) _) (App (App isCons ty) xs) =

24+ Just [ NamePart (NS (UN "cadr") ["FunErrTest"])

25+ , TextPart "requires that its argument contain at least two elements."

26+ , TextPart "This fails because: "

27+ , SubReport [ TextPart "There is no proof that"

28+ , TermPart xs

29+ , TextPart "is non-empty."

30+ ]

31+ ]

32+eltsErr _ _ = Nothing

33+

34+total

35+has2elts : Err -> Maybe (List ErrorReportPart)

36+has2elts (CantUnify _ tm1 tm2 e _ _) = eltsErr tm1 tm2 <|> has2elts e

37+has2elts e = Just [TextPart (show e)]

38+

39+%error_handlers cadr cons1 has2elts

40+%error_handlers cadr cons2 has2elts

41+

42+problem1 : List a -> a

43+problem1 xs = cadr xs

44+

45+problem2 : Int

46+problem2 = cadr [1]

47+

48+problem3 : Int

49+problem3 = cadr []

test/test038/expectednew file+47

@@ -0,0 +1,47 @@

1+FunErrTest.idr:43:10:When elaborating right hand side of problem1:

2+FunErrTest.cadr requires that its argument contain at least two elements. This fails because:

3+ There is no proof that xs is non-empty.

5+Original error:

7+ Can't unify

8+ True = True

9+ with

10+ isCons xs = True

11+

12+ Specifically:

13+ Can't unify

14+ True

15+ with

16+ isCons xs

17+

18+FunErrTest.idr:46:10:When elaborating right hand side of problem2:

19+FunErrTest.cadr requires that its argument contain at least two elements.

20+Original error:

21+

22+ Can't unify

23+ x = x

24+ with

25+ False = True

26+

27+ Specifically:

28+ Can't unify

29+ False

30+ with

31+ True

32+

33+FunErrTest.idr:49:10:When elaborating right hand side of problem3:

34+FunErrTest.cadr requires that its argument contain at least two elements.

35+Original error:

36+

37+ Can't unify

38+ x = x

39+ with

40+ False = True

41+

42+ Specifically:

43+ Can't unify

44+ False

45+ with

46+ True

47+

test/test038/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ FunErrTest.idr --nocolour --check

3+rm -f *.ibc