search

aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

StackOverflow #1000

Open HoshinoTented opened 1 year ago

HoshinoTented commented 1 year ago

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 ```plain 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 commented 1 year ago

Match should probably be done after termination check IMO