Reduction Rule #32
GitHub Actions / junit-tests
failed
Oct 16, 2023 in 0s
92 tests run, 82 passed, 0 skipped, 10 failed.
Annotations
Check failure on line 37 in base/src/test/java/org/aya/core/NormalizeTest.java
github-actions / junit-tests
NormalizeTest.unfoldPatterns()
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
Raw output
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
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.AssertTrue.failNotTrue(AssertTrue.java:63)
at app//org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:36)
at app//org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:31)
at app//org.junit.jupiter.api.Assertions.assertTrue(Assertions.java:179)
at app//org.aya.core.NormalizeTest.unfoldPatterns(NormalizeTest.java:37)
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)
Check failure on line 57 in base/src/test/java/org/aya/core/NormalizeTest.java
github-actions / junit-tests
NormalizeTest.unfoldPrim()
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
Raw output
org.opentest4j.AssertionFailedError: expected: <true> but was: <false>
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.AssertTrue.failNotTrue(AssertTrue.java:63)
at app//org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:36)
at app//org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:31)
at app//org.junit.jupiter.api.Assertions.assertTrue(Assertions.java:179)
at app//org.aya.core.NormalizeTest.unfoldPrim(NormalizeTest.java:57)
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)
Check failure on line 98 in base/src/test/java/org/aya/core/NormalizeTest.java
github-actions / junit-tests
NormalizeTest.recommitLamApp()
org.opentest4j.AssertionFailedError: expected: <suc zero :< nil> but was: <1 :< nil>
Raw output
org.opentest4j.AssertionFailedError: expected: <suc zero :< nil> but was: <1 :< nil>
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.AssertEquals.assertEquals(AssertEquals.java:177)
at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1141)
at app//org.aya.core.NormalizeTest.recommitLamApp(NormalizeTest.java:98)
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)
Check failure on line 119 in base/src/test/java/org/aya/literate/AyaMdParserTest.java
github-actions / junit-tests
AyaMdParserTest.[5] compiler-output
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc (a + b)
Raw output
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc (a + b)
at app//org.aya.tyck.unify.TermComparator.noRules(TermComparator.java:555)
at app//org.aya.tyck.unify.TermComparator.doCompareUntyped(TermComparator.java:541)
at app//org.aya.tyck.unify.TermComparator.compareUntyped(TermComparator.java:151)
at app//org.aya.tyck.unify.TermComparator.doCompareTyped(TermComparator.java:351)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:140)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:117)
at app//org.aya.tyck.tycker.UnifiedTycker.unifyReported(UnifiedTycker.java:127)
at app//org.aya.tyck.tycker.UnifiedTycker.unifyReported(UnifiedTycker.java:140)
at app//org.aya.tyck.tycker.UnifiedTycker.boundary(UnifiedTycker.java:179)
at app//org.aya.tyck.tycker.UnifiedTycker.lambda$checkBoundaries$3(UnifiedTycker.java:159)
at app//org.aya.guest0x0.cubical.CofThy.vdash(CofThy.java:89)
at app//org.aya.guest0x0.cubical.CofThy.conv(CofThy.java:50)
at app//org.aya.guest0x0.cubical.CofThy.conv(CofThy.java:35)
at app//org.aya.tyck.tycker.UnifiedTycker.lambda$checkBoundaries$4(UnifiedTycker.java:159)
at app//kala.collection.IndexedSeqLike.allMatch(IndexedSeqLike.java:203)
at app//org.aya.tyck.tycker.UnifiedTycker.lambda$checkBoundaries$5(UnifiedTycker.java:158)
at app//org.aya.tyck.env.LocalCtx.withIntervals(LocalCtx.java:70)
at app//org.aya.tyck.tycker.UnifiedTycker.checkBoundaries(UnifiedTycker.java:155)
at app//org.aya.tyck.tycker.UnifiedTycker.tryEtaCompatiblePath(UnifiedTycker.java:172)
at app//org.aya.tyck.tycker.UnifiedTycker.inheritFallbackUnify(UnifiedTycker.java:95)
at app//org.aya.tyck.ExprTycker.doInherit(ExprTycker.java:205)
at app//org.aya.tyck.ExprTycker.lambda$inherit$8(ExprTycker.java:215)
at app//org.aya.tyck.tycker.ConcreteAwareTycker.traced(ConcreteAwareTycker.java:65)
at app//org.aya.tyck.ExprTycker.inherit(ExprTycker.java:210)
at app//org.aya.tyck.ExprTycker.lambda$check$9(ExprTycker.java:220)
at app//org.aya.tyck.tycker.PropTycker.withInProp(PropTycker.java:37)
at app//org.aya.tyck.ExprTycker.check(ExprTycker.java:220)
at app//org.aya.tyck.pat.ClauseTycker.lambda$checkRhs$14(ClauseTycker.java:183)
at app//kala.control.Option.map(Option.java:163)
at app//org.aya.tyck.pat.ClauseTycker.lambda$checkRhs$15(ClauseTycker.java:177)
at app//org.aya.tyck.tycker.MockTycker.subscoped(MockTycker.java:89)
at app//org.aya.tyck.tycker.LetListTycker.subscoped(LetListTycker.java:31)
at app//org.aya.tyck.pat.ClauseTycker.lambda$checkRhs$16(ClauseTycker.java:173)
at app//org.aya.tyck.tycker.MockTycker.subscoped(MockTycker.java:89)
at app//org.aya.tyck.tycker.LetListTycker.subscoped(LetListTycker.java:31)
at app//org.aya.tyck.pat.ClauseTycker.checkRhs(ClauseTycker.java:171)
at app//org.aya.tyck.pat.ClauseTycker.lambda$checkAllRhs$5(ClauseTycker.java:92)
at app//org.aya.tyck.tycker.TracedTycker.traced(TracedTycker.java:46)
at app//org.aya.tyck.pat.ClauseTycker.lambda$checkAllRhs$6(ClauseTycker.java:90)
at app//kala.collection.immutable.ImmutableVectors$Vector1.mapIndexed(ImmutableVectors.java:409)
at app//kala.collection.immutable.ImmutableVectors$Vector1.mapIndexed(ImmutableVectors.java:163)
at app//org.aya.tyck.pat.ClauseTycker.checkAllRhs(ClauseTycker.java:90)
at app//org.aya.tyck.pat.ClauseTycker.elabClausesDirectly(ClauseTycker.java:48)
at app//org.aya.tyck.StmtTycker.doTyck(StmtTycker.java:89)
at app//org.aya.tyck.StmtTycker.lambda$traced$1(StmtTycker.java:54)
at app//org.aya.tyck.tycker.MockTycker.subscoped(MockTycker.java:89)
at app//org.aya.tyck.tycker.LetListTycker.subscoped(LetListTycker.java:31)
at app//org.aya.tyck.StmtTycker.lambda$traced$2(StmtTycker.java:54)
at app//org.aya.tyck.tycker.TracedTycker.traced(TracedTycker.java:46)
at app//org.aya.tyck.StmtTycker.traced(StmtTycker.java:53)
at app//org.aya.tyck.StmtTycker.tyck(StmtTycker.java:58)
at app//org.aya.tyck.order.AyaSccTycker.checkBody(AyaSccTycker.java:172)
at app//org.aya.tyck.order.AyaSccTycker.check(AyaSccTycker.java:161)
at app//org.aya.tyck.order.AyaSccTycker.checkUnit(AyaSccTycker.java:125)
at app//org.aya.tyck.order.AyaSccTycker.tyckSCC(AyaSccTycker.java:63)
at app//org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
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.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:42)
at app//org.aya.literate.AyaMdParserTest.testHighlight(AyaMdParserTest.java:119)
at java.base@20.0.2/java.lang.reflect.Method.invoke(Method.java:578)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:1006)
at java.base@20.0.2/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base@20.0.2/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base@20.0.2/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base@20.0.2/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base@20.0.2/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base@20.0.2/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
at java.base@20.0.2/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base@20.0.2/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base@20.0.2/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base@20.0.2/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base@20.0.2/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base@20.0.2/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
at java.base@20.0.2/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base@20.0.2/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base@20.0.2/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base@20.0.2/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base@20.0.2/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
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)
Check failure on line 106 in base/src/test/java/org/aya/repr/ShapeMatcherTest.java
github-actions / junit-tests
ShapeMatcherTest.matchPlus()
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc a
Raw output
org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc a
at app//org.aya.tyck.unify.TermComparator.noRules(TermComparator.java:555)
at app//org.aya.tyck.unify.TermComparator.doCompareUntyped(TermComparator.java:541)
at app//org.aya.tyck.unify.TermComparator.compareUntyped(TermComparator.java:151)
at app//org.aya.tyck.unify.TermComparator.doCompareTyped(TermComparator.java:351)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:140)
at app//org.aya.tyck.unify.TermComparator.visitLists(TermComparator.java:240)
at app//org.aya.tyck.unify.TermComparator.visitArgs(TermComparator.java:228)
at app//org.aya.tyck.unify.TermComparator.visitCall(TermComparator.java:254)
at app//org.aya.tyck.unify.TermComparator.compareApprox(TermComparator.java:181)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:122)
at app//org.aya.tyck.unify.TermComparator.visitLists(TermComparator.java:240)
at app//org.aya.tyck.unify.TermComparator.visitArgs(TermComparator.java:228)
at app//org.aya.tyck.unify.TermComparator.visitCall(TermComparator.java:254)
at app//org.aya.tyck.unify.TermComparator.compareApprox(TermComparator.java:188)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:122)
at app//org.aya.tyck.unify.TermComparator.compare(TermComparator.java:117)
at app//org.aya.tyck.tycker.UnifiedTycker.unifyReported(UnifiedTycker.java:127)
at app//org.aya.tyck.pat.YouTrack.unifyClauses(YouTrack.java:60)
at app//org.aya.tyck.pat.YouTrack.lambda$check$4(YouTrack.java:83)
at app//kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:441)
at app//org.aya.tyck.pat.YouTrack.check(YouTrack.java:78)
at app//org.aya.tyck.StmtTycker.doTyck(StmtTycker.java:94)
at app//org.aya.tyck.StmtTycker.lambda$traced$1(StmtTycker.java:54)
at app//org.aya.tyck.tycker.MockTycker.subscoped(MockTycker.java:89)
at app//org.aya.tyck.tycker.LetListTycker.subscoped(LetListTycker.java:31)
at app//org.aya.tyck.StmtTycker.lambda$traced$2(StmtTycker.java:54)
at app//org.aya.tyck.tycker.TracedTycker.traced(TracedTycker.java:46)
at app//org.aya.tyck.StmtTycker.traced(StmtTycker.java:53)
at app//org.aya.tyck.StmtTycker.tyck(StmtTycker.java:58)
at app//org.aya.tyck.TyckDeclTest.tyck(TyckDeclTest.java:33)
at app//org.aya.tyck.TyckDeclTest.lambda$successTyckDecls$0(TyckDeclTest.java:62)
at app//kala.collection.base.Iterators$3.next(Iterators.java:777)
at app//kala.collection.base.Iterators$Filter.hasNext(Iterators.java:1757)
at app//kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:159)
at app//kala.collection.immutable.ImmutableVector.from(ImmutableVector.java:140)
at app//kala.collection.CollectionLike.toImmutableVector(CollectionLike.java:107)
at app//kala.collection.CollectionLike.toImmutableSeq(CollectionLike.java:95)
at app//org.aya.tyck.TyckDeclTest.successTyckDecls(TyckDeclTest.java:63)
at app//org.aya.repr.ShapeMatcherTest.match(ShapeMatcherTest.java:139)
at app//org.aya.repr.ShapeMatcherTest.matchPlus(ShapeMatcherTest.java:106)
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)
Check failure on line 53 in base/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.fastTestOnDisk()
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]Raw output
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]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:62)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:762)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:79)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:32)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:32)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:77)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:377)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:364)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:46)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:733)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:738)
at kala.collection.immutable.ImmutableVectors$BigVector.forEach(ImmutableVectors.java:568)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:959)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:264)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:233)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:30)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:154)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
at org.aya.test.LibraryTest.compile(LibraryTest.java:148)
at org.aya.test.LibraryTest.compile(LibraryTest.java:139)
at org.aya.test.LibraryTest.fastTestOnDisk(LibraryTest.java:53)
at java.base/java.lang.reflect.Method.invoke(Method.java:578)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
Check failure on line 78 in base/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testInMemoryAndPrim()
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]Raw output
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]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:62)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:762)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:79)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:32)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:32)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:77)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:377)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:364)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:46)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:733)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:738)
at kala.collection.immutable.ImmutableVectors$BigVector.forEach(ImmutableVectors.java:568)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:959)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:264)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:233)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:30)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:154)
at org.aya.test.LibraryTest.compile(LibraryTest.java:152)
at org.aya.test.LibraryTest.testInMemoryAndPrim(LibraryTest.java:78)
at java.base/java.lang.reflect.Method.invoke(Method.java:578)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
Check failure on line 44 in base/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.[1] success
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]Raw output
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]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:62)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:762)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:79)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:32)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:32)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:77)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:377)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:364)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:46)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:733)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:738)
at kala.collection.immutable.ImmutableVectors$BigVector.forEach(ImmutableVectors.java:568)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:959)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:264)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:233)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:30)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:154)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
at org.aya.test.LibraryTest.compile(LibraryTest.java:148)
at org.aya.test.LibraryTest.compile(LibraryTest.java:139)
at org.aya.test.LibraryTest.testOnDisk(LibraryTest.java:44)
at java.base/java.lang.reflect.Method.invoke(Method.java:578)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:183)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:1006)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:150)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:173)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
Check failure on line 64 in base/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testLiterate()
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]Raw output
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]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:62)
at kala.collection.IndexedSeqLike.forEach(IndexedSeqLike.java:762)
at org.aya.util.reporter.DelayedReporter.reportNow(DelayedReporter.java:21)
at org.aya.util.reporter.DelayedReporter.close(DelayedReporter.java:26)
at org.aya.resolve.module.ModuleLoader.tyckModule(ModuleLoader.java:43)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:79)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:32)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:32)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:77)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:377)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:364)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:46)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:733)
at kala.collection.immutable.ImmutableVectors.forEachRec(ImmutableVectors.java:738)
at kala.collection.immutable.ImmutableVectors$BigVector.forEach(ImmutableVectors.java:568)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:959)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:264)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:233)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:30)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:154)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
at org.aya.test.LibraryTest.compile(LibraryTest.java:148)
at org.aya.test.LibraryTest.compile(LibraryTest.java:144)
at org.aya.test.LibraryTest.testLiterate(LibraryTest.java:64)
at java.base/java.lang.reflect.Method.invoke(Method.java:578)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1511)
Check failure on line 50 in base/src/test/java/org/aya/test/TestRunner.java
github-actions / junit-tests
TestRunner.runAllAyaTests()
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
>Raw output
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
>
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.forEachRec(ImmutableVectors.java:738)
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