git.iko.soy/Idris-dev
on master help sign in
Consolidate unique001 into unique004
commit006b884bae9bcc3762e613da85073149133b36ca authorSteven Shaw <steven@steshaw.org> dateFri 5 Aug 2016, 22:32 (10 years ago) parent51da43f
9 files changed+30−22
compare with master
unifiedsplit
test/unique001/expected−17 test/unique001/run+2−5 test/unique004/expected+17 test/unique004/run+11 test/unique001/unique001a.idr → test/unique004/unique001a.idr test/unique001/unique001b.idr → test/unique004/unique001b.idr test/unique001/unique001c.idr → test/unique004/unique001c.idr test/unique001/unique001d.idr → test/unique004/unique001d.idr test/unique001/unique001e.idr → test/unique004/unique001e.idr
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
2+
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
5+
96rm -f unique001 *.ibc
test/unique004/expectednew file+17
@@ -0,0 +1,17 @@
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
test/unique004/runnew file+11
@@ -0,0 +1,11 @@
1+#!/usr/bin/env bash
2+
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+!
10+
11+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.