be093dc · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

329 showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n

330 showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n

331 showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err

332− showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm

332+ showPrec d (NoRewriting ltm rtm typ) = showCon d "NoRewriting" $ showArg ltm ++ showArg rtm ++ showArg typ

333 showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x

334 showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err

335

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

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

43 | NonCollapsiblePostulate TTName

44 | AlreadyDefined TTName

45 | ProofSearchFail Err

46− | NoRewriting TT

46+ | NoRewriting TT TT TT

47 | ProviderError String

48 | LoadingFailed String Err

49

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

@@ -146,8 +146,10 @@ instance Binary a => Binary (Err' a) where

146 put n

147 put (ProofSearchFail e) = do putWord8 25

148 put e

149− put (NoRewriting t) = do putWord8 26

149+ put (NoRewriting l r t) = do putWord8 26

150+ put l

151+ put r

150− put t

152+ put t

151 put (At fc e) = do putWord8 27

153 put (At fc e) = do putWord8 27

152 put fc

154 put fc

153 put e

155 put e

@@ -237,7 +239,8 @@ instance Binary a => Binary (Err' a) where

237 23 -> fmap NonCollapsiblePostulate get

239 23 -> fmap NonCollapsiblePostulate get

238 24 -> fmap AlreadyDefined get

240 24 -> fmap AlreadyDefined get

239 25 -> fmap ProofSearchFail get

241 25 -> fmap ProofSearchFail get

242+ 26 -> do l <- get; r <- get; t <- get

240− 26 -> fmap NoRewriting get

243+ return $ NoRewriting l r t

241 27 -> do x <- get ; y <- get

244 27 -> do x <- get ; y <- get

242 return $ At x y

245 return $ At x y

243 28 -> do w <- get; x <- get ; y <- get ; z <- get

246 28 -> do w <- get; x <- get ; y <- get ; z <- get

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

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

154 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

155 rnf (AlreadyDefined x1) = rnf x1 `seq` ()

156 rnf (ProofSearchFail x1) = rnf x1 `seq` ()

157− rnf (NoRewriting x1) = rnf x1 `seq` ()

157+ rnf (NoRewriting x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

158 rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

159 rnf (Elaborating x1 x2 x3 x4)

160 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

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

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

295 | NonCollapsiblePostulate Name

296 | AlreadyDefined Name

297 | ProofSearchFail (Err' t)

298− | NoRewriting t

298+ | NoRewriting t t t

299 | At FC (Err' t)

300 | Elaborating String Name (Maybe t) (Err' t)

301 | ElaboratingArg Name Name [(Name, Name)] (Err' t)

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

365 size (NoTypeDecl name) = size name

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

367 size (CantResolve _ trm _) = size trm

368− size (NoRewriting trm) = size trm

368+ size (NoRewriting l r t) = size l + size r + size t

369 size (CantResolveAlts _) = 1

370 size (IncompleteTerm trm) = size trm

371 size ProgramLineComment = 1

src/Idris/Delaborate.hs+1−1

@@ -452,7 +452,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <

452pprintErr' i (AlreadyDefined n) = annName n<+>

453 text "is already defined"

454pprintErr' i (ProofSearchFail e) = pprintErr' i e

455−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))

455+pprintErr' i (NoRewriting l r tm) = text "rewriting" <+> annTm l (pprintTerm i (delabSugared i l)) <+> text "to" <+> annTm r (pprintTerm i (delabSugared i r)) <+> text "did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))

456pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

457pprintErr' i (Elaborating s n ty e) = text "When checking" <+> text s <>

458 annName' n (showqual i n) <>

src/Idris/Elab/Rewrite.hs+1−1

@@ -74,7 +74,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

74 (P _ (UN q) _, [lt, rt, l, r]) | q == txt "=" ->

75 do substfn <- findSubstFn substfn_in ist lt rt

76 let pred_tt = mkP (P Bound rname rt) l r g

77− when (g == pred_tt) $ lift $ tfail (NoRewriting g)

77+ when (g == pred_tt) $ lift $ tfail (NoRewriting l r g)

78 let pred = PLam fc rname fc Placeholder

79 (delab ist pred_tt)

80 let rewrite = stripImpls $

src/Idris/IBC.hs+1−1

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

47import Codec.Archive.Zip

48

49ibcVersion :: Word16

50−ibcVersion = 143

50+ibcVersion = 144

51

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

53-- different structures/definitions) depending on which phase we're in.

src/Idris/Reflection.hs+1−1

@@ -924,7 +924,7 @@ reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit

924reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

925reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

926reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

927−reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

927+reflectErr (NoRewriting l r tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect l, reflect r, reflect tm]

928reflectErr (ProviderError str) =

929 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

930reflectErr (LoadingFailed str err) =

test/proof011/expected+6−4

@@ -2,11 +2,13 @@ proof011.idr:19:9:

2When checking right hand side of vassoc' with expected type

3 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

4

5+rewriting xs ++ ys ++ xs to (xs ++ ys) ++

5−rewrite did not change type x :: xs ++ ys ++ zs =

6+ xs did not change type x :: xs ++ ys ++ zs =

6− x :: (xs ++ ys) ++ zs

7+ x :: (xs ++ ys) ++ zs

7proof011a.idr:13:9:

8proof011a.idr:13:9:

8When checking right hand side of vassoc' with expected type

9When checking right hand side of vassoc' with expected type

9 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

10 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

10

11

12+rewriting xs ++ ys ++ xs to (xs ++ ys) ++

11−rewrite did not change type x :: xs ++ ys ++ zs =

13+ xs did not change type x :: xs ++ ys ++ zs =

12− x :: (xs ++ ys) ++ zs

14+ x :: (xs ++ ys) ++ zs