9916b3f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3338 from steshaw/consolidate-unique-tests

Consolidate unique tests

commit9916b3f6909095e4306e1ba111cb444f818b98b6 authorNiklas Larsson <metaniklas@gmail.com> dateSat 6 Aug 2016, 12:12 (10 years ago) parentace75af 6f243b1

18 files changed+46−46

compare with master

unifiedsplit

idris.cabal+3−6

@@ -864,12 +864,9 @@ Extra-source-files:

864864 test/unique001/run

865865 test/unique001/*.idr

866866 test/unique001/expected

867− test/unique002/run

868− test/unique002/*.idr

869− test/unique002/expected

870− test/unique003/run

871− test/unique003/*.idr

872− test/unique003/expected

867+ test/unique004/run

868+ test/unique004/*.idr

869+ test/unique004/expected

873870

874871 test/views001/run

875872 test/views001/*.idr

test/TestData.hs+1−2

@@ -296,8 +296,7 @@ testFamiliesData = [

296296 ( 7, C_CG )]),

297297 ("unique", "Uniqueness types",

298298 [ ( 1, ANY ),

299− ( 2, ANY ),

300− ( 3, ANY )]),

299+ ( 4, ANY )]),

301300 ("universes", "Universes",

302301 [ ( 1, ANY ),

303302 ( 2, ANY )]),

test/unique001/expected−17

@@ -2,20 +2,3 @@

2219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

3338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

4438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5−unique001a.idr:33:11:Type mismatch between

6− Int -> String

7−and

8− UniqueType (Int -> String)

9−unique001a.idr:44:12:Type mismatch between

10− Int -> String

11−and

12− UniqueType (Int -> String)

13−unique001a.idr:55:12:Type mismatch between

14− UniqueType (Int -> String)

15−and

16− Int -> String

17−unique001b.idr:16:7:Borrowed name xs must not be used on RHS

18−unique001c.idr:46:6:Unique name f is used more than once

19−unique001d.idr:3:7:Borrowed name x must not be used on RHS

20−unique001e.idr:3:10:

21−Constructor Main.Nil has a UniqueType, but the data type does not

test/unique001/run+2−5

@@ -1,9 +1,6 @@

11#!/usr/bin/env bash

23${IDRIS:-idris} $@ --nocolour unique001.idr -o unique001

34./unique001

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

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

6−${IDRIS:-idris} $@ --nocolour unique001c.idr --check

7−${IDRIS:-idris} $@ --nocolour unique001d.idr --check

8−${IDRIS:-idris} $@ --nocolour unique001e.idr --check

96rm -f unique001 *.ibc

test/unique002/expecteddeleted−5

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

1−unique002.idr:15:5:Unique name xs is used more than once

2−unique002a.idr:15:5:Type mismatch between

3− Int -> String

4−and

5− UniqueType (Int -> String)

test/unique002/rundeleted−4

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

1−#!/usr/bin/env bash

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

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

4−rm -f *.ibc

test/unique003/expecteddeleted−4

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

1−unique003.idr:18:5:Type mismatch between

2− Int -> String

3−and

4− UniqueType (Int -> String)

test/unique003/rundeleted−3

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

1−#!/usr/bin/env bash

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

3−rm -f *.ibc

test/unique004/expectednew file+26

@@ -0,0 +1,26 @@

1+unique001a.idr:33:11:Type mismatch between

2+ Int -> String

3+and

4+ UniqueType (Int -> String)

5+unique001a.idr:44:12:Type mismatch between

6+ Int -> String

7+and

8+ UniqueType (Int -> String)

9+unique001a.idr:55:12:Type mismatch between

10+ UniqueType (Int -> String)

11+and

12+ Int -> String

13+unique001b.idr:16:7:Borrowed name xs must not be used on RHS

14+unique001c.idr:46:6:Unique name f is used more than once

15+unique001d.idr:3:7:Borrowed name x must not be used on RHS

16+unique001e.idr:3:10:

17+Constructor Main.Nil has a UniqueType, but the data type does not

18+unique002.idr:15:5:Unique name xs is used more than once

19+unique002a.idr:15:5:Type mismatch between

20+ Int -> String

21+and

22+ UniqueType (Int -> String)

23+unique003.idr:18:5:Type mismatch between

24+ Int -> String

25+and

26+ UniqueType (Int -> String)

test/unique004/runnew file+14

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

1+#!/usr/bin/env bash

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

4+:load unique001a.idr

5+:load unique001b.idr

6+:load unique001c.idr

7+:load unique001d.idr

8+:load unique001e.idr

9+:load unique002.idr

10+:load unique002a.idr

11+:load unique003.idr

12+!

13+

14+rm -f *.ibc

test/unique001/unique001a.idr → test/unique004/unique001a.idrrenamed

The content is the same.

test/unique001/unique001b.idr → test/unique004/unique001b.idrrenamed

The content is the same.

test/unique001/unique001c.idr → test/unique004/unique001c.idrrenamed

The content is the same.

test/unique001/unique001d.idr → test/unique004/unique001d.idrrenamed

The content is the same.

test/unique001/unique001e.idr → test/unique004/unique001e.idrrenamed

The content is the same.

test/unique002/unique002.idr → test/unique004/unique002.idrrenamed

The content is the same.

test/unique002/unique002a.idr → test/unique004/unique002a.idrrenamed

The content is the same.

test/unique003/unique003.idr → test/unique004/unique003.idrrenamed

The content is the same.