edu.mit.csail.sdg.alloy4compiler.parser
Class CompModule

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.ast.Browsable
      edu.mit.csail.sdg.alloy4compiler.parser.CompModule

All Implemented Interfaces:

Module

public final class CompModule
extends Browsable
implements Module

Mutable; this class represents an Alloy module; equals() uses object identity.

Nested Class Summary

static class

CompModule.Open Mutable; this class represents an untypechecked Alloy module import statement; equals() uses object identity.

Field Summary

java.lang.String

path The simplest path pointing to this Module ("" if this is the main module)

Method Summary

void	addGlobal(java.lang.String name, Expr value) Add a global expression; if the name already exists, it is removed first.
ConstList<Pair<java.lang.String,Expr>>	getAllAssertions() Return an unmodifiable list of all assertions in this module.
ConstList<Command>	getAllCommands() Return an unmodifiable list of all commands in this module.
SafeList<Pair<java.lang.String,Expr>>	getAllFacts() Return an unmodifiable list of all facts in this module.
SafeList<Func>	getAllFunc() Return an unmodifiable list of all functions in this module.
Expr	getAllReachableFacts() Return the conjunction of all facts in this module and all reachable submodules (not including field constraints, nor including sig appended constraints)
SafeList<CompModule>	getAllReachableModules() Return the list containing THIS MODULE and all modules reachable from this module.
java.util.List<java.lang.String>	getAllReachableModulesFilenames() Return the list of all relative filenames included from this MODULE.
ConstList<Sig>	getAllReachableSigs() Return the list containing UNIV, SIGINT, SEQIDX, STRING, NONE, and all sigs defined in this module or a reachable submodule.
SafeList<Sig>	getAllSigs() Returns an unmodifiable list of all signatures defined inside this module.
java.lang.String	getHTML() Returns the description (as HTML) to show for this node.
java.lang.String	getModelName() Returns the text of the "MODULE" line at the top of the file; "unknown" if the line has not be parsed from the file yet.
ConstList<CompModule.Open>	getOpens() Returns an unmodifiable copy of the current list of OPEN statements.
CompModule	getRootModule() Returns a pointer to the root module in this world.
java.util.List<? extends Browsable>	getSubnodes() Returns a list of subnodes for this node.
Sig.PrimSig	metaField() Returns the meta signature "field$" (or null if such a sig does not exist)
Sig.PrimSig	metaSig() Returns the meta signature "sig$" (or null if such a sig does not exist)
Expr	parseOneExpressionFromString(java.lang.String input) Parse one expression by starting fromt this module as the root module.
java.lang.String	path() Return the simplest path pointing to this Module ("" if this is the main module)
Pos	pos() Returns a Pos object representing the position of this Expr.
Pos	span() Returns a Pos object representing the entire span of this Expr and all its subexpressions.
java.lang.String	toString() Returns a short description for this module.

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

make, make, make, make, showAsTree

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface edu.mit.csail.sdg.alloy4compiler.ast.Module

showAsTree

Field Detail

path

public final java.lang.String path

The simplest path pointing to this Module ("" if this is the main module)

Method Detail

path

public java.lang.String path()

Return the simplest path pointing to this Module ("" if this is the main module)

Specified by:

path in interface Module

pos

public final Pos pos()

Returns a Pos object representing the position of this Expr.

Overrides:

pos in class Browsable

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

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

metaSig

public Sig.PrimSig metaSig()

Returns the meta signature "sig$" (or null if such a sig does not exist)

metaField

public Sig.PrimSig metaField()

Returns the meta signature "field$" (or null if such a sig does not exist)

parseOneExpressionFromString

public Expr parseOneExpressionFromString(java.lang.String input)
                                  throws Err,
                                         java.io.FileNotFoundException,
                                         java.io.IOException

Parse one expression by starting fromt this module as the root module.

Specified by:

parseOneExpressionFromString in interface Module

Throws:

Err

java.io.FileNotFoundException

java.io.IOException

getAllReachableModules

public SafeList<CompModule> getAllReachableModules()

Return the list containing THIS MODULE and all modules reachable from this module.

Specified by:

getAllReachableModules in interface Module

getAllReachableModulesFilenames

public java.util.List<java.lang.String> getAllReachableModulesFilenames()

Return the list of all relative filenames included from this MODULE.

Specified by:

getAllReachableModulesFilenames in interface Module

getAllReachableSigs

public ConstList<Sig> getAllReachableSigs()

Return the list containing UNIV, SIGINT, SEQIDX, STRING, NONE, and all sigs defined in this module or a reachable submodule.

Specified by:

getAllReachableSigs in interface Module

toString

public java.lang.String toString()

Returns a short description for this module.

Overrides:

toString in class java.lang.Object

getRootModule

public CompModule getRootModule()

Returns a pointer to the root module in this world.

getModelName

public java.lang.String getModelName()

Returns the text of the "MODULE" line at the top of the file; "unknown" if the line has not be parsed from the file yet.

Specified by:

getModelName in interface Module

getOpens

public ConstList<CompModule.Open> getOpens()

Returns an unmodifiable copy of the current list of OPEN statements.

getAllSigs

public SafeList<Sig> getAllSigs()

Returns an unmodifiable list of all signatures defined inside this module.

Specified by:

getAllSigs in interface Module

getAllFunc

public SafeList<Func> getAllFunc()

Return an unmodifiable list of all functions in this module.

Specified by:

getAllFunc in interface Module

getAllAssertions

public ConstList<Pair<java.lang.String,Expr>> getAllAssertions()

Return an unmodifiable list of all assertions in this module.

Specified by:

getAllAssertions in interface Module

getAllFacts

public SafeList<Pair<java.lang.String,Expr>> getAllFacts()

Return an unmodifiable list of all facts in this module.

Specified by:

getAllFacts in interface Module

getAllReachableFacts

public Expr getAllReachableFacts()

Return the conjunction of all facts in this module and all reachable submodules (not including field constraints, nor including sig appended constraints)

Specified by:

getAllReachableFacts in interface Module

getAllCommands

public ConstList<Command> getAllCommands()

Return an unmodifiable list of all commands in this module.

Specified by:

getAllCommands in interface Module

addGlobal

public void addGlobal(java.lang.String name,
                      Expr value)

Add a global expression; if the name already exists, it is removed first.

Specified by:

addGlobal in interface Module