1cf8fe9 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+1−1

compare with master

unifiedsplit

@@ -303,7 +303,7 @@ implementation Show Err where

303 showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm

304 showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n

305 showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'

306− showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm

306+ showPrec d (CantResolve tm e) = showCon d "CantResolve" $ showArg tm ++ showArg e

307 showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm

308 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

309 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

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

@@ -30,7 +30,7 @@ data Err = Msg String

30 | CantMatch TT

31 | NoTypeDecl TTName

32 | NotInjective TT TT TT

33− | CantResolve TT

33+ | CantResolve TT Err

34 | InvalidTCArg TTName TT

35 | CantResolveAlts (List TTName)

36 | NoValidAlts (List TTName)

libs/prelude/Prelude.idr+2−2

@@ -272,7 +272,7 @@ cast_part x = TermPart x

272

273%error_handler export

274cast_error : Err -> Maybe (List ErrorReportPart)

275−cast_error (CantResolve `(Cast ~x ~y))

275+cast_error (CantResolve `(Cast ~x ~y) _)

276 = Just [TextPart "Can't cast from",

277 cast_part x,

278 TextPart "to",

@@ -282,6 +282,6 @@ cast_error _ = Nothing

282%error_handler

283export

284num_error : Err -> Maybe (List ErrorReportPart)

285−num_error (CantResolve `(Num ~x))

285+num_error (CantResolve `(Num ~x) _)

286 = Just [TermPart x, TextPart "is not a numeric type"]

287num_error _ = Nothing

src/Idris/Core/Binary.hs+4−3

@@ -113,8 +113,9 @@ instance Binary a => Binary (Err' a) where

113 put x

114 put y

115 put z

116− put (CantResolve _ t) = do putWord8 15

116+ put (CantResolve _ t u) = do putWord8 15

117− put t

117+ put t

118+ put u

118 put (CantResolveAlts ns) = do putWord8 16

119 put (CantResolveAlts ns) = do putWord8 16

119 put ns

120 put ns

120 put (IncompleteTerm t) = do putWord8 17

121 put (IncompleteTerm t) = do putWord8 17

@@ -218,7 +219,7 @@ instance Binary a => Binary (Err' a) where

218 13 -> fmap NoTypeDecl get

219 13 -> fmap NoTypeDecl get

219 14 -> do x <- get ; y <- get ; z <- get

220 14 -> do x <- get ; y <- get ; z <- get

220 return $ NotInjective x y z

221 return $ NotInjective x y z

221− 15 -> fmap (CantResolve False) get

222+ 15 -> CantResolve False <$> get <*> get

222 16 -> fmap CantResolveAlts get

223 16 -> fmap CantResolveAlts get

223 17 -> fmap IncompleteTerm get

224 17 -> fmap IncompleteTerm get

224 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get

225 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get

src/Idris/Core/DeepSeq.hs+1−1

@@ -134,7 +134,7 @@ instance NFData Err where

134 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

135 rnf (NotInjective x1 x2 x3)

136 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

137− rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

137+ rnf (CantResolve x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

138 rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

140 rnf (NoValidAlts x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+3−3

@@ -268,7 +268,7 @@ data Err' t

268 | NoTypeDecl Name

269 | NotInjective t t t

270 | CantResolve Bool -- True if postponed, False if fatal

271− t

271+ t (Err' t) -- any further information

272 | InvalidTCArg Name t

273 | CantResolveAlts [Name]

274 | NoValidAlts [Name]

@@ -354,7 +354,7 @@ instance Sized Err where

354 size (NoSuchVariable name) = size name

355 size (NoTypeDecl name) = size name

356 size (NotInjective l c r) = size l + size c + size r

357− size (CantResolve _ trm) = size trm

357+ size (CantResolve _ trm _) = size trm

358 size (NoRewriting trm) = size trm

359 size (CantResolveAlts _) = 1

360 size (IncompleteTerm trm) = size trm

@@ -397,7 +397,7 @@ instance Show Err where

397 show (WithFnType _) = "WithFnType"

398 show (NoTypeDecl _) = "NoTypeDecl"

399 show (NotInjective _ _ _) = "NotInjective"

400− show (CantResolve _ _) = "CantResolve"

400+ show (CantResolve _ _ _) = "CantResolve"

401 show (InvalidTCArg _ _) = "InvalidTCArg"

402 show (CantResolveAlts _) = "CantResolveAlts"

403 show (NoValidAlts _) = "NoValidAlts"

src/Idris/Delaborate.hs+7−1

@@ -346,7 +346,13 @@ pprintErr' i (NotInjective p x y) =

346 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>

347 text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>

348 annTm y (pprintTerm i (delabSugared i y))

349+pprintErr' i (CantResolve _ c e)

349−pprintErr' i (CantResolve _ c) = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)

350+ = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)

351+ <>

352+ case e of

353+ Msg "" -> empty

354+ _ -> line <> line <> text "Possible cause:" <>

355+ indented (pprintErr' i e)

350pprintErr' i (InvalidTCArg n t)

356pprintErr' i (InvalidTCArg n t)

351 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "

357 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "

352 <> annName n <$>

358 <> annName n <$>

src/Idris/Elab/Term.hs+2−2

@@ -1704,8 +1704,8 @@ solveAutos ist fn ambigok

1704-- Return true if the given error suggests a type class failure is

1705-- recoverable

1706tcRecoverable :: ElabMode -> Err -> Bool

1707−tcRecoverable ERHS (CantResolve f g) = f

1707+tcRecoverable ERHS (CantResolve f g _) = f

1708−tcRecoverable ETyDecl (CantResolve f g) = f

1708+tcRecoverable ETyDecl (CantResolve f g _) = f

1709tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err

1710tcRecoverable e (At _ err) = tcRecoverable e err

1711tcRecoverable _ _ = True

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 132

43+ibcVersion = 133

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

src/Idris/ProofSearch.hs+9−3

@@ -383,8 +383,10 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

383 let (argsok, okholePos) = case tcArgsOK g topholes of

384 Nothing -> (False, [])

385 Just hs -> (True, hs)

386+ env <- get_env

387+ probs <- get_probs

386 if not argsok -- && not mvok)

388 if not argsok -- && not mvok)

387− then lift $ tfail $ CantResolve True topg

389+ then lift $ tfail $ CantResolve True topg (probErr probs)

388 else do

390 else do

389 ptm <- get_term

391 ptm <- get_term

390 ulog <- getUnifyLog

392 ulog <- getUnifyLog

@@ -431,6 +433,9 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

431 _ -> Just rs

433 _ -> Just rs

432 tcDetArgsOK _ _ _ [] = Just []

434 tcDetArgsOK _ _ _ [] = Just []

433

435

436+ probErr [] = Msg ""

437+ probErr ((_,_,_,_,err,_,_) : _) = err

438+

434 isMeta :: [Name] -> Term -> Bool

439 isMeta :: [Name] -> Term -> Bool

435 isMeta ns (P _ n _) = n `elem` ns

440 isMeta ns (P _ n _) = n `elem` ns

436 isMeta _ _ = False

441 isMeta _ _ = False

@@ -462,12 +467,13 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

462 boundVar (P Bound _ _) = True

467 boundVar (P Bound _ _) = True

463 boundVar _ = False

468 boundVar _ = False

464

469

470+ blunderbuss t d stk [] = do ps <- get_probs

465− blunderbuss t d stk [] = lift $ tfail $ CantResolve False topg

471+ lift $ tfail $ CantResolve False topg (probErr ps)

466 blunderbuss t d stk (n:ns)

472 blunderbuss t d stk (n:ns)

467 | n /= fn -- && (n `elem` stk)

473 | n /= fn -- && (n `elem` stk)

468 = tryCatch (resolve n d)

474 = tryCatch (resolve n d)

469 (\e -> case e of

475 (\e -> case e of

470− CantResolve True _ -> lift $ tfail e

476+ CantResolve True _ _ -> lift $ tfail e

471 _ -> blunderbuss t d stk ns)

477 _ -> blunderbuss t d stk ns)

472 | otherwise = blunderbuss t d stk ns

478 | otherwise = blunderbuss t d stk ns

473

479

src/Idris/Reflection.hs+2−1

@@ -896,7 +896,8 @@ reflectErr (NotInjective t1 t2 t3) =

896 , reflect t2

897 , reflect t3

898 ]

899+reflectErr (CantResolve _ t more)

899−reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

900+ = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]

900reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

901reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

901reflectErr (CantResolveAlts ss) =

902reflectErr (CantResolveAlts ss) =

902 raw_apply (Var $ reflErrName "CantResolveAlts")

903 raw_apply (Var $ reflErrName "CantResolveAlts")