ad11ce5 · Idris-dev · git.iko.soy

idris.cabal+2

compare with master

unifiedsplit

@@ -235,6 +235,8 @@ Extra-source-files:

235 test/reg042/run

236 test/reg042/*.idr

237 test/reg042/expected

238+ test/reg043/run

239+ test/reg043/expected

238

240

239 test/basic001/run

241 test/basic001/run

240 test/basic001/*.idr

242 test/basic001/*.idr

src/Idris/AbsSyntaxTree.hs+6−5

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

1193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1194 | otherwise =

1195 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)

1197 where

1198 st =

1199 case s of

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

1225 else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

1226 prettySe p bnd (PAppBind _ (PRef _ f) [])

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

1229 | UN nm <- basename op

1230 , not (tnull nm) &&

1231 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

@@ -1249,10 +1249,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1249 Just f' -> prettySe (prec f'-1) bnd r

1250 inFix l r = align . group $

1251 (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

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

1254+ f == sUN "Symbol_" = annotate AnnConstType $

1254− f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

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

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

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

1256 let args = getExps as

1257 let args = getExps as

1257 fp = prettySe 1 bnd f

1258 fp = prettySe 1 bnd f

1258 in

1259 in

test/reg041/expected+1−1

@@ -1,3 +1,3 @@

1Type 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)

3Z

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+