624d6c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix precedence of application vs arrows in pprint

Changes Prelude.Applicative.<$> : Applicative f => (f (a -> b)) -> (f a) -> f b into Prelude.Applicative.<$> : Applicative f => f (a -> b) -> f a -> f b

commit624d6c71264a08034f31600005efc8b83d2e0d37 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 4 May 2014, 19:40 (12 years ago) parent8c5bef6

5 files changed+9−3

compare with master

unifiedsplit

idris.cabal+2 src/Idris/AbsSyntaxTree.hs+2−2 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+2−2

@@ -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

@@ -1253,7 +1253,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12531253 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

12541254 f == sUN "Symbol_" = annotate AnnConstType $

12551255 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1256− prettySe p bnd (PApp _ f as) =

1256+ prettySe p bnd (PApp _ f as) = -- Normal prefix applications

12571257 let args = getExps as

12581258 fp = prettySe 1 bnd f

12591259 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}"