StackOverflow

[HoshinoTented]

Aya version: Aya 0.30-SNAPSHOT (9134503de233dad58f12e83920d9445829542578)

Code:

> open data Nat | O | S Nat
data Nat : Type 0
  | O
  | S (_5 : Nat)
> :{
| overlap def badPlus Nat Nat : Nat
| | a, O => a
| | O, b => b
| | a, S b => badPlus (S a) b
| | S a, b => badPlus a (S b)
| :}

Stacktrace (too long):

java.lang.StackOverflowError

java.lang.StackOverflowError
        at kala.collection.internal.hash.HashUtils.computeHash(HashUtils.java:26)
        at kala.collection.mutable.MutableHashMap.put(MutableHashMap.java:526)
        at org.aya.core.visitor.Subst.addDirectly(Subst.java:67)
        at org.aya.core.pat.PatMatcher.match(PatMatcher.java:57)
        at org.aya.core.pat.PatMatcher.match(PatMatcher.java:52)
        at kala.function.CheckedBiConsumer.accept(CheckedBiConsumer.java:23)
        at kala.collection.base.Iterators.forEachWith(Iterators.java:1289)
        at kala.collection.base.Traversable.forEachWith(Traversable.java:1043)
        at kala.collection.base.Traversable.forEachWithChecked(Traversable.java:1048)
        at org.aya.core.pat.PatMatcher.visitList(PatMatcher.java:129)
        at org.aya.core.pat.PatMatcher.match(PatMatcher.java:64)
        at org.aya.core.pat.PatMatcher.match(PatMatcher.java:52)
        at kala.function.CheckedBiConsumer.accept(CheckedBiConsumer.java:23)
        at kala.collection.base.Iterators.forEachWith(Iterators.java:1289)
        at kala.collection.base.Traversable.forEachWith(Traversable.java:1043)
        at kala.collection.base.Traversable.forEachWithChecked(Traversable.java:1048)
        at org.aya.core.pat.PatMatcher.tryBuildSubst(PatMatcher.java:43)
        at org.aya.core.visitor.DeltaExpander.tryUnfoldClauses(DeltaExpander.java:75)
        at org.aya.core.visitor.DeltaExpander.lambda$post$3(DeltaExpander.java:47)
        at kala.control.Either$Right.fold(Either.java:332)
        at org.aya.core.visitor.DeltaExpander.post(DeltaExpander.java:45)
        at org.aya.core.visitor.Expander.post(Expander.java:17)
        at org.aya.core.visitor.EndoTerm.apply(EndoTerm.java:46)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:27)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:22)
        at kala.control.Option.map(Option.java:163)
        at org.aya.core.visitor.DeltaExpander.lambda$post$3(DeltaExpander.java:48)
        at kala.control.Either$Right.fold(Either.java:332)
        at org.aya.core.visitor.DeltaExpander.post(DeltaExpander.java:45)
        at org.aya.core.visitor.Expander.post(Expander.java:17)
        at org.aya.core.visitor.EndoTerm.apply(EndoTerm.java:46)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:27)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:22)
        at kala.control.Option.map(Option.java:163)
        at org.aya.core.visitor.DeltaExpander.lambda$post$3(DeltaExpander.java:48)
        at kala.control.Either$Right.fold(Either.java:332)
        at org.aya.core.visitor.DeltaExpander.post(DeltaExpander.java:45)
        at org.aya.core.visitor.Expander.post(Expander.java:17)
        at org.aya.core.visitor.EndoTerm.apply(EndoTerm.java:46)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:27)
        at org.aya.core.visitor.Expander$WHNFer.apply(Expander.java:22)
        ...... (too long)

[ice1000]

Match should probably be done after termination check IMO