Reduction Rule #27
Annotations
10 errors
NormalizeTest.unfoldPatterns():
base/src/test/java/org/aya/core/NormalizeTest.java#L37
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
|
NormalizeTest.unfoldPrim():
base/src/test/java/org/aya/core/NormalizeTest.java#L57
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
|
NormalizeTest.recommitLamApp():
base/src/test/java/org/aya/core/NormalizeTest.java#L98
org.opentest4j.AssertionFailedError: expected: <suc zero :< nil> but was: <1 :< nil>
|
AyaMdParserTest.[5] compiler-output:
base/src/test/java/org/aya/literate/AyaMdParserTest.java#L119
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc (a + b)
|
ShapeMatcherTest.matchPlus():
base/src/test/java/org/aya/repr/ShapeMatcherTest.java#L106
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc a
|
LibraryTest.fastTestOnDisk():
base/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 ->
38 | tighter = ==< qed
39 |
40 | def +'-comm (a b : Nat) : a +' b = b +' a
| ^-----^
Error: The recursive definition `+'-comm` is not structurally recursive
note: In particular, the problematic call is:
+'-comm (suc a) b
whose call matrix is:
? ?
? ?
whose diagonal is:
? ?
at (936-942) [40,4-40,10]
|
LibraryTest.testInMemoryAndPrim():
base/src/test/java/org/aya/test/LibraryTest.java#L78
java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 ->
38 | tighter = ==< qed
39 |
40 | def +'-comm (a b : Nat) : a +' b = b +' a
| ^-----^
Error: The recursive definition `+'-comm` is not structurally recursive
note: In particular, the problematic call is:
+'-comm (suc a) b
whose call matrix is:
? ?
? ?
whose diagonal is:
? ?
at (936-942) [40,4-40,10]
|
LibraryTest.[1] success:
base/src/test/java/org/aya/test/LibraryTest.java#L44
java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 ->
38 | tighter = ==< qed
39 |
40 | def +'-comm (a b : Nat) : a +' b = b +' a
| ^-----^
Error: The recursive definition `+'-comm` is not structurally recursive
note: In particular, the problematic call is:
+'-comm (suc a) b
whose call matrix is:
? ?
? ?
whose diagonal is:
? ?
at (936-942) [40,4-40,10]
|
LibraryTest.testLiterate():
base/src/test/java/org/aya/test/LibraryTest.java#L64
java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 ->
38 | tighter = ==< qed
39 |
40 | def +'-comm (a b : Nat) : a +' b = b +' a
| ^-----^
Error: The recursive definition `+'-comm` is not structurally recursive
note: In particular, the problematic call is:
+'-comm (suc a) b
whose call matrix is:
? ?
? ?
whose diagonal is:
? ?
at (936-942) [40,4-40,10]
|
TestRunner.runAllAyaTests():
base/src/test/java/org/aya/test/TestRunner.java#L50
org.opentest4j.AssertionFailedError: confl-literal.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
│ ╰────╯ (confluence check: this clause is substituted to) `114514`
6 │ | suc a => suc a
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
10 │ | 114514 => 1919
│ ╰────────────╯ (confluence check: this clause is substituted
to) `1919`
Error: The 2nd and the 7th clauses are not confluent because we failed to unify
1919
and
114514
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
6 │ | suc a => suc a
│ ╰────────────╯ (confluence check: this clause is substituted to)
`suc (suc a)`
7 │ | suc (suc a) => a
│ ╰──────────────╯ (confluence check: this clause is substituted
to) `a`
Error: The 4th and the 3rd clauses are not confluent because we failed to unify
suc (suc a)
and
a
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
6 │ | suc a => suc a
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
│ ╰─────────────╯ (confluence check: this clause is substituted
to) `3`
9 │ | 2147483647 => 4
│ ╰─────────────╯ (confluence check: this clause is substituted
to) `4`
Error: The 6th and the 5th clauses are not confluent because we failed to unify
3
and
4
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
│ ╰────╯ (confluence check: this clause is substituted to) `2147483647`
6 │ | suc a => suc a
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
│ ╰─────────────╯ (confluence check: this clause is substituted
to) `4`
Error: The 2nd and the 6th clauses are not confluent because we failed to unify
4
and
2147483647
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
6 │ | suc a => suc a
│ ╰────────────╯ (confluence check: this clause is substituted to)
`suc (suc a)`
7 │ | suc (suc a) => a
│ ╰──────────────╯ (confluence check: this clause is substituted
to) `a`
Error: The 4th and the 3rd clauses are not confluent because we failed to unify
suc (suc a)
and
a
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
6 │ | suc a => suc a
│ ╰────────────╯ (confluence check: this clause is substituted to)
`suc (suc a)`
7 │ | suc (suc a) => a
│ ╰──────────────╯ (confluence check: this clause is substituted
to) `a`
Error: The 4th and the 3rd clauses are not confluent because we failed to unify
suc (suc a)
and
a
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:4:4 ->
2 │
3 │ overlap def test Nat : Nat
4 │ | 0 => 0
│ ╰────╯
Warning: The 2nd clause dominates the 1st clause. The 1st clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:6:4 ->
4 │ | 0 => 0
5 │ | a => a
6 │ | suc a => suc a
│ ╰────────────╯
Warning: The 2nd clause dominates the 3rd clause. The 3rd clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:10:4 ->
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
10 │ | 114514 => 1919
│ ╰────────────╯
Warning: The 2nd clause dominates the 7th clause. The 7th clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:7:4 ->
5 │ | a => a
6 │ | suc a => suc a
7 │ | suc (suc a) => a
│ ╰──────────────╯
Warning: The 3rd clause dominates the 4th clause. The 4th clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:9:4 ->
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
│ ╰─────────────╯
Warning: The 5th clause dominates the 6th clause. The 6th clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:8:4 ->
6 │ | suc a => suc a
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
│ ╰─────────────╯
Warning: The 6th clause dominates the 5th clause. The 5th clause will be
unreachable
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:9:4 ->
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
│ ╰─────────────╯
Warning: The 2nd clause dominates the 6th clause. The 6th clause will be
unreachable
6 error(s), 7 warning(s).
What are you doing?
> but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 ->
1 │ open data Nat | zero | suc Nat
2 │
3 │ overlap def test Nat : Nat
│ ╰──╯
4 │ | 0 => 0
5 │ | a => a
│ ╰────╯ (confluence check: this clause is substituted to) `114514`
6 │ | suc a => suc a
7 │ | suc (suc a) => a
8 │ | 2147483647 => 3
9 │ | 2147483647 => 4
10 │ | 114514 => 1919
│ ╰────────────╯ (confluence check: this clause is substituted
to) `1919`
Error: The 2nd and the 7th clauses are not confluent because we failed to unify
1919
and
114514
Internal error
>
|