Add utilities to check if ESValue is boolean/wildcard constant
This commit is contained in:
+3
-2
@@ -21,6 +21,7 @@ import org.jetbrains.kotlin.contracts.model.ConditionalEffect
|
|||||||
import org.jetbrains.kotlin.contracts.model.ESEffect
|
import org.jetbrains.kotlin.contracts.model.ESEffect
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESConstant
|
import org.jetbrains.kotlin.contracts.model.structure.ESConstant
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.isReturns
|
import org.jetbrains.kotlin.contracts.model.structure.isReturns
|
||||||
|
import org.jetbrains.kotlin.contracts.model.structure.isWildcard
|
||||||
|
|
||||||
abstract class AbstractBinaryFunctor : AbstractReducingFunctor() {
|
abstract class AbstractBinaryFunctor : AbstractReducingFunctor() {
|
||||||
override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
|
override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
|
||||||
@@ -33,9 +34,9 @@ abstract class AbstractBinaryFunctor : AbstractReducingFunctor() {
|
|||||||
if (right is ESConstant) return invokeWithConstant(left, right)
|
if (right is ESConstant) return invokeWithConstant(left, right)
|
||||||
|
|
||||||
val leftValueReturning =
|
val leftValueReturning =
|
||||||
left.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { value != ESConstant.WILDCARD } }
|
left.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { !value.isWildcard } }
|
||||||
val rightValueReturning =
|
val rightValueReturning =
|
||||||
right.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { value != ESConstant.WILDCARD } }
|
right.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { !value.isWildcard } }
|
||||||
|
|
||||||
val nonInterestingEffects =
|
val nonInterestingEffects =
|
||||||
left.effects - leftValueReturning + right.effects - rightValueReturning
|
left.effects - leftValueReturning + right.effects - rightValueReturning
|
||||||
|
|||||||
+2
-2
@@ -19,8 +19,8 @@ package org.jetbrains.kotlin.contracts.model.functors
|
|||||||
import org.jetbrains.kotlin.contracts.model.Computation
|
import org.jetbrains.kotlin.contracts.model.Computation
|
||||||
import org.jetbrains.kotlin.contracts.model.ConditionalEffect
|
import org.jetbrains.kotlin.contracts.model.ConditionalEffect
|
||||||
import org.jetbrains.kotlin.contracts.model.ESEffect
|
import org.jetbrains.kotlin.contracts.model.ESEffect
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESConstant
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.isReturns
|
import org.jetbrains.kotlin.contracts.model.structure.isReturns
|
||||||
|
import org.jetbrains.kotlin.contracts.model.structure.isWildcard
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Unary functor that has sequential semantics, i.e. it won't apply to
|
* Unary functor that has sequential semantics, i.e. it won't apply to
|
||||||
@@ -37,7 +37,7 @@ abstract class AbstractUnaryFunctor : AbstractReducingFunctor() {
|
|||||||
|
|
||||||
fun invokeWithArguments(arg: Computation): List<ESEffect> {
|
fun invokeWithArguments(arg: Computation): List<ESEffect> {
|
||||||
val returning =
|
val returning =
|
||||||
arg.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { value != ESConstant.WILDCARD } }
|
arg.effects.filterIsInstance<ConditionalEffect>().filter { it.simpleEffect.isReturns { !value.isWildcard } }
|
||||||
val rest = arg.effects - returning
|
val rest = arg.effects - returning
|
||||||
|
|
||||||
val evaluatedByFunctor = invokeWithReturningEffects(returning)
|
val evaluatedByFunctor = invokeWithReturningEffects(returning)
|
||||||
|
|||||||
+5
-8
@@ -16,15 +16,12 @@
|
|||||||
|
|
||||||
package org.jetbrains.kotlin.contracts.model.functors
|
package org.jetbrains.kotlin.contracts.model.functors
|
||||||
|
|
||||||
import org.jetbrains.kotlin.builtins.DefaultBuiltIns
|
|
||||||
import org.jetbrains.kotlin.builtins.KotlinBuiltIns
|
import org.jetbrains.kotlin.builtins.KotlinBuiltIns
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESReturns
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESConstant
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESEqual
|
|
||||||
import org.jetbrains.kotlin.contracts.model.ESValue
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.lift
|
|
||||||
import org.jetbrains.kotlin.contracts.model.*
|
|
||||||
import org.jetbrains.kotlin.contracts.model.Computation
|
import org.jetbrains.kotlin.contracts.model.Computation
|
||||||
|
import org.jetbrains.kotlin.contracts.model.ConditionalEffect
|
||||||
|
import org.jetbrains.kotlin.contracts.model.ESEffect
|
||||||
|
import org.jetbrains.kotlin.contracts.model.ESValue
|
||||||
|
import org.jetbrains.kotlin.contracts.model.structure.*
|
||||||
|
|
||||||
class EqualsFunctor(val isNegated: Boolean) : AbstractReducingFunctor() {
|
class EqualsFunctor(val isNegated: Boolean) : AbstractReducingFunctor() {
|
||||||
/*
|
/*
|
||||||
@@ -74,7 +71,7 @@ class EqualsFunctor(val isNegated: Boolean) : AbstractReducingFunctor() {
|
|||||||
val resultingClauses = mutableListOf<ESEffect>()
|
val resultingClauses = mutableListOf<ESEffect>()
|
||||||
|
|
||||||
for (effect in call.effects) {
|
for (effect in call.effects) {
|
||||||
if (effect !is ConditionalEffect || effect.simpleEffect !is ESReturns || effect.simpleEffect.value == ESConstant.WILDCARD) {
|
if (effect !is ConditionalEffect || effect.simpleEffect !is ESReturns || effect.simpleEffect.value.isWildcard) {
|
||||||
resultingClauses += effect
|
resultingClauses += effect
|
||||||
continue
|
continue
|
||||||
}
|
}
|
||||||
|
|||||||
+6
-13
@@ -16,15 +16,8 @@
|
|||||||
|
|
||||||
package org.jetbrains.kotlin.contracts.model.functors
|
package org.jetbrains.kotlin.contracts.model.functors
|
||||||
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESCalls
|
import org.jetbrains.kotlin.contracts.model.*
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESReturns
|
import org.jetbrains.kotlin.contracts.model.structure.*
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESConstant
|
|
||||||
import org.jetbrains.kotlin.contracts.model.ESValue
|
|
||||||
import org.jetbrains.kotlin.contracts.model.structure.ESVariable
|
|
||||||
import org.jetbrains.kotlin.contracts.model.ConditionalEffect
|
|
||||||
import org.jetbrains.kotlin.contracts.model.ESEffect
|
|
||||||
import org.jetbrains.kotlin.contracts.model.SimpleEffect
|
|
||||||
import org.jetbrains.kotlin.contracts.model.Computation
|
|
||||||
import org.jetbrains.kotlin.contracts.model.visitors.Substitutor
|
import org.jetbrains.kotlin.contracts.model.visitors.Substitutor
|
||||||
import org.jetbrains.kotlin.descriptors.FunctionDescriptor
|
import org.jetbrains.kotlin.descriptors.FunctionDescriptor
|
||||||
import org.jetbrains.kotlin.descriptors.ValueDescriptor
|
import org.jetbrains.kotlin.descriptors.ValueDescriptor
|
||||||
@@ -54,8 +47,8 @@ class SubstitutingFunctor(private val basicEffects: List<ESEffect>, private val
|
|||||||
}
|
}
|
||||||
|
|
||||||
is ESCalls -> {
|
is ESCalls -> {
|
||||||
val subsitutionForCallable = substitutions[effect.callable] as? ESValue ?: continue@effectsLoop
|
val substitutionForCallable = substitutions[effect.callable] as? ESValue ?: continue@effectsLoop
|
||||||
substitutedClauses += ESCalls(subsitutionForCallable, effect.kind)
|
substitutedClauses += ESCalls(substitutionForCallable, effect.kind)
|
||||||
}
|
}
|
||||||
|
|
||||||
else -> substitutedClauses += effect
|
else -> substitutedClauses += effect
|
||||||
@@ -69,9 +62,9 @@ class SubstitutingFunctor(private val basicEffects: List<ESEffect>, private val
|
|||||||
if (substitutedCondition !is ConditionalEffect) return null
|
if (substitutedCondition !is ConditionalEffect) return null
|
||||||
|
|
||||||
val effectFromCondition = substitutedCondition.simpleEffect
|
val effectFromCondition = substitutedCondition.simpleEffect
|
||||||
if (effectFromCondition !is ESReturns || effectFromCondition.value == ESConstant.WILDCARD) return substitutedCondition
|
if (effectFromCondition !is ESReturns || effectFromCondition.value.isWildcard) return substitutedCondition
|
||||||
|
|
||||||
if (effectFromCondition.value != ESConstant.TRUE) return null
|
if (!effectFromCondition.value.isTrue) return null
|
||||||
|
|
||||||
return ConditionalEffect(substitutedCondition.condition, effect)
|
return ConditionalEffect(substitutedCondition.condition, effect)
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -16,7 +16,6 @@
|
|||||||
|
|
||||||
package org.jetbrains.kotlin.contracts.model.structure
|
package org.jetbrains.kotlin.contracts.model.structure
|
||||||
|
|
||||||
import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
|
|
||||||
import org.jetbrains.kotlin.contracts.description.InvocationKind
|
import org.jetbrains.kotlin.contracts.description.InvocationKind
|
||||||
import org.jetbrains.kotlin.contracts.model.ESEffect
|
import org.jetbrains.kotlin.contracts.model.ESEffect
|
||||||
import org.jetbrains.kotlin.contracts.model.ESValue
|
import org.jetbrains.kotlin.contracts.model.ESValue
|
||||||
@@ -40,7 +39,7 @@ data class ESReturns(val value: ESValue) : SimpleEffect() {
|
|||||||
if (this.value !is ESConstant || other.value !is ESConstant) return this.value == other.value
|
if (this.value !is ESConstant || other.value !is ESConstant) return this.value == other.value
|
||||||
|
|
||||||
// ESReturns(x) implies ESReturns(?) for any 'x'
|
// ESReturns(x) implies ESReturns(?) for any 'x'
|
||||||
if (other.value.constantReference == ConstantReference.WILDCARD) return true
|
if (other.value.isWildcard) return true
|
||||||
|
|
||||||
return value == other.value
|
return value == other.value
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -17,11 +17,12 @@
|
|||||||
package org.jetbrains.kotlin.contracts.model.structure
|
package org.jetbrains.kotlin.contracts.model.structure
|
||||||
|
|
||||||
import org.jetbrains.kotlin.builtins.DefaultBuiltIns
|
import org.jetbrains.kotlin.builtins.DefaultBuiltIns
|
||||||
import org.jetbrains.kotlin.descriptors.ValueDescriptor
|
|
||||||
import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
|
|
||||||
import org.jetbrains.kotlin.contracts.description.expressions.BooleanConstantReference
|
import org.jetbrains.kotlin.contracts.description.expressions.BooleanConstantReference
|
||||||
|
import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
|
||||||
|
import org.jetbrains.kotlin.contracts.model.ESExpression
|
||||||
import org.jetbrains.kotlin.contracts.model.ESExpressionVisitor
|
import org.jetbrains.kotlin.contracts.model.ESExpressionVisitor
|
||||||
import org.jetbrains.kotlin.contracts.model.ESValue
|
import org.jetbrains.kotlin.contracts.model.ESValue
|
||||||
|
import org.jetbrains.kotlin.descriptors.ValueDescriptor
|
||||||
import org.jetbrains.kotlin.types.KotlinType
|
import org.jetbrains.kotlin.types.KotlinType
|
||||||
import org.jetbrains.kotlin.types.typeUtil.makeNullable
|
import org.jetbrains.kotlin.types.typeUtil.makeNullable
|
||||||
import java.util.*
|
import java.util.*
|
||||||
@@ -75,3 +76,12 @@ open class ESConstant private constructor(open val constantReference: ConstantRe
|
|||||||
}
|
}
|
||||||
|
|
||||||
fun Boolean.lift(): ESConstant = if (this) ESConstant.TRUE else ESConstant.FALSE
|
fun Boolean.lift(): ESConstant = if (this) ESConstant.TRUE else ESConstant.FALSE
|
||||||
|
|
||||||
|
internal val ESExpression.isTrue: Boolean
|
||||||
|
get() = this is ESConstant && constantReference == BooleanConstantReference.TRUE
|
||||||
|
|
||||||
|
internal val ESExpression.isFalse: Boolean
|
||||||
|
get() = this is ESConstant && constantReference == BooleanConstantReference.FALSE
|
||||||
|
|
||||||
|
internal val ESValue.isWildcard: Boolean
|
||||||
|
get() = this is ESConstant && constantReference == ConstantReference.WILDCARD
|
||||||
|
|||||||
@@ -36,10 +36,10 @@ class Reducer : ESExpressionVisitor<ESExpression?> {
|
|||||||
val reducedCondition = effect.condition.accept(this) ?: return null
|
val reducedCondition = effect.condition.accept(this) ?: return null
|
||||||
|
|
||||||
// Filter never executed conditions
|
// Filter never executed conditions
|
||||||
if (reducedCondition is ESConstant && reducedCondition == ESConstant.FALSE) return null
|
if (reducedCondition.isFalse) return null
|
||||||
|
|
||||||
// Add always firing effects
|
// Add always firing effects
|
||||||
if (reducedCondition is ESConstant && reducedCondition == ESConstant.TRUE) return effect.simpleEffect
|
if (reducedCondition.isTrue) return effect.simpleEffect
|
||||||
|
|
||||||
// Leave everything else as is
|
// Leave everything else as is
|
||||||
return effect
|
return effect
|
||||||
@@ -76,9 +76,9 @@ class Reducer : ESExpressionVisitor<ESExpression?> {
|
|||||||
val reducedRight = and.right.accept(this) ?: return null
|
val reducedRight = and.right.accept(this) ?: return null
|
||||||
|
|
||||||
return when {
|
return when {
|
||||||
reducedLeft == false.lift() || reducedRight == false.lift() -> false.lift()
|
reducedLeft.isFalse || reducedRight.isFalse -> reducedLeft
|
||||||
reducedLeft == true.lift() -> reducedRight
|
reducedLeft.isTrue -> reducedRight
|
||||||
reducedRight == true.lift() -> reducedLeft
|
reducedRight.isTrue -> reducedLeft
|
||||||
else -> ESAnd(reducedLeft, reducedRight)
|
else -> ESAnd(reducedLeft, reducedRight)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -88,9 +88,9 @@ class Reducer : ESExpressionVisitor<ESExpression?> {
|
|||||||
val reducedRight = or.right.accept(this) ?: return null
|
val reducedRight = or.right.accept(this) ?: return null
|
||||||
|
|
||||||
return when {
|
return when {
|
||||||
reducedLeft == true.lift() || reducedRight == true.lift() -> true.lift()
|
reducedLeft.isTrue || reducedRight.isTrue -> reducedLeft
|
||||||
reducedLeft == false.lift() -> reducedRight
|
reducedLeft.isFalse -> reducedRight
|
||||||
reducedRight == false.lift() -> reducedLeft
|
reducedRight.isFalse -> reducedLeft
|
||||||
else -> ESOr(reducedLeft, reducedRight)
|
else -> ESOr(reducedLeft, reducedRight)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
Reference in New Issue
Block a user