212587b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove 'score' and guesswork from error messages

212587bEdwin Brady11 years ago

src/Idris/Core/Elaborate.hs+15−27

compare with master

unifiedsplit

@@ -95,9 +95,11 @@ errAt thing n elab = do s <- get

95 case runStateT elab s of

96 OK (a, s') -> do put s'

97 return $! a

98− Error (At f e) ->

98+ Error e -> lift $ Error (rewriteErr e)

99− lift $ Error (At f (Elaborating thing n e))

99+ where

100+ rewriteErr (At f e) = At f (rewriteErr e)

101+ rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)

100− Error e -> lift $ Error (Elaborating thing n e)

102+ rewriteErr e = Elaborating thing n e

101

103

102erun :: FC -> Elab' aux a -> Elab' aux a

104erun :: FC -> Elab' aux a -> Elab' aux a

103erun f elab = do s <- get

105erun f elab = do s <- get

@@ -780,9 +782,7 @@ handleError p t1 t2

780 Error e1 -> if p e1 then

782 Error e1 -> if p e1 then

781 do case runStateT t2 s of

783 do case runStateT t2 s of

782 OK (v, s') -> do put s'; return $! v

784 OK (v, s') -> do put s'; return $! v

783− Error e2 -> if score e1 >= score e2

784− then lift (tfail e1)

785− else lift (tfail e2)

785+ Error e2 -> lift (tfail e2)

786 else lift (tfail e1)

787

788try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

@@ -798,9 +798,7 @@ try' t1 t2 proofSearch

798 if recoverableErr e1 then

799 do case runStateT t2 s of

800 OK (v, s') -> do put s'; return $! v

801− Error e2 -> if score e1 >= score e2

802− then lift (tfail e1)

803− else lift (tfail e2)

801+ Error e2 -> lift (tfail e2)

804 else lift (tfail e1)

802 else lift (tfail e1)

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

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

806 = -- traceWhen r (show err) $

804 = -- traceWhen r (show err) $

@@ -827,9 +825,7 @@ tryCatch t1 t2

827 case runStateT (t2 e1) s of

825 case runStateT (t2 e1) s of

828 OK (v, s') -> do put s'

826 OK (v, s') -> do put s'

829 return $! v

827 return $! v

830− Error e2 -> if score e1 >= score e2

831− then lift (tfail e1)

832− else lift (tfail e2)

828+ Error e2 -> lift (tfail e2)

833

829

834tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

830tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

835tryWhen True a b = try a b

831tryWhen True a b = try a b

@@ -839,7 +835,7 @@ tryWhen False a b = a

839-- to False, then the whole tactic fails if there are any new problems

835-- to False, then the whole tactic fails if there are any new problems

840tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

836tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

841tryAll [(x, _)] = x

837tryAll [(x, _)] = x

842−tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

838+tryAll xs = tryAll' [] 999999 xs

843 where

839 where

844 cantResolve :: Elab' aux a

840 cantResolve :: Elab' aux a

845 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

841 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

@@ -849,13 +845,12 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

849

845

850 tryAll' :: [Elab' aux a] -> -- successes

846 tryAll' :: [Elab' aux a] -> -- successes

851 Int -> -- most problems

847 Int -> -- most problems

852− (Elab' aux a, Int) -> -- smallest failure

853 [(Elab' aux a, Name)] -> -- still to try

848 [(Elab' aux a, Name)] -> -- still to try

854 Elab' aux a

849 Elab' aux a

855− tryAll' [res] pmax _ [] = res

850+ tryAll' [res] pmax [] = res

856− tryAll' (_:_) pmax _ [] = cantResolve

851+ tryAll' (_:_) pmax [] = cantResolve

857− tryAll' [] pmax (f, _) [] = noneValid

852+ tryAll' [] pmax [] = noneValid

858− tryAll' cs pmax f ((x, msg):xs)

853+ tryAll' cs pmax ((x, msg):xs)

859 = do s <- get

854 = do s <- get

860 ps <- get_probs

855 ps <- get_probs

861 case prunStateT pmax True ps x s of

856 case prunStateT pmax True ps x s of

@@ -863,16 +858,9 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

863 do let cs' = if (newps < pmax)

858 do let cs' = if (newps < pmax)

864 then [do put s'; return $! v]

859 then [do put s'; return $! v]

865 else (do put s'; return $! v) : cs

860 else (do put s'; return $! v) : cs

866− tryAll' cs' newps f xs

861+ tryAll' cs' newps xs

867 Error err -> do put s

862 Error err -> do put s

868−-- if (score err) < 100

869− tryAll' cs pmax (better err f) xs

863+ tryAll' cs pmax xs

870−-- else tryAll' [] pmax (better err f) xs -- give up

871−

872−

873− better err (f, i) = let s = score err in

874− if (s >= i) then (lift (tfail err), s)

875− else (f, i)

876

864

877-- Run an elaborator, and fail if any problems are introduced

865-- Run an elaborator, and fail if any problems are introduced

878prunStateT

866prunStateT

src/Idris/Core/TT.hs+1−14

@@ -37,7 +37,7 @@ module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

37 nextName, noOccurrence, nsroot, occurrences, orderPats,

38 pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV,

39 pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,

40− safeForgetEnv, score, showCG, showEnv, showEnvDbg, showSep,

40+ safeForgetEnv, showCG, showEnv, showEnvDbg, showSep,

41 sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,

42 substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,

43 toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,

@@ -358,19 +358,6 @@ instance Sized Err where

358 size (LoadingFailed fn e) = 1 + length fn + size e

359 size _ = 1

360

361−score :: Err -> Int

362−score (CantUnify _ _ _ m _ s) = 1 + s + score m

363−score (CantResolve _ _) = 20

364−score (NoValidAlts _) = 0

365−score (NoSuchVariable _) = 1000

366−score (ProofSearchFail e) = score e

367−score (CantSolveGoal _ _) = 100000

368−score (InternalMsg _) = -1

369−score (At _ e) = score e

370−score (ElaboratingArg _ _ _ e) = score e

371−score (Elaborating _ _ e) = score e

372−score _ = 0

373−

374instance Show Err where

361instance Show Err where

375 show (Msg s) = s

362 show (Msg s) = s

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

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

src/Idris/Elab/Term.hs−6

@@ -1379,12 +1379,6 @@ elab ist info emode opts fn tm

1379 (t : map (mkCoerce env t) cs)

1380 return t'

1381 where

1382−-- mkCoerce env (PAlternative ns aty alts@(a : as)) n

1383−-- = let fc = maybe (fileFC "Coercion") id (highestFC a) in

1384−-- addImplBound ist (map fst env)

1385−-- (PAlternative ns aty

1386−-- (map (\t -> PApp fc (PRef fc n) [pexp (PCoerced t)])

1387−-- alts))

1388 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1382 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1389 addImplBound ist (map fst env)

1383 addImplBound ist (map fst env)

1390 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1384 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])