Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bump com.diffplug.spotless from 6.18.0 to 6.25.0 #741

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,8 @@ allprojects {
}

/** Kotlin Conventions */
// TODO: move into buildSrc when this is fixed: https://youtrack.jetbrains.com/issue/KT-41142
subprojects {
// TODO: move into buildSrc when this is fixed: https://youtrack.jetbrains.com/issue/KT-41142
pluginManager.withPlugin("kotlin") {
apply(plugin = "jacoco")
apply(plugin = "org.jetbrains.dokka")
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,13 +51,14 @@ internal fun ParameterHolder.verbosity(): OptionDelegate<Int> =
// Set the global logging level.
// Note: this is not how `.validate` is meant to be used, but it's the closest feature Clikt provides.

val level = when (it) {
0 -> null
1 -> Level.INFO
2 -> Level.DEBUG
3 -> Level.TRACE
else -> Level.ALL
}
val level =
when (it) {
0 -> null
1 -> Level.INFO
2 -> Level.DEBUG
3 -> Level.TRACE
else -> Level.ALL
}

if (level != null) Configurator.setRootLevel(level)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -47,5 +47,4 @@ internal class CommandLineInterfaceTest {
}

/** Calls the command line interface with [arguments]. */
private fun cli(vararg arguments: String) =
Viaduct().parse(arrayOf(*arguments))
private fun cli(vararg arguments: String) = Viaduct().parse(arrayOf(*arguments))
26 changes: 13 additions & 13 deletions compiler/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -100,12 +100,10 @@ abstract class CompileCupTask : DefaultTask() {
}

@Internal
override fun getGroup(): String =
LifecycleBasePlugin.BUILD_TASK_NAME
override fun getGroup(): String = LifecycleBasePlugin.BUILD_TASK_NAME

@Internal
override fun getDescription(): String =
"Generates Java sources from CUP grammar files."
override fun getDescription(): String = "Generates Java sources from CUP grammar files."

@TaskAction
fun compileAll() {
Expand All @@ -128,15 +126,17 @@ abstract class CompileCupTask : DefaultTask() {
val className: String = cupFile.nameWithoutExtension

project.mkdir(targetDirectory)
val args: List<String> = cupArguments.get() + listOf(
"-destdir",
targetDirectory.get().asFile.path,
"-package",
packageName,
"-parser",
className,
cupFile.path,
)
val args: List<String> =
cupArguments.get() +
listOf(
"-destdir",
targetDirectory.get().asFile.path,
"-package",
packageName,
"-parser",
className,
cupFile.path,
)
logger.info("java_cup ${args.joinToString(" ")}}")
java_cup.Main.main(args.toTypedArray())
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,136 +17,138 @@ private typealias JoinOfMeets<A> = PersistentSet<Meet<A>>
*/
class FreeDistributiveLattice<A> private constructor(joinOfMeets: JoinOfMeets<A>) :
HeytingAlgebra<FreeDistributiveLattice<A>> {
val joinOfMeets = removeRedundant(joinOfMeets)

constructor(element: A) : this(persistentSetOf(persistentSetOf(element)))

/**
* Represents the assumption that [from] is below [to].
*
* @see FreeDistributiveLattice.lessThanOrEqualTo
*/
data class LessThanOrEqualTo<A>(val from: FreeDistributiveLattice<A>, val to: FreeDistributiveLattice<A>)

fun lessThanOrEqualTo(that: FreeDistributiveLattice<A>, assumptions: List<LessThanOrEqualTo<A>>): Boolean {
return this.joinOfMeets.all { given ->
val (applicable, inapplicable) = assumptions.partition { it.isApplicable(given) }
if (applicable.isEmpty()) {
that.joinOfMeets.any { required -> given.containsAll(required) }
} else {
applicable
.map { it.to }
.fold(FreeDistributiveLattice(persistentSetOf(given)), FreeDistributiveLattice<A>::meet)
.lessThanOrEqualTo(that, inapplicable)
val joinOfMeets = removeRedundant(joinOfMeets)

constructor(element: A) : this(persistentSetOf(persistentSetOf(element)))

/**
* Represents the assumption that [from] is below [to].
*
* @see FreeDistributiveLattice.lessThanOrEqualTo
*/
data class LessThanOrEqualTo<A>(val from: FreeDistributiveLattice<A>, val to: FreeDistributiveLattice<A>)

fun lessThanOrEqualTo(
that: FreeDistributiveLattice<A>,
assumptions: List<LessThanOrEqualTo<A>>,
): Boolean {
return this.joinOfMeets.all { given ->
val (applicable, inapplicable) = assumptions.partition { it.isApplicable(given) }
if (applicable.isEmpty()) {
that.joinOfMeets.any { required -> given.containsAll(required) }
} else {
applicable
.map { it.to }
.fold(FreeDistributiveLattice(persistentSetOf(given)), FreeDistributiveLattice<A>::meet)
.lessThanOrEqualTo(that, inapplicable)
}
}
}
}

override fun join(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
return FreeDistributiveLattice(joinOfMeets.addAll(that.joinOfMeets))
}
override fun join(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
return FreeDistributiveLattice(joinOfMeets.addAll(that.joinOfMeets))
}

override fun meet(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
var candidates: JoinOfMeets<A> = persistentSetOf()
for (meet1 in joinOfMeets) {
for (meet2 in that.joinOfMeets) {
candidates = candidates.add(meet1.addAll(meet2))
override fun meet(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
var candidates: JoinOfMeets<A> = persistentSetOf()
for (meet1 in joinOfMeets) {
for (meet2 in that.joinOfMeets) {
candidates = candidates.add(meet1.addAll(meet2))
}
}
return FreeDistributiveLattice(candidates)
}
return FreeDistributiveLattice(candidates)
}

/**
* Returns the relative pseudocomplement of `this` relative to `that`. the relative
* pseudocomplement is greatest x s.t. `this & x <= that`.
*
*
* How does this work? we are dealing with constraints of the form `(A1 | ... | Am) & x
* <= B1 | ... | Bn`
*
*
* which can be rewritten as `(A1&x) | ... | (Am&x) <= B1 | ... | Bn`
*
*
* This inequality only holds true if every meet on the left can be "covered" on the right s.t.
* a meet on the right side is a subset of the meet on the left side. For every meet on the left
* Ai, we complement it with every meet on the right Bj. because we want the greatest solution, we
* join these complements together, arriving at an upper bound for x: `x <= Ci1 | ... | Cin`
*
*
* where `Cij = Bj \ Ai`.
*
*
* But we have to do the same process for all meets on the left, so we get m upper bounds.
* these have to be all simultaneously satisfied, so we take the meet of the upper bounds: `x = (C11 | ... | C1n) & ... & (Cm1 | ... | Cmn)`
*
*
* The algorithm below computes exactly this solution.
*/
override fun imply(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
var result = bounds<A>().top
joinOfMeets.forEach { thisMeet ->
val newJoinOfMeets =
that.joinOfMeets.map { thatMeet -> thatMeet.removeAll(thisMeet) }.toPersistentSet()
result = result.meet(FreeDistributiveLattice(newJoinOfMeets))
/**
* Returns the relative pseudocomplement of `this` relative to `that`. the relative
* pseudocomplement is greatest x s.t. `this & x <= that`.
*
*
* How does this work? we are dealing with constraints of the form `(A1 | ... | Am) & x
* <= B1 | ... | Bn`
*
*
* which can be rewritten as `(A1&x) | ... | (Am&x) <= B1 | ... | Bn`
*
*
* This inequality only holds true if every meet on the left can be "covered" on the right s.t.
* a meet on the right side is a subset of the meet on the left side. For every meet on the left
* Ai, we complement it with every meet on the right Bj. because we want the greatest solution, we
* join these complements together, arriving at an upper bound for x: `x <= Ci1 | ... | Cin`
*
*
* where `Cij = Bj \ Ai`.
*
*
* But we have to do the same process for all meets on the left, so we get m upper bounds.
* these have to be all simultaneously satisfied, so we take the meet of the upper bounds: `x = (C11 | ... | C1n) & ... & (Cm1 | ... | Cmn)`
*
*
* The algorithm below computes exactly this solution.
*/
override fun imply(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A> {
var result = bounds<A>().top
joinOfMeets.forEach { thisMeet ->
val newJoinOfMeets =
that.joinOfMeets.map { thatMeet -> thatMeet.removeAll(thisMeet) }.toPersistentSet()
result = result.meet(FreeDistributiveLattice(newJoinOfMeets))
}
return result
}
return result
}

override fun equals(other: Any?): Boolean =
other is FreeDistributiveLattice<*> && this.joinOfMeets == other.joinOfMeets
override fun equals(other: Any?): Boolean = other is FreeDistributiveLattice<*> && this.joinOfMeets == other.joinOfMeets

override fun hashCode(): Int =
joinOfMeets.hashCode()
override fun hashCode(): Int = joinOfMeets.hashCode()

override fun toString(): String {
fun meetToString(meet: Meet<A>): String {
val elements = meet.map { it.toString() }.sorted()
val body = elements.joinToString(" \u2227 ")
return if (meet.size > 1) "($body)" else body
}
override fun toString(): String {
fun meetToString(meet: Meet<A>): String {
val elements = meet.map { it.toString() }.sorted()
val body = elements.joinToString(" \u2227 ")
return if (meet.size > 1) "($body)" else body
}

return when (this) {
bounds<A>().top ->
"\u22A4"
return when (this) {
bounds<A>().top ->
"\u22A4"

bounds<A>().bottom ->
"\u22A5"
bounds<A>().bottom ->
"\u22A5"

else -> {
val meets = joinOfMeets.map { meetToString(it) }.sorted()
val body = meets.joinToString(" \u2228 ")
if (joinOfMeets.size > 1) "($body)" else body
else -> {
val meets = joinOfMeets.map { meetToString(it) }.sorted()
val body = meets.joinToString(" \u2228 ")
if (joinOfMeets.size > 1) "($body)" else body
}
}
}
}

companion object {
private object Bounds : BoundedLattice<FreeDistributiveLattice<Nothing>> {
override val bottom: FreeDistributiveLattice<Nothing> =
FreeDistributiveLattice(persistentSetOf())
companion object {
private object Bounds : BoundedLattice<FreeDistributiveLattice<Nothing>> {
override val bottom: FreeDistributiveLattice<Nothing> =
FreeDistributiveLattice(persistentSetOf())

override val top: FreeDistributiveLattice<Nothing> =
FreeDistributiveLattice(persistentSetOf(persistentSetOf()))
}
override val top: FreeDistributiveLattice<Nothing> =
FreeDistributiveLattice(persistentSetOf(persistentSetOf()))
}

@Suppress("UNCHECKED_CAST")
fun <A> bounds(): BoundedLattice<FreeDistributiveLattice<A>> =
Bounds as BoundedLattice<FreeDistributiveLattice<A>>
@Suppress("UNCHECKED_CAST")
fun <A> bounds(): BoundedLattice<FreeDistributiveLattice<A>> = Bounds as BoundedLattice<FreeDistributiveLattice<A>>

/** Remove redundant meets according to [isRedundant]. */
private fun <A> removeRedundant(joinOfMeets: JoinOfMeets<A>): JoinOfMeets<A> {
return joinOfMeets.filter { meet -> !isRedundant(joinOfMeets, meet) }.toPersistentSet()
}

/**
* Given `m_1 \/ m_2 \/ ... \/ m_n`, if any `m_i` is a strict subset of `m_j`,
* then `m_j` is redundant.
*/
private fun <A> isRedundant(joinOfMeets: JoinOfMeets<A>, j: Meet<A>): Boolean =
joinOfMeets.any { it != j && j.containsAll(it) }
/** Remove redundant meets according to [isRedundant]. */
private fun <A> removeRedundant(joinOfMeets: JoinOfMeets<A>): JoinOfMeets<A> {
return joinOfMeets.filter { meet -> !isRedundant(joinOfMeets, meet) }.toPersistentSet()
}

private fun <A> LessThanOrEqualTo<A>.isApplicable(given: Meet<A>): Boolean =
this.from.joinOfMeets.any { required -> given.containsAll(required) }
/**
* Given `m_1 \/ m_2 \/ ... \/ m_n`, if any `m_i` is a strict subset of `m_j`,
* then `m_j` is redundant.
*/
private fun <A> isRedundant(
joinOfMeets: JoinOfMeets<A>,
j: Meet<A>,
): Boolean = joinOfMeets.any { it != j && j.containsAll(it) }

private fun <A> LessThanOrEqualTo<A>.isApplicable(given: Meet<A>): Boolean =
this.from.joinOfMeets.any { required -> given.containsAll(required) }
}
}
}
Original file line number Diff line number Diff line change
@@ -1,16 +1,24 @@
package io.github.aplcornell.viaduct.algebra

interface LatticeCongruence<A : Lattice<A>> {
fun equals(first: A, second: A): Boolean
fun lessThanOrEqualTo(first: A, second: A): Boolean
fun equals(
first: A,
second: A,
): Boolean

fun lessThanOrEqualTo(
first: A,
second: A,
): Boolean
}

class FreeDistributiveLatticeCongruence<A>(
private val congruence: List<FreeDistributiveLattice.LessThanOrEqualTo<A>>,
) : LatticeCongruence<FreeDistributiveLattice<A>> {

override fun equals(first: FreeDistributiveLattice<A>, second: FreeDistributiveLattice<A>) =
lessThanOrEqualTo(first, second) && lessThanOrEqualTo(second, first)
override fun equals(
first: FreeDistributiveLattice<A>,
second: FreeDistributiveLattice<A>,
) = lessThanOrEqualTo(first, second) && lessThanOrEqualTo(second, first)

override fun lessThanOrEqualTo(
first: FreeDistributiveLattice<A>,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,5 @@ class ConstraintSolution<C : Lattice<C>, V> internal constructor(
is Meet -> evaluate(term.lhs) meet evaluate(term.rhs)
}

override fun invoke(variable: V): C =
solution.getOrDefault(variable, default)
override fun invoke(variable: V): C = solution.getOrDefault(variable, default)
}
Loading
Loading