can be separated into two categories - declarations (constants and structures - includes are a special case of structures) and modules (theories and views). They can be links between two theories (structures and views) and can have a body containing declarations (declared theories, structures and views).
api.StructuralElement is the top level data structure for declarations and modules. It provides the methods
getDeclarations and inherits
foreachDeclarationmethod to structural elements, that takes a function argument and applies it to all content elements recursively contained within it (including itself). The
pathmethod returns a
modules.Bodyis the trait governing all declared content elements that contain declarations (such as theories, views, structures). It provides the following useful methods:
addadds a new Declaration to the body.
gettakes a LocalName and returns the declaration of that name. If no declaration by that name exists, it throws an error. The method
getOdoes not, but returns an
LocalNameand returns a
boolindicating, whether a declaration by that name exists in the body.
LocalNameand deletes the declaration by that name from the body.
Declarationand adds it to the body, if no declaration by that name already exists, or replaces the existing one otherwise.
List[Declaration]of all declarations in the body.
The convention is to give a structural element class that extends
Elem with the trait
DeclaredElem (as opposed to
modules.Linkis the trait for theory morphisms like views and structures. It has the methods
Term) for domain and codomain,
toTerm. The trait
modules.Moduleis the top level data structure for theories and views. The
modules.Theory is the data structure representing theories - the subclass
DeclaredTheory is the important case. The class constructor takes as arguments the document/namespace containing the theory (
DPath), its name (
LocalName) and an optional meta theory (
DeclaredTheory provides the following useful methods:
getConstantsyields those declarations in the body, that are constants (as
List[MPath]of the included theories, including the meta theory.
getIncludesWithoutMetadoes the same without the meta theory.
List[Structure]of those structures, that are not plain inclusions.
symbols.Declarationrepresents everything on the declaration level - this entails constants and structures. The
homemethod returns the containing module (as
symbols.Constant represents a constant declaration. Constants are ultimately instantiated with the subclass
FinalConstant. Constants use
TermContainers to store their type and definition (in their different states
analyzed), which can be accessed by the methods
tpC (for types) and
dfC (for definitions). The methods
df circumvent the containers and directly yield their type or definition as
The helper object
symbols.Constant has an apply method to conveniently create new instances of
FinalConstant. It takes as arguments the containing home module (
Term), the name of the constant (
LocalName), and optionally aliases (
List[LocalName]), type (
Option[Term]), definition (
Option[Term]), role (
Option[String]) and notation (
NotationContainer, by default a new empty one).
Declaration. It has a
isInclude signifying whether the structure is a simple theory inclusion.
Structure with a
The helper objects
symbols.SimpleDeclaredStructure add convenient apply/unapply methods, where
Simple indicates the case where the domain is an
MPath (as opposed to a complex term representing a theory expression). The helper objects
symbols.PlainInclude offer apply/unapply methods for theory inclusions.