package symbols
MMT Declarations are the elements of Modules. The kinds of declarations are documented at Declaration.
ObjContainer are owned by structural elements, in particular by declarations, to store objects.
- Source
- package.scala
- Alphabetic
- By Inheritance
- symbols
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
ApplyMorphism(lup: Lookup, morph: Term) extends UniformTranslator with Product with Serializable
a translator that applies a morphism (lazily)
-
case class
ApplyMorphismLazy(morph: Term) extends UniformTranslator with Product with Serializable
a translator that applies a morphism (lazily)
-
case class
ApplySubs(subs: Substitution) extends UniformTranslator with Product with Serializable
a translator that performs substitution
- class BoundTheoryParameters extends StructuralFeature with IncludeLike
-
abstract
class
Constant extends Declaration with HasType with HasDefiniens with HasNotation
the abstract interface to MMT constants with a few basic methods
-
class
ContextContainer extends ObjContainer[Context]
container for mutable contexts
-
abstract
class
Declaration extends ContentElement
Declarations are the children of Modules.
Declarations are the children of Modules.
They are mostly Constants for the syntax and RuleConstants for the semantics (= rule-based implementation). The MMT data model is extensible via DerivedDeclarations.
Structures (except for includes) are conceptually a derived declaration but are hard-coded as a separate kind of declaration. Inlcudes are represented as special cases of structures.
-
trait
DerivedContentElement extends AbstractTheory with HasType with HasNotation
A DerivedContentElement unifies feature of Constant and Theory but without a commitment to the semantics.
A DerivedContentElement unifies feature of Constant and Theory but without a commitment to the semantics. The semantics is defined by the corresponding StructuralFeature
-
class
DerivedDeclaration extends Declaration with DerivedContentElement
a declarations that is elaborated into more primitive declarations
-
class
DerivedModule extends Module with DerivedContentElement
a module that is elaborated into more primitive module
-
abstract
class
Elaboration extends ElementContainer[Declaration]
the return type of elaborating a DerivedDeclaration by a StructuralFeature
-
class
FinalConstant extends Constant
the main class for a concrete MMT constant
-
abstract
class
GeneralStructuralFeature[Level <: DerivedContentElement] extends FormatBasedExtension
A StructureFeature defines the semantics of a DerivedDeclaration
A StructureFeature defines the semantics of a DerivedDeclaration
The semantics consists of a set of declarations that are injected into the parent theory after the DerivedDeclaration These are called the 'outer declarations'.
All methods that take a dd:DerivedDeclaration can assume - dd.feature == this.feature - dd.getComponents has the same components as this.expectedComponents and in the same order
-
class
GenerativePushout extends StructuralFeature with IncludeLike
Generative, definitional functors/pushouts with free instantiation called structures in original MMT
- trait HasDefiniens extends AnyRef
-
trait
HasNotation extends AnyRef
declarations that have a notation
- trait HasType extends AnyRef
-
case class
IncludeData(home: Term, from: MPath, args: List[Term], df: Option[Term], total: Boolean) extends Product with Serializable
Auxiliary class that collects information about a structure that acts like an include.
Auxiliary class that collects information about a structure that acts like an include.
- home
The module in which this include is declared (e.g. a theory T, view V, etc.)
- from
The domain D of the included theory (into T, or into domain of V)
- args
Instantiations of the parameters of from (if any, e.g. for parametric theories)
- df
Definiens (of type D(args) -> T, or D(args) -> codomain of V)
- total
A total include is one that must be implemented by the containing theory this becomes available as a morphism only at the end of the containing theory (even if there is a definiens, which can happen, e.g., if the definiens refers to other total includes) invariants: if df contains mor then args.isEmpty && from is domain of df else OMPMOD(from,args) is included theory Note that concrete syntax may allow "include df" because D because can be infered; in a theory, "include D" is the standard for includes without definiens; in a view, we may also allow "include D" for the case where df is the identity of D. See the examples below!
A Theory T includes a theory S in the usual way: theory S : ?someMetaTheory = ... ❚ theory T : ?someMetaTheory = include ?S ❙ ❚ Both theories are non-parametric, i.e. as usual. Then T.getAllIncludes will contain an
IncludeData(T.path, S.path, Nil, None, false). , Assume S, T as above, as well as a View v: T -> R including another view w: S -> R: view w : S -> R = ... ❚ view v : T -> R = include ?S ❘ = ?w ❙ ❚ Then v.getAllIncludes will contain an
IncludeData(v.path, S.path, Nil, w.path, false). , Let R, S, T be as below: theory R : ?someMetaTheory = ... ❚ theory S : ?someMetaTheory = include ?R❙ ... ❚ theory T : ?someMetaTheory = include ?R ❙ ... ❚ Pictorially, this is an inclusion triangle (with one missing edge): R / \ T S Now suppose we want a View v: T -> S which is the identity on R, i.e. v_R = id_R. In surface syntax we can do this as follows: view v: T -> S = include ?R❙ ❚ With this v.getAllIncludes will contain an
IncludeData(v.path, R.path, Nil, Some(OMIDENT(R.path)), false). , If you have a View v: T -> S between two theories with the same meta theory mt, then v.getAllIncludes will automatically include
IncludeData(v.path, mt.path, Nil, Some(OMIDENT(mt.path)), false)similar to the previous example where the view is the identity on the included theory.- See also
Examples: -
trait
IncludeLike extends AnyRef
for structural features with unnamed declarations whose type is an instance of a named theory
-
abstract
class
LazyConstant extends Constant
a Constant whose fields are computed on demand
- abstract class ModuleLevelFeature extends GeneralStructuralFeature[DerivedModule]
-
class
NestedModule extends Declaration with ModuleWrapper
a Module as a Declaration, i.e., inside some other module
-
class
OMLReplacer extends StatelessTraverser
replaces all naked OML's; for convenience a substitution is used even though we are replacing OML's not OMV's
-
abstract
class
OMSReplacer extends StatelessTraverser
A traverser to replace references to GlobalNames by a custom term given by the abstract method OMSReplacer.replace.
-
trait
ObjContainer[T <: Obj] extends AbstractObjectContainer
TermContainer acts as the interface between the structural and the object level
TermContainer acts as the interface between the structural and the object level
Elements like info.kwarc.mmt.api.symbols.Constant that have a info.kwarc.mmt.api.objects.Term as a component will not declare a term directly but a TermContainer.
TermContainer keeps track of different syntactic representations of the same semantic term. It also stores additional status information.
The representations are read < parsed < analyzed < normalized. Setting a representation marks the higher representations as dirty.
- T
the type of objects stored; the type bound is not actually needed, but it helps putting sharper bound on some return types
-
class
ObjDimension[T] extends AnyRef
a mutable wrapper around a value together with status information
-
trait
ParametricTheoryLike extends StructuralFeature
for structural features that are parametric theories with special meaning, e.g., patterns, inductive types
-
class
Renamer extends OMSReplacer
a translator that renames local names of a module
-
class
RuleConstant extends Declaration
A RuleConstant is a declaration whose value is an externally provided rule.
A RuleConstant is a declaration whose value is an externally provided rule. Its inner structure is not representable in or accessible to MMT, but it exposes functionality that MMT can use and that defines the semantics of MMT.
-
class
RuleConstantInterpreter extends AnyRef
loads a rule (by reflection) given by a LocalName corresponding to a java name of a Rule object or of a StructuralFeature class
- class RuleConstantParser extends ParserExtension
- abstract class SimpleLazyConstant extends LazyConstant
- abstract class StructuralFeature extends GeneralStructuralFeature[DerivedDeclaration]
-
case class
StructuralFeatureRule(cls: Class[_ <: StructuralFeature], feature: String) extends Rule with Product with Serializable
a rule that legitimizes a StructuralFeature
-
class
Structure extends Declaration with Link with HasType
MMT structures, given by a body and an optional definiens
-
class
TermContainer extends ObjContainer[Term] with AbstractTermContainer
container for mutable terms
- trait TheoryLike extends StructuralFeature
-
abstract
class
Translator extends AnyRef
a general purpose term translator
a general purpose term translator
There are a number of desirable properties that Translator can have. In particular: preservation of typing, equality; commute with substitution.
-
abstract
class
TraversingTranslator extends UniformTranslator
a translator obtained from a traverser
- trait TypedConstantLike extends AnyRef
-
trait
TypedParametricTheoryLike extends StructuralFeature with ParametricTheoryLike
for structural features that take both parameters and a type Examples are structural features which build structures defined via a derived declaration of another structural feature like inductively-defined functions or proofs by induction over an inductively-defined type or terms of a record In such a case the type is the other derived declaration instantiated with values for its parameters
-
abstract
class
UniformTranslator extends Translator
a translator that maps all terms in the same way (i.e., applyDef and applyType are the same)
- trait UnnamedUntyped extends AnyRef
- trait Untyped extends AnyRef
-
case class
Visibility(tp: Boolean, _df: Boolean) extends Product with Serializable
visibility information for a Constant
visibility information for a Constant
- tp
type is visible
- _df
definiens is visible (must be invisible if type is)
Value Members
-
object
Constant
helper object
-
object
ConstantAssignment
An MMT assignment to a constant is a special case of a Constant.
- object ContextContainer
-
object
DefLinkAssignment
An MMT assignment to a definitional link is a special case of a DefinedStructure.
- object Elaboration
-
object
IdentityInclude
a LinkInclude of the identity morphism: the analog to a plain include in a theory
-
object
IdentityTranslator extends UniformTranslator
identity (non-traversing)
-
object
Include
unnamed imports with automatic sharing are represented as special Structures
unnamed imports with automatic sharing are represented as special Structures
they do not carry assignments their name is LocalName(from)
-
object
LinkInclude
include of a morphism into a link
- object OMLReplacer
- object OMSReplacer
-
object
ParametricTheoryLike
helper object
-
object
PlainInclude
A PlainInclude represents an MMT inclusion between theories.
- object Renamer
- object RuleConstant
-
object
SimpleDeclaredStructure
apply/unapply functions for SimpleDeclaredStructures whose domain is an MPath
-
object
SimpleStructure
this can be wrapped around a pattern for matching a structure, e.g., case SimpleStructure(s, fromPath)
- object StructuralFeatureUtil
-
object
Structure
auxiliary functions
-
object
TermContainer
helper object
- object TraversingTranslator
-
object
TypedParametricTheoryLike
helper object
- object Visibility extends Serializable