e34849f · Idris-dev · git.iko.soy

CHANGELOG.md+1

compare with master

unifiedsplit

@@ -79,6 +79,7 @@

79 `Prelude.WellFounded`.

80* Added `Data.List.Views` with views on `List` and their covering functions.

81* Added `Data.Nat.Views` with views on `Nat` and their covering functions.

82+* Added `Data.Primitives.Views` with views on various primitive types and their covering functions.

82

83

83## Miscellaneous updates

84## Miscellaneous updates

84

85

src/Idris/AbsSyntaxTree.hs+3

@@ -1816,6 +1816,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1816 depth d . bracket p startPrec $

1817 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1818 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1819+ prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])

1820+ | basename neg == sUN "negate" =

1821+ lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen

1819 -- This case preserves the behavior of the former constructor PEq.

1822 -- This case preserves the behavior of the former constructor PEq.

1820 -- It should be removed if feasible when the pretty-printing of infix

1823 -- It should be removed if feasible when the pretty-printing of infix

1821 -- operators in general is improved.

1824 -- operators in general is improved.

src/Idris/CaseSplit.hs+5−3

@@ -285,10 +285,12 @@ splitOnLine l n fn = do

285

286replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]

287replaceSplits l ups impossible

288+ = do ist <- getIState

288− = updateRHSs 1 (map (rep (expandBraces l)) ups)

289+ updateRHSs 1 (map (rep ist (expandBraces l)) ups)

289 where

290 where

290− rep str [] = str ++ "\n"

291+ rep ist str [] = str ++ "\n"

292+ rep ist str ((n, tm) : ups)

291− rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups

293+ = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups

292

294

293 updateRHSs i [] = return []

295 updateRHSs i [] = return []

294 updateRHSs i (x : xs)

296 updateRHSs i (x : xs)

test/reg072/expected+1−1

@@ -6,7 +6,7 @@ When checking argument value to function Prelude.Basics.the:

6 Type mismatch between

7 x = x (Type of Refl)

8 and

9− negate 0.0 = 0.0 (Expected type)

9+ (-0.0) = 0.0 (Expected type)

10

11 Specifically:

12 Type mismatch between