Merge branch 'master' into pr137

src/main/kotlin/org/arend/ArendDocumentationProvider.kt

@@ -112,7 +112,7 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() {
         is ArendClassImplement -> "implementation"
         is ArendDefData -> "data"
         is ArendConstructor -> "constructor"
-        is ArendDefFunction -> "function"
+        is ArendDefFunction, is ArendCoClauseDef -> "function"
         is ArendLetClause -> "let"
         is ArendDefIdentifier -> if (element.parent is ArendLetClause) "let" else "variable"
         else -> null

src/main/kotlin/org/arend/intention/SelfTargetingIntention.kt

@@ -40,15 +40,16 @@ abstract class SelfTargetingIntention<T : PsiElement>(
         val leaf2 = file.findElementAt(offset - 1)
         val commonParent = if (leaf1 != null && leaf2 != null) PsiTreeUtil.findCommonParent(leaf1, leaf2) else null
 
-        var elementsToCheck: Sequence<PsiElement> = emptySequence()
-        if (leaf1 != null) {
-            elementsToCheck += leaf1.ancestors.takeWhile { it != commonParent }
-        }
-        if (leaf2 != null) {
-            elementsToCheck += leaf2.ancestors.takeWhile { it != commonParent }
-        }
-        if (commonParent != null && commonParent !is PsiFile) {
-            elementsToCheck += commonParent.ancestors
+        val elementsToCheck = sequence {
+            if (leaf1 != null) {
+                yieldAll(leaf1.ancestors.takeWhile { it != commonParent })
+            }
+            if (leaf2 != null) {
+                yieldAll(leaf2.ancestors.takeWhile { it != commonParent })
+            }
+            if (commonParent != null && commonParent !is PsiFile) {
+                yieldAll(commonParent.ancestors)
+            }
         }
 
         for (element in elementsToCheck) {

src/main/kotlin/org/arend/intention/SplitAtomPatternIntention.kt

@@ -4,45 +4,38 @@ import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiElement
-import org.arend.core.context.binding.Binding
 import org.arend.core.context.binding.Variable
 import org.arend.core.context.param.DependentLink
 import org.arend.core.definition.ClassDefinition
 import org.arend.core.definition.Constructor
+import org.arend.core.definition.FunctionDefinition
+import org.arend.core.elimtree.ElimBody
+import org.arend.core.elimtree.IntervalElim
 import org.arend.core.expr.ClassCallExpression
 import org.arend.core.expr.DataCallExpression
 import org.arend.core.expr.Expression
 import org.arend.core.expr.SigmaExpression
 import org.arend.core.expr.visitor.ToAbstractVisitor
 import org.arend.core.pattern.BindingPattern
-import org.arend.core.pattern.ConstructorPattern
+import org.arend.core.pattern.ConstructorExpressionPattern
+import org.arend.core.pattern.ExpressionPattern
 import org.arend.core.pattern.Pattern
-import org.arend.error.ListErrorReporter
 import org.arend.ext.core.ops.NormalizationMode
 import org.arend.ext.prettyprinting.PrettyPrinterConfig
 import org.arend.naming.reference.Referable
 import org.arend.naming.reference.UnresolvedReference
-import org.arend.naming.reference.converter.IdReferableConverter
 import org.arend.naming.renamer.StringRenamer
-import org.arend.naming.resolving.visitor.ExpressionResolveNameVisitor
-import org.arend.naming.scope.ConvertingScope
-import org.arend.naming.scope.ListScope
-import org.arend.naming.scope.Scope
 import org.arend.prelude.Prelude
 import org.arend.psi.*
 import org.arend.psi.ext.*
 import org.arend.quickfix.referenceResolve.ResolveReferenceAction.Companion.getTargetName
 import org.arend.refactoring.VariableImpl
 import org.arend.term.abs.Abstract
-import org.arend.term.abs.ConcreteBuilder
 import org.arend.term.concrete.Concrete
 import org.arend.term.prettyprint.PrettyPrintVisitor
 import org.arend.typechecking.ArendTypecheckingListener
 import org.arend.typechecking.TypeCheckingService
-import org.arend.typechecking.patternmatching.ElimTypechecking
-import org.arend.typechecking.patternmatching.PatternTypechecking
-import org.arend.typechecking.provider.EmptyConcreteProvider
-import org.arend.typechecking.visitor.DesugarVisitor
+import java.lang.IllegalStateException
 import java.util.*
 import java.util.Collections.singletonList
 
@@ -97,12 +90,14 @@ class SplitAtomPatternIntention : SelfTargetingIntention<PsiElement>(PsiElement:
             val ownerParent = (patternOwner as PsiElement).parent
             var abstractPatterns: List<Abstract.Pattern>? = null
 
+            var clauseIndex = -1
             if (patternOwner is ArendClause && ownerParent is ArendFunctionClauses) {
                 val body = ownerParent.parent
                 val func = body?.parent
                 if (body is ArendFunctionBody && func is ArendFunctionalDefinition) {
                     abstractPatterns = patternOwner.patterns
                     definition = func as? TCDefinition
+                    clauseIndex = ownerParent.clauseList.indexOf(patternOwner)
                 }
             }
             if (patternOwner is ArendConstructorClause && ownerParent is ArendDataBody) {
@@ -112,12 +107,24 @@ class SplitAtomPatternIntention : SelfTargetingIntention<PsiElement>(PsiElement:
                 return null // TODO: Implement some behavior for constructor clauses as well
             }
 
-            if (definition != null) {
+            if (definition != null && clauseIndex != -1) {
                 val typeCheckedDefinition = project.service<TypeCheckingService>().getTypechecked(definition)
-                if (typeCheckedDefinition != null && abstractPatterns != null) {
-                    val (patterns, isElim) = computePatterns(abstractPatterns, typeCheckedDefinition.parameters, definition as? Abstract.EliminatedExpressionsHolder, definition.scope, project)
-                    if (patterns != null && indexList.size > 0) {
-                        val typecheckedPattern = if (isElim) patterns.getOrNull(indexList[0]) else findMatchingPattern(abstractPatterns, typeCheckedDefinition.parameters, patterns, indexList[0])
+                if (typeCheckedDefinition is FunctionDefinition && definition is Abstract.ParametersHolder && definition is Abstract.EliminatedExpressionsHolder && abstractPatterns != null) {
+                    val elimBody = (typeCheckedDefinition.body as? IntervalElim)?.otherwise ?: (typeCheckedDefinition.body as? ElimBody) ?: return null
+                    val patterns = elimBody.clauses.getOrNull(clauseIndex)?.patterns?.let { Pattern.toExpressionPatterns(it, typeCheckedDefinition.parameters) } ?: return null
+
+                    val parameters = ArrayList<Referable>(); for (pp in definition.parameters) parameters.addAll(pp.referableList)
+                    val elimVars = definition.eliminatedExpressions ?: emptyList()
+                    val isElim = elimVars.isNotEmpty()
+                    val elimVarPatterns : List<ExpressionPattern> = if (isElim) elimVars.map { reference ->
+                        if (reference is ArendRefIdentifier) {
+                            val parameterIndex = (reference.reference?.resolve() as? Referable)?.let{ parameters.indexOf(it) } ?: -1
+                            if (parameterIndex < patterns.size && parameterIndex != -1) patterns[parameterIndex] else throw IllegalStateException()
+                        } else throw IllegalStateException()
+                    } else patterns
+
+                    if (indexList.size > 0) {
+                        val typecheckedPattern = if (isElim) elimVarPatterns.getOrNull(indexList[0]) else findMatchingPattern(abstractPatterns, typeCheckedDefinition.parameters, patterns, indexList[0])
                         if (typecheckedPattern != null) {
                             val patternPart = findPattern(indexList.drop(1), typecheckedPattern, abstractPatterns[indexList[0]]) as? BindingPattern ?: return null
                             return patternPart.binding.typeExpr
@@ -374,48 +381,10 @@ class SplitAtomPatternIntention : SelfTargetingIntention<PsiElement>(PsiElement:
             return Pair(clause, indexList)
         }
 
-        private fun computePatterns(abstractPatterns: List<Abstract.Pattern>, parameters: DependentLink, elimExprHolder: Abstract.EliminatedExpressionsHolder?, scope: Scope, project: Project): Pair<List<Pattern>?, Boolean> {
-            val listErrorReporter = ListErrorReporter()
-            val concreteParameters = elimExprHolder?.parameters?.let { params ->
-                ConcreteBuilder.convert(IdReferableConverter.INSTANCE, true) { it.buildTelescopeParameters(params) }
-            }
-            val elimVars = elimExprHolder?.eliminatedExpressions?.let { vars ->
-                ConcreteBuilder.convert(IdReferableConverter.INSTANCE, true) { it.buildReferences(vars) }
-            }
-            val elimParams = if (concreteParameters != null && elimVars != null) {
-                val context = LinkedHashMap<Referable, Binding>()
-                var link = parameters
-                loop@ for (parameter in concreteParameters) {
-                    for (referable in parameter.referableList) {
-                        if (!link.hasNext()) break@loop
-
-                        context[referable] = link
-                        link = link.next
-                    }
-                }
-                val listScope = ListScope(context.keys.toList())
-                for (elimVar in elimVars) ExpressionResolveNameVisitor.resolve(elimVar, listScope, null)
-
-                ElimTypechecking.getEliminatedParameters(elimVars, emptyList(), parameters, listErrorReporter, context)
-                        ?: return Pair(null, true)
-            } else {
-                emptyList()
-            }
-
-            val concretePatterns = ConcreteBuilder.convert(IdReferableConverter.INSTANCE, true) { it.buildPatterns(abstractPatterns) }
-            DesugarVisitor.desugarPatterns(concretePatterns, listErrorReporter)
-            val service = project.service<TypeCheckingService>()
-            ExpressionResolveNameVisitor(EmptyConcreteProvider.INSTANCE, ConvertingScope(service.newReferableConverter(true), scope), ArrayList(), listErrorReporter, null).visitPatterns(concretePatterns)
-            // TODO: This won't work with defined constructors
-            val patternTypechecking = PatternTypechecking(listErrorReporter, PatternTypechecking.Mode.CONSTRUCTOR, service.typecheckerState)
-            val patterns = patternTypechecking.typecheckPatterns(concretePatterns, parameters, elimParams)
-            return Pair(if (listErrorReporter.errorList.isEmpty()) patterns else null, elimParams.isNotEmpty())
-        }
-
-        private fun findPattern(indexList: List<Int>, typecheckedPattern: Pattern, abstractPattern: Abstract.Pattern): Pattern? {
+        private fun findPattern(indexList: List<Int>, typecheckedPattern: ExpressionPattern, abstractPattern: Abstract.Pattern): ExpressionPattern? {
             if (indexList.isEmpty()) return typecheckedPattern
-            if (typecheckedPattern is ConstructorPattern) {
-                val typecheckedPatternChild = findMatchingPattern(abstractPattern.arguments, typecheckedPattern.parameters, typecheckedPattern.patterns.patternList, indexList[0])
+            if (typecheckedPattern is ConstructorExpressionPattern) {
+                val typecheckedPatternChild = findMatchingPattern(abstractPattern.arguments, typecheckedPattern.parameters, typecheckedPattern.subPatterns, indexList[0])
                 val abstractPatternChild = abstractPattern.arguments.getOrNull(indexList[0])
                 if (typecheckedPatternChild != null && abstractPatternChild != null)
                     return findPattern(indexList.drop(1), typecheckedPatternChild, abstractPatternChild)
@@ -430,7 +399,7 @@ class SplitAtomPatternIntention : SelfTargetingIntention<PsiElement>(PsiElement:
             return null
         }
 
-        private fun findMatchingPattern(abstractPatterns: List<Abstract.Pattern>, parameters: DependentLink, typecheckedPatterns: List<Pattern>, index: Int): Pattern? {
+        private fun findMatchingPattern(abstractPatterns: List<Abstract.Pattern>, parameters: DependentLink, typecheckedPatterns: List<ExpressionPattern>, index: Int): ExpressionPattern? {
             var link = parameters
             var i = 0
             var j = 0

src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt

@@ -12,8 +12,8 @@ import org.arend.core.context.param.DependentLink
 import org.arend.core.definition.ClassDefinition
 import org.arend.core.definition.Definition
 import org.arend.core.pattern.BindingPattern
-import org.arend.core.pattern.ConstructorPattern
-import org.arend.core.pattern.Pattern
+import org.arend.core.pattern.ConstructorExpressionPattern
+import org.arend.core.pattern.ExpressionPattern
 import org.arend.naming.renamer.StringRenamer
 import org.arend.prelude.Prelude
 import org.arend.psi.*
@@ -45,7 +45,7 @@ class ImplementMissingClausesQuickFix(private val missingClausesError: MissingCl
 
         missingClausesError.setMaxListSize(service<ArendSettings>().clauseActualLimit)
         for (clause in missingClausesError.limitedMissingClauses.reversed()) if (clause != null) {
-            val filters = HashMap<ConstructorPattern, List<Boolean>>()
+            val filters = HashMap<ConstructorExpressionPattern, List<Boolean>>()
             val previewResults = ArrayList<PatternKind>()
             run {
                 var parameter: DependentLink? = if (!missingClausesError.isElim) missingClausesError.parameters else null
@@ -183,13 +183,13 @@ class ImplementMissingClausesQuickFix(private val missingClausesError: MissingCl
             }
         }
 
-        fun previewPattern(pattern: Pattern, filters: MutableMap<ConstructorPattern, List<Boolean>>, paren: Braces): PatternKind {
+        fun previewPattern(pattern: ExpressionPattern, filters: MutableMap<ConstructorExpressionPattern, List<Boolean>>, paren: Braces): PatternKind {
             when (pattern) {
-                is ConstructorPattern -> {
+                is ConstructorExpressionPattern -> {
                     val definition: Definition? = pattern.definition
                     val previewResults = ArrayList<PatternKind>()
 
-                    val patternIterator = pattern.patterns.patternList.iterator()
+                    val patternIterator = pattern.subPatterns.iterator()
                     var constructorArgument: DependentLink? = definition?.parameters
 
                     while (patternIterator.hasNext()) {
@@ -209,14 +209,15 @@ class ImplementMissingClausesQuickFix(private val missingClausesError: MissingCl
             throw IllegalStateException()
         }
 
-        private fun getIntegralNumber(pattern: ConstructorPattern): Int? {
+        private fun getIntegralNumber(pattern: ConstructorExpressionPattern): Int? {
             val isSuc = pattern.definition == Prelude.SUC
             val isPos = pattern.definition == Prelude.POS
             val isNeg = pattern.definition == Prelude.NEG
             if (isSuc || isPos || isNeg) {
-                val argumentList = pattern.patterns.patternList
+                val argumentList = pattern.subPatterns
                 if (argumentList.size != 1) return null
-                val firstArgument = argumentList.first() as? ConstructorPattern ?: return null
+                val firstArgument = argumentList.first() as? ConstructorExpressionPattern
+                    ?: return null
                 val number = getIntegralNumber(firstArgument)
                 if (isSuc && number != null) return number + 1
                 if (isPos && number != null) return number
@@ -226,11 +227,11 @@ class ImplementMissingClausesQuickFix(private val missingClausesError: MissingCl
             return null
         }
 
-        fun doTransformPattern(pattern: Pattern, cause: ArendCompositeElement, editor: Editor?,
-                               filters: Map<ConstructorPattern, List<Boolean>>, paren: Braces,
+        fun doTransformPattern(pattern: ExpressionPattern, cause: ArendCompositeElement, editor: Editor?,
+                               filters: Map<ConstructorExpressionPattern, List<Boolean>>, paren: Braces,
                                occupiedNames: MutableList<Variable>): String {
             when (pattern) {
-                is ConstructorPattern -> {
+                is ConstructorExpressionPattern -> {
                     val definition: Definition? = pattern.definition
                     val referable = if (definition != null) PsiLocatedReferable.fromReferable(definition.referable) else null
 
@@ -243,7 +244,7 @@ class ImplementMissingClausesQuickFix(private val missingClausesError: MissingCl
 
                     val argumentPatterns = ArrayList<String>()
                     run {
-                        val patternIterator = pattern.patterns.patternList.iterator()
+                        val patternIterator = pattern.subPatterns.iterator()
                         var constructorArgument: DependentLink? = definition?.parameters
 
                         while (patternIterator.hasNext()) {

src/main/kotlin/org/arend/settings/ArendProjectSettings.kt

@@ -16,10 +16,8 @@ class ArendProjectSettings : PersistentStateComponent<ArendProjectSettingsState>
     var messagesFilterSet = EnumSet.of(MessageType.ERROR, MessageType.WARNING, MessageType.GOAL, MessageType.TYPECHECKING, MessageType.SHORT, MessageType.RESOLVING)!!
     var errorPrintingOptionsFilterSet = PrettyPrinterConfig.DEFAULT.expressionFlags
     var goalPrintingOptionsFilterSet = EnumSet.of<PrettyPrinterFlag>(PrettyPrinterFlag.SHOW_FIELD_INSTANCE)!!
-    // var goalPrintingOptionsFilterSet = EnumSet.of(ToAbstractVisitor.Flag.SHOW_FIELD_INSTANCE)!! // master
 
     // for show-type and show-normalized
-    //var popupPrintingOptionsFilterSet = EnumSet.of(ToAbstractVisitor.Flag.SHOW_FIELD_INSTANCE)!! //master
     var popupPrintingOptionsFilterSet = EnumSet.of(PrettyPrinterFlag.SHOW_FIELD_INSTANCE)!!
 
     fun setAutoScrollFromSource(type: MessageType, enabled: Boolean) {
@@ -62,6 +60,10 @@ class ArendProjectSettings : PersistentStateComponent<ArendProjectSettingsState>
         data.showResolving = messagesFilterSet.contains(MessageType.RESOLVING)
         data.showParsing = messagesFilterSet.contains(MessageType.PARSING)
 
+        data.popupPrintingOptions = ArendPrintingOptions()
+        data.errorPrintingOptions = ArendPrintingOptions()
+        data.goalPrintingOptions = ArendPrintingOptions()
+
         getPrintingOptions(errorPrintingOptionsFilterSet, data.errorPrintingOptions)
         getPrintingOptions(goalPrintingOptionsFilterSet, data.goalPrintingOptions)
         getPrintingOptions(popupPrintingOptionsFilterSet, data.popupPrintingOptions)

src/main/kotlin/org/arend/settings/ArendProjectSettingsState.kt

@@ -28,10 +28,10 @@ class ArendProjectSettingsState {
     var showResolving = true
     var showParsing = false
 
-    //Printing options
-    val errorPrintingOptions = ArendPrintingOptions()
-    val goalPrintingOptions = ArendPrintingOptions()
-    val popupPrintingOptions = ArendPrintingOptions()
+    // Printing options
+    var errorPrintingOptions = ArendPrintingOptions()
+    var goalPrintingOptions = ArendPrintingOptions()
+    var popupPrintingOptions = ArendPrintingOptions()
 
 }
 

src/test/kotlin/org/arend/intention/SplitAtomPatternIntentionTest.kt

@@ -25,6 +25,17 @@ class SplitAtomPatternIntentionTest: QuickFixTestBase() {
          | suc (suc n) => 1 
     """)
 
+    fun testBasicSplitElim() = typedQuickFixTest("Split", """
+       \func isLessThan2 (a b : Nat) : Nat \elim b
+         | 0 => 1
+         | suc _{-caret-} => 1        
+    """, """
+       \func isLessThan2 (a b : Nat) : Nat \elim b
+         | 0 => 1
+         | 1 => 1
+         | suc (suc n) => 1 
+    """)
+
     fun testBasicSplitWithImplicitArgs() = typedQuickFixTest("Split", """
        \func isLessThan2 {a : Nat} : Nat
          | {0} => 1