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

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

public final class ExprList
extends Expr

Immutable; represents disjoint[] or pred/totalOrder[] or (... and ... and ..) and other similar list of arugments.

Invariant: type!=EMPTY => (all x:args | x.mult==0)


Nested Class Summary
static class ExprList.Op
          This class contains all possible builtin predicates.
 
Field Summary
 ConstList<Expr> args
          The unmodifiable list of arguments.
 ExprList.Op op
          The builtin operator.
 
Fields inherited from class edu.mit.csail.sdg.alloy4compiler.ast.Expr
ambiguous, closingBracket, errors, mult, pos, weight
 
Method Summary
 ExprList addArg(Expr x)
          Return a new ExprList object that is the same as this one except with one additional argument.
 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.
static ExprList make(Pos pos, Pos closingBracket, ExprList.Op op, java.util.List<? extends Expr> args)
          Generates a call to a builtin predicate
static ExprList makeAND(Pos pos, Pos closingBracket, Expr a, Expr b)
          Generates the expression (arg1 and arg2)
static ExprList makeDISJOINT(Pos pos, Pos closingBracket, java.util.List<? extends Expr> args)
          Generates the expression disj[arg1, args2, arg3...]
static ExprList makeOR(Pos pos, Pos closingBracket, Expr a, Expr b)
          Generates the expression (arg1 || arg2)
static ExprList makeTOTALORDER(Pos pos, Pos closingBracket, java.util.List<? extends Expr> args)
          Generates the expression pred/totalOrder[arg1, args2, arg3...]
 Expr resolve(Type p, 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 ExprList.Op op
The builtin operator.


args

public final ConstList<Expr> args
The unmodifiable list of arguments.

Method Detail

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

make

public static ExprList make(Pos pos,
                            Pos closingBracket,
                            ExprList.Op op,
                            java.util.List<? extends Expr> args)
Generates a call to a builtin predicate


makeAND

public static ExprList makeAND(Pos pos,
                               Pos closingBracket,
                               Expr a,
                               Expr b)
Generates the expression (arg1 and arg2)


makeOR

public static ExprList makeOR(Pos pos,
                              Pos closingBracket,
                              Expr a,
                              Expr b)
Generates the expression (arg1 || arg2)


makeTOTALORDER

public static ExprList makeTOTALORDER(Pos pos,
                                      Pos closingBracket,
                                      java.util.List<? extends Expr> args)
Generates the expression pred/totalOrder[arg1, args2, arg3...]


makeDISJOINT

public static ExprList makeDISJOINT(Pos pos,
                                    Pos closingBracket,
                                    java.util.List<? extends Expr> args)
Generates the expression disj[arg1, args2, arg3...]


addArg

public ExprList addArg(Expr x)
Return a new ExprList object that is the same as this one except with one additional argument.


resolve

public Expr resolve(Type p,
                    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

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