git.iko.soy/Idris-dev
on master help sign in
Pretty-printer for new nested dependent pair syntax
7bf0ea3David Raymond Christiansen
src/Idris/AbsSyntaxTree.hs+27−7
compare with master
unifiedsplit
@@ -1820,20 +1820,35 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1820 TypeOrTerm -> id
1820 TypeOrTerm -> id
1821 IsType -> annName pairTy
1821 IsType -> annName pairTy
1822 IsTerm -> annName pairCon
1822 IsTerm -> annName pairCon
1823− prettySe d p bnd (PDPair _ _ pun l t r) =
1823+ prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1824− depth d $
1824+ | Just elts <- dPairElts dpair
1825+ = depth d . enclose (annotated lparen) (annotated rparen) .
1826+ align . group . vsep . punctuate (space <> annotated (text "**")) $
1827+ ppElts elts bnd
1828+ | otherwise
1829+ = depth d $
1825− annotated lparen <>
1830+ annotated lparen <>
1826− left <+>
1831+ left <+>
1827− annotated (text "**") <+>
1832+ annotated (text "**") <+>
1828− prettySe (decD d) startPrec (addBinding bnd) r <>
1833+ prettySe (decD d) startPrec (addBinding bnd) r <>
1829− annotated rparen
1834+ annotated rparen
1830 where annotated = case pun of
1835 where annotated = case pun of
1831 IsType -> annName sigmaTy
1836 IsType -> annName sigmaTy
1832 IsTerm -> annName sigmaCon
1837 IsTerm -> annName sigmaCon
1833 TypeOrTerm -> id
1838 TypeOrTerm -> id
1839+
1834 (left, addBinding) = case (l, pun) of
1840 (left, addBinding) = case (l, pun) of
1835 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1841 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1836 _ -> (prettySe (decD d) startPrec bnd l, id)
1842 _ -> (prettySe (decD d) startPrec bnd l, id)
1843+
1844+ ppElts [] bs = []
1845+ ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1846+ ppElts ((PRef _ _ n, t):rs) bs
1847+ | IsType <- pun
1848+ = (bindingOf n False <+> colon <+>
1849+ prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1850+ ppElts ((l, t):rs) bs
1851+ = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1837 prettySe d p bnd (PAlternative ns a as) =
1852 prettySe d p bnd (PAlternative ns a as) =
1838 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1853 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1839 where
1854 where
@@ -1951,6 +1966,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1951 | otherwise = Just [x, y]
1966 | otherwise = Just [x, y]
1952 pairElts _ = Nothing
1967 pairElts _ = Nothing
1953
1968
1969+ dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
1970+ dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
1971+ | otherwise = Just [(l, t), (Placeholder, r)]
1972+ dPairElts _ = Nothing
1973+
1954 natns = "Prelude.Nat."
1974 natns = "Prelude.Nat."
1955
1975
1956 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
1976 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
test/proof003/expected−12
@@ -1,15 +1,3 @@
1−Parity.idr:15:18-23:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
3−Parity.idr:22:18-23:
4−This style of tactic proof is deprecated. See %runElab for the replacement.
5−test015.idr:88:15-20:
6−This style of tactic proof is deprecated. See %runElab for the replacement.
7−test015.idr:97:16-21:
8−This style of tactic proof is deprecated. See %runElab for the replacement.
9−test015.idr:108:20-25:
10−This style of tactic proof is deprecated. See %runElab for the replacement.
11−test015.idr:136:20-25:
12−This style of tactic proof is deprecated. See %runElab for the replacement.
1300101010
100101010
1401011001
201011001
15010000011
3010000011
test/proof003/run+1−1
@@ -1,4 +1,4 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−idris $@ test015.idr --nocolour --consolewidth 80 -o test015
2+idris $@ test015.idr --nocolour --consolewidth 80 --no-tactic-deprecation-warnings -o test015
3./test015
3./test015
4rm -f test015 Parity.ibc test015.ibc
4rm -f test015 Parity.ibc test015.ibc