on master help sign in
Fix buglet in rendering of Nat patterns in :cs
commitc58738777b17da2dcfb5adf143ce0a1551196229 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 3 Dec 2013, 15:40 (13 years ago) parente6a906a
1 file changed+5−6
src/Idris/CaseSplit.hs+5−6
src/Idris/CaseSplit.hs+5−6
@@ -245,7 +245,7 @@ replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
245245replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
246246 where
247247 rep str [] = str ++ "\n"
248− rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
248+ rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
249249
250250 updateRHSs i [] = return []
251251 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
@@ -264,11 +264,10 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
264264
265265 -- TMP HACK: If there are Nats, we don't want to show as numerals since
266266 -- this isn't supported in a pattern, so special case here
267− nshow brack (PRef _ (UN "Z")) = "Z"
268− nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
269− if brack then "(S " else "S " ++ nshow True (getTm x) ++
270− if brack then ")" else ""
271− nshow _ t = show t
267+ nshow (PRef _ (UN "Z")) = "Z"
268+ nshow (PApp _ (PRef _ (UN "S")) [x]) =
269+ "S " ++ addBrackets (nshow (getTm x))
270+ nshow t = show t
272271
273272 -- if there's any {n} replace with {n=n}
274273 expandBraces ('{' : xs)