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

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

Direct Known Subclasses:

Sig.PrimSig, Sig.SubsetSig

public abstract class Sig
extends Expr

Mutable; represents a signature.

Nested Class Summary

static class	Sig.Field Mutable; represents a field.
static class	Sig.PrimSig Mutable; reresents a non-subset signature.
static class	Sig.SubsetSig Mutable; reresents a subset signature.

Field Summary

ConstList<Attr>	attributes Store the list of attributes.
boolean	builtin True if this sig is one of the built-in sig.
Decl	decl The declaration that quantifies over each atom in this sig.
static Sig.PrimSig	GHOST The built-in "none" signature.
Pos	isAbstract Nonnull if this sig is abstract.
Pos	isEnum Nonnull if the sig is toplevel and is an enum.
Pos	isLone Nonnull if this sig's multiplicity is declared to be lone.
Pos	isMeta Nonnull if this sig is a meta sig.
Pos	isOne Nonnull if this sig's multiplicity is declared to be one.
Pos	isPrivate Nonnull if the user wanted this sig to be private.
Pos	isSome Nonnull if this sig's multiplicity is declared to be some.
Pos	isSubset Nonnull if this sig is a SubsetSig and therefore not a PrimSig.
Pos	isSubsig Nonnull if this sig is a PrimSig and therefore not a SubsetSig.
java.lang.String	label The label for this sig; this name does not need to be unique.
static Sig.PrimSig	NONE The built-in "none" signature.
static Sig.PrimSig	SEQIDX The built-in "seq/Int" signature.
static Sig.PrimSig	SIGINT The built-in "Int" signature.
static Sig.PrimSig	STRING The built-in "String" signature.
static Sig.PrimSig	UNIV The built-in "univ" signature.

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

ambiguous, closingBracket, errors, mult, pos, weight

Method Summary

Sig.Field	addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, java.lang.String label, Expr bound) Add then return a new field F where this.F is bound to an exact "definition" expression.
void	addFact(Expr fact) Add a new per-atom fact; this expression is allowed to refer to this.decl.get()
Sig.Field	addField(java.lang.String label, Expr bound) Add then return a new field, where "all x: ThisSig | x.F in bound"
Sig.Field[]	addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos isDisjoint2, Pos isMeta, java.lang.String[] labels, Expr bound) Add then return a new field, where "all x: ThisSig | x.F in bound"
int	getDepth() Returns the height of the abstract syntax tree starting from this node.
SafeList<Expr>	getFacts() Return the list of per-atom facts; each expression is allowed to refer to this.decl.get()
SafeList<Decl>	getFieldDecls() Return the list of fields as a unmodifiable list of declarations (where you can see which fields are declared to be disjoint)
SafeList<Sig.Field>	getFields() Return the list of fields as a combined unmodifiable list (without telling you which fields are declared to be disjoint)
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.
boolean	isSame(Expr obj) Returns true if we can determine the two expressions are equivalent; may sometimes return false.
abstract boolean	isSameOrDescendentOf(Sig that) Returns true iff "this is equal or subtype of that"
boolean	isTopLevel() Returns true if this sig is a toplevel sig (meaning: it is UNIV, or it is a non-subset sig with parent==UNIV)
Expr	resolve(Type t, 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.
java.lang.String	toString() Returns the name for this sig; this name need not be unique.
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, 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, 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

UNIV

public static final Sig.PrimSig UNIV

The built-in "univ" signature.

SIGINT

public static final Sig.PrimSig SIGINT

The built-in "Int" signature.

SEQIDX

public static final Sig.PrimSig SEQIDX

The built-in "seq/Int" signature.

STRING

public static final Sig.PrimSig STRING

The built-in "String" signature.

NONE

public static final Sig.PrimSig NONE

The built-in "none" signature.

GHOST

public static final Sig.PrimSig GHOST

The built-in "none" signature.

attributes

public final ConstList<Attr> attributes

Store the list of attributes.

builtin

public final boolean builtin

True if this sig is one of the built-in sig.

Note: if builtin==true, then we ensure it is not abstract

isAbstract

public final Pos isAbstract

Nonnull if this sig is abstract.

Note: if a sig is abstract, then it cannot and will not be a subset sig.

isSubsig

public final Pos isSubsig

Nonnull if this sig is a PrimSig and therefore not a SubsetSig.

isSubset

public final Pos isSubset

Nonnull if this sig is a SubsetSig and therefore not a PrimSig.

Note: if a sig is a subset sig, then it cannot and will not be abstract.

isLone

public final Pos isLone

Nonnull if this sig's multiplicity is declared to be lone.

Note: at most one of "lone", "one", "some" can be nonnull for each sig.

isOne

public final Pos isOne

Nonnull if this sig's multiplicity is declared to be one.

Note: at most one of "lone", "one", "some" can be nonnull for each sig.

isSome

public final Pos isSome

Nonnull if this sig's multiplicity is declared to be some.

Note: at most one of "lone", "one", "some" can be nonnull for each sig.

isPrivate

public final Pos isPrivate

Nonnull if the user wanted this sig to be private.

Note: this value is always null for builtin sigs.

isEnum

public final Pos isEnum

Nonnull if the sig is toplevel and is an enum.

Note: this value is always null for builtin sigs.

isMeta

public final Pos isMeta

Nonnull if this sig is a meta sig.

Note: this value is always null for builtin sigs.

label

public final java.lang.String label

The label for this sig; this name does not need to be unique.

decl

public final Decl decl

The declaration that quantifies over each atom in this sig.

Method Detail

toString

public final java.lang.String toString()

Returns the name for this sig; this name need not be unique.

Overrides:

toString in class Expr

toString

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

span

public final Pos span()

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

Overrides:

span in class Browsable

resolve

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

isTopLevel

public final boolean isTopLevel()

Returns true if this sig is a toplevel sig (meaning: it is UNIV, or it is a non-subset sig with parent==UNIV)

isSame

public boolean isSame(Expr obj)

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

Overrides:

isSame in class Expr

isSameOrDescendentOf

public abstract boolean isSameOrDescendentOf(Sig that)

Returns true iff "this is equal or subtype of that"

getDepth

public int getDepth()

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

Specified by:

getDepth in class Expr

addFact

public void addFact(Expr fact)
             throws Err

Add a new per-atom fact; this expression is allowed to refer to this.decl.get()

Throws:

Err

getFacts

public SafeList<Expr> getFacts()

Return the list of per-atom facts; each expression is allowed to refer to this.decl.get()

getHTML

public final java.lang.String getHTML()

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

Specified by:

getHTML in class Browsable

getSubnodes

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

Returns a list of subnodes for this node.

Specified by:

getSubnodes in class Browsable

getFieldDecls

public final SafeList<Decl> getFieldDecls()

Return the list of fields as a unmodifiable list of declarations (where you can see which fields are declared to be disjoint)

getFields

public final SafeList<Sig.Field> getFields()

Return the list of fields as a combined unmodifiable list (without telling you which fields are declared to be disjoint)

addField

public final Sig.Field addField(java.lang.String label,
                                Expr bound)
                         throws Err

Add then return a new field, where "all x: ThisSig | x.F in bound"

Note: the bound must be fully-typechecked and have exactly 0 free variable, or have "x" as its sole free variable.

Parameters:

label - - the name of this field (it does not need to be unique)

bound - - the new field will be bound by "all x: one ThisSig | x.ThisField in bound"

Throws:

ErrorSyntax - if the sig is one of the builtin sig

ErrorSyntax - if the bound contains a predicate/function call

ErrorType - if the bound is not fully typechecked or is not a set/relation

Err

addTrickyField

public final Sig.Field[] addTrickyField(Pos pos,
                                        Pos isPrivate,
                                        Pos isDisjoint,
                                        Pos isDisjoint2,
                                        Pos isMeta,
                                        java.lang.String[] labels,
                                        Expr bound)
                                 throws Err

Add then return a new field, where "all x: ThisSig | x.F in bound"

Note: the bound must be fully-typechecked and have exactly 0 free variable, or have "x" as its sole free variable.

Parameters:

pos - - the position in the original file where this field was defined (can be null if unknown)

isPrivate - - if nonnull, that means the user intended this field to be "private"

isMeta - - if nonnull, that means the user intended this field to be "meta"

labels - - the names of the fields to be added (these names does not need to be unique)

bound - - the new field will be bound by "all x: one ThisSig | x.ThisField in bound"

Throws:

ErrorSyntax - if the sig is one of the builtin sig

ErrorSyntax - if the bound contains a predicate/function call

ErrorType - if the bound is not fully typechecked or is not a set/relation

Err

addDefinedField

public final Sig.Field addDefinedField(Pos pos,
                                       Pos isPrivate,
                                       Pos isMeta,
                                       java.lang.String label,
                                       Expr bound)
                                throws Err

Add then return a new field F where this.F is bound to an exact "definition" expression.

Note: the definition must be fully-typechecked and have exactly 0 free variables.

Note: currently the defined field must consist product and union operators over sigs.

Parameters:

pos - - the position in the original file where this field was defined (can be null if unknown)

isPrivate - - if nonnull, that means this field should be marked as private

isMeta - - if nonnull, that means this field should be marked as meta

label - - the name of this field (it does not need to be unique)

bound - - the new field will be defined to be exactly equal to sig.product(definition)

Throws:

ErrorSyntax - if the sig is one of the builtin sig

ErrorSyntax - if the bound contains a predicate/function call

ErrorType - if the bound is not fully typechecked or is not a set/relation

Err