06fd947 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Errors.idr+1

compare with master

unifiedsplit

@@ -15,6 +15,7 @@ data Err = Msg String

15 -- unification succeed

16 | InfiniteUnify TTName TT (List (TTName, TT))

17 | CantConvert TT TT (List (TTName, TT))

18+ | CantSolveGoal TT (List (TTName, TT))

18 | UnifyScope TTName TTName TT (List (TTName, TT))

19 | UnifyScope TTName TTName TT (List (TTName, TT))

19 | CantInferType String

20 | CantInferType String

20 | NonFunctionType TT TT

21 | NonFunctionType TT TT

src/Idris/Core/Elaborate.hs+19−11

@@ -604,17 +604,24 @@ arg n tyhole = do ty <- unique_hole tyhole

604 forall n (Var ty)

605

606-- try a tactic, if it adds any unification problem, return an error

607−no_errors :: Elab' aux () -> Elab' aux ()

607+no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

608−no_errors tac

608+no_errors tac err

609− = do ps <- get_probs

609+ = do ps <- get_probs

610− tac

610+ s <- get

611+ case err of

612+ Nothing -> tac

613+ Just e -> -- update the error, if there is one.

614+ case runStateT tac s of

615+ Error _ -> lift $ Error e

616+ OK (a, s') -> do put s'

617+ return a

611− ps' <- get_probs

618+ ps' <- get_probs

612− if (length ps' > length ps) then

619+ if (length ps' > length ps) then

613− case reverse ps' of

620+ case reverse ps' of

614− ((x,y,env,err) : _) ->

621+ ((x,y,env,err) : _) ->

615− let env' = map (\(x, b) -> (x, binderTy b)) env in

622+ let env' = map (\(x, b) -> (x, binderTy b)) env in

616− lift $ tfail $ CantUnify False x y err env' 0

623+ lift $ tfail $ CantUnify False x y err env' 0

617− else return $! ()

624+ else return $! ()

618

625

619-- Try a tactic, if it fails, try another

626-- Try a tactic, if it fails, try another

620try :: Elab' aux a -> Elab' aux a -> Elab' aux a

627try :: Elab' aux a -> Elab' aux a -> Elab' aux a

@@ -637,6 +644,7 @@ try' t1 t2 proofSearch

637 where recoverableErr err@(CantUnify r x y _ _ _)

644 where recoverableErr err@(CantUnify r x y _ _ _)

638 = -- traceWhen r (show err) $

645 = -- traceWhen r (show err) $

639 r || proofSearch

646 r || proofSearch

647+ recoverableErr (CantSolveGoal _ _) = False

640 recoverableErr (ProofSearchFail _) = False

648 recoverableErr (ProofSearchFail _) = False

641 recoverableErr _ = True

649 recoverableErr _ = True

642

650

src/Idris/Core/TT.hs+3

@@ -98,6 +98,7 @@ data Err = Msg String

98 -- unification succeed

99 | InfiniteUnify Name Term [(Name, Type)]

100 | CantConvert Term Term [(Name, Type)]

101+ | CantSolveGoal Term [(Name, Type)]

101 | UnifyScope Name Name Term [(Name, Type)]

102 | UnifyScope Name Name Term [(Name, Type)]

102 | CantInferType String

103 | CantInferType String

103 | NonFunctionType Term Term

104 | NonFunctionType Term Term

@@ -155,6 +156,7 @@ score (CantUnify _ _ _ m _ s) = s + score m

155score (CantResolve _) = 20

156score (CantResolve _) = 20

156score (NoSuchVariable _) = 1000

157score (NoSuchVariable _) = 1000

157score (ProofSearchFail _) = 10000

158score (ProofSearchFail _) = 10000

159+score (CantSolveGoal _ _) = 10000

158score (InternalMsg _) = -1

160score (InternalMsg _) = -1

159score _ = 0

161score _ = 0

160

162

@@ -163,6 +165,7 @@ instance Show Err where

163 show (InternalMsg s) = "Internal error: " ++ show s

165 show (InternalMsg s) = "Internal error: " ++ show s

164 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

166 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

165 ++ show e ++ " in " ++ show sc ++ " " ++ show i

167 ++ show e ++ " in " ++ show sc ++ " " ++ show i

168+ show (CantSolveGoal g _) = "CantSolve " ++ show g

166 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

169 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

167 show (ProviderError msg) = "Type provider error: " ++ msg

170 show (ProviderError msg) = "Type provider error: " ++ msg

168 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

171 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

src/Idris/Delaborate.hs+5

@@ -142,6 +142,11 @@ pshow i (CantConvert x y env)

142 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

143 ++ indented (showImp (Just i) imps colour (delab i y)) ++

144 if (opt_errContext (idris_options i)) then showSc i env else ""

145+pshow i (CantSolveGoal x env)

146+ = let imps = opt_showimp (idris_options i) in

147+ let colour = idris_colourRepl i in

148+ "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

149+ if (opt_errContext (idris_options i)) then showSc i env else ""

145pshow i (UnifyScope n out tm env)

150pshow i (UnifyScope n out tm env)

146 = let imps = opt_showimp (idris_options i) in

151 = let imps = opt_showimp (idris_options i) in

147 let colour = idris_colourRepl i in

152 let colour = idris_colourRepl i in

src/Idris/ElabTerm.hs+8−1

@@ -810,7 +810,9 @@ collectDeferred top t = return t

810runTac :: Bool -> IState -> PTactic -> ElabD ()

811runTac autoSolve ist tac

812 = do env <- get_env

813+ g <- goal

813− no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)

814+ no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

815+ (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

814 where

816 where

815 runT (Intro []) = do g <- goal

817 runT (Intro []) = do g <- goal

816 attack; intro (bname g)

818 attack; intro (bname g)

@@ -1414,6 +1416,11 @@ reflectErr (CantConvert t t' ctxt) =

1414 , reflect t'

1416 , reflect t'

1415 , reflectCtxt ctxt

1417 , reflectCtxt ctxt

1416 ]

1418 ]

1419+reflectErr (CantSolveGoal t ctxt) =

1420+ raw_apply (Var $ reflErrName "CantSolveGoal")

1421+ [ reflect t

1422+ , reflectCtxt ctxt

1423+ ]

1417reflectErr (UnifyScope n n' t ctxt) =

1424reflectErr (UnifyScope n n' t ctxt) =

1418 raw_apply (Var $ reflErrName "UnifyScope")

1425 raw_apply (Var $ reflErrName "UnifyScope")

1419 [ reflectName n

1426 [ reflectName n