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

git.iko.soy/Idris-dev

Remove 'score' and guesswork from error messages

In a try or handleError, just take the message from the second thing that failed. (This may turn out to need more control depending on the use of the try/handleError. We'll see.)

commit212587bc46cc9da9adf4dc9bd3fb929fc7e0f417 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Jul 2015, 02:16 (11 years ago) parente1c79ef

3 files changed+16−47

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+15−27 src/Idris/Core/TT.hs+1−14 src/Idris/Elab/Term.hs−6

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

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

9595 case runStateT elab s of

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

9797 return $! a

98− Error (At f e) ->

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

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

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

99+ where

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

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

102+ rewriteErr e = Elaborating thing n e

101103

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

103105erun f elab = do s <- get

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

780782 Error e1 -> if p e1 then

781783 do case runStateT t2 s of

782784 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)

786786 else lift (tfail e1)

787787

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

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

798798 if recoverableErr e1 then

799799 do case runStateT t2 s of

800800 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)

804802 else lift (tfail e1)

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

806804 = -- traceWhen r (show err) $

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

827825 case runStateT (t2 e1) s of

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

829827 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)

833829

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

835831tryWhen True a b = try a b

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

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

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

841837tryAll [(x, _)] = x

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

838+tryAll xs = tryAll' [] 999999 xs

843839 where

844840 cantResolve :: Elab' aux a

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

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

849845

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

851847 Int -> -- most problems

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

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

854849 Elab' aux a

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

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

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

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

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

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

852+ tryAll' [] pmax [] = noneValid

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

859854 = do s <- get

860855 ps <- get_probs

861856 case prunStateT pmax True ps x s of

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

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

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

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

866− tryAll' cs' newps f xs

861+ tryAll' cs' newps xs

867862 Error err -> do put s

868−-- if (score err) < 100

869− tryAll' cs pmax (better err f) 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)

863+ tryAll' cs pmax xs

876864

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

878866prunStateT

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

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

3737 nextName, noOccurrence, nsroot, occurrences, orderPats,

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

3939 pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,

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

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

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

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

4343 toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,

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

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

359359 size _ = 1

360360

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−

374361instance Show Err where

375362 show (Msg s) = s

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

src/Idris/Elab/Term.hs−6

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

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

13801380 return t'

13811381 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))

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

13891383 addImplBound ist (map fst env)

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