07f572a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3336 from steshaw/consolidate-regxxx-non-executable-tests-into-regression002

Consolidate regxxx tests into regression002

commit07f572a1ececf8f592b74b9a9fe9ff18b34e6924 authorNiklas Larsson <metaniklas@gmail.com> dateSun 7 Aug 2016, 16:46 (10 years ago) parent54fadff 46209a7

70 files changed+171−203

compare with master

unifiedsplit

test/TestData.hs+3−21

@@ -215,48 +215,30 @@ testFamiliesData = [

215215 ( 5, ANY )]),

216216 ("reg", "Regressions",

217217 [ ( 2, ANY ),

218− ( 3, ANY ),

219218 ( 4, ANY ),

220219 ( 5, ANY ),

221− ( 6, ANY ),

222− ( 7, ANY ),

223− ( 10, ANY ),

224220 ( 13, ANY ),

225221 ( 16, ANY ),

226222 ( 17, ANY ),

227− ( 18, ANY ),

228223 ( 20, ANY ),

229− ( 23, ANY ),

230224 ( 24, ANY ),

231225 ( 25, ANY ),

232226 ( 27, ANY ),

233− ( 28, ANY ),

234227 ( 29, C_CG ),

235228 ( 31, ANY ),

236229 ( 32, ANY ),

237− ( 34, ANY ),

238− ( 35, ANY ),

239230 ( 39, ANY ),

240231 ( 40, ANY ),

241232 ( 41, ANY ),

242233 ( 42, ANY ),

243− ( 44, ANY ),

244234 ( 45, ANY ),

245235 ( 48, ANY ),

246− ( 49, ANY ),

247− ( 50, ANY ),

248236 ( 52, C_CG ),

249− ( 54, ANY ),

250− ( 55, ANY ),

251− ( 56, ANY ),

252237 ( 67, ANY ),

253− ( 68, ANY ),

254− ( 69, ANY ),

255− ( 70, ANY ),

256− ( 72, ANY ),

257238 ( 75, ANY )]),

258− ("regression", "Regression (loner)",

259− [ ( 1 , ANY )]),

239+ ("regression", "Regression",

240+ [ ( 1 , ANY ),

241+ ( 2 , ANY )]),

260242 ("sourceLocation", "Source location",

261243 [ ( 1 , ANY )]),

262244 ("sugar", "Syntactic sugar",

test/reg003/expecteddeleted−6

@@ -1,6 +0,0 @@

1−reg003a.idr:4:11:When checking type of Main.ECons:

2−No such variable OddList

3−reg003a.idr:7:11:When checking type of Main.OCons:

4−No such variable EvenList

5−reg003a.idr:9:6:When checking type of Main.test:

6−No such variable EvenList

test/reg003/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --check reg003.idr

3−${IDRIS:-idris} $@ --check reg003a.idr

4−rm -f *.ibc

test/reg006/expecteddeleted−2

@@ -1,2 +0,0 @@

1−reg006.idr:17:1:

2−RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

test/reg006/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg006.idr --check

3−rm -f *.ibc

test/reg010/expecteddeleted−3

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

1−reg010.idr:5:15:

2−When checking left hand side of with block in usubst.unsafeSubst:

3−Can't match on with block in usubst.unsafeSubst warg a P x x px

test/reg010/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg010.idr --check --nocolour

test/reg018/expecteddeleted−11

@@ -1,11 +0,0 @@

1−reg018a.idr:16:1:

2−conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

3−reg018a.idr:21:1:

4−conat.loopForever is possibly not total due to: conat.minusCoNat

5−reg018b.idr:8:1:

6−A.showB is possibly not total due to recursive path A.showB --> A.showB

7−reg018b.idr:11:1:

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

9−reg018c.idr:21:1:

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

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

test/reg018/rundeleted−6

@@ -1,6 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg018a.idr --check

3−${IDRIS:-idris} $@ reg018b.idr --check

4−${IDRIS:-idris} $@ reg018c.idr --check

5−${IDRIS:-idris} $@ reg018d.idr --check

6−rm *.ibc

test/reg023/expecteddeleted−7

@@ -1,7 +0,0 @@

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

2− f Nat

3−

4−Type mismatch between

5− Nat (Type of 0)

6−and

7− f Nat (Expected type)

test/reg023/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg023.idr --check

3−rm -f *.ibc

test/reg028/expecteddeleted−5

@@ -1,5 +0,0 @@

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

2−reg028a.idr:17:14-19:

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

4−reg028a.idr:11:1:

5−tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/reg028/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg028.idr --check

3−${IDRIS:-idris} $@ reg028a.idr --check

4−rm -f *.ibc

test/reg034/expecteddeleted−4

@@ -1,4 +0,0 @@

1−reg034.idr:6:5:When checking left hand side of bar:

2−Can't match on bar xs xs Refl

3−reg034.idr:9:5:When checking left hand side of foo:

4−Can't match on foo f x x Refl

test/reg034/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --check reg034.idr

3−rm -f reg034 *.ibc

test/reg035/expecteddeleted−1

@@ -1 +0,0 @@

1−reg035b.idr:8:6:No such variable __pi_arg

test/reg035/rundeleted−5

@@ -1,5 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --check reg035.idr

3−${IDRIS:-idris} $@ --nocolour --check reg035a.lidr

4−${IDRIS:-idris} $@ --nocolour --check reg035b.idr

5−rm -f *.ibc

test/reg044/expecteddeleted−15

@@ -1,15 +0,0 @@

1−reg044.idr:4:6-11:

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

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

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

5−

6−Type mismatch between

7− b = b (Type of Refl)

8−and

9− a = b (Expected type)

10−

11−Specifically:

12− Type mismatch between

13− b

14− and

15− a

test/reg044/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg044.idr --check

3−rm -f *.ibc

test/reg049/expecteddeleted−6

@@ -1,6 +0,0 @@

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

2−Void is not Main.Foo

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

4− Void

5−

6−No such variable Bogus

test/reg049/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --check $@ reg049.idr

3−rm -f *.ibc

test/reg050/expecteddeleted−10

@@ -1,10 +0,0 @@

1−./badbangop.idr:7:1: error: ! is

2− not a valid

3− operator, expected: space

4−(!) : List a -> Nat -> Maybe a

5−^

6−./baddoublebang.idr:6:28: error: unexpected

7− Operator without known fixity:

8− !!, expected: space

9−doubleBang mmn = do pure !!mmn

10− ^

test/reg050/rundeleted−5

@@ -1,5 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --check working.idr

3−${IDRIS:-idris} $@ --nocolour --check badbangop.idr

4−${IDRIS:-idris} $@ --nocolour --check baddoublebang.idr

5−rm -f *.ibc

test/reg054/expecteddeleted−13

@@ -1,13 +0,0 @@

1−reg054.idr:18:5:When checking left hand side of inf:

2−When checking an application of constructor Main.MkInfer:

3− Attempting concrete match on polymorphic argument: 0

4−reg054.idr:34:7:When checking left hand side of weird:

5−No explicit types on left hand side: Char

6−reg054.idr:37:8:When checking left hand side of weird':

7−No explicit types on left hand side: Nat

8−reg054.idr:40:1-8:When checking left hand side of tctrick:

9−When checking an application of Main.tctrick:

10− Type mismatch between

11− Maybe a1 (Type of Just x)

12− and

13− a (Expected type)

test/reg054/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg054.idr --check

test/reg055/expecteddeleted−9

@@ -1,9 +0,0 @@

1−reg055.idr:5:3:When checking left hand side of g:

2−Can't match on g (f 0)

3−reg055.idr:8:3:When checking left hand side of h:

4−Can't match on h x x

5−reg055a.idr:8:5:When checking left hand side of foo:

6−When checking an application of constructor Foo.CAny:

7− Attempting concrete match on polymorphic argument: Nothing

8−reg055a.idr:13:7:When checking left hand side of Foo.apply:

9−Can't match on apply (\x => \y => x) a

test/reg055/rundeleted−5

@@ -1,5 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg055.idr --check

3−${IDRIS:-idris} $@ --nocolour reg055a.idr --check

4−rm -f *.ibc

5−

test/reg056/expecteddeleted−2

@@ -1,2 +0,0 @@

1−reg056.idr:7:7:dodgy n m Refl is a valid case

2−reg056.idr:10:6:nonk Refl is a valid case

test/reg056/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg056.idr -o reg056

3−rm -f *.ibc

test/reg068/expecteddeleted−8

@@ -1,8 +0,0 @@

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

2−This is likely to lead to problems!

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

4−This is likely to lead to problems!

5−reg068.idr:2:8-11:WARNING: nat is bound as an implicit

6− Did you mean to refer to Main.nat?

7−reg068.idr:2:6:When checking constructor Main.ze:

8−Type level variable nat is not Main.nat

test/reg068/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg068.idr --check

3−rm -f *.ibc

test/reg069/expecteddeleted−1

@@ -1 +0,0 @@

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

test/reg069/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg069.idr --check

3−rm -f *.ibc

test/reg070/expecteddeleted−2

@@ -1,2 +0,0 @@

1−reg070.idr:7:1:

2−Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

test/reg070/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ reg070.idr --check

3−rm -f *.ibc

test/reg072/expecteddeleted−14

@@ -1,14 +0,0 @@

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

2− Void

3−

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

5− Type mismatch between

6− x = x (Type of Refl)

7− and

8− (-0.0) = 0.0 (Expected type)

9−

10− Specifically:

11− Type mismatch between

12− -0.0

13− and

14− 0.0

test/reg072/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ DoubleEquality.idr --check

3−rm -f *.ibc

test/reg007/A.lidr → test/regression002/A.lidrrenamed

The content is the same.

test/reg072/DoubleEquality.idr → test/regression002/DoubleEquality.idrrenamed

The content is the same.

test/reg069/Mod.idr → test/regression002/Mod.idrrenamed

The content is the same.

test/reg050/badbangop.idr → test/regression002/badbangop.idrrenamed

The content is the same.

test/reg050/baddoublebang.idr → test/regression002/baddoublebang.idrrenamed

The content is the same.

test/regression002/expectednew file+133

@@ -0,0 +1,133 @@

1+reg003a.idr:4:11:When checking type of Main.ECons:

2+No such variable OddList

3+reg003a.idr:7:11:When checking type of Main.OCons:

4+No such variable EvenList

5+reg003a.idr:9:6:When checking type of Main.test:

6+No such variable EvenList

7+reg006.idr:17:1:

8+RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

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

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

11+ 0 = 1

12+

13+Type mismatch between

14+ n = lala (Type of isSame)

15+and

16+ 0 = 1 (Expected type)

17+

18+Specifically:

19+ Type mismatch between

20+ 1

21+ and

22+ 0

23+reg010.idr:5:15:

24+When checking left hand side of with block in usubst.unsafeSubst:

25+Can't match on with block in usubst.unsafeSubst warg a P x x px

26+reg018a.idr:16:1:

27+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

28+reg018a.idr:21:1:

29+conat.loopForever is possibly not total due to: conat.minusCoNat

30+reg018b.idr:8:1:

31+A.showB is possibly not total due to recursive path A.showB --> A.showB

32+reg018b.idr:11:1:

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

34+reg018c.idr:21:1:

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

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

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

38+ f Nat

39+

40+Type mismatch between

41+ Nat (Type of 0)

42+and

43+ f Nat (Expected type)

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

45+reg028a.idr:17:14-19:

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

47+reg028a.idr:11:1:

48+tbad.qsort' is possibly not total due to: with block in tbad.qsort'

49+reg034.idr:6:5:When checking left hand side of bar:

50+Can't match on bar xs xs Refl

51+reg034.idr:9:5:When checking left hand side of foo:

52+Can't match on foo f x x Refl

53+reg035b.idr:8:6:No such variable __pi_arg

54+reg044.idr:4:6-11:

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

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

57+ (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

58+

59+Type mismatch between

60+ b = b (Type of Refl)

61+and

62+ a = b (Expected type)

63+

64+Specifically:

65+ Type mismatch between

66+ b

67+ and

68+ a

69+reg049.idr:2:9:When checking constructor Main.Bogus:

70+Void is not Main.Foo

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

72+ Void

73+

74+No such variable Bogus

75+./badbangop.idr:7:1: error: ! is

76+ not a valid

77+ operator, expected: space

78+(!) : List a -> Nat -> Maybe a

79+^

80+./baddoublebang.idr:6:28: error: unexpected

81+ Operator without known fixity:

82+ !!, expected: space

83+doubleBang mmn = do pure !!mmn

84+ ^

85+reg054.idr:18:5:When checking left hand side of inf:

86+When checking an application of constructor Main.MkInfer:

87+ Attempting concrete match on polymorphic argument: 0

88+reg054.idr:34:7:When checking left hand side of weird:

89+No explicit types on left hand side: Char

90+reg054.idr:37:8:When checking left hand side of weird':

91+No explicit types on left hand side: Nat

92+reg054.idr:40:1-8:When checking left hand side of tctrick:

93+When checking an application of Main.tctrick:

94+ Type mismatch between

95+ Maybe a1 (Type of Just x)

96+ and

97+ a (Expected type)

98+reg055.idr:5:3:When checking left hand side of g:

99+Can't match on g (f 0)

100+reg055.idr:8:3:When checking left hand side of h:

101+Can't match on h x x

102+reg055a.idr:8:5:When checking left hand side of foo:

103+When checking an application of constructor Foo.CAny:

104+ Attempting concrete match on polymorphic argument: Nothing

105+reg055a.idr:13:7:When checking left hand side of Foo.apply:

106+Can't match on apply (\x => \y => x) a

107+reg056.idr:7:7:dodgy n m Refl is a valid case

108+reg056.idr:10:6:nonk Refl is a valid case

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

110+This is likely to lead to problems!

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

112+This is likely to lead to problems!

113+reg068.idr:2:8-11:WARNING: nat is bound as an implicit

114+ Did you mean to refer to Main.nat?

115+reg068.idr:2:6:When checking constructor Main.ze:

116+Type level variable nat is not Main.nat

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

118+reg070.idr:7:1:

119+Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

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

121+ Void

122+

123+When checking argument value to function Prelude.Basics.the:

124+ Type mismatch between

125+ x = x (Type of Refl)

126+ and

127+ (-0.0) = 0.0 (Expected type)

128+

129+ Specifically:

130+ Type mismatch between

131+ -0.0

132+ and

133+ 0.0

test/reg003/reg003.idr → test/regression002/reg003.idrrenamed

The content is the same.

test/reg003/reg003a.idr → test/regression002/reg003a.idrrenamed

The content is the same.

test/reg006/reg006.idr → test/regression002/reg006.idrrenamed

The content is the same.

test/reg007/reg007.lidr → test/regression002/reg007.lidrrenamed

The content is the same.

test/reg010/reg010.idr → test/regression002/reg010.idrrenamed

The content is the same.

test/reg018/reg018a.idr → test/regression002/reg018a.idrrenamed

The content is the same.

test/reg018/reg018b.idr → test/regression002/reg018b.idrrenamed

The content is the same.

test/reg018/reg018c.idr → test/regression002/reg018c.idrrenamed

The content is the same.

test/reg018/reg018d.idr → test/regression002/reg018d.idrrenamed

The content is the same.

test/reg023/reg023.idr → test/regression002/reg023.idrrenamed

The content is the same.

test/reg028/reg028.idr → test/regression002/reg028.idrrenamed

The content is the same.

test/reg028/reg028a.idr → test/regression002/reg028a.idrrenamed

The content is the same.

test/reg034/reg034.idr → test/regression002/reg034.idrrenamed

The content is the same.

test/reg035/reg035.idr → test/regression002/reg035.idrrenamed

The content is the same.

test/reg035/reg035a.lidr → test/regression002/reg035a.lidrrenamed

The content is the same.

test/reg035/reg035b.idr → test/regression002/reg035b.idrrenamed

The content is the same.

test/reg044/reg044.idr → test/regression002/reg044.idrrenamed

The content is the same.

test/reg049/reg049.idr → test/regression002/reg049.idrrenamed

The content is the same.

test/reg054/reg054.idr → test/regression002/reg054.idrrenamed

The content is the same.

test/reg055/reg055.idr → test/regression002/reg055.idrrenamed

The content is the same.

test/reg055/reg055a.idr → test/regression002/reg055a.idrrenamed

The content is the same.

test/reg056/reg056.idr → test/regression002/reg056.idrrenamed

The content is the same.

test/reg068/reg068.idr → test/regression002/reg068.idrrenamed

The content is the same.

test/reg069/reg069.idr → test/regression002/reg069.idrrenamed

The content is the same.

test/reg070/reg070.idr → test/regression002/reg070.idrrenamed

The content is the same.

test/regression002/runnew file+35

@@ -0,0 +1,35 @@

1+#!/usr/bin/env bash

3+${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!

4+:load reg003.idr

5+:load reg003a.idr

6+:load reg006.idr

7+:load reg007.lidr

8+:load reg010.idr

9+:load reg018a.idr

10+:load reg018b.idr

11+:load reg018c.idr

12+:load reg018d.idr

13+:load reg023.idr

14+:load reg028.idr

15+:load reg028a.idr

16+:load reg034.idr

17+:load reg035.idr

18+:load reg035a.lidr

19+:load reg035b.idr

20+:load reg044.idr

21+:load reg049.idr

22+:load working.idr

23+:load badbangop.idr

24+:load baddoublebang.idr

25+:load reg054.idr

26+:load reg055.idr

27+:load reg055a.idr

28+:load reg056.idr

29+:load reg068.idr

30+:load reg069.idr

31+:load reg070.idr

32+:load DoubleEquality.idr

33+!

34+

35+rm -f *.ibc

test/reg050/working.idr → test/regression002/working.idrrenamed

The content is the same.