Reduction Rule #29
HoshinoTentedAnnotations
10 errors
|
NormalizeTest.unfoldPatterns():
base/src/test/java/org/aya/core/NormalizeTest.java#L23
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Confluence`: In file main.aya:2:12 ->
1 | open data Nat : Type | zero | suc Nat
2 | overlap def tracy (a b : Nat) : Nat
| ^---^
3 | | zero, a => a
| ^----------^ (confluence check: this clause is substituted to) `suc
b`
4 | | a, zero => a
5 | | suc a, b => suc (tracy a b)
6 | | a, suc b => suc (tracy a b)
| ^-------------------------^ (confluence check: this clause is
substituted to) `suc (tracy zero b)`
7 | def xyr : Nat => tracy zero (suc zero)
Error: The 4th and the 1st clauses are not confluent because we failed to unify
suc b
and
suc (tracy zero b)
(Normalized: suc (tracy 0 b))
In particular, we failed to unify
b
with
tracy 0 b
at (50-54) [2,12-2,16]
|
|
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#L65
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Confluence`: In file main.aya:5:19 ->
3 | | nil
4 | | infixr :< A (List A)
5 | overlap def infixl + (a b : Nat) : Nat
| ^^
6 | | zero, a => a
| ^----------^ (confluence check: this clause is substituted to) `suc
b`
7 | | a, zero => a
8 | | suc a, b => suc (a + b)
9 | | a, suc b => suc (a + b)
| ^---------------------^ (confluence check: this clause is
substituted to) `suc (zero + b)`
Error: The 4th and the 1st clauses are not confluent because we failed to unify
suc b
and
suc (zero + b)
(Normalized: suc (0 + b))
In particular, we failed to unify
b
with
0 + b
at (116-116) [5,19-5,19]
|
|
ShapeMatcherTest.matchPlus():
base/src/test/java/org/aya/repr/ShapeMatcherTest.java#L106
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Confluence`: In file main.aya:8:12 ->
6 | | zero, right => right
7 | | suc left, right => suc (plusLeft left right)
8 | overlap def plusOverlap0 Nat Nat : Nat
| ^----------^
9 | | a, zero => a
10 | | zero, b => b
| ^----------^ (confluence check: this clause is substituted to) `suc
b`
11 | | a, suc b => suc (plusOverlap0 a b)
| ^--------------------------------^ (confluence check: this clause
is substituted to) `suc (plusOverlap0
zero b)`
Error: The 3rd and the 2nd clauses are not confluent because we failed to unify
suc b
and
suc (plusOverlap0 zero b)
(Normalized: suc (plusOverlap0 0 b))
In particular, we failed to unify
b
with
plusOverlap0 0 b
at (227-238) [8,12-8,23]
|
|
LibraryTest.fastTestOnDisk():
base/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Conditions`: In file Arith/Int.aya:17:4 ->
15 | | posneg i => posneg (~ i)
16 |
17 | def succInt Int : Int
| ^-----^
18 | | signed true n => pos (suc n)
19 | | signed false (suc n) => neg n
20 | | signed false zero => pos 1
21 | | posneg i => pos 1
| ^---------------^ (confluence check: this clause is substituted to)
`pos 1`
Error: The 4th clause matches on a constructor with condition(s). When checking
the 1st condition, we failed to unify
pos 1
(Normalized: signed true 1)
for the arguments:
posneg 0
Normalized:
signed false 0
succInt (signed false 0)
at (301-307) [17,4-17,10]
|
|
LibraryTest.testInMemoryAndPrim():
base/src/test/java/org/aya/test/LibraryTest.java#L78
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Conditions`: In file Arith/Int.aya:17:4 ->
15 | | posneg i => posneg (~ i)
16 |
17 | def succInt Int : Int
| ^-----^
18 | | signed true n => pos (suc n)
19 | | signed false (suc n) => neg n
20 | | signed false zero => pos 1
21 | | posneg i => pos 1
| ^---------------^ (confluence check: this clause is substituted to)
`pos 1`
Error: The 4th clause matches on a constructor with condition(s). When checking
the 1st condition, we failed to unify
pos 1
(Normalized: signed true 1)
for the arguments:
posneg 0
Normalized:
signed false 0
succInt (signed false 0)
at (301-307) [17,4-17,10]
|
|
LibraryTest.[1] success:
base/src/test/java/org/aya/test/LibraryTest.java#L44
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Conditions`: In file Arith/Int.aya:17:4 ->
15 | | posneg i => posneg (~ i)
16 |
17 | def succInt Int : Int
| ^-----^
18 | | signed true n => pos (suc n)
19 | | signed false (suc n) => neg n
20 | | signed false zero => pos 1
21 | | posneg i => pos 1
| ^---------------^ (confluence check: this clause is substituted to)
`pos 1`
Error: The 4th clause matches on a constructor with condition(s). When checking
the 1st condition, we failed to unify
pos 1
(Normalized: signed true 1)
for the arguments:
posneg 0
Normalized:
signed false 0
succInt (signed false 0)
at (301-307) [17,4-17,10]
|
|
LibraryTest.testLiterate():
base/src/test/java/org/aya/test/LibraryTest.java#L64
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Conditions`: In file Arith/Int.aya:17:4 ->
15 | | posneg i => posneg (~ i)
16 |
17 | def succInt Int : Int
| ^-----^
18 | | signed true n => pos (suc n)
19 | | signed false (suc n) => neg n
20 | | signed false zero => pos 1
21 | | posneg i => pos 1
| ^---------------^ (confluence check: this clause is substituted to)
`pos 1`
Error: The 4th clause matches on a constructor with condition(s). When checking
the 1st condition, we failed to unify
pos 1
(Normalized: signed true 1)
for the arguments:
posneg 0
Normalized:
signed false 0
succInt (signed false 0)
at (301-307) [17,4-17,10]
|
|
TestRunner.runAllAyaTests():
base/src/test/java/org/aya/test/TestRunner.java#L50
org.opentest4j.AssertionFailedError: list-unknown.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/tyck/list-unknown.aya:5:11 ->
3 │
4 │ def good : List Unit => [ ]
5 │ def bad => [ ]
│ ╰─╯
Error: Unsolved meta _
in `List _`
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/tyck/list-unknown.aya:5:11 ->
3 │
4 │ def good : List Unit => [ ]
5 │ def bad => [ ]
│ ╰─╯
Error: Unsolved meta _
in `List _`
in `[ ]`
2 error(s), 0 warning(s).
What are you doing?
> but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/success/common/src/Arith/Nat/Order.aya:18:6 ->
16 │
17 │ def asym (a < b) : ¬ (b < a)
18 │ | zc, ()
│ ╰╯
Error: Unsure if this pattern is actually impossible, as constructor selection
is blocked on:
<(suc <m>)> < <zero>
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/success/common/src/Data/List/Core.aya:16:10 ->
14 │ | _ :< l => suc (length l)
15 │
16 │ def infix !! (l : List A) (i : Fin (length l)) : A
│ ╰╯
Error: Unhandled case:
{A}, nil, fzero
{A}, nil, fsuc fzero
{A}, nil, fsuc (fsuc ...)
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/tyck/list-unknown.aya:5:11 ->
3 │
4 │ def good : List Unit => [ ]
5 │ def bad => [ ]
│ ╰─╯
Error: Unsolved meta _
in `List _`
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/tyck/list-unknown.aya:5:11 ->
3 │
4 │ def good : List Unit => [ ]
5 │ def bad => [ ]
│ ╰─╯
Error: Unsolved meta _
in `List _`
in `[ ]`
4 error(s), 0 warning(s).
What are you doing?
>
|
|
PatCCTest.addCC():
base/src/test/java/org/aya/tyck/PatCCTest.java#L32
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.ClausesProblem$Confluence`: In file main.aya:2:12 ->
1 | open data Nat : Type | zero | suc Nat
2 | overlap def add (a b : Nat) : Nat
| ^-^
3 | | zero, b => b
| ^----------^ (confluence check: this clause is substituted to) `suc
b`
4 | | a, zero => a
5 | | suc a, b => suc (add a b)
6 | | a, suc b => suc (add a b)
| ^-----------------------^ (confluence check: this clause is
substituted to) `suc (add zero b)`
Error: The 4th and the 1st clauses are not confluent because we failed to unify
suc b
and
suc (add zero b)
(Normalized: suc (add 0 b))
In particular, we failed to unify
b
with
add 0 b
at (50-52) [2,12-2,14]
|