be9ffc9 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

31 | CantResolve TT

32 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34+ | NoEliminator String TT

34 | UniverseError

35 | UniverseError

35 | ProgramLineComment

36 | ProgramLineComment

36 | Inaccessible TTName

37 | Inaccessible TTName

src/Idris/Core/Binary.hs+6

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

146 put x1

147 put x2

148 put x3

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

150+ put s

151+ put t

149

152

150 get = do i <- getWord8

153 get = do i <- getWord8

151 case i of

154 case i of

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

205 x2 <- get

208 x2 <- get

206 x3 <- get

209 x3 <- get

207 return (ElabDebug x1 x2 x3)

210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

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

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

209----- Generated by 'derive'

215----- Generated by 'derive'

210

216

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

86 rnf UniverseError = ()

87 rnf UniverseError = ()

87 rnf ProgramLineComment = ()

88 rnf ProgramLineComment = ()

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

89 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

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

682 let tmt' = normalise ctxt env tmt

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

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

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

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

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

686 case unApply tmt' of

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

688 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

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

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

719 return scv'

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

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

721 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'

723 where scname = sMN 0 "scarg"

724 where scname = sMN 0 "scarg"

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

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

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

726 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

159 t

160 | CantResolveAlts [Name]

161 | IncompleteTerm t

162+ | NoEliminator String t

162 | UniverseError

163 | UniverseError

163 | UniqueError Universe Name

164 | UniqueError Universe Name

164 | UniqueKindError Universe Name

165 | UniqueKindError Universe Name

src/Idris/Delaborate.hs+6

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

299pprintErr' i (CantMatch t) =

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

301pprintErr' 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."

302pprintErr' i UniverseError = text "Universe inconsistency"

308pprintErr' i UniverseError = text "Universe inconsistency"

303pprintErr' i (UniqueError NullType n)

309pprintErr' i (UniqueError NullType n)

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

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

src/Idris/ElabTerm.hs+3

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

2639 raw_apply (Var $ reflErrName "CantResolveAlts")

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

2641reflectErr (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]

2642reflectErr UniverseError = Var $ reflErrName "UniverseError"

2645reflectErr UniverseError = Var $ reflErrName "UniverseError"

2643reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2646reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

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

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