edu.mit.csail.sdg.alloy4compiler.ast
Interface Module

All Known Implementing Classes:

CompModule

public interface Module

This interface represents an Alloy 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<? extends Module>	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	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.
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)
javax.swing.JFrame	showAsTree(Listener listener) Display this object (and so objects) as a tree; if listener!=null, it will receive OurTree.Event.SELECT events.

Method Detail

getModelName

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.

path

java.lang.String path()

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

getAllReachableModules

SafeList<? extends Module> getAllReachableModules()

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

getAllReachableModulesFilenames

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

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

getAllReachableSigs

ConstList<Sig> getAllReachableSigs()

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

getAllSigs

SafeList<Sig> getAllSigs()

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

getAllFunc

SafeList<Func> getAllFunc()

Return an unmodifiable list of all functions in this module.

getAllAssertions

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

Return an unmodifiable list of all assertions in this module.

getAllFacts

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

Return an unmodifiable list of all facts in this module.

getAllReachableFacts

Expr getAllReachableFacts()

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

getAllCommands

ConstList<Command> getAllCommands()

Return an unmodifiable list of all commands in this module.

addGlobal

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

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

showAsTree

javax.swing.JFrame showAsTree(Listener listener)

Display this object (and so objects) as a tree; if listener!=null, it will receive OurTree.Event.SELECT events.

parseOneExpressionFromString

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.

Throws:

Err

java.io.FileNotFoundException

java.io.IOException