format code in :unify

unify/build.gradle.kts

@@ -1,29 +1,9 @@
-// Project specific kotlin multiplatform configuration
 kotlin {
-
     sourceSets {
         val commonMain by getting {
             dependencies {
-//                api("com.github.gciatto:kt-math-metadata:0.+")
                 api(project(":core"))
             }
         }
-
-        // Default source set for JVM-specific sources and dependencies:
-        jvm {
-            compilations["main"].defaultSourceSet {
-                dependencies {
-//                    api(project(":core"))
-                }
-            }
-        }
-
-        js {
-            compilations["main"].defaultSourceSet {
-                dependencies {
-//                    api(project(":core"))
-                }
-            }
-        }
     }
 }

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/AbstractUnificator.kt

@@ -6,7 +6,10 @@ import it.unibo.tuprolog.core.Substitution.Companion.empty
 import it.unibo.tuprolog.core.Substitution.Companion.failed
 import it.unibo.tuprolog.core.Term
 import it.unibo.tuprolog.core.Var
-import it.unibo.tuprolog.unify.Equation.*
+import it.unibo.tuprolog.unify.Equation.Assignment
+import it.unibo.tuprolog.unify.Equation.Comparison
+import it.unibo.tuprolog.unify.Equation.Contradiction
+import it.unibo.tuprolog.unify.Equation.Identity
 import it.unibo.tuprolog.utils.dequeOf
 import kotlin.jvm.JvmOverloads
 
@@ -41,7 +44,6 @@ abstract class AbstractUnificator @JvmOverloads constructor(override val context
         equations: MutableList<Equation<Term, Term>>,
         exceptIndex: Int
     ): Boolean {
-
         var changed = false
 
         for (i in equations.indices) {
@@ -120,4 +122,4 @@ abstract class AbstractUnificator @JvmOverloads constructor(override val context
         val equations = dequeOf(contextEquations + equationsFor(substitution1, substitution2))
         return mgu(equations, occurCheckEnabled)
     }
-}
+}

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/CachedUnificator.kt

@@ -46,4 +46,4 @@ class CachedUnificator(
             }
         }
     }
-}
+}

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/Equation.kt

@@ -1,6 +1,14 @@
 package it.unibo.tuprolog.unify
 
-import it.unibo.tuprolog.core.*
+import it.unibo.tuprolog.core.Atom
+import it.unibo.tuprolog.core.Cons
+import it.unibo.tuprolog.core.Constant
+import it.unibo.tuprolog.core.Struct
+import it.unibo.tuprolog.core.Substitution
+import it.unibo.tuprolog.core.Term
+import it.unibo.tuprolog.core.ToTermConvertible
+import it.unibo.tuprolog.core.Tuple
+import it.unibo.tuprolog.core.Var
 import kotlin.js.JsName
 import kotlin.jvm.JvmOverloads
 import kotlin.jvm.JvmStatic
@@ -18,7 +26,6 @@ sealed class Equation<out A : Term, out B : Term>(
     @JsName("rhs") open val rhs: B
 ) : ToTermConvertible {
 
-
     /** An equation of identical [Term]s */
     data class Identity<out T : Term>(override val lhs: T, override val rhs: T) : Equation<T, T>(lhs, rhs)
 
@@ -55,7 +62,6 @@ sealed class Equation<out A : Term, out B : Term>(
     ): Equation<Term, Term> =
         of(lhs[substitution], rhs[substitution], equalityChecker)
 
-
     /** Equation companion object */
     companion object {
 
@@ -64,7 +70,8 @@ sealed class Equation<out A : Term, out B : Term>(
         @JvmOverloads
         @JsName("of")
         fun <A : Term, B : Term> of(
-            lhs: A, rhs: B,
+            lhs: A,
+            rhs: B,
             equalityChecker: (Term, Term) -> Boolean = Term::equals
         ): Equation<Term, Term> =
             when {
@@ -126,7 +133,8 @@ sealed class Equation<out A : Term, out B : Term>(
             allOf(pair.first, pair.second, equalityChecker)
 
         private fun allOfLists(
-            lhs: LogicList, rhs: LogicList,
+            lhs: LogicList,
+            rhs: LogicList,
             equalityChecker: (Term, Term) -> Boolean = Term::equals
         ): Sequence<Equation<Term, Term>> {
             return lhs.unfold().zip(rhs.unfold()).flatMap { (l, r) ->
@@ -140,7 +148,8 @@ sealed class Equation<out A : Term, out B : Term>(
         }
 
         private fun allOfTuples(
-            lhs: Tuple, rhs: Tuple,
+            lhs: Tuple,
+            rhs: Tuple,
             equalityChecker: (Term, Term) -> Boolean = Term::equals
         ): Sequence<Equation<Term, Term>> {
             return lhs.unfold().zip(rhs.unfold()).flatMap { (l, r) ->
@@ -156,7 +165,8 @@ sealed class Equation<out A : Term, out B : Term>(
         @JvmOverloads
         @JsName("allOf")
         fun <A : Term, B : Term> allOf(
-            lhs: A, rhs: B,
+            lhs: A,
+            rhs: B,
             equalityChecker: (Term, Term) -> Boolean = Term::equals
         ): Sequence<Equation<Term, Term>> =
             when {
@@ -178,5 +188,3 @@ sealed class Equation<out A : Term, out B : Term>(
             }
     }
 }
-
-

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/UnificationUtils.kt

@@ -5,7 +5,6 @@ package it.unibo.tuprolog.unify
 import it.unibo.tuprolog.core.Substitution
 import it.unibo.tuprolog.core.Term
 import it.unibo.tuprolog.core.Var
-import kotlin.js.JsName
 import kotlin.jvm.JvmName
 
 /** Transforms an [Equation] of a [Var] with a [Term] to the corresponding [Substitution] */
@@ -22,4 +21,4 @@ fun Substitution.toEquations(): List<Equation<Var, Term>> =
 
 /** Creates an equation with [this] and [that] terms */
 @Suppress("unused", "FunctionName")
-infix fun Term.eq(that: Term): Equation<Term, Term> = Equation.of(this, that)
+infix fun Term.eq(that: Term): Equation<Term, Term> = Equation.of(this, that)

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/Unificator.kt

@@ -137,4 +137,4 @@ interface Unificator {
 
         const val DEFAULT_CACHE_CAPACITY = 32
     }
-}
+}

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/exception/NoUnifyException.kt

@@ -11,4 +11,3 @@ open class NoUnifyException(private val term1: Term, private val term2: Term, ot
     override val message: String?
         get() = "Cannot match term `$term1` with term `$term2`"
 }
-

unify/src/commonMain/kotlin/it/unibo/tuprolog/unify/exception/OccurCheckException.kt

@@ -11,10 +11,9 @@ class OccurCheckException(
     other: Throwable?
 ) : NoUnifyException(term1, term2, other) {
 
-    constructor(term1: Term, term2: Term, innerVar: Var, innerTerm: Term)
-            : this(term1, term2, innerVar, innerTerm, null)
-
+    constructor(term1: Term, term2: Term, innerVar: Var, innerTerm: Term) :
+        this(term1, term2, innerVar, innerTerm, null)
 
     override val message: String?
         get() = "${super.message} because variable `$innerVar` occurs in term `$innerTerm`"
-}
+}

unify/src/commonTest/kotlin/it/unibo/tuprolog/unify/AbstractUnificatorTest.kt

@@ -1,6 +1,11 @@
 package it.unibo.tuprolog.unify
 
-import it.unibo.tuprolog.core.*
+import it.unibo.tuprolog.core.Atom
+import it.unibo.tuprolog.core.Integer
+import it.unibo.tuprolog.core.Struct
+import it.unibo.tuprolog.core.Substitution
+import it.unibo.tuprolog.core.Term
+import it.unibo.tuprolog.core.Var
 import it.unibo.tuprolog.unify.testutils.UnificatorUtils
 import it.unibo.tuprolog.unify.testutils.UnificatorUtils.assertMatchCorrect
 import it.unibo.tuprolog.unify.testutils.UnificatorUtils.assertMguCorrect
@@ -119,7 +124,7 @@ internal class AbstractUnificatorTest {
 
         val correctnessMap = mapOf(
             (xVar eq structWithX) to
-                    Triple(Substitution.of(xVar, structWithX), true, structWithX)
+                Triple(Substitution.of(xVar, structWithX), true, structWithX)
         )
 
         assertMguCorrect(correctnessMap) { term1, term2 -> myStrategy.mgu(term1, term2, false) }
@@ -129,19 +134,13 @@ internal class AbstractUnificatorTest {
 
     @Test
     fun sequenceOfEquationsSuccessUnification() {
-        forEquationSequence(::assertMguCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
+        forEquationSequence(::assertMguCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
 
-        forEquationSequence(::assertMguCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
+        forEquationSequence(::assertMguCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
 
+        forEquationSequence(::assertMatchCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
 
-        forEquationSequence(::assertMatchCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
-
-        forEquationSequence(::assertMatchCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
-
+        forEquationSequence(::assertMatchCorrect, UnificatorUtils.successSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
 
         forEquationSequence(
             ::assertUnifiedTermCorrect,
@@ -180,19 +179,13 @@ internal class AbstractUnificatorTest {
 
     @Test
     fun sequenceOfEquationsFailedUnification() {
-        forEquationSequence(::assertMguCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
-
-        forEquationSequence(::assertMguCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
+        forEquationSequence(::assertMguCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
 
+        forEquationSequence(::assertMguCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).mgu(t1, t2) }
 
-        forEquationSequence(::assertMatchCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
-
-        forEquationSequence(::assertMatchCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor)
-        { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
+        forEquationSequence(::assertMatchCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
 
+        forEquationSequence(::assertMatchCorrect, UnificatorUtils.failSequenceOfUnification, myStrategyConstructor) { context, t1, t2 -> myStrategyConstructor(context).match(t1, t2) }
 
         forEquationSequence(
             ::assertUnifiedTermCorrect,
@@ -210,10 +203,10 @@ internal class AbstractUnificatorTest {
     @Test
     fun unificationWorksForBigLists() {
         val n = 10_000
-        val ints = LogicList.of((0 .. n).map { Integer.of(it) })
-        val intsAndVars = LogicList.of((0 .. n).map { if (it % 100 == 0) Var.anonymous() else Integer.of(it) })
-        val atoms = LogicList.of((0 .. n).map { Atom.of("a$it") })
-        val atomsAndVars = LogicList.of((0 .. n).map { if (it % 100 == 0) Var.anonymous() else Atom.of("a$it") })
+        val ints = LogicList.of((0..n).map { Integer.of(it) })
+        val intsAndVars = LogicList.of((0..n).map { if (it % 100 == 0) Var.anonymous() else Integer.of(it) })
+        val atoms = LogicList.of((0..n).map { Atom.of("a$it") })
+        val atomsAndVars = LogicList.of((0..n).map { if (it % 100 == 0) Var.anonymous() else Atom.of("a$it") })
 
         with(myStrategyConstructor(Substitution.empty())) {
             assertFalse { match(ints, atoms, true) }
@@ -227,6 +220,5 @@ internal class AbstractUnificatorTest {
             assertTrue { match(atoms, atomsAndVars, true) }
             assertTrue { match(atoms, atomsAndVars, false) }
         }
-
     }
 }

unify/src/commonTest/kotlin/it/unibo/tuprolog/unify/EquationTest.kt

@@ -1,6 +1,10 @@
 package it.unibo.tuprolog.unify
 
-import it.unibo.tuprolog.core.*
+import it.unibo.tuprolog.core.Atom
+import it.unibo.tuprolog.core.Struct
+import it.unibo.tuprolog.core.Substitution
+import it.unibo.tuprolog.core.Term
+import it.unibo.tuprolog.core.Var
 import it.unibo.tuprolog.unify.testutils.EquationUtils
 import it.unibo.tuprolog.unify.testutils.EquationUtils.assertAllIdentities
 import it.unibo.tuprolog.unify.testutils.EquationUtils.assertAnyAssignment
@@ -23,9 +27,9 @@ internal class EquationTest {
     /** Correct instances of equations, whose type is recognizable without exploring in deep the components */
     private val correctShallowEquationsInstances =
         EquationUtils.shallowIdentityEquations.map { (lhs, rhs) -> Equation.Identity(lhs, rhs) } +
-                EquationUtils.assignmentEquations.map { (lhs, rhs) -> Equation.Assignment(lhs, rhs) } +
-                EquationUtils.comparisonEquations.map { (lhs, rhs) -> Equation.Comparison(lhs, rhs) } +
-                EquationUtils.shallowContradictionEquations.map { (lhs, rhs) -> Equation.Contradiction(lhs, rhs) }
+            EquationUtils.assignmentEquations.map { (lhs, rhs) -> Equation.Assignment(lhs, rhs) } +
+            EquationUtils.comparisonEquations.map { (lhs, rhs) -> Equation.Comparison(lhs, rhs) } +
+            EquationUtils.shallowContradictionEquations.map { (lhs, rhs) -> Equation.Contradiction(lhs, rhs) }
 
     @Test
     fun identityLhsAndRhsCorrect() {
@@ -80,10 +84,10 @@ internal class EquationTest {
     @Test
     fun equationOfAutomaticallySwapsAssignments() {
         val correct = EquationUtils.assignmentEquations.map { (lhs, rhs) -> Equation.of(lhs, rhs) } +
-                EquationUtils.assignmentEquations.map { Equation.of(it) }
+            EquationUtils.assignmentEquations.map { Equation.of(it) }
 
         val toBeTested = EquationUtils.assignmentEquationsShuffled.map { (lhs, rhs) -> Equation.of(lhs, rhs) } +
-                EquationUtils.assignmentEquationsShuffled.map { Equation.of(it) }
+            EquationUtils.assignmentEquationsShuffled.map { Equation.of(it) }
 
         assertEquals(correct, toBeTested)
     }
@@ -133,11 +137,11 @@ internal class EquationTest {
     @Test
     fun equationAllOfAutomaticallySwapsAssignments() {
         val correct = EquationUtils.assignmentEquations.map { (lhs, rhs) -> Equation.allOf(lhs, rhs).toList() } +
-                EquationUtils.assignmentEquations.map { Equation.allOf(it).toList() }
+            EquationUtils.assignmentEquations.map { Equation.allOf(it).toList() }
 
         val toBeTested =
             EquationUtils.assignmentEquationsShuffled.map { (lhs, rhs) -> Equation.allOf(lhs, rhs).toList() } +
-                    EquationUtils.assignmentEquationsShuffled.map { Equation.allOf(it).toList() }
+                EquationUtils.assignmentEquationsShuffled.map { Equation.allOf(it).toList() }
 
         assertEquals(correct, toBeTested)
     }
@@ -166,8 +170,8 @@ internal class EquationTest {
     @Test
     fun swapCanInvertAllInvertibleEquations() {
         val testableItems = EquationUtils.allIdentityEquations +
-                EquationUtils.allContradictionEquations +
-                EquationUtils.comparisonEquations
+            EquationUtils.allContradictionEquations +
+            EquationUtils.comparisonEquations
 
         val correct = testableItems.map { (lhs, rhs) -> rhs to lhs }.map { Equation.of(it) }
         val toBeTested = testableItems.map { Equation.of(it) }.map(Equation<*, *>::swap)
@@ -188,30 +192,38 @@ internal class EquationTest {
 
     @Test
     fun equationOfLhsAndRhsUsesProvidedEqualityCheckerToTestIdentity() {
-        assertNoIdentities(EquationUtils.mixedAllEquations.map { (lhs, rhs) ->
-            Equation.of(lhs, rhs, { _, _ -> false })
-        }.asSequence())
+        assertNoIdentities(
+            EquationUtils.mixedAllEquations.map { (lhs, rhs) ->
+                Equation.of(lhs, rhs, { _, _ -> false })
+            }.asSequence()
+        )
     }
 
     @Test
     fun equationOfPairUsesProvidedEqualityCheckerToTestIdentity() {
-        assertNoIdentities(EquationUtils.mixedAllEquations.map {
-            Equation.of(it) { _, _ -> false }
-        }.asSequence())
+        assertNoIdentities(
+            EquationUtils.mixedAllEquations.map {
+                Equation.of(it) { _, _ -> false }
+            }.asSequence()
+        )
     }
 
     @Test
     fun equationAllOfLhsAndRhsUsesProvidedEqualityCheckerToTestIdentity() {
-        assertNoIdentities(EquationUtils.mixedAllEquations.flatMap { (lhs, rhs) ->
-            Equation.allOf(lhs, rhs, { _, _ -> false }).asIterable()
-        }.asSequence())
+        assertNoIdentities(
+            EquationUtils.mixedAllEquations.flatMap { (lhs, rhs) ->
+                Equation.allOf(lhs, rhs, { _, _ -> false }).asIterable()
+            }.asSequence()
+        )
     }
 
     @Test
     fun equationAllOfPairUsesProvidedEqualityCheckerToTestIdentity() {
-        assertNoIdentities(EquationUtils.mixedAllEquations.flatMap {
-            Equation.allOf(it) { _, _ -> false }.asIterable()
-        }.asSequence())
+        assertNoIdentities(
+            EquationUtils.mixedAllEquations.flatMap {
+                Equation.allOf(it) { _, _ -> false }.asIterable()
+            }.asSequence()
+        )
     }
 
     @Test