fc3e88c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commitfc3e88c9a467817342294dbfbb9617eea2be02c4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 5 Jun 2016, 23:13 (10 years ago) parentfdfa04c da1d168

9 files changed+20−15

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr+1−1 libs/prelude/Language/Reflection/Errors.idr+1−1 src/Idris/Core/Binary.hs+6−3 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/TT.hs+2−2 src/Idris/Delaborate.hs+1−1 src/Idris/Elab/Rewrite.hs+1−1 src/Idris/Reflection.hs+1−1 test/proof011/expected+6−4

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

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

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

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

331331 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

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

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

335335

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

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

4343 | NonCollapsiblePostulate TTName

4444 | AlreadyDefined TTName

4545 | ProofSearchFail Err

46− | NoRewriting TT

46+ | NoRewriting TT TT TT

4747 | ProviderError String

4848 | LoadingFailed String Err

4949

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

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

146146 put n

147147 put (ProofSearchFail e) = do putWord8 25

148148 put e

149− put (NoRewriting t) = do putWord8 26

150− put t

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

150+ put l

151+ put r

152+ put t

151153 put (At fc e) = do putWord8 27

152154 put fc

153155 put e

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

237239 23 -> fmap NonCollapsiblePostulate get

238240 24 -> fmap AlreadyDefined get

239241 25 -> fmap ProofSearchFail get

240− 26 -> fmap NoRewriting get

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

243+ return $ NoRewriting l r t

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

242245 return $ At x y

243246 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

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

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

156156 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` ()

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

159159 rnf (Elaborating x1 x2 x3 x4)

160160 = 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

295295 | NonCollapsiblePostulate Name

296296 | AlreadyDefined Name

297297 | ProofSearchFail (Err' t)

298− | NoRewriting t

298+ | NoRewriting t t t

299299 | At FC (Err' t)

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

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

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

365365 size (NoTypeDecl name) = size name

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

367367 size (CantResolve _ trm _) = size trm

368− size (NoRewriting trm) = size trm

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

369369 size (CantResolveAlts _) = 1

370370 size (IncompleteTerm trm) = size trm

371371 size ProgramLineComment = 1

src/Idris/Delaborate.hs+1−1

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

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

453453 text "is already defined"

454454pprintErr' 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))

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

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

458458 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

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

7575 do substfn <- findSubstFn substfn_in ist lt rt

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

7878 let pred = PLam fc rname fc Placeholder

7979 (delab ist pred_tt)

8080 let rewrite = stripImpls $

src/Idris/Reflection.hs+1−1

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

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

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

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

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

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

930930reflectErr (ProviderError str) =

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

932932reflectErr (LoadingFailed str err) =

test/proof011/expected+6−4

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

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

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

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

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

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

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

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

78proof011a.idr:13:9:

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

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

1011

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

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

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

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

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