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

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.Browsable
      edu.mit.csail.sdg.alloy4compiler.ast.Expr

Direct Known Subclasses:

ExprBad, ExprBadCall, ExprBadJoin, ExprBinary, ExprCall, ExprChoice, ExprConstant, ExprCustom, ExprHasName, ExprITE, ExprLet, ExprList, ExprQt, ExprUnary, Sig

public abstract class Expr
extends Browsable

Immutable; represents a formula or expression.

Invariant: pos!=null
Invariant: type!=null
Invariant: type==EMPTY iff errors.size()>0
Invariant: mult==0 || mult==1 || mult==2
Invariant: weight>0

Field Summary

boolean	ambiguous True if this expression is not fully resolved.
Pos	closingBracket The filename, line, and column position in the original Alloy model file of the closing bracket).
JoinableList<Err>	errors The list of errors on this node; nonempty iff this.type==EMPTY
int	mult This field records whether the node is a multiplicity constraint.
Pos	pos The filename, line, and column position in the original Alloy model file (cannot be null).
long	weight Each leaf Expr has a weight value (which can be 0 or higher); by default, each nonleaf Expr's weight is the sum of its children's weights.

Method Summary

Expr	and(Expr x) Returns the formula (this and x)
Expr	any_arrow_lone(Expr x) Returns the multiplicity constraint (this set->lone x)
Expr	any_arrow_one(Expr x) Returns the multiplicity constraint (this set->one x)
Expr	any_arrow_some(Expr x) Returns the multiplicity constraint (this set->some x)
Expr	cardinality() Returns the integer expression (#this) truncated to the current integer bitwidth.
Expr	cast2int() Returns the integer expression "int[this]"
Expr	cast2sigint() Returns the singleton set "Int[this]"
Expr	closure() Returns the expression (^this)
Expr	comprehensionOver(Decl firstDecl, Decl... moreDecls) Returns the comprehension expression {...|this}
Expr	deNOP() Remove the "NOP" in front of an expression (if any).
Expr	div(Expr x) Returns the formula "this.div[x]" (the quotient of dividing this by x)
Expr	domain(Expr x) Returns the expression (this <: x)
Expr	equal(Expr x) Returns the formula (this==x)
boolean	equals(java.lang.Object other)
java.lang.Iterable<Func>	findAllFunctions() Transitively returns a set that contains all predicates/functions that this expression calls directly or indirectly.
Expr	forAll(Decl firstDecl, Decl... moreDecls) Returns the formula (all...| this)
Expr	forLone(Decl firstDecl, Decl... moreDecls) Returns the formula (lone...| this)
Expr	forNo(Decl firstDecl, Decl... moreDecls) Returns the formula (no...| this)
Expr	forOne(Decl firstDecl, Decl... moreDecls) Returns the formula (one ...| this)
Expr	forSome(Decl firstDecl, Decl... moreDecls) Returns the formula (some...| this)
abstract int	getDepth() Returns the height of the abstract syntax tree starting from this node.
Expr	gt(Expr x) Returns the formula (this > x)
Expr	gte(Expr x) Returns the formula (this >= x)
int	hashCode()
boolean	hasVar(ExprVar goal) Returns true if the node is well-typed, unambiguous, and contains the given variable.
Expr	iff(Expr x) Returns the formula (this iff x)
Expr	iminus(Expr x)
Expr	implies(Expr x) Returns the formula (this implies x)
Expr	in(Expr x) Returns the formula (this in x)
Expr	intersect(Expr x) Returns the expression (this intersects x)
Expr	iplus(Expr x)
boolean	isSame(Expr obj) Returns true if we can determine the two expressions are equivalent; may sometimes return false.
Expr	isSeq_arrow_lone(Expr x) Returns the multiplicity constraint (this isSeq->lone x)
Expr	ite(Expr x, Expr y) Returns the expression/integer/formula (this => x else y)
Expr	join(Expr x) Returns the expression (this.x)
Expr	lone_arrow_any(Expr x) Returns the multiplicity constraint (this lone->set x)
Expr	lone_arrow_lone(Expr x) Returns the multiplicity constraint (this lone->lone x)
Expr	lone_arrow_one(Expr x) Returns the multiplicity constraint (this lone->one x)
Expr	lone_arrow_some(Expr x) Returns the multiplicity constraint (this lone->some x)
Expr	lone() Returns the formula (lone this)
Expr	loneOf() Return the multiplicity expression "lone this"
Decl	loneOf(java.lang.String label) Return a new declaration "v: lone this"
Expr	lt(Expr x) Returns the formula (this < x)
Expr	lte(Expr x) Returns the formula (this <= x)
Expr	minus(Expr x) Returns the expression (this-x)
Expr	mul(Expr x) Returns the formula "this.mul[x]" (the result of multiplying this by x)
ExprUnary.Op	mult() If this is loneOf/oneOf/someOf/exactlyOf expression, return loneOf/oneOf/someOf/exactlyOf, otherwise returns setOf.
Expr	no() Returns the formula (no this)
Expr	not() Returns the formula (not this)
Expr	one_arrow_any(Expr x) Returns the multiplicity constraint (this one->set x)
Expr	one_arrow_lone(Expr x) Returns the multiplicity constraint (this one->lone x)
Expr	one_arrow_one(Expr x) Returns the multiplicity constraint (this one->one x)
Expr	one_arrow_some(Expr x) Returns the multiplicity constraint (this one->some x)
Expr	one() Returns the formula (one this)
Expr	oneOf() Return the multiplicity expression "one this"
Decl	oneOf(java.lang.String label) Return a new declaration "v: one this"
Expr	or(Expr x) Returns the formula (this or x)
Expr	override(Expr x) Returns the expression (this++x)
Expr	plus(Expr x) Returns the expression (this+x)
Pos	pos() Returns a Pos object representing the position of this Expr.
Expr	product(Expr x) Returns the expression (this -> x) which can also be regarded as a multiplicity constraint (this set->set x)
Expr	range(Expr x) Returns the expression (this :> x)
Expr	reflexiveClosure() Returns the expression (*this)
Expr	rem(Expr x) Returns the formula "this.rem[x]" (the remainder of dividing this by x)
Expr	resolve_as_formula(java.util.Collection<ErrorWarning> warnings) Converts this into a "formula" if possible, then resolves it if ambiguous.
Expr	resolve_as_int(java.util.Collection<ErrorWarning> warnings) Converts this into an "integer expression" if possible, then resolves it if ambiguous.
Expr	resolve_as_set(java.util.Collection<ErrorWarning> warnings) Converts this into a "set or relation" if possible, then resolves it if ambiguous.
abstract Expr	resolve(Type t, java.util.Collection<ErrorWarning> warnings) Resolves this expression if ambiguous.
Expr	setOf() Return the multiplicity expression "set this"
Decl	setOf(java.lang.String label) Return a new declaration "v: set this"
Expr	sha(Expr x) Returns the integer expression (this >> x)
Expr	shl(Expr x) Returns the integer expression (this << x)
Expr	shr(Expr x) Returns the integer expression (this >>> x)
Expr	some_arrow_any(Expr x) Returns the multiplicity constraint (this some->set x)
Expr	some_arrow_lone(Expr x) Returns the multiplicity constraint (this some->lone x)
Expr	some_arrow_one(Expr x) Returns the multiplicity constraint (this some->one x)
Expr	some_arrow_some(Expr x) Returns the multiplicity constraint (this some->some x)
Expr	some() Returns the formula (some this)
Expr	someOf() Return the multiplicity expression "some this"
Decl	someOf(java.lang.String label) Return a new declaration "v: some this"
Expr	sumOver(Decl firstDecl, Decl... moreDecls) Returns the integer (sum...| this)
java.lang.String	toString() Print a brief text description of it and all subnodes.
abstract void	toString(java.lang.StringBuilder out, int indent) Print a textual description of it and all subnodes to a StringBuilder, with the given level of indentation.
Expr	transpose() Returns the expression (~this)
Type	type() Return the type for this node; EMPTY if it is not well-typed.
Expr	typecheck_as_formula() Converts this into a "formula" if possible; otherwise, returns an Expr with a nonempty error list
Expr	typecheck_as_int() Converts this into an "integer expression" if possible; otherwise, returns an Expr with a nonempty error list
Expr	typecheck_as_set() Converts this into a "set or relation" if possible; otherwise, returns an Expr with a nonempty error list

Methods inherited from class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

getHTML, getSubnodes, make, make, make, make, showAsTree, span

Methods inherited from class java.lang.Object

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

Field Detail

pos

public final Pos pos

The filename, line, and column position in the original Alloy model file (cannot be null).

closingBracket

public final Pos closingBracket

The filename, line, and column position in the original Alloy model file of the closing bracket).

errors

public final JoinableList<Err> errors

The list of errors on this node; nonempty iff this.type==EMPTY

mult

public final int mult

This field records whether the node is a multiplicity constraint.
If it's 2, that means it is an arrow multiplicity constraint (X ?->? X), or has the form (A -> B) where A and/or B is an arrow multiplicity constraint.
If it's 1, that means it is a multiplicity constraint of the form (? X)
If it's 0, that means it does not have either form.

weight

public final long weight

Each leaf Expr has a weight value (which can be 0 or higher); by default, each nonleaf Expr's weight is the sum of its children's weights.

ambiguous

public final boolean ambiguous

True if this expression is not fully resolved.

Method Detail

type

public final Type type()

Return the type for this node; EMPTY if it is not well-typed.

pos

public final Pos pos()

Returns a Pos object representing the position of this Expr.

Overrides:

pos in class Browsable

toString

public abstract void toString(java.lang.StringBuilder out,
                              int indent)

Print a textual description of it and all subnodes to a StringBuilder, with the given level of indentation. (If indent<0, it will be printed in one line without line break)

toString

public java.lang.String toString()

Print a brief text description of it and all subnodes.

Overrides:

toString in class java.lang.Object

hashCode

public final int hashCode()

Overrides:

hashCode in class java.lang.Object

equals

public final boolean equals(java.lang.Object other)

Overrides:

equals in class java.lang.Object

typecheck_as_formula

public final Expr typecheck_as_formula()

Converts this into a "formula" if possible; otherwise, returns an Expr with a nonempty error list

typecheck_as_int

public final Expr typecheck_as_int()

Converts this into an "integer expression" if possible; otherwise, returns an Expr with a nonempty error list

typecheck_as_set

public final Expr typecheck_as_set()

Converts this into a "set or relation" if possible; otherwise, returns an Expr with a nonempty error list

resolve

public abstract Expr resolve(Type t,
                             java.util.Collection<ErrorWarning> warnings)

Resolves this expression if ambiguous. (And if t.size()>0, it represents the set of tuples whose presence/absence is relevent to the parent expression) (Note: it's possible for t to be EMPTY, or even ambiguous!)

On success: the return value will be well-typed and unambiguous

On failure: the return value's "errors" list will be nonempty

If we detect any type warnings, we will add the type warnings to the "warnings" collection.

Parameters:

warnings - - the list that will receive any warning we generate; can be null if we wish to ignore warnings

resolve_as_formula

public final Expr resolve_as_formula(java.util.Collection<ErrorWarning> warnings)

Converts this into a "formula" if possible, then resolves it if ambiguous.

On success: the return value will be a well-typed unambiguous formula expression

On failure: the return value's "errors" list will be nonempty

If we detect any type warnings, we will add the type warnings to the "warnings" collection.

Parameters:

warnings - - the list that will receive any warning we generate; can be null if we wish to ignore warnings

resolve_as_int

public final Expr resolve_as_int(java.util.Collection<ErrorWarning> warnings)

Converts this into an "integer expression" if possible, then resolves it if ambiguous.

On success: the return value will be a well-typed unambiguous integer expression

On failure: the return value's "errors" list will be nonempty

If we detect any type warnings, we will add the type warnings to the "warnings" collection.

Parameters:

warnings - - the list that will receive any warning we generate; can be null if we wish to ignore warnings

resolve_as_set

public final Expr resolve_as_set(java.util.Collection<ErrorWarning> warnings)

Converts this into a "set or relation" if possible, then resolves it if ambiguous.

On success: the return value will be a well-typed unambiguous set or relation expression

On failure: the return value's "errors" list will be nonempty

If we detect any type warnings, we will add the type warnings to the "warnings" collection.

Parameters:

warnings - - the list that will receive any warning we generate; can be null if we wish to ignore warnings

isSame

public boolean isSame(Expr obj)

Returns true if we can determine the two expressions are equivalent; may sometimes return false.

deNOP

public final Expr deNOP()

Remove the "NOP" in front of an expression (if any).

mult

public final ExprUnary.Op mult()

If this is loneOf/oneOf/someOf/exactlyOf expression, return loneOf/oneOf/someOf/exactlyOf, otherwise returns setOf.

hasVar

public final boolean hasVar(ExprVar goal)

Returns true if the node is well-typed, unambiguous, and contains the given variable.

findAllFunctions

public final java.lang.Iterable<Func> findAllFunctions()

Transitively returns a set that contains all predicates/functions that this expression calls directly or indirectly.

getDepth

public abstract int getDepth()

Returns the height of the abstract syntax tree starting from this node.

and

public final Expr and(Expr x)

Returns the formula (this and x)

this and x must both be formulas

Note: as a special guarantee, if x==null, then the method will return this Expr object as-is.

or

public final Expr or(Expr x)

Returns the formula (this or x)

this and x must both be formulas

Note: as a special guarantee, if x==null, then the method will return this Expr object as-is.

iff

public final Expr iff(Expr x)

Returns the formula (this iff x)

this and x must both be formulas

implies

public final Expr implies(Expr x)

Returns the formula (this implies x)

this and x must both be formulas

join

public final Expr join(Expr x)

Returns the expression (this.x)

1. this must be a set or relation

2. x must be a set or relation

3. at most one of them can be a unary set

domain

public final Expr domain(Expr x)

Returns the expression (this <: x)

this must be a unary set

x must be a set or relation

range

public final Expr range(Expr x)

Returns the expression (this :> x)

this must be a set or relation

x must be a unary set

intersect

public final Expr intersect(Expr x)

Returns the expression (this intersects x)

this and x must be expressions with the same arity

override

public final Expr override(Expr x)

Returns the expression (this++x)

this and x must be expressions with the same arity

plus

public final Expr plus(Expr x)

Returns the expression (this+x)

this and x must be expressions with the same arity, or both be integer expressions

Note: as a special guarantee, if x==null, then the method will return this Expr object as-is.

iplus

public final Expr iplus(Expr x)

minus

public final Expr minus(Expr x)

Returns the expression (this-x)

this and x must be expressions with the same arity, or both be integer expressions

iminus

public final Expr iminus(Expr x)

mul

public final Expr mul(Expr x)

Returns the formula "this.mul[x]" (the result of multiplying this by x)

this and x must both be integer expressions

div

public final Expr div(Expr x)

Returns the formula "this.div[x]" (the quotient of dividing this by x)

this and x must both be integer expressions

rem

public final Expr rem(Expr x)

Returns the formula "this.rem[x]" (the remainder of dividing this by x)

this and x must both be integer expressions

equal

public final Expr equal(Expr x)

Returns the formula (this==x)

this and x must be expressions with the same arity, or both be integer expressions

lt

public final Expr lt(Expr x)

Returns the formula (this < x)

this and x must both be integer expressions

lte

public final Expr lte(Expr x)

Returns the formula (this <= x)

this and x must both be integer expressions

gt

public final Expr gt(Expr x)

Returns the formula (this > x)

this and x must both be integer expressions

gte

public final Expr gte(Expr x)

Returns the formula (this >= x)

this and x must both be integer expressions

shl

public final Expr shl(Expr x)

Returns the integer expression (this << x)

this and x must both be integer expressions

shr

public final Expr shr(Expr x)

Returns the integer expression (this >>> x)

this and x must both be integer expressions

sha

public final Expr sha(Expr x)

Returns the integer expression (this >> x)

this and x must both be integer expressions

in

public final Expr in(Expr x)

Returns the formula (this in x)

this must be a set or relation

x must be a set or relation or multiplicity constraint

this and x must have the same arity

product

public final Expr product(Expr x)

Returns the expression (this -> x) which can also be regarded as a multiplicity constraint (this set->set x)

this must be a set or relation

x must be a set or relation

any_arrow_some

public final Expr any_arrow_some(Expr x)

Returns the multiplicity constraint (this set->some x)

this must be a set or relation

x must be a set or relation

any_arrow_one

public final Expr any_arrow_one(Expr x)

Returns the multiplicity constraint (this set->one x)

this must be a set or relation

x must be a set or relation

any_arrow_lone

public final Expr any_arrow_lone(Expr x)

Returns the multiplicity constraint (this set->lone x)

this must be a set or relation

x must be a set or relation

some_arrow_any

public final Expr some_arrow_any(Expr x)

Returns the multiplicity constraint (this some->set x)

this must be a set or relation

x must be a set or relation

some_arrow_some

public final Expr some_arrow_some(Expr x)

Returns the multiplicity constraint (this some->some x)

this must be a set or relation

x must be a set or relation

some_arrow_one

public final Expr some_arrow_one(Expr x)

Returns the multiplicity constraint (this some->one x)

this must be a set or relation

x must be a set or relation

some_arrow_lone

public final Expr some_arrow_lone(Expr x)

Returns the multiplicity constraint (this some->lone x)

this must be a set or relation

x must be a set or relation

one_arrow_any

public final Expr one_arrow_any(Expr x)

Returns the multiplicity constraint (this one->set x)

this must be a set or relation

x must be a set or relation

one_arrow_some

public final Expr one_arrow_some(Expr x)

Returns the multiplicity constraint (this one->some x)

this must be a set or relation

x must be a set or relation

one_arrow_one

public final Expr one_arrow_one(Expr x)

Returns the multiplicity constraint (this one->one x)

this must be a set or relation

x must be a set or relation

one_arrow_lone

public final Expr one_arrow_lone(Expr x)

Returns the multiplicity constraint (this one->lone x)

this must be a set or relation

x must be a set or relation

lone_arrow_any

public final Expr lone_arrow_any(Expr x)

Returns the multiplicity constraint (this lone->set x)

this must be a set or relation

x must be a set or relation

lone_arrow_some

public final Expr lone_arrow_some(Expr x)

Returns the multiplicity constraint (this lone->some x)

this must be a set or relation

x must be a set or relation

lone_arrow_one

public final Expr lone_arrow_one(Expr x)

Returns the multiplicity constraint (this lone->one x)

this must be a set or relation

x must be a set or relation

lone_arrow_lone

public final Expr lone_arrow_lone(Expr x)

Returns the multiplicity constraint (this lone->lone x)

this must be a set or relation

x must be a set or relation

isSeq_arrow_lone

public final Expr isSeq_arrow_lone(Expr x)

Returns the multiplicity constraint (this isSeq->lone x)

this must be a set or relation

x must be a set or relation

ite

public final Expr ite(Expr x,
                      Expr y)

Returns the expression/integer/formula (this => x else y)

this must be a formula

x and y must both be expressions of the same arity, or both be integer expressions, or both be formulas

forAll

public final Expr forAll(Decl firstDecl,
                         Decl... moreDecls)
                  throws Err

Returns the formula (all...| this)

this must be a formula

Throws:

Err

forNo

public final Expr forNo(Decl firstDecl,
                        Decl... moreDecls)
                 throws Err

Returns the formula (no...| this)

this must be a formula

Throws:

Err

forLone

public final Expr forLone(Decl firstDecl,
                          Decl... moreDecls)
                   throws Err

Returns the formula (lone...| this)

this must be a formula

Throws:

Err

forOne

public final Expr forOne(Decl firstDecl,
                         Decl... moreDecls)
                  throws Err

Returns the formula (one ...| this)

this must be a formula

Throws:

Err

forSome

public final Expr forSome(Decl firstDecl,
                          Decl... moreDecls)
                   throws Err

Returns the formula (some...| this)

this must be a formula

Throws:

Err

comprehensionOver

public final Expr comprehensionOver(Decl firstDecl,
                                    Decl... moreDecls)
                             throws Err

Returns the comprehension expression {...|this}

this must be a formula

each declaration must be a "one-of" quantification over a unary set

Throws:

Err

sumOver

public final Expr sumOver(Decl firstDecl,
                          Decl... moreDecls)
                   throws Err

Returns the integer (sum...| this)

this must be an integer expression

each declaration must be a "one-of" quantification over a unary set

Throws:

Err

someOf

public final Expr someOf()

Return the multiplicity expression "some this"

this must be already fully typechecked, and must be a unary set

someOf

public final Decl someOf(java.lang.String label)
                  throws Err

Return a new declaration "v: some this"

this must be already fully typechecked, and must be a unary set

the label is only used for pretty-printing, and does not have to be unique

Throws:

Err

loneOf

public final Expr loneOf()

Return the multiplicity expression "lone this"

this must be already fully typechecked, and must be a unary set

loneOf

public final Decl loneOf(java.lang.String label)
                  throws Err

Return a new declaration "v: lone this"

this must be already fully typechecked, and must be a unary set

the label is only used for pretty-printing, and does not have to be unique

Throws:

Err

oneOf

public final Expr oneOf()

Return the multiplicity expression "one this"

this must be already fully typechecked, and must be a unary set

oneOf

public final Decl oneOf(java.lang.String label)
                 throws Err

Return a new declaration "v: one this"

this must be already fully typechecked, and must be a unary set

the label is only used for pretty-printing, and does not have to be unique

Throws:

Err

setOf

public final Expr setOf()

Return the multiplicity expression "set this"

this must be already fully typechecked, and must be a set or relation

setOf

public final Decl setOf(java.lang.String label)
                 throws Err

Return a new declaration "v: set this"

this must be already fully typechecked, and must be a set or relation

the label is only used for pretty-printing, and does not have to be unique

Throws:

Err

not

public final Expr not()

Returns the formula (not this)

this must be a formula

no

public final Expr no()

Returns the formula (no this)

this must be a set or a relation

some

public final Expr some()

Returns the formula (some this)

this must be a set or a relation

lone

public final Expr lone()

Returns the formula (lone this)

this must be a set or a relation

one

public final Expr one()

Returns the formula (one this)

this must be a set or a relation

transpose

public final Expr transpose()

Returns the expression (~this)

this must be a binary relation

reflexiveClosure

public final Expr reflexiveClosure()

Returns the expression (*this)

this must be a binary relation

closure

public final Expr closure()

Returns the expression (^this)

this must be a binary relation

cardinality

public final Expr cardinality()

Returns the integer expression (#this) truncated to the current integer bitwidth.

this must be a set or a relation

cast2int

public final Expr cast2int()

Returns the integer expression "int[this]"

this must be a unary set

cast2sigint

public final Expr cast2sigint()

Returns the singleton set "Int[this]"

this must be an integer expression