09263c1 · Idris-dev · git.iko.soy

src/Idris/Output.hs+3−1

compare with master

unifiedsplit

@@ -21,6 +21,7 @@ import Idris.IdeMode

21

22import Util.Pretty

23import Util.ScreenSize (getScreenWidth)

24+import Util.System (isATTY)

24

25

25import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

26import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

26

27

@@ -67,13 +68,14 @@ iRender d = do w <- getWidth

67 let ideMode = case idris_outputmode ist of

68 let ideMode = case idris_outputmode ist of

68 IdeMode _ _ -> True

69 IdeMode _ _ -> True

69 _ -> False

70 _ -> False

71+ tty <- runIO isATTY

70 case w of

72 case w of

71 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

73 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

72 ColsWide n -> return $

74 ColsWide n -> return $

73 if n < 1

75 if n < 1

74 then renderPretty 1.0 1000000000 d

76 then renderPretty 1.0 1000000000 d

75 else renderPretty 0.8 n d

77 else renderPretty 0.8 n d

76− AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d

78+ AutomaticWidth | ideMode || not tty -> return $ renderPretty 1.0 80 d

77 | otherwise -> do width <- runIO getScreenWidth

79 | otherwise -> do width <- runIO getScreenWidth

78 return $ renderPretty 0.8 width d

80 return $ renderPretty 0.8 width d

79

81

test/TestRun.hs+4−3

@@ -9,6 +9,7 @@ import qualified Data.IntMap as IMap

9

10import System.Directory

11import System.Environment

12+import System.Exit

12import System.Process

13import System.Process

13import System.Info

14import System.Info

14import System.IO

15import System.IO

@@ -90,10 +91,10 @@ mkGoldenTests testFamilies flags =

90-- this thing.

91-- this thing.

91runTest :: String -> Flags -> IO ()

92runTest :: String -> Flags -> IO ()

92runTest path flags = do

93runTest path flags = do

93− let run = (proc "bash" ("run" : flags)) {cwd = Just path,

94+ let run = (proc "bash" ("run" : flags)) {cwd = Just path}

94− std_out = CreatePipe}

95− (_, output, _) <- readCreateProcessWithExitCode run ""

95+ (_, output, error_out) <- readCreateProcessWithExitCode run ""

96 writeFile (path </> "output") (normalise output)

97+ when (error_out /= "") $ hPutStrLn stderr ("\nError: " ++ path ++ "\n" ++ error_out)

97 where

98 where

98 -- Normalise paths e.g. '.\foo.idr' to './foo.idr'.

99 -- Normalise paths e.g. '.\foo.idr' to './foo.idr'.

99 -- Also embedded paths e.g. ".\\Prelude\\List.idr" to "./Prelude/List.idr".

100 -- Also embedded paths e.g. ".\\Prelude\\List.idr" to "./Prelude/List.idr".

test/basic006/expected+1−2

@@ -1,5 +1,4 @@

1−test020a.idr:16:18:

2−When checking right hand side of foo with expected type

1+test020a.idr:16:18:When checking right hand side of foo with expected type

3 List a

2 List a

4

3

5When checking an application of function Prelude.List.reverse:

4When checking an application of function Prelude.List.reverse:

test/basic009/expected+1−2

@@ -1,8 +1,7 @@

1MAIN-PASS

2Faulty.idr:6:9-12:WARNING: num is bound as an implicit

3 Did you mean to refer to A.num?

4−Faulty.idr:7:7:

5−When checking right hand side of fault with expected type

4+Faulty.idr:7:7:When checking right hand side of fault with expected type

6 num = 0

5 num = 0

7

6

8Type mismatch between

7Type mismatch between

test/basic018/expected+1−2

@@ -2,8 +2,7 @@ basic018.idr:7:12-17:WARNING: thing is bound as an implicit

2 Did you mean to refer to Main.thing?

3basic018.idr:12:8-13:WARNING: thing is bound as an implicit

4 Did you mean to refer to Main.thing?

5−basic018.idr:13:6:

6−When checking right hand side of test with expected type

5+basic018.idr:13:6:When checking right hand side of test with expected type

7 thing = S 41

6 thing = S 41

8

7

9Type mismatch between

8Type mismatch between

test/directives001/expected+2−4

@@ -6,9 +6,7 @@ directives001.idr:15:7:Use of deprecated name directives001.Foo

6To be replaced with `Bar`.

7directives001.idr:15:7:Use of deprecated name directives001.Foo

8To be replaced with `Bar`.

9−directives001.idr:26:8:

10−Use of a fragile construct directives001.mkBar

9+directives001.idr:26:8:Use of a fragile construct directives001.mkBar

11How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

10How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

12−directives001.idr:26:8:

13−Use of a fragile construct directives001.mkBar

11+directives001.idr:26:8:Use of a fragile construct directives001.mkBar

14How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

12How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

test/docs003/expected+1−2

@@ -6,8 +6,7 @@ Parameters:

6

7Methods:

8 map : Functor f => (func : a -> b) -> f a -> f b

9− Apply a function across everything of type 'a' in a

9+ Apply a function across everything of type 'a' in a parameterised type

10− parameterised type

11

10

12 The function is Total

11 The function is Total

13Implementations:

12Implementations:

test/error003/expected+1−2

@@ -1,5 +1,4 @@

1−ErrorReflection.idr:68:5:

2−When checking right hand side of bad with expected type

1+ErrorReflection.idr:68:5:When checking right hand side of bad with expected type

3 Tm [] TUnit

2 Tm [] TUnit

4

3

5DSL type error: (t(504) => t'(503)) doesn't match ()

4DSL type error: (t(504) => t'(503)) doesn't match ()

test/error005/expected+5−10

@@ -1,34 +1,29 @@

1−error005.idr:13:1:

2−When checking right hand side of two with expected type

1+error005.idr:13:1:When checking right hand side of two with expected type

3 Fin 2

2 Fin 2

4

3

5When checking argument prf to function Data.Fin.fromInteger:

4When checking argument prf to function Data.Fin.fromInteger:

6 When using 2 as a literal for a Fin 2

5 When using 2 as a literal for a Fin 2

7 2 is not strictly less than 2

6 2 is not strictly less than 2

8−error005.idr:16:1:

9−When checking right hand side of hahaha with expected type

7+error005.idr:16:1:When checking right hand side of hahaha with expected type

10 Fin n

8 Fin n

11

9

12When checking argument prf to function Data.Fin.fromInteger:

10When checking argument prf to function Data.Fin.fromInteger:

13 When using 0 as a literal for a Fin n

11 When using 0 as a literal for a Fin n

14 0 is not strictly less than n

12 0 is not strictly less than n

15−error005.idr:22:1:

16−When checking right hand side of notOk with expected type

13+error005.idr:22:1:When checking right hand side of notOk with expected type

17 Fin (plus 2 n)

14 Fin (plus 2 n)

18

15

19When checking argument prf to function Data.Fin.fromInteger:

16When checking argument prf to function Data.Fin.fromInteger:

20 When using 2 as a literal for a Fin (S (S n))

17 When using 2 as a literal for a Fin (S (S n))

21 2 is not strictly less than S (S n)

18 2 is not strictly less than S (S n)

22−error005.idr:23:24:

23−When checking right hand side of b0rken with expected type

19+error005.idr:23:24:When checking right hand side of b0rken with expected type

24 Fin 3

20 Fin 3

25

21

26When checking argument prf to function Data.Fin.fromInteger:

22When checking argument prf to function Data.Fin.fromInteger:

27 When using n as a literal for a Fin 3

23 When using n as a literal for a Fin 3

28 Could not show that n is less than 3 because n is a bound

24 Could not show that n is less than 3 because n is a bound

29 variable instead of a constant Integer

25 variable instead of a constant Integer

30−error005.idr:28:1:

31−When checking right hand side of x with expected type

26+error005.idr:28:1:When checking right hand side of x with expected type

32 Fin 4

27 Fin 4

33

28

34When checking argument prf to function Data.Fin.fromInteger:

29When checking argument prf to function Data.Fin.fromInteger:

test/layout001/expected+1−2

@@ -72,8 +72,7 @@ y

72^

73Checking layout001n.idr

74Checking mplus1.idr

75−mplus1.idr:13:31:

76−When checking right hand side of term with expected type

75+mplus1.idr:13:31:When checking right hand side of term with expected type

77 Maybe Int

76 Maybe Int

78

77

79When checking an application of function Prelude.Applicative.pure:

78When checking an application of function Prelude.Applicative.pure:

test/proof011/expected+14−10

@@ -1,14 +1,18 @@

1−proof011.idr:19:9:

2−When checking right hand side of vassoc' with expected type

1+proof011.idr:19:9:When checking right hand side of vassoc' with expected type

3 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

2 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

4

3

5−rewriting xs ++ ys ++ xs to (xs ++ ys) ++

4+rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

6− xs did not change type x :: xs ++ ys ++ zs =

5+ xs ++

6+ ys ++ zs =

7+ x ::

7− x :: (xs ++ ys) ++ zs

8+ (xs ++ ys) ++

8−proof011a.idr:13:9:

9+ zs

9−When checking right hand side of vassoc' with expected type

10+proof011a.idr:13:9:When checking right hand side of vassoc' with expected type

10 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

11 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

11

12

12−rewriting xs ++ ys ++ xs to (xs ++ ys) ++

13+rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

13− xs did not change type x :: xs ++ ys ++ zs =

14+ xs ++

15+ ys ++ zs =

16+ x ::

14− x :: (xs ++ ys) ++ zs

17+ (xs ++ ys) ++

18+ zs

test/quasiquote003/expected+1−2

@@ -1,5 +1,4 @@

1−NoInfer.idr:11:5:

2−When checking right hand side of zzz with expected type

1+NoInfer.idr:11:5:When checking right hand side of zzz with expected type

3 TT

2 TT

4

3

5No such variable k

4No such variable k

test/reg007/expected+1−2

@@ -1,6 +1,5 @@

1reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:11-17:

3−When checking right hand side of hurrah with expected type

2+reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type

4 0 = 1

3 0 = 1

5

4

6Type mismatch between

5Type mismatch between

test/reg018/expected+1−2

@@ -8,5 +8,4 @@ reg018b.idr:11:1:

8A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

9reg018c.idr:21:1:

10CodataTest.inf is possibly not total due to: with block in CodataTest.inf

11−reg018d.idr:8:1:

12−Main.pull is not total as there are missing cases

11+reg018d.idr:8:1:Main.pull is not total as there are missing cases

test/reg023/expected+1−2

@@ -1,5 +1,4 @@

1−reg023.idr:7:5:

2−When checking right hand side of bad with expected type

1+reg023.idr:7:5:When checking right hand side of bad with expected type

3 f Nat

2 f Nat

4

3

5Type mismatch between

4Type mismatch between

test/reg027/expected+1−2

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

1<<int fn>>

26

3−reg027a.idr:9:16:

4−Overlapping implementation: Show (Int -> a) already defined

3+reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined

test/reg028/expected+1−2

@@ -1,5 +1,4 @@

1−reg028.idr:5:1:

2−tbad.bad is possibly not total due to: with block in tbad.bad

1+reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

3reg028a.idr:17:14-19:

2reg028a.idr:17:14-19:

4This style of tactic proof is deprecated. See %runElab for the replacement.

3This style of tactic proof is deprecated. See %runElab for the replacement.

5reg028a.idr:11:1:

4reg028a.idr:11:1:

test/reg044/expected+1−2

@@ -1,7 +1,6 @@

1reg044.idr:4:6-11:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−reg044.idr:4:4:

4−When checking right hand side of Main.pf with expected type

3+reg044.idr:4:4:When checking right hand side of Main.pf with expected type

5 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

4 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

6

5

7Type mismatch between

6Type mismatch between

test/reg049/expected+1−2

@@ -1,7 +1,6 @@

1reg049.idr:2:9:When checking constructor Main.Bogus:

2Void is not Main.Foo

3−reg049.idr:5:6:

4−When checking right hand side of uhOh with expected type

3+reg049.idr:5:6:When checking right hand side of uhOh with expected type

5 Void

4 Void

6

5

7No such variable Bogus

6No such variable Bogus

test/reg068/expected+1−2

@@ -1,5 +1,4 @@

1−reg068.idr:1:6:

2−Main.nat has a name which may be implicitly bound.

1+reg068.idr:1:6:Main.nat has a name which may be implicitly bound.

3This is likely to lead to problems!

2This is likely to lead to problems!

4reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

3reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

5This is likely to lead to problems!

4This is likely to lead to problems!

test/reg069/expected+1−2

@@ -1,2 +1 @@

1−Mod.idr:11:1:

2−public export Mod.natexp can't refer to export Mod.natfn

1+Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn

test/reg072/expected+1−2

@@ -1,5 +1,4 @@

1−DoubleEquality.idr:4:87:

2−When checking right hand side of oops with expected type

1+DoubleEquality.idr:4:87:When checking right hand side of oops with expected type

3 Void

2 Void

4

3

5When checking argument value to function Prelude.Basics.the:

4When checking argument value to function Prelude.Basics.the:

test/syntax001/expected+2−4

@@ -1,5 +1,4 @@

1−Syntax.idr:6:7-9:1:

2−When checking right hand side of foo with expected type

1+Syntax.idr:6:7-9:1:When checking right hand side of foo with expected type

3 Nat

2 Nat

4

3

5When checking an application of function Prelude.Interfaces.+:

4When checking an application of function Prelude.Interfaces.+:

@@ -7,8 +6,7 @@ When checking an application of function Prelude.Interfaces.+:

7 String (Type of "argh")

6 String (Type of "argh")

8 and

7 and

9 Nat (Expected type)

8 Nat (Expected type)

10−SyntaxTest.idr:5:7-6:1:

11−When checking right hand side of foo with expected type

9+SyntaxTest.idr:5:7-6:1:When checking right hand side of foo with expected type

12 Nat

10 Nat

13

11

14When checking an application of function Prelude.Interfaces.+:

12When checking an application of function Prelude.Interfaces.+:

test/totality001/expected+3−6

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

1−test010.idr:15:1:

2−Main.foo is possibly not total due to: Main.MkBad

1+test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad

3−test010a.idr:9:1:

4−main.bar is possibly not total due to: main.MkBad

2+test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

5−test010b.idr:9:1:

6−main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

test/totality002/expected+1−2

@@ -2,5 +2,4 @@ test017.idr:94:26-31:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3test017a.idr:7:1:

4scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

5−test017b.idr:4:1:

6−foo.foo is possibly not total due to recursive path foo.foo

5+test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

test/totality004/expected+1−2

@@ -1,5 +1,4 @@

1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2totality004a.idr:13:1:

3Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4−totality004a.idr:24:1:

5−Main.main is possibly not total due to: Main.process

4+totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

test/totality006/expected+1−2

@@ -1,5 +1,4 @@

1−totality006.idr:8:1:

2−Main.prf is not total as there are missing cases

1+totality006.idr:8:1:Main.prf is not total as there are missing cases

3totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

2totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

4totality006b.idr:10:1:

3totality006b.idr:10:1:

5totality006b.blargh is not total as there are missing cases

4totality006b.blargh is not total as there are missing cases

test/totality008/expected+1−2

@@ -1,2 +1 @@

1−totality008.idr:7:1:

2−Main.ElimT is possibly not total due to: Main.C2

1+totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.C2

test/totality010/expected+2−4

@@ -1,4 +1,2 @@

1−totality010.idr:27:1:

2−Main.evenNotS is not total as there are missing cases

1+totality010.idr:27:1:Main.evenNotS is not total as there are missing cases

3−totality010.idr:30:1:

4−Main.bad is possibly not total due to: Main.evenNotS

2+totality010.idr:30:1:Main.bad is possibly not total due to: Main.evenNotS

test/totality015/expected+2−4

@@ -1,6 +1,4 @@

1totality015a.idr:52:3:

2Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3−totality015a.idr:42:3:

4−Main.correct is possibly not total due to: Main.quiz

3+totality015a.idr:42:3:Main.correct is possibly not total due to: Main.quiz

5−totality015a.idr:47:3:

6−Main.wrong is possibly not total due to: Main.quiz

4+totality015a.idr:47:3:Main.wrong is possibly not total due to: Main.quiz