search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
690 stars 33 forks source link

AssertionError in UnparsedConstructorPattern #328

Closed valis closed 2 years ago

valis commented 2 years ago 
java.lang.AssertionError
    at org.arend.term.concrete.Concrete$UnparsedConstructorPattern.<init>(Concrete.java:2968)
    at org.arend.term.abs.ConcreteBuilder.buildPattern(ConcreteBuilder.java:514)
    at org.arend.term.abs.ConcreteBuilder.buildPattern(ConcreteBuilder.java:512)
    at org.arend.term.abs.ConcreteBuilder.buildPattern(ConcreteBuilder.java:477)
    at org.arend.term.abs.ConcreteBuilder.buildPattern(ConcreteBuilder.java:512)
    at org.arend.term.abs.ConcreteBuilder.buildPattern(ConcreteBuilder.java:477)
    at org.arend.term.abs.ConcreteBuilder.visitLet(ConcreteBuilder.java:775)
    at org.arend.term.abs.ConcreteBuilder.visitLet(ConcreteBuilder.java:30)
    at org.arend.psi.ext.ArendLetExpr.accept(ArendLetExpr.kt:22)
    at org.arend.term.abs.ConcreteBuilder.visitFunction(ConcreteBuilder.java:136)
    at org.arend.term.abs.ConcreteBuilder.visitFunction(ConcreteBuilder.java:30)
    at org.arend.psi.ext.ArendFunctionDefinition.accept(ArendFunctionDefinition.kt:64)
    at org.arend.term.abs.ConcreteBuilder.convert(ConcreteBuilder.java:53)
    at org.arend.psi.ext.ArendDefinition.computeConcrete(ArendDefinition.kt:40)
    at org.arend.resolving.PsiConcreteProvider$getConcreteDefinition$$inlined$runReadAction$1.compute(actions.kt:66)
    at com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:928)
    at org.arend.resolving.PsiConcreteProvider.getConcreteDefinition(PsiConcreteProvider.kt:142)
    at org.arend.resolving.PsiConcreteProvider.getConcrete(PsiConcreteProvider.kt:113)
    at org.arend.resolving.ArendReferenceImpl$resolve$resolver$1.invoke(ArendReference.kt:170)
    at org.arend.resolving.ArendReferenceImpl$resolve$resolver$1.invoke(ArendReference.kt:145)
    at org.arend.resolving.ArendResolveCache.resolveCached(ArendResolveCache.kt:31)
    at org.arend.resolving.ArendReferenceImpl.resolve(ArendReference.kt:182)
    at org.arend.resolving.ArendReferenceImpl.resolve(ArendReference.kt:141)
    at org.arend.codeInsight.ImportStructureCollector.visitReferenceElement(ArendImportOptimizer.kt:437)
    at org.arend.codeInsight.ImportStructureCollector.visitElement(ArendImportOptimizer.kt:386)
    at com.intellij.psi.impl.PsiElementBase.accept(PsiElementBase.java:273)
    at com.intellij.psi.PsiWalkingState.visit(PsiWalkingState.java:67)
    at com.intellij.psi.PsiWalkingState.visit(PsiWalkingState.java:24)
    at com.intellij.util.WalkingState.walkChildren(WalkingState.java:62)
    at com.intellij.util.WalkingState.elementStarted(WalkingState.java:49)
    at com.intellij.psi.PsiWalkingState.elementStarted(PsiWalkingState.java:76)
    at com.intellij.psi.PsiRecursiveElementWalkingVisitor.visitElement(PsiRecursiveElementWalkingVisitor.java:48)
    at org.arend.codeInsight.ImportStructureCollector.visitElement(ArendImportOptimizer.kt:383)
    at com.intellij.psi.PsiElementVisitor.visitFile(PsiElementVisitor.java:35)
    at com.intellij.psi.PsiRecursiveElementWalkingVisitor.visitFile(PsiRecursiveElementWalkingVisitor.java:70)
    at com.intellij.extapi.psi.PsiFileBase.accept(PsiFileBase.java:60)
    at org.arend.codeInsight.ArendImportOptimizerKt.getOptimalImportStructure(ArendImportOptimizer.kt:348)
    at org.arend.highlight.ArendUnusedImportHighlightingPass.doCollectInformation(ArendUnusedImportHighlightingPass.kt:38)
    at com.intellij.codeHighlighting.TextEditorHighlightingPass.collectInformation(TextEditorHighlightingPass.java:57)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$1(PassExecutorService.java:400)
    at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1154)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$2(PassExecutorService.java:393)
    at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$executeProcessUnderProgress$12(CoreProgressManager.java:608)
    at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:683)
    at com.intellij.openapi.progress.impl.CoreProgressManager.computeUnderProgress(CoreProgressManager.java:639)
    at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:607)
    at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:60)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.doRun(PassExecutorService.java:392)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$run$0(PassExecutorService.java:368)
    at com.intellij.openapi.application.impl.ReadMostlyRWLock.executeByImpatientReader(ReadMostlyRWLock.java:174)
    at com.intellij.openapi.application.impl.ApplicationImpl.executeByImpatientReader(ApplicationImpl.java:215)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.run(PassExecutorService.java:366)
    at com.intellij.concurrency.JobLauncherImpl$VoidForkJoinTask$1.exec(JobLauncherImpl.java:184)
    at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:373)
    at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1182)
    at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1655)
    at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1622)
    at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:165)