git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1185 from david-christiansen/pprint-stuff

Pretty-print fixes

commitad11ce50c08870f0fb8b8048eb8f29d8b14ffc23 authorDavid Christiansen <david@davidchristiansen.dk> dateSun 4 May 2014, 20:16 (12 years ago) parent304fff1624d6c7
5 files changed+13−6
compare with master
unifiedsplit
idris.cabal+2 src/Idris/AbsSyntaxTree.hs+6−5 test/reg041/expected+1−1 test/reg043/expected+1 test/reg043/run+3
idris.cabal+2
@@ -235,6 +235,8 @@ Extra-source-files:
235235 test/reg042/run
236236 test/reg042/*.idr
237237 test/reg042/expected
238+ test/reg043/run
239+ test/reg043/expected
238240
239241 test/basic001/run
240242 test/basic001/*.idr
src/Idris/AbsSyntaxTree.hs+6−5
@@ -1193,7 +1193,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
11931193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
11941194 | otherwise =
11951195 bracket p 2 . group $
1196− group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1196+ group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
11971197 where
11981198 st =
11991199 case s of
@@ -1225,7 +1225,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12251225 else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f
12261226 prettySe p bnd (PAppBind _ (PRef _ f) [])
12271227 | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f
1228− prettySe p bnd (PApp _ (PRef _ op) args)
1228+ prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
12291229 | UN nm <- basename op
12301230 , not (tnull nm) &&
12311231 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
@@ -1249,10 +1249,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12491249 Just f' -> prettySe (prec f'-1) bnd r
12501250 inFix l r = align . group $
12511251 (left l <+> opName) <$> group (right r)
1252− prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1252+ prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
12531253 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1254− f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1255− prettySe p bnd (PApp _ f as) =
1254+ f == sUN "Symbol_" = annotate AnnConstType $
1255+ char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1256+ prettySe p bnd (PApp _ f as) = -- Normal prefix applications
12561257 let args = getExps as
12571258 fp = prettySe 1 bnd f
12581259 in
test/reg041/expected+1−1
@@ -1,3 +1,3 @@
11Type checking ./ott.idr
2−?prf : (x : Bool) -> (x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)
2+?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)
33Z
test/reg043/expectednew file+1
@@ -0,0 +1 @@
1+take : (m : Fin 3) -> Vect 2 Nat -> Vect (finToNat m) Nat
test/reg043/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --nocolour -e "Vect.take {n=2} {a=Nat}"
3+