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

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

public final class ExprQt
extends Expr

Immutable; represents a quantified expression. It can have one of the following forms:

( all a,b:t | formula )
( no a,b:t | formula )
( lone a,b:t | formula )
( one a,b:t | formula )
( some a,b:t | formula )
( sum a,b:t | integer expression )
{ a,b:t | formula }
{ a,b:t }

Invariant: type!=EMPTY => sub.mult==0
Invariant: type!=EMPTY => vars.size()>0

Nested Class Summary

static class

ExprQt.Op This class contains all possible quantification operators.

Field Summary

ConstList<Decl>	decls The unmodifiable list of variables.
ExprQt.Op	op The operator (ALL, NO, LONE, ONE, SOME, SUM, or COMPREHENSION)
Expr	sub The body of the quantified expression.

Fields inherited from class edu.mit.csail.sdg.alloy4compiler.ast.Expr

ambiguous, closingBracket, errors, mult, pos, weight

Method Summary

int	count() Return the number of variables.
Expr	desugar() This method desugars away the "disjoint" keyword by prefixing the subexpression with the appropriate disjointness guard condition.
ExprVar	get(int i) Return the i-th variable.
Expr	getBound(int i) Return the i-th variable's bound.
int	getDepth() Returns the height of the abstract syntax tree starting from this node.
java.lang.String	getHTML() Returns the description (as HTML) to show for this node.
java.util.List<? extends Browsable>	getSubnodes() Returns a list of subnodes for this node.
Expr	resolve(Type unused, java.util.Collection<ErrorWarning> warns) Resolves this expression if ambiguous.
Pos	span() Returns a Pos object representing the entire span of this Expr and all its subexpressions.
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.

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

and, any_arrow_lone, any_arrow_one, any_arrow_some, cardinality, cast2int, cast2sigint, closure, comprehensionOver, deNOP, div, domain, equal, equals, findAllFunctions, forAll, forLone, forNo, forOne, forSome, gt, gte, hashCode, hasVar, iff, iminus, implies, in, intersect, iplus, isSame, isSeq_arrow_lone, ite, join, lone_arrow_any, lone_arrow_lone, lone_arrow_one, lone_arrow_some, lone, loneOf, loneOf, lt, lte, minus, mul, mult, no, not, one_arrow_any, one_arrow_lone, one_arrow_one, one_arrow_some, one, oneOf, oneOf, or, override, plus, pos, product, range, reflexiveClosure, rem, resolve_as_formula, resolve_as_int, resolve_as_set, setOf, setOf, sha, shl, shr, some_arrow_any, some_arrow_lone, some_arrow_one, some_arrow_some, some, someOf, someOf, sumOver, toString, transpose, type, typecheck_as_formula, typecheck_as_int, typecheck_as_set

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

make, make, make, make, showAsTree

Methods inherited from class java.lang.Object

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

Field Detail

op

public final ExprQt.Op op

The operator (ALL, NO, LONE, ONE, SOME, SUM, or COMPREHENSION)

decls

public final ConstList<Decl> decls

The unmodifiable list of variables.

sub

public final Expr sub

The body of the quantified expression.

Method Detail

count

public int count()

Return the number of variables.

get

public ExprVar get(int i)

Return the i-th variable.

getBound

public Expr getBound(int i)

Return the i-th variable's bound.

span

public Pos span()

Returns a Pos object representing the entire span of this Expr and all its subexpressions.

Overrides:

span in class Browsable

toString

public 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)

Specified by:

toString in class Expr

resolve

public Expr resolve(Type unused,
                    java.util.Collection<ErrorWarning> warns)

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.

Specified by:

resolve in class Expr

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

desugar

public Expr desugar()
             throws ErrorSyntax

This method desugars away the "disjoint" keyword by prefixing the subexpression with the appropriate disjointness guard condition.

Throws:

ErrorSyntax

getDepth

public int getDepth()

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

Specified by:

getDepth in class Expr

getHTML

public java.lang.String getHTML()

Returns the description (as HTML) to show for this node.

Specified by:

getHTML in class Browsable

getSubnodes

public java.util.List<? extends Browsable> getSubnodes()

Returns a list of subnodes for this node.

Specified by:

getSubnodes in class Browsable