git.iko.soy/Idris-dev
on master help sign in
Modify pretty printer for lambdas
4057b48Edwin Brady
src/Idris/AbsSyntaxTree.hs+12−3
compare with master
unifiedsplit
@@ -1788,9 +1788,18 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1788 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1788 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1789 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1789 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1790 prettySe d p bnd (PLam fc n nfc ty sc) =
1790 prettySe d p bnd (PLam fc n nfc ty sc) =
1791+ let (ns, sc') = getLamNames [n] sc in
1791− depth d . bracket p startPrec . group . align . hang 2 $
1792+ depth d . bracket p startPrec . group . align . hang 2 $
1792− text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1793+ text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1793− prettySe (decD d) startPrec ((n, False):bnd) sc
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
1794 prettySe d p bnd (PLet fc n nfc ty v sc) =
1803 prettySe d p bnd (PLet fc n nfc ty v sc) =
1795 depth d . bracket p startPrec . group . align $
1804 depth d . bracket p startPrec . group . align $
1796 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1805 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:
103When checking an application of constructor Foo.CAny:
103When checking an application of constructor Foo.CAny:
104 Attempting concrete match on polymorphic argument: Nothing
104 Attempting concrete match on polymorphic argument: Nothing
105reg055a.idr:13:7:When checking left hand side of Foo.apply:
105reg055a.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
107reg056.idr:7:7:dodgy n m Refl is a valid case
107reg056.idr:7:7:dodgy n m Refl is a valid case
108reg056.idr:10:6:nonk Refl is a valid case
108reg056.idr:10:6:nonk Refl is a valid case
109reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
109reg068.idr:1:6:Main.nat has a name which may be implicitly bound.