Reduction Rule #30
GitHub Actions / junit-tests
failed
Oct 18, 2023 in 0s
92 tests run, 91 passed, 0 skipped, 1 failed.
Annotations
Check failure on line 50 in base/src/test/java/org/aya/test/TestRunner.java
github-actions / junit-tests
TestRunner.runAllAyaTests()
org.opentest4j.AssertionFailedError: issue366.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 ->
1 │ open data Nat : Type 0 | zero | suc Nat
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
│ ╰────────╯
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯ (confluence check: this clause is
substituted to) `suc zero`
5 │ | zero, eldath => zero
│ ╰──────────────────╯ (confluence check: this clause is
substituted to) `zero`
Error: The 2nd and the 1st clauses are not confluent because we failed to unify
suc zero
and
zero
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 ->
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
5 │ | zero, eldath => zero
│ ╰──────────────────╯
Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 ->
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯
Warning: The 2nd clause dominates the 1st clause. The 1st clause will be
unreachable
1 error(s), 2 warning(s).
What are you doing?
> but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 ->
1 │ open data Nat : Type 0 | zero | suc Nat
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
│ ╰────────╯
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯ (confluence check: this clause is
substituted to) `suc zero`
5 │ | zero, eldath => zero
│ ╰──────────────────╯ (confluence check: this clause is
substituted to) `zero`
Error: The 2nd and the 1st clauses are not confluent because we failed to unify
suc zero
(Normalized: 1)
and
zero
(Normalized: 0)
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 ->
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
5 │ | zero, eldath => zero
│ ╰──────────────────╯
Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 ->
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯
Warning: The 2nd clause dominates the 1st clause. The 1st clause will be
unreachable
1 error(s), 2 warning(s).
What are you doing?
>
Raw output
org.opentest4j.AssertionFailedError: issue366.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 ->
1 │ open data Nat : Type 0 | zero | suc Nat
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
│ ╰────────╯
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯ (confluence check: this clause is
substituted to) `suc zero`
5 │ | zero, eldath => zero
│ ╰──────────────────╯ (confluence check: this clause is
substituted to) `zero`
Error: The 2nd and the 1st clauses are not confluent because we failed to unify
suc zero
and
zero
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 ->
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
5 │ | zero, eldath => zero
│ ╰──────────────────╯
Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 ->
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯
Warning: The 2nd clause dominates the 1st clause. The 1st clause will be
unreachable
1 error(s), 2 warning(s).
What are you doing?
> but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 ->
1 │ open data Nat : Type 0 | zero | suc Nat
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
│ ╰────────╯
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯ (confluence check: this clause is
substituted to) `suc zero`
5 │ | zero, eldath => zero
│ ╰──────────────────╯ (confluence check: this clause is
substituted to) `zero`
Error: The 2nd and the 1st clauses are not confluent because we failed to unify
suc zero
(Normalized: 1)
and
zero
(Normalized: 0)
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 ->
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
5 │ | zero, eldath => zero
│ ╰──────────────────╯
Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 ->
2 │ open data Ray (a : Nat) : Type | zero => eldath
3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat
4 │ | zero, eldath => suc zero
│ ╰──────────────────────╯
Warning: The 2nd clause dominates the 1st clause. The 1st clause will be
unreachable
1 error(s), 2 warning(s).
What are you doing?
>
at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
at app//org.junit.jupiter.api.AssertEquals.failNotEqual(AssertEquals.java:197)
at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:182)
at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1152)
at app//org.aya.test.TestRunner.checkOutput(TestRunner.java:150)
at app//org.aya.test.TestRunner.postRun(TestRunner.java:99)
at app//org.aya.test.TestRunner.runFile(TestRunner.java:84)
at app//org.aya.test.TestRunner.lambda$runDir$2(TestRunner.java:71)
at app//kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:733)
at app//kala.collection.immutable.ImmutableVectors$BigVector.forEach(ImmutableVectors.java:568)
at app//org.aya.test.TestRunner.runDir(TestRunner.java:71)
at app//org.aya.test.TestRunner.runAllAyaTests(TestRunner.java:50)
at java.base@20.0.2/java.lang.reflect.Method.invoke(Method.java:578)
at java.base@20.0.2/java.util.ArrayList.forEach(ArrayList.java:1511)
at java.base@20.0.2/java.util.ArrayList.forEach(ArrayList.java:1511)
Loading