Merge pull request #143 from KalkulierbaR/dev

Update yarn and vite major version

backend/build.gradle.kts

@@ -1,8 +1,8 @@
 plugins {
-    kotlin("jvm") version "1.7.20"
+    kotlin("jvm") version "1.9.23"
     kotlin("plugin.serialization") version "1.9.23"
     application
-    id("org.jmailen.kotlinter") version "3.10.0"
+    id("org.jmailen.kotlinter") version "3.16.0"
     id("io.gitlab.arturbosch.detekt") version "1.23.6"
     id("com.github.johnrengelman.shadow") version "7.1.2"
     id("java")
@@ -66,5 +66,4 @@ detekt {
 kotlinter {
     ignoreFailures = false
     reporters = arrayOf("checkstyle", "plain")
-    experimentalRules = false
 }

backend/src/main/kotlin/Main.kt

@@ -32,7 +32,7 @@ val endpoints: Set<Calculus> = setOf<Calculus>(
     NonClausalTableaux(),
     PropositionalSequent(),
     FirstOrderSequent(),
-    SignedModalTableaux()
+    SignedModalTableaux(),
 )
 
 fun main(args: Array<String>) {
@@ -43,7 +43,7 @@ fun main(args: Array<String>) {
     // Verify that no calculus is overriding /admin and /config endpoints
     if (endpoints.any { it.identifier == "admin" || it.identifier == "config" || it.identifier == "stats" }) {
         throw KalkulierbarException(
-            "Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\""
+            "Set of active calculi contains forbidden identifiers \"admin\", \"config\" or \"stats\"",
         )
     }
     // Pass list of available calculi to StateKeeper
@@ -66,7 +66,6 @@ fun getEnvPort() = System.getenv("PORT")?.toInt() ?: KBAR_DEFAULT_PORT
  */
 @Suppress("ThrowsCount", "MagicNumber", "LongMethod", "ComplexMethod")
 fun httpApi(port: Int, endpoints: Set<Calculus>, listenGlobally: Boolean = false) {
-
     val host = if (listenGlobally) "0.0.0.0" else "localhost"
 
     val app = Javalin.create { config ->
@@ -97,7 +96,7 @@ fun httpApi(port: Int, endpoints: Set<Calculus>, listenGlobally: Boolean = false
                 |
                 |Available calculus endpoints:
                 |${ids.joinToString("\n")}
-            """.trimMargin()
+            """.trimMargin(),
         )
     }
 
@@ -160,7 +159,7 @@ fun createCalculusEndpoints(app: Javalin, calculus: Calculus) {
             """
                 |Calculus "$name" loaded.
                 |Interact via the /parse /move /close and /validate endpoints
-            """.trimMargin()
+            """.trimMargin(),
         )
     }
 

backend/src/main/kotlin/kalkulierbar/ScoredCalculus.kt

@@ -42,7 +42,7 @@ abstract class ScoredCalculus<State, Move, Param> : JSONCalculus<State, Move, Pa
 
 @Serializable
 data class Scores(
-    val entries: List<Map<String, String>>
+    val entries: List<Map<String, String>>,
 ) {
     val keys = if (entries.isEmpty()) emptyList() else entries[0].keys.toList()
 }

backend/src/main/kotlin/kalkulierbar/dpll/DPLL.kt

@@ -10,7 +10,10 @@ import kotlinx.serialization.modules.plus
 class DPLL : JSONCalculus<DPLLState, DPLLMove, Unit>() {
     override val identifier = "dpll"
 
-    override val serializer = Json { serializersModule = dpllMoveModule + clausesetDiffModule; encodeDefaults = true }
+    override val serializer = Json {
+        serializersModule = dpllMoveModule + clausesetDiffModule
+        encodeDefaults = true
+    }
     override val moveSerializer = DPLLMove.serializer()
     override val stateSerializer = DPLLState.serializer()
 

backend/src/main/kotlin/kalkulierbar/logic/LogicNodes.kt

@@ -164,7 +164,7 @@ class Relation(val spelling: String, var arguments: List<FirstOrderTerm>) : Synt
 class UniversalQuantifier(
     override var varName: String,
     override var child: LogicNode,
-    override val boundVariables: MutableList<QuantifiedVariable>
+    override val boundVariables: MutableList<QuantifiedVariable>,
 ) : Quantifier() {
 
     override fun toString() = "(∀$varName: $child)"
@@ -215,7 +215,7 @@ class UniversalQuantifier(
 class ExistentialQuantifier(
     override var varName: String,
     override var child: LogicNode,
-    override val boundVariables: MutableList<QuantifiedVariable>
+    override val boundVariables: MutableList<QuantifiedVariable>,
 ) : Quantifier() {
 
     override fun toString() = "(∃$varName: $child)"

backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt

@@ -55,7 +55,7 @@ class FreeVariableCollector : DoNothingCollector() {
  * @param boundVariables: set of bound variables to compare with variables in first-order term
  */
 class FreeVariableTermCollector(
-    val boundVariables: Set<QuantifiedVariable>
+    val boundVariables: Set<QuantifiedVariable>,
 ) : FirstOrderTermVisitor<Set<QuantifiedVariable>>() {
     override fun visit(node: Constant): Set<QuantifiedVariable> {
         return mutableSetOf()

backend/src/main/kotlin/kalkulierbar/logic/transform/PrenexNormalForm.kt

@@ -53,11 +53,10 @@ class PrenexNormalForm : DoNothingVisitor() {
      * @return quantified sub-formula
      */
     override fun visit(node: UniversalQuantifier): LogicNode {
-
         if (encounteredVars.contains(node.varName)) {
             throw FormulaConversionException(
                 "Prenex Normal Form conversion encountered " +
-                    "double-binding of variable '${node.varName}'"
+                    "double-binding of variable '${node.varName}'",
             )
         }
 
@@ -74,11 +73,10 @@ class PrenexNormalForm : DoNothingVisitor() {
      * @return quantified sub-formula
      */
     override fun visit(node: ExistentialQuantifier): LogicNode {
-
         if (encounteredVars.contains(node.varName)) {
             throw FormulaConversionException(
                 "Prenex Normal Form conversion encountered " +
-                    " double-binding of variable '${node.varName}'"
+                    " double-binding of variable '${node.varName}'",
             )
         }
 

backend/src/main/kotlin/kalkulierbar/logic/transform/Signature.kt

@@ -43,8 +43,10 @@ data class Signature(
     companion object {
         fun empty(): Signature {
             return Signature(
-                constants = setOf(), functions = setOf(),
-                relations = setOf(), boundVariables = setOf()
+                constants = setOf(),
+                functions = setOf(),
+                relations = setOf(),
+                boundVariables = setOf(),
             )
         }
 
@@ -82,7 +84,7 @@ data class Signature(
             constants = constants + sig.constants,
             functions = functions + sig.functions,
             relations = relations + sig.relations,
-            boundVariables = boundVariables + sig.boundVariables
+            boundVariables = boundVariables + sig.boundVariables,
         )
     }
 
@@ -152,7 +154,7 @@ class SignatureExtractor : DoNothingCollector() {
                 constants = instance.constants,
                 functions = instance.functions,
                 relations = instance.relations,
-                boundVariables = instance.boundVariables
+                boundVariables = instance.boundVariables,
             )
         }
     }
@@ -201,7 +203,7 @@ class TermSignatureExtractor(
 
 class SignatureAdherenceChecker(
     private val sig: Signature,
-    private val allowNewConstants: Boolean = true
+    private val allowNewConstants: Boolean = true,
 ) : FirstOrderTermVisitor<Unit>() {
 
     override fun visit(node: Constant) {

backend/src/main/kotlin/kalkulierbar/logic/transform/Skolemization.kt

@@ -63,11 +63,10 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() {
      * @return Skolemized subformula without the existential quantifier
      */
     override fun visit(node: ExistentialQuantifier): LogicNode {
-
         if (quantifierScope.size > quantifierScope.distinctBy { it.varName }.size) {
             throw FormulaConversionException(
                 "Double-bound universally quantified variable encountered " +
-                    "during Skolemization"
+                    "during Skolemization",
             )
         }
 
@@ -127,7 +126,7 @@ class Skolemization(private val signature: Signature) : DoNothingVisitor() {
  */
 class SkolemTermReplacer(
     private val replacementMap: Map<QuantifiedVariable, FirstOrderTerm>,
-    private val bindingQuantifiers: List<UniversalQuantifier>
+    private val bindingQuantifiers: List<UniversalQuantifier>,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     /**

backend/src/main/kotlin/kalkulierbar/logic/transform/TermVariableManipulation.kt

@@ -8,7 +8,7 @@ import kalkulierbar.logic.QuantifiedVariable
 import kalkulierbar.logic.Quantifier
 
 class VariableInstantiator(
-    private val replacementMap: Map<String, FirstOrderTerm>
+    private val replacementMap: Map<String, FirstOrderTerm>,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     companion object {
@@ -172,7 +172,7 @@ class TermContainsVariable(val variable: String) : FirstOrderTermVisitor<Boolean
  */
 class QuantifierLinker(
     private val quantifiers: List<Quantifier>,
-    private val enforceUnique: Boolean
+    private val enforceUnique: Boolean,
 ) : FirstOrderTermVisitor<Unit>() {
 
     /**
@@ -185,12 +185,12 @@ class QuantifierLinker(
         if (matchingQuantifiers.isEmpty()) {
             throw FormulaConversionException(
                 "Error linking variables to quantifiers: " +
-                    "Variable '${node.spelling}' is not bound by any quantifier"
+                    "Variable '${node.spelling}' is not bound by any quantifier",
             )
         } else if (matchingQuantifiers.size > 1 && enforceUnique) {
             throw FormulaConversionException(
                 "Error linking variables to quantifiers: " +
-                    "Variable '${node.spelling}' is bound by more than one quantifier"
+                    "Variable '${node.spelling}' is bound by more than one quantifier",
             )
         }
 

backend/src/main/kotlin/kalkulierbar/logic/transform/UniqueVariables.kt

@@ -31,8 +31,10 @@ class UniqueVariables : DoNothingVisitor() {
 
     // Keep track of variable version numbers already used
     private val variableDisambCounter = mutableMapOf<String, Int>()
+
     // Keep track of variable names encountered to prevent possible double-binding
     private val seenVarNames = mutableListOf<String>()
+
     // Map of all QuantifiedVariables to be renamed
     private val replacementMap = mutableMapOf<QuantifiedVariable, String>()
 
@@ -114,7 +116,7 @@ class UniqueVariables : DoNothingVisitor() {
  */
 class VariableRenamer(
     private val replacementMap: Map<QuantifiedVariable, String>,
-    val strict: Boolean = true
+    val strict: Boolean = true,
 ) : FirstOrderTermVisitor<Unit>() {
     /**
      * Change the variable name to the new spelling

backend/src/main/kotlin/kalkulierbar/logic/util/Unification.kt

@@ -41,7 +41,7 @@ class Unification {
         private fun findTermsToUnify(
             terms: MutableList<Pair<FirstOrderTerm, FirstOrderTerm>>,
             r1: Relation,
-            r2: Relation
+            r2: Relation,
         ) {
             val arg1 = r1.arguments
             val arg2 = r2.arguments
@@ -69,7 +69,6 @@ class Unification {
 
             // As long as both relations aren't the same
             while (terms.isNotEmpty()) {
-
                 var (term1, term2) = terms.removeAt(0)
 
                 // Apply gathered substitutions just-in-time

backend/src/main/kotlin/kalkulierbar/logic/util/UnifierEquivalence.kt

@@ -62,7 +62,7 @@ class UnifierEquivalence {
          * @return List of pairs of terms with canonical names applied
          */
         private fun canonicalVarNames(
-            list: List<Pair<FirstOrderTerm, FirstOrderTerm>>
+            list: List<Pair<FirstOrderTerm, FirstOrderTerm>>,
         ): List<Pair<FirstOrderTerm, FirstOrderTerm>> {
             val canon1 = VariableCanonicizer()
             val canon2 = VariableCanonicizer()

backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/BasicMoves.kt

@@ -210,7 +210,7 @@ fun applyClose(
     state: NcTableauxState,
     nodeID: Int,
     closeID: Int,
-    varAssign: Map<String, FirstOrderTerm>?
+    varAssign: Map<String, FirstOrderTerm>?,
 ): NcTableauxState {
     checkCloseIDRestrictions(state, nodeID, closeID)
 
@@ -243,7 +243,7 @@ fun applyClose(
     if (!nodeRelation.synEq(closeRelation)) {
         throw IllegalMove(
             "Relations '$nodeRelation' and '$closeRelation' are" +
-                " not equal after variable instantiation"
+                " not equal after variable instantiation",
         )
     }
 

backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/DeltaSkolemization.kt

@@ -16,7 +16,7 @@ import kalkulierbar.logic.transform.FreeVariableCollector
  */
 class DeltaSkolemization(
     private val toReplace: List<QuantifiedVariable>,
-    private val term: FirstOrderTerm
+    private val term: FirstOrderTerm,
 ) : DoNothingVisitor() {
 
     companion object Companion {
@@ -29,7 +29,7 @@ class DeltaSkolemization(
         fun transform(
             formula: ExistentialQuantifier,
             blacklist: MutableSet<String>,
-            skolemCounter: Int
+            skolemCounter: Int,
         ): LogicNode {
             // Collect free variables in formula
             val freeVariables = FreeVariableCollector.collect(formula)
@@ -50,7 +50,7 @@ class DeltaSkolemization(
         private fun getSkolemTerm(
             skolemBaseCount: Int,
             nameBlacklist: MutableSet<String>,
-            freeVariables: Set<QuantifiedVariable>
+            freeVariables: Set<QuantifiedVariable>,
         ): FirstOrderTerm {
             var skolemCounter = skolemBaseCount
             var skolemName = "sk$skolemCounter"
@@ -96,7 +96,7 @@ class DeltaSkolemization(
  */
 class DeltaSkolemTermReplacer(
     private val toReplace: List<QuantifiedVariable>,
-    private val term: FirstOrderTerm
+    private val term: FirstOrderTerm,
 ) : FirstOrderTermVisitor<FirstOrderTerm>() {
 
     /**

backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NcTableauxMove.kt

@@ -54,7 +54,7 @@ class DeltaMove(val nodeID: Int) : NcTableauxMove() {
 class CloseMove(
     val nodeID: Int,
     val closeID: Int,
-    val varAssign: Map<String, String>?
+    val varAssign: Map<String, String>?,
 ) : NcTableauxMove() {
     /**
      * Parses map values to first-order terms

backend/src/main/kotlin/kalkulierbar/nonclausaltableaux/NonClausalTableauxMisc.kt

@@ -10,7 +10,7 @@ import kotlinx.serialization.Serializable
 @Serializable
 class NcTableauxState(
     val formula: LogicNode,
-    val backtracking: Boolean = true
+    val backtracking: Boolean = true,
 ) : ProtectedState(), TreeGardener<NcTableauxNode> {
     override val tree = mutableListOf(NcTableauxNode(null, formula.clone()))
     val moveHistory = mutableListOf<NcTableauxMove>()
@@ -67,7 +67,7 @@ class NcTableauxState(
 @Serializable
 class NcTableauxNode(
     override var parent: Int?,
-    var formula: LogicNode
+    var formula: LogicNode,
 ) : GenericTreeNode {
 
     var isClosed = false

backend/src/main/kotlin/kalkulierbar/parsers/ClauseSetParser.kt

@@ -26,9 +26,8 @@ object ClauseSetParser {
         formula: String,
         clauseSeparator: String,
         atomSeparator: String,
-        negSign: Char
+        negSign: Char,
     ): ClauseSet<String> {
-
         val aSep = Regex.escape(atomSeparator)
         val cSep = Regex.escape(clauseSeparator)
         val nSig = Regex.escape(negSign.toString())
@@ -49,7 +48,7 @@ object ClauseSetParser {
         if (!(Regex(formulaFormat) matches pf)) {
             throw InvalidFormulaFormat(
                 "Please use alphanumeric variables only, " +
-                    "separate atoms with '$atomSeparator' and clauses with '$clauseSeparator'."
+                    "separate atoms with '$atomSeparator' and clauses with '$clauseSeparator'.",
             )
         }
 

backend/src/main/kotlin/kalkulierbar/parsers/FirstOrderParser.kt

@@ -133,7 +133,6 @@ class FirstOrderParser : PropositionalParser() {
      * @return LogicNode representing the series of quantifiers
      */
     private fun parseQuantifier(): LogicNode {
-
         if (!nextTokenIs(TokenType.UNIVERSALQUANT) && !nextTokenIs(TokenType.EXISTENTIALQUANT)) {
             return parseParen()
         }
@@ -207,7 +206,7 @@ class FirstOrderParser : PropositionalParser() {
 
         // Relation may have an arbitrary amount of argument terms
         val arguments = mutableListOf<FirstOrderTerm>()
-        if (! nextTokenIs(TokenType.RPAREN)) {
+        if (!nextTokenIs(TokenType.RPAREN)) {
             arguments.add(parseTerm())
         }
         while (nextTokenIs(TokenType.COMMA)) {