wyil.util.type

Class SubtypeOperator

java.lang.Object

wyil.util.type.SubtypeOperator

Direct Known Subclasses:

ExplicitCoercionOperator

public class SubtypeOperator
extends Object

The subtype operator implements the algorithm for determining whether or not one type is a subtype of another. For the most part, one can take subtype to mean subset (this analogy breaks down with function types, however). Following this analogy, T1 is a subtype of T2 (denoted T1 <: T2) if the set of values represented by T1 is a subset of those represented by T2.

The algorithm actually operates by computing the intersection relation for two types (i.e. whether or not an intersection exists between their set of values). Subtyping is closely related to intersection and, in fact, we have that T1 :> T2 iff !(!T1 & T2) (where & is the intersection relation). The choice to compute intersections, rather than subtypes, was for simplicity. Namely, it was considered conceptually easier to think about intersections rather than subtypes.

NOTE: for this algorithm to return correct results in all cases, both types must have been normalised first.

References

• David J. Pearce and James Noble. Structural and Flow-Sensitive Types for Whiley. Technical Report, Victoria University of Wellington, 2010.

• A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping. In Proceedings of the Symposium on Logic in Computer Science, pages 137--146. IEEE Computer Society Press, 2002.

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In Proceedings of the ACM Conference on Principles of Programming Languages, pages 419--428, 1993.

• Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15:575--631, 1993.

Author:

David J. Pearce

Field Summary

Fields

Modifier and Type	Field and Description
protected Automaton	from
protected Automaton	to

Constructor Summary

Constructors

Constructor and Description
SubtypeOperator(Automaton from, Automaton to, LifetimeRelation lr)

Method Summary

Modifier and Type	Method and Description
protected boolean	intersectRecords(int fromIndex, boolean fromSign, int toIndex, boolean toSign) Check for intersection between two states with kind K_RECORD.
protected boolean	isIntersection(int fromIndex, boolean fromSign, int toIndex, boolean toSign) Determine whether there is a non-empty intersection between the state rooted at fromIndex and that rooted at toIndex.
protected boolean	isIntersectionInner(int fromIndex, boolean fromSign, int toIndex, boolean toSign)
boolean	isSubtype(int fromIndex, int toIndex) Test whether from :> to
boolean	isSupertype(int fromIndex, int toIndex) Test whether from <: to

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

from

protected final Automaton from

to

protected final Automaton to

Constructor Detail

SubtypeOperator

public SubtypeOperator(Automaton from,
                       Automaton to,
                       LifetimeRelation lr)

Method Detail

isSubtype

public final boolean isSubtype(int fromIndex,
                               int toIndex)

Test whether from :> to

Parameters:

fromIndex -

toIndex -

Returns:

isSupertype

public final boolean isSupertype(int fromIndex,
                                 int toIndex)

Test whether from <: to

Parameters:

fromIndex -

toIndex -

Returns:

isIntersection

protected boolean isIntersection(int fromIndex,
                                 boolean fromSign,
                                 int toIndex,
                                 boolean toSign)

Determine whether there is a non-empty intersection between the state rooted at fromIndex and that rooted at toIndex. The signs indicate whether or not the state should be taken as its inverse.

Parameters:

fromIndex - --- index of from state

fromSign - --- sign of from state (true = normal, false = inverted).

toIndex - --- index of to state

toSign - --- sign of from state (true = normal, false = inverted).

Returns:

--- true if such an intersection exists, false otherwise.

isIntersectionInner

protected boolean isIntersectionInner(int fromIndex,
                                      boolean fromSign,
                                      int toIndex,
                                      boolean toSign)

intersectRecords

protected boolean intersectRecords(int fromIndex,
                                   boolean fromSign,
                                   int toIndex,
                                   boolean toSign)

Check for intersection between two states with kind K_RECORD. The distinction between open and closed records adds complexity here.

Intersection between closed records is the easiest case. The main examples are:

• {T1 f, T2 g} & {T3 f, T4 g} = if T1&T3 and T2&T4.
• {T1 f, T2 g} & {T3 f, T4 h} = false.
• {T1 f, T2 g} & !{T3 f, T4 g} = if T1&!T3 or T2&!T4.
• {T1 f, T2 g} & !{T3 f} = false.
• !{T1 f} & !{T2 f} = true.

Intersection between a closed and open record is similar. The main examples are:

• {T1 f, T2 g, ...} & {T3 f, T4 g} = if T1&T3 and T2&T4.
• {T1 f, ...} & {T2 f, T3 g} = if T1&T2.
• {T1 f, T2 g, ...} & {T3 f, T4 h} = false.
• {T1 f, T2 g, ...} & !{T3 f, T4 g} = if T1&!T3 or T2&!T4.
*
• !{T1 f, T2 g, ...} & {T3 f, T4 g} = if T1&!T3 or T2&!T4.
*
• {T1 f, ...} & !{T2 f, T3 g} = true.
• {T1 f, T2 g, ...} & !{T3 f, T4 h} = false.
• !{T1 f,...} & !{T2 f} = true.

Parameters:

fromIndex - --- index of from state

fromSign - --- sign of from state (true = normal, false = inverted).

toIndex - --- index of to state

toSign - --- sign of from state (true = normal, false = inverted).

Returns:

--- true if such an intersection exists, false otherwise.