git.iko.soy/Idris-dev
on master help sign in
Prettier printing in case splitting

In particular, resugar before printing the patterns, and pretty print 'negate x' as '-x'.

commite34849f16be45b5362b0e92eb0909c4f5e319be9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 May 2016, 20:46 (10 years ago) parentf2ab362
4 files changed+10−4
compare with master
unifiedsplit
CHANGELOG.md+1 src/Idris/AbsSyntaxTree.hs+3 src/Idris/CaseSplit.hs+5−3 test/reg072/expected+1−1
CHANGELOG.md+1
@@ -79,6 +79,7 @@
7979 `Prelude.WellFounded`.
8080* Added `Data.List.Views` with views on `List` and their covering functions.
8181* 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.
8283
8384## Miscellaneous updates
8485
src/Idris/AbsSyntaxTree.hs+3
@@ -1816,6 +1816,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18161816 depth d . bracket p startPrec $
18171817 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
18181818 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
18191822 -- This case preserves the behavior of the former constructor PEq.
18201823 -- It should be removed if feasible when the pretty-printing of infix
18211824 -- operators in general is improved.
src/Idris/CaseSplit.hs+5−3
@@ -285,10 +285,12 @@ splitOnLine l n fn = do
285285
286286replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
287287replaceSplits l ups impossible
288− = updateRHSs 1 (map (rep (expandBraces l)) ups)
288+ = do ist <- getIState
289+ updateRHSs 1 (map (rep ist (expandBraces l)) ups)
289290 where
290− rep str [] = str ++ "\n"
291− rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
291+ rep ist str [] = str ++ "\n"
292+ rep ist str ((n, tm) : ups)
293+ = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups
292294
293295 updateRHSs i [] = return []
294296 updateRHSs i (x : xs)
test/reg072/expected+1−1
@@ -6,7 +6,7 @@ When checking argument value to function Prelude.Basics.the:
66 Type mismatch between
77 x = x (Type of Refl)
88 and
9− negate 0.0 = 0.0 (Expected type)
9+ (-0.0) = 0.0 (Expected type)
1010
1111 Specifically:
1212 Type mismatch between