be9ffc9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proper error message for missing eliminators

Fixes #1888

commitbe9ffc92c032feed9a296b0887c60611710b130e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 Mar 2015, 12:28 (12 years ago) parent5ce7362

7 files changed+23−4

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Errors.idr+1 src/Idris/Core/Binary.hs+6 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/ProofState.hs+5−4 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+6 src/Idris/ElabTerm.hs+3

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

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

3131 | CantResolve TT

3232 | CantResolveAlts (List TTName)

3333 | IncompleteTerm TT

34+ | NoEliminator String TT

3435 | UniverseError

3536 | ProgramLineComment

3637 | Inaccessible TTName

src/Idris/Core/Binary.hs+6

@@ -146,6 +146,9 @@ instance Binary a => Binary (Err' a) where

146146 put x1

147147 put x2

148148 put x3

149+ put (NoEliminator s t) = do putWord8 37

150+ put s

151+ put t

149152

150153 get = do i <- getWord8

151154 case i of

@@ -205,6 +208,9 @@ instance Binary a => Binary (Err' a) where

205208 x2 <- get

206209 x3 <- get

207210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

208214 _ -> error "Corrupted binary data for Err'"

209215----- Generated by 'derive'

210216

src/Idris/Core/DeepSeq.hs+1

@@ -83,6 +83,7 @@ instance NFData Err where

8383 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8484 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

8585 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86+ rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8687 rnf UniverseError = ()

8788 rnf ProgramLineComment = ()

8889 rnf (Inaccessible x1) = rnf x1 `seq` ()

src/Idris/Core/ProofState.hs+5−4

@@ -681,8 +681,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

681681 (tmv, tmt) <- lift $ check ctxt env tm

682682 let tmt' = normalise ctxt env tmt

683683 let (tacn, tacstr, tactt) = if induction

684− then (ElimN, "an eliminator", "Induction")

685− else (CaseN, "a case function", "Case analysis")

684+ then (ElimN, "eliminator", "Induction")

685+ else (CaseN, "case analysis", "Case analysis")

686686 case unApply tmt' of

687687 (P _ tnm _, tyargs) -> do

688688 case lookupTy (SN (tacn tnm)) ctxt of

@@ -717,9 +717,10 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

717717 (scv, sct) <- lift $ check ctxt env res'

718718 let (scv', _) = specialise ctxt env [] scv

719719 return scv'

720− [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

720+ [] -> lift $ tfail $ NoEliminator tacstr tmt'

721721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

722− _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

722+ _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

723+ tmt'

723724 where scname = sMN 0 "scarg"

724725 makeConsArg (nm, ty) = P Bound nm ty

725726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

src/Idris/Core/TT.hs+1

@@ -159,6 +159,7 @@ data Err' t

159159 t

160160 | CantResolveAlts [Name]

161161 | IncompleteTerm t

162+ | NoEliminator String t

162163 | UniverseError

163164 | UniqueError Universe Name

164165 | UniqueKindError Universe Name

src/Idris/Delaborate.hs+6

@@ -299,6 +299,12 @@ pprintErr' i (WithFnType ty) =

299299pprintErr' i (CantMatch t) =

300300 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

301301pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

302+pprintErr' i (NoEliminator s t)

303+ = text "No " <> text s <> text " for type " <+>

304+ annTm t (pprintTerm i (delab i t)) <$>

305+ text "Please note that 'induction' is experimental." <$>

306+ text "Only types declared with '%elim' can be used." <$>

307+ text "Consider writing a pattern matching definition instead."

302308pprintErr' i UniverseError = text "Universe inconsistency"

303309pprintErr' i (UniqueError NullType n)

304310 = text "Borrowed name" <+> annName' n (showbasic n)

src/Idris/ElabTerm.hs+3

@@ -2639,6 +2639,9 @@ reflectErr (CantResolveAlts ss) =

26392639 raw_apply (Var $ reflErrName "CantResolveAlts")

26402640 [rawList (Var $ reflm "TTName") (map reflectName ss)]

26412641reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2642+reflectErr (NoEliminator str t)

2643+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2644+ reflect t]

26422645reflectErr UniverseError = Var $ reflErrName "UniverseError"

26432646reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

26442647reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]