edu.mit.csail.sdg.alloy4compiler.ast
Class Type

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.Type

All Implemented Interfaces:

java.lang.Iterable<Type.ProductType>

public final class Type
extends java.lang.Object
implements java.lang.Iterable<Type.ProductType>

Immutable; represents the type of an expression.

Invariant: all x:entries | x.arity()>0

Note: except for "toString()" and "fold()", the return value of every method is always valid for all time; for example, given types A and B, and you call C=A.intersect(B), then the result C will always be the intersection of A and B even if the caller later constructs more sigs or subsigs or subsetsigs...

Nested Class Summary

static class

Type.ProductType Immutable; represents a list of PrimSig objects.

Field Summary

static Type	EMPTY Constant value with is_int==false, is_bool==false, and entries.size()==0.
static Type	FORMULA Constant value with is_int==false, is_bool==true, and entries.size()==0.
static Type	INTANDFORMULA Constant value with is_int==true, is_bool==true, and entries.size()==0.
boolean	is_bool True if primitive boolean value is a possible value in this type.

Method Summary

int	arity() If every entry has the same arity, that arity is returned; else if some entries have different arities, we return -1; else we return 0 (which only happens when there are no entries at all).
boolean	canOverride(Type that) Returns true if exists some A in this, some B in that, where (A.arity==B.arity, and A[0]&B[0]!=empty)
Type	closure() Returns a new type u + u.u + u.u.u + ...
Type	domainRestrict(Type that) Returns a new type { R[0]->..->R[n-1] | exists n-ary A in this, exists unary B in that, such that R[i]==A[i] except R[0]==(A[0] & B)
boolean	equals(java.lang.Object that) Returns true iff ((this subsumes that) and (that subsumes this))
Type	extract(int arity) Returns a new type { A | (A in this) and (A.arity == arity) }
boolean	firstColumnOverlaps(Type that) Returns true if exists some A in this, some B in that, where (A[0]&B[0]!=empty)
java.util.List<java.util.List<Sig.PrimSig>>	fold() Return the result of folding this Type (that is, whenever a subset of relations are identical except for 1 position, where together they comprise of all direct subsigs of an abstract sig, then we merge them)
boolean	hasArity(int arity) Returns true iff this contains an entry of the given arity.
boolean	hasCommonArity(Type that) Returns true iff exists some A in this, some B in that, where A.arity==B.arity
int	hashCode() Returns a hash code consistent with equals()
boolean	hasNoTuple() Returns true if this.size()==0 or every entry consists only of NONE.
boolean	hasTuple() Returns true if this.size()>0 and at least one entry consists of something other than NONE.
Type	intersect(Type.ProductType that) Returns a new type { A&that | A is in this }
Type	intersect(Type that) Returns a new type { A&B | A is in this, and B is in that }
boolean	intersects(Type that) Returns true iff { A&B | A is in this, and B is in that } can have tuples.
boolean	is_int()
boolean	is_small_int()
boolean	isSubtypeOf(Type that) Returns true if for all A in this, there exists B in that, where A is equal or subset of B.
java.util.Iterator<Type.ProductType>	iterator() Returns an iterator that iterates over the ProductType entries in this type.
Type	join(Type that) Returns a new type { A.B | exists A in this, exists B in that, where A.arity+B.arity>2 }
Type	merge(java.util.List<Sig.PrimSig> that) Returns a new type { A | A is in this, or A == that }
Type	merge(Type.ProductType that) Returns a new type { A | A is in this, or A == that }
Type	merge(Type.ProductType that, int begin, int end) Returns a new type { A | A is in this, or A == that.subList(begin,end) }
Type	merge(Type that) Returns a new type { A | A is in this, or A is in that }
Type	pickBinary() Returns a new type { A in this | A.artiy==2 }
Type	pickCommonArity(Type that) Returns a new type { A | (A is in this && A.arity in that) }
Type	pickUnary() Returns a new type { A in this | A.artiy==1 }
Type	product(Type that) Returns a new type { A->B | A is in this, and B is in that }
Type	rangeRestrict(Type that) Returns a new type { R[0]->..->R[n-1] | exists n-ary A in this, exists unary B in that, such that R[i]==A[i] except R[n-1]==(A[n-1] & B)
static Type	removesBoolAndInt(Type old) Create a new type that is the same as "old", except the "is_bool" and "is_int" flags are both set to false.
int	size() Returns the number of ProductType entries in this type.
static Type	smallIntType()
Expr	toExpr() Convert this type into a UNION of PRODUCT of sigs.
java.lang.String	toString() Returns a human-readable description of this type.
Type	transpose() Returns a new type { A | A is binary and ~A is in this }
Type	unionWithCommonArity(Type that) Returns a new type { A | (A is in this && A.arity in that) or (A is in that && A.arity in this) }

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

EMPTY

public static final Type EMPTY

Constant value with is_int==false, is_bool==false, and entries.size()==0.

FORMULA

public static final Type FORMULA

Constant value with is_int==false, is_bool==true, and entries.size()==0.

INTANDFORMULA

public static final Type INTANDFORMULA

Constant value with is_int==true, is_bool==true, and entries.size()==0.

is_bool

public final boolean is_bool

True if primitive boolean value is a possible value in this type.

Method Detail

is_int

public boolean is_int()

is_small_int

public boolean is_small_int()

smallIntType

public static Type smallIntType()

iterator

public java.util.Iterator<Type.ProductType> iterator()

Returns an iterator that iterates over the ProductType entries in this type.

This iterator will reject all modification requests.

Specified by:

iterator in interface java.lang.Iterable<Type.ProductType>

removesBoolAndInt

public static Type removesBoolAndInt(Type old)

Create a new type that is the same as "old", except the "is_bool" and "is_int" flags are both set to false.

equals

public boolean equals(java.lang.Object that)

Returns true iff ((this subsumes that) and (that subsumes this))

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Returns a hash code consistent with equals()

Overrides:

hashCode in class java.lang.Object

hasNoTuple

public boolean hasNoTuple()

Returns true if this.size()==0 or every entry consists only of NONE.

hasTuple

public boolean hasTuple()

Returns true if this.size()>0 and at least one entry consists of something other than NONE.

size

public int size()

Returns the number of ProductType entries in this type.

hasArity

public boolean hasArity(int arity)

Returns true iff this contains an entry of the given arity.

arity

public int arity()

If every entry has the same arity, that arity is returned;
else if some entries have different arities, we return -1;
else we return 0 (which only happens when there are no entries at all).

firstColumnOverlaps

public boolean firstColumnOverlaps(Type that)

Returns true if exists some A in this, some B in that, where (A[0]&B[0]!=empty)

This method ignores the "is_int" and "is_bool" flags.

canOverride

public boolean canOverride(Type that)

Returns true if exists some A in this, some B in that, where (A.arity==B.arity, and A[0]&B[0]!=empty)

This method ignores the "is_int" and "is_bool" flags.

hasCommonArity

public boolean hasCommonArity(Type that)

Returns true iff exists some A in this, some B in that, where A.arity==B.arity

product

public Type product(Type that)

Returns a new type { A->B | A is in this, and B is in that }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or that.size()==0, then result.size()==0

intersects

public boolean intersects(Type that)

Returns true iff { A&B | A is in this, and B is in that } can have tuples.

intersect

public Type intersect(Type that)

Returns a new type { A&B | A is in this, and B is in that }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or that.size()==0, or they do not have entries with same arity, then result.size()==0

intersect

public Type intersect(Type.ProductType that)

Returns a new type { A&that | A is in this }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If (this.size()==0), or (that.arity is not in this), then result.size()==0

merge

public Type merge(Type that)

Returns a new type { A | A is in this, or A is in that }

ReturnValue.is_int == this.is_int || that.is_int
ReturnValue.is_bool == this.is_bool || that.is_bool

If this.size()==0 and that.size()==0, then result.size()==0

As a special guarantee: if that==null, then the merge() method just returns the current object

merge

public Type merge(Type.ProductType that)

Returns a new type { A | A is in this, or A == that }

ReturnValue.is_int == this.is_int
ReturnValue.is_bool == this.is_bool

merge

public Type merge(Type.ProductType that,
                  int begin,
                  int end)

Returns a new type { A | A is in this, or A == that.subList(begin,end) }

ReturnValue.is_int == this.is_int
ReturnValue.is_bool == this.is_bool

merge

public Type merge(java.util.List<Sig.PrimSig> that)

Returns a new type { A | A is in this, or A == that }

ReturnValue.is_int == this.is_int
ReturnValue.is_bool == this.is_bool

unionWithCommonArity

public Type unionWithCommonArity(Type that)

Returns a new type { A | (A is in this && A.arity in that) or (A is in that && A.arity in this) }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0 or that.size()==0, then result.size()==0

Special promise: if the result would be identical to this, then we will return "this" as-is, without constructing a new object

pickCommonArity

public Type pickCommonArity(Type that)

Returns a new type { A | (A is in this && A.arity in that) }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0 or that.size()==0, then result.size()==0

pickUnary

public Type pickUnary()

Returns a new type { A in this | A.artiy==1 }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or does not contain any ProductType entries of the given arity, then result.size()==0

pickBinary

public Type pickBinary()

Returns a new type { A in this | A.artiy==2 }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or does not contain any ProductType entries of the given arity, then result.size()==0

transpose

public Type transpose()

Returns a new type { A | A is binary and ~A is in this }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or does not contain any binary ProductType entries, then result.size()==0

isSubtypeOf

public boolean isSubtypeOf(Type that)

Returns true if for all A in this, there exists B in that, where A is equal or subset of B.

Note: if this.is_int && !that.is_int, we return false immediately.

Note: if this.is_bool && !that.is_bool, we return false immediately.

Note: if this nothing above is violated, and this type has no relational entry in it, we return true.

join

public Type join(Type that)

Returns a new type { A.B | exists A in this, exists B in that, where A.arity+B.arity>2 }

If this.size()==0, or that.size()==0, or none of the entries have the right arity, then result.size()==0.

ReturnValue.is_int == false
ReturnValue.is_bool == false

domainRestrict

public Type domainRestrict(Type that)

Returns a new type { R[0]->..->R[n-1] | exists n-ary A in this, exists unary B in that, such that R[i]==A[i] except R[0]==(A[0] & B)

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or that does not contain any unary entry, then result.size()==0

rangeRestrict

public Type rangeRestrict(Type that)

Returns a new type { R[0]->..->R[n-1] | exists n-ary A in this, exists unary B in that, such that R[i]==A[i] except R[n-1]==(A[n-1] & B)

ReturnValue.is_int == false
ReturnValue.is_bool == false

If this.size()==0, or that does not contain any unary entry, then result.size()==0

extract

public Type extract(int arity)

Returns a new type { A | (A in this) and (A.arity == arity) }

ReturnValue.is_int == false
ReturnValue.is_bool == false

If it does not contain any entry with the given arity, then result.size()==0

closure

public Type closure()

Returns a new type u + u.u + u.u.u + ... (where u == the set of binary entries in this type)

ReturnValue.is_int == false
ReturnValue.is_bool == false

If it does not contain any binary entries, then result.size()==0

toExpr

public Expr toExpr()
            throws Err

Convert this type into a UNION of PRODUCT of sigs.

Throws:

ErrorType - if it does not contain exactly one arity

ErrorType - if is_int is true

ErrorType - if is_bool is true

Err

fold

public java.util.List<java.util.List<Sig.PrimSig>> fold()

Return the result of folding this Type (that is, whenever a subset of relations are identical except for 1 position, where together they comprise of all direct subsigs of an abstract sig, then we merge them)

Note: the result is only current with respect to the current existing sig objects

toString

public java.lang.String toString()

Returns a human-readable description of this type.

Overrides:

toString in class java.lang.Object