git.iko.soy/Idris-dev
on master help sign in
Modify pretty printer for lambdas

Batch sequences of lambdas into comma separated lists, as a user would most likely write

commit4057b48929863615be067acdb1bcf4d4ac0016fe authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Nov 2016, 13:41 (10 years ago) parent9dd3e00
2 files changed+13−4
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+12−3 test/regression002/expected+1−1
src/Idris/AbsSyntaxTree.hs+12−3
@@ -1788,9 +1788,18 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17881788 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
17891789 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
17901790 prettySe d p bnd (PLam fc n nfc ty sc) =
1791− depth d . bracket p startPrec . group . align . hang 2 $
1792− text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1793− prettySe (decD d) startPrec ((n, False):bnd) sc
1791+ let (ns, sc') = getLamNames [n] sc in
1792+ depth d . bracket p startPrec . group . align . hang 2 $
1793+ text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1794+ prettySe (decD d) startPrec ((n, False):bnd) sc'
1795+ where
1796+ getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1797+ getLamNames acc sc = (reverse acc, sc)
1798+
1799+ prettyBindingsOf [] t = text ""
1800+ prettyBindingsOf [n] t = prettyBindingOf n t
1801+ prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1802+ prettyBindingsOf ns t
17941803 prettySe d p bnd (PLet fc n nfc ty v sc) =
17951804 depth d . bracket p startPrec . group . align $
17961805 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
test/regression002/expected+1−1
@@ -103,7 +103,7 @@ reg055a.idr:8:5:When checking left hand side of foo:
103103When checking an application of constructor Foo.CAny:
104104 Attempting concrete match on polymorphic argument: Nothing
105105reg055a.idr:13:7:When checking left hand side of Foo.apply:
106−Can't match on apply (\x => \y => x) a
106+Can't match on apply (\x, y => x) a
107107reg056.idr:7:7:dodgy n m Refl is a valid case
108108reg056.idr:10:6:nonk Refl is a valid case
109109reg068.idr:1:6:Main.nat has a name which may be implicitly bound.