Skip to content

Commit 807592d

Browse files
committed
Refactoring empty type stream
1 parent 6da10bb commit 807592d

3 files changed

Lines changed: 16 additions & 20 deletions

File tree

usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class USupportTypeStream<Type> private constructor(
4343
if (type == supportType && filtering(type) && typeSystem.isInstantiable(type)) { // exact type
4444
USingleTypeStream(typeSystem, type)
4545
} else {
46-
UEmptyTypeStream()
46+
emptyTypeStream()
4747
}
4848
}
4949

@@ -61,7 +61,7 @@ class USupportTypeStream<Type> private constructor(
6161
override fun filterByNotSupertype(type: Type): UTypeStream<Type> {
6262
return when {
6363
typeSystem.isSupertype(type, supportType) -> {
64-
UEmptyTypeStream()
64+
emptyTypeStream()
6565
}
6666

6767
else -> {

usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ open class UTypeRegion<Type>(
2222
* Returns region that represents empty set of types. Called when type
2323
* constraints contradict, for example if X <: Y and X </: Y.
2424
*/
25-
protected fun contradiction() = UTypeRegion(typeSystem, UEmptyTypeStream())
25+
protected fun contradiction() = UTypeRegion(typeSystem, emptyTypeStream())
2626
// TODO: generate unsat core for DPLL(T)
2727

2828
/**

usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt

Lines changed: 13 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -53,28 +53,24 @@ interface UTypeStream<Type> {
5353
/**
5454
* An empty type stream.
5555
*/
56-
class UEmptyTypeStream<Type> private constructor() : UTypeStream<Type> {
57-
override fun filterBySupertype(type: Type): UTypeStream<Type> = this
56+
object UEmptyTypeStream : UTypeStream<Nothing> {
57+
override fun filterBySupertype(type: Nothing): UTypeStream<Nothing> = this
5858

59-
override fun filterBySubtype(type: Type): UTypeStream<Type> = this
59+
override fun filterBySubtype(type: Nothing): UTypeStream<Nothing> = this
6060

61-
override fun filterByNotSupertype(type: Type): UTypeStream<Type> = this
61+
override fun filterByNotSupertype(type: Nothing): UTypeStream<Nothing> = this
6262

63-
override fun filterByNotSubtype(type: Type): UTypeStream<Type> = this
63+
override fun filterByNotSubtype(type: Nothing): UTypeStream<Nothing> = this
6464

65-
override fun take(n: Int): Collection<Type> = emptyList()
65+
override fun take(n: Int): Collection<Nothing> = emptyList()
6666

6767
override val isEmpty: Boolean
6868
get() = true
69-
70-
companion object {
71-
@Suppress("UNCHECKED_CAST")
72-
operator fun <Type> invoke() = instance as UEmptyTypeStream<Type>
73-
74-
val instance = UEmptyTypeStream<Nothing>()
75-
}
7669
}
7770

71+
@Suppress("UNCHECKED_CAST")
72+
fun <Type> emptyTypeStream(): UTypeStream<Type> = UEmptyTypeStream as UTypeStream<Type>
73+
7874
fun <Type> UTypeStream<Type>.takeFirst(): Type = take(1).single()
7975

8076
/**
@@ -86,28 +82,28 @@ class USingleTypeStream<Type>(
8682
) : UTypeStream<Type> {
8783
override fun filterBySupertype(type: Type): UTypeStream<Type> =
8884
if (!typeSystem.isSupertype(type, singleType)) {
89-
UEmptyTypeStream()
85+
emptyTypeStream()
9086
} else {
9187
this
9288
}
9389

9490
override fun filterBySubtype(type: Type): UTypeStream<Type> =
9591
if (!typeSystem.isSupertype(singleType, type)) {
96-
UEmptyTypeStream()
92+
emptyTypeStream()
9793
} else {
9894
this
9995
}
10096

10197
override fun filterByNotSupertype(type: Type): UTypeStream<Type> =
10298
if (typeSystem.isSupertype(type, singleType)) {
103-
UEmptyTypeStream()
99+
emptyTypeStream()
104100
} else {
105101
this
106102
}
107103

108104
override fun filterByNotSubtype(type: Type): UTypeStream<Type> =
109105
if (typeSystem.isSupertype(singleType, type)) {
110-
UEmptyTypeStream()
106+
emptyTypeStream()
111107
} else {
112108
this
113109
}

0 commit comments

Comments
 (0)