Skip to content

Reduction Rule

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

See this annotation in the file changed.

@github-actions 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)