The following are all the classes that form the semantic tree of the Euclid.tla specification in examples

1. Language

containers and interfaces

tlatools/src/tla2sany/semantic/ModuleNode.java

tlatools/src/tla2sany/semantic/SymbolNode.java
xml export not implemented but is added to the interface

tlatools/src/tla2sany/semantic/SemanticNode.java
Dummy - throws an exception if the xml export method is not being overriedn in a subclass

specification language

tlatools/src/tla2sany/semantic/OpDeclNode.java

kind: ConstantDeclKind

tla keyword supported:
  1. CONSTANTS
  2. VARIABLES

tlatools/src/tla2sany/semantic/OpDefNode.java

kind: UserDefinedOpKind

Used to define all TLA specs operators: Both in the library modules (Naturals, TLAPS, etc.) and in user defined ones.

tlatools/src/tla2sany/semantic/OpApplNode.java

Application of an operator to a list of arguments with a possible list of bound variables, each with a possible domain element.

tlatools/src/tla2sany/semantic/FormalParamNode.java

represents:
  1. bound variables

tlatools/src/tla2sany/semantic/NumeralNode.java

represents:
  1. integers

proof language

tlatools/src/tla2sany/semantic/UseOrHideNode.java

tlatools/src/tla2sany/semantic/AssumeProveNode.java

tlatools/src/tla2sany/semantic/NonLeafProofNode.java

tlatools/src/tla2sany/semantic/TheoremNode.java:

tlatools/src/tla2sany/semantic/NewSymbNode.java

tlatools/src/tla2sany/semantic/LeafProofNode.java

tlatools/src/tla2sany/semantic/AssumeNode.java

tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java

2. Euclid symbols

Last edited Jun 19, 2013 at 8:31 AM by libal, version 7