git.iko.soy/Idris-dev
on master help sign in
Pretty-printer for new nested dependent pair syntax
commit7bf0ea306c1fda4907c372fa8a6238d910796550 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 27 Sep 2015, 11:24 (11 years ago) parentf3ce68e
3 files changed+28−20
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+27−7 test/proof003/expected−12 test/proof003/run+1−1
src/Idris/AbsSyntaxTree.hs+27−7
@@ -1820,20 +1820,35 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
18201820 TypeOrTerm -> id
18211821 IsType -> annName pairTy
18221822 IsTerm -> annName pairCon
1823− prettySe d p bnd (PDPair _ _ pun l t r) =
1824− depth d $
1825− annotated lparen <>
1826− left <+>
1827− annotated (text "**") <+>
1828− prettySe (decD d) startPrec (addBinding bnd) r <>
1829− annotated rparen
1823+ prettySe d p bnd dpair@(PDPair _ _ pun l t r)
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 $
1830+ annotated lparen <>
1831+ left <+>
1832+ annotated (text "**") <+>
1833+ prettySe (decD d) startPrec (addBinding bnd) r <>
1834+ annotated rparen
18301835 where annotated = case pun of
18311836 IsType -> annName sigmaTy
18321837 IsTerm -> annName sigmaCon
18331838 TypeOrTerm -> id
1839+
18341840 (left, addBinding) = case (l, pun) of
18351841 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
18361842 _ -> (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
18371852 prettySe d p bnd (PAlternative ns a as) =
18381853 lparen <> text "|" <> prettyAs <> text "|" <> rparen
18391854 where
@@ -1951,6 +1966,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
19511966 | otherwise = Just [x, y]
19521967 pairElts _ = Nothing
19531968
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+
19541974 natns = "Prelude.Nat."
19551975
19561976 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.
13100101010
14201011001
153010000011
test/proof003/run+1−1
@@ -1,4 +1,4 @@
11#!/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
33./test015
44rm -f test015 Parity.ibc test015.ibc