wyil.util

Class TypeSystem

java.lang.Object

wyil.util.TypeSystem

public class TypeSystem
extends Object

The type system is responsible for managing the relationship between nominal types and their underlying types. Every visible type has an underlying type associated with it which, in some cases, will be the same. For example, the underlying type associated with type int is simply int. However, in many cases, there is a difference. For example:

 type nat is (int x) where x >= 0
 

In this case, the underlying type associated with the type nat is int. This class provides a way to determine the underlying type associated with a given type.

NOTE: in principle, this could cache expanded types for performance reasons (though it currently does not).

Author:

David J. Pearce

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	TypeSystem.FunctionOrMethodState
static class	TypeSystem.RecordState

Field Summary

Fields

Modifier and Type	Field and Description
static byte	K_ANY
static byte	K_ARRAY
static byte	K_BOOL
static byte	K_BYTE
static byte	K_FUNCTION
static byte	K_INT
static int	K_INTERSECTION
static byte	K_META
static byte	K_METHOD
static byte	K_NEGATION
static byte	K_NOMINAL
static byte	K_NULL
static byte	K_PROPERTY
static byte	K_RECORD
static byte	K_REFERENCE
static byte	K_UNION
static byte	K_VOID

Constructor Summary

Constructors

Constructor and Description
TypeSystem(wybs.lang.Build.Project project)

Method Summary

Modifier and Type	Method and Description
Type.EffectiveArray	expandAsEffectiveArray(Type type) Assuming given type is an effective array of some sort, expand to ensure array structure is visible.
Type.EffectiveRecord	expandAsEffectiveRecord(Type type) Assuming given type is an effective record of some sort, expand to ensure record structure is visible.
Type.FunctionOrMethod	expandAsFunctionOrMethod(Type type) Assuming given type is an effective function or method type of some sort, expand to ensure structure is visible.
Type.Reference	expandAsReference(Type type) Assuming given type is an effective reference of some sort, expand to ensure reference structure is visible.
Type	expandOneLevel(Type type) Expand a given syntactic type by exactly one level.
boolean	isContractive(Type type) Contractive types are types which cannot accept value because they have an unterminated cycle.
boolean	isEmpty(Type type) Determine whether or not this type corresponds to the empty type or not.
boolean	isExplicitCoerciveSubtype(Type t1, Type t2) Determine whether type t2 is an explicit coercive subtype of type t1.
boolean	isExplicitCoerciveSubtype(Type t1, Type t2, LifetimeRelation lr) Determine whether type t2 is an explicit coercive subtype of type t1.
boolean	isSubtype(Type t1, Type t2) Determine whether type t2 is a subtype of type t1 (written t1 :> t2).
boolean	isSubtype(Type t1, Type t2, LifetimeRelation lr) Determine whether type t2 is a subtype of type t1 (written t1 :> t2).
Automaton	toAutomaton(Type type) Expand a given type by inlining all visible nominal information.

Methods inherited from class java.lang.Object

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

Field Detail

K_VOID

public static final byte K_VOID

See Also:

Constant Field Values

K_ANY

public static final byte K_ANY

See Also:

Constant Field Values

K_META

public static final byte K_META

See Also:

Constant Field Values

K_NULL

public static final byte K_NULL

See Also:

Constant Field Values

K_BOOL

public static final byte K_BOOL

See Also:

Constant Field Values

K_BYTE

public static final byte K_BYTE

See Also:

Constant Field Values

K_INT

public static final byte K_INT

See Also:

Constant Field Values

K_ARRAY

public static final byte K_ARRAY

See Also:

Constant Field Values

K_REFERENCE

public static final byte K_REFERENCE

See Also:

Constant Field Values

K_RECORD

public static final byte K_RECORD

See Also:

Constant Field Values

K_UNION

public static final byte K_UNION

See Also:

Constant Field Values

K_INTERSECTION

public static final int K_INTERSECTION

See Also:

Constant Field Values

K_NEGATION

public static final byte K_NEGATION

See Also:

Constant Field Values

K_FUNCTION

public static final byte K_FUNCTION

See Also:

Constant Field Values

K_METHOD

public static final byte K_METHOD

See Also:

Constant Field Values

K_NOMINAL

public static final byte K_NOMINAL

See Also:

Constant Field Values

K_PROPERTY

public static final byte K_PROPERTY

See Also:

Constant Field Values

Constructor Detail

TypeSystem

public TypeSystem(wybs.lang.Build.Project project)

Method Detail

isEmpty

public boolean isEmpty(Type type)
                throws wybs.util.ResolveError

Determine whether or not this type corresponds to the empty type or not. This can happen in a number of ways.

Parameters:

type -

Returns:

Throws:

wybs.util.ResolveError

isContractive

public boolean isContractive(Type type)
                      throws wybs.util.ResolveError

Contractive types are types which cannot accept value because they have an unterminated cycle. An unterminated cycle has no leaf nodes terminating it. For example, X<{X field}> is contractive, where as X<{null|X field}> is not.

This method returns true if the type is contractive, or contains a contractive subcomponent. For example, null|X<{X field}> is considered contracted.

Parameters:

type - --- type to test for contractivity.

Returns:

Throws:

wybs.util.ResolveError

expandAsEffectiveRecord

public Type.EffectiveRecord expandAsEffectiveRecord(Type type)
                                             throws wybs.util.ResolveError

Assuming given type is an effective record of some sort, expand to ensure record structure is visible. For example a type myRecord would expanded one level to look like {T aField,...} for some (potentially nominal) element type T.

Parameters:

type - The type to be expanded

Returns:

null if given type is not an effective record

Throws:

wybs.util.ResolveError

expandAsEffectiveArray

public Type.EffectiveArray expandAsEffectiveArray(Type type)
                                           throws wybs.util.ResolveError

Assuming given type is an effective array of some sort, expand to ensure array structure is visible. For example a type myArray would expanded one level to look like T[] for some (potentially nominal) element type T.

Parameters:

type - The type to be expanded

Returns:

null if type is no an effective array

Throws:

wybs.util.ResolveError

expandAsReference

public Type.Reference expandAsReference(Type type)
                                 throws wybs.util.ResolveError

Assuming given type is an effective reference of some sort, expand to ensure reference structure is visible. For example a type myRef would expanded one level to look like &T for some (potentially nominal) element type T.

Parameters:

type - The type to be expanded

Returns:

Throws:

wybs.util.ResolveError

expandAsFunctionOrMethod

public Type.FunctionOrMethod expandAsFunctionOrMethod(Type type)
                                               throws wybs.util.ResolveError

Assuming given type is an effective function or method type of some sort, expand to ensure structure is visible.

Parameters:

type - The type to be expanded

Returns:

Throws:

wybs.util.ResolveError

isExplicitCoerciveSubtype

public boolean isExplicitCoerciveSubtype(Type t1,
                                         Type t2,
                                         LifetimeRelation lr)
                                  throws wybs.util.ResolveError

Determine whether type t2 is an explicit coercive subtype of type t1.

Throws:

wybs.util.ResolveError - If a named type within either of the operands cannot be resolved within the enclosing project.

isExplicitCoerciveSubtype

public boolean isExplicitCoerciveSubtype(Type t1,
                                         Type t2)
                                  throws wybs.util.ResolveError

Determine whether type t2 is an explicit coercive subtype of type t1.

Throws:

wybs.util.ResolveError - If a named type within either of the operands cannot be resolved within the enclosing project.

isSubtype

public boolean isSubtype(Type t1,
                         Type t2,
                         LifetimeRelation lr)
                  throws wybs.util.ResolveError

Determine whether type t2 is a subtype of type t1 (written t1 :> t2). In other words, whether the set of all possible values described by the type t2 is a subset of that described by t1.

Throws:

wybs.util.ResolveError - If a named type within either of the operands cannot be resolved within the enclosing project.

isSubtype

public boolean isSubtype(Type t1,
                         Type t2)
                  throws wybs.util.ResolveError

Determine whether type t2 is a subtype of type t1 (written t1 :> t2). In other words, whether the set of all possible values described by the type t2 is a subset of that described by t1.

Throws:

wybs.util.ResolveError - If a named type within either of the operands cannot be resolved within the enclosing project.

expandOneLevel

public Type expandOneLevel(Type type)
                    throws wybs.util.ResolveError

Expand a given syntactic type by exactly one level.

Parameters:

type -

Returns:

Throws:

IOException

wybs.util.ResolveError

toAutomaton

public Automaton toAutomaton(Type type)
                      throws wybs.util.ResolveError

Expand a given type by inlining all visible nominal information. For example:

 type nat is (int x) where x >= 0
 type listnat is [nat]
 

Expanding the type [nat] will result in the type [int]. The key challenge here lies in handling nominal types when they are encountered. We need to determine where the type is located, and then incorporate the (expanded) body of that type into this type. In some cases, we're not permitted to inline the body because it's not visible to this file (e.g. it is marked as private).

Parameters:

type -

Returns:

Throws:

wybs.util.ResolveError