abstract class RealizationInScala extends RealizedTheory
a model of an MMT theory written in Scala
- Source
- RealizedTheory.scala
- Alphabetic
- By Inheritance
- RealizationInScala
- RealizedTheory
- SemanticObject
- Theory
- AbstractTheory
- Module
- ModuleOrLink
- HasDefiniens
- ContainerElement
- MutableElementContainer
- ElementContainer
- ContentElement
- StructuralElement
- NamedElement
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new RealizationInScala()
Abstract Value Members
-
abstract
val
_domain: TheoryScala
the modelled theory
-
abstract
val
under: List[GlobalName]
the HOAS apply operators in applications
Concrete Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def _assert(name: String, term: () ⇒ Term, assertion: (Term) ⇒ Boolean): Unit
-
lazy val
_name: LocalName
the name of the modelled theory
-
lazy val
_path: MPath
the MMT URI of the modelled theory
- def _test(controller: Controller, log: (String) ⇒ Unit): Unit
-
def
add(d: Declaration, at: AddPosition = AtEnd): Unit
adds a named declaration, throws exception if name already declared
adds a named declaration, throws exception if name already declared
- d
declaration to add
- at
the position where to add, at end by default this throws an errors if a declaration for that name already exists; exception: if the two declarations are equivalent, the old one is overridden
- Definition Classes
- ModuleOrLink → MutableElementContainer
-
def
addAfterNarrative(d: Declaration, after: LocalName): Unit
like add, but treats the second argument as the name of a NarrativeElement
like add, but treats the second argument as the name of a NarrativeElement
- Definition Classes
- ModuleOrLink
-
def
asDocument: Document
the narrative structure
the narrative structure
- Definition Classes
- ModuleOrLink
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
clientProperty: ListMap[URI, Any]
- Definition Classes
- ClientProperties
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
compatible(that: StructuralElement): Boolean
two StructuralElement's are compatible if they have the same type, same Path, and agree in all parts that are TermContainer's
two StructuralElement's are compatible if they have the same type, same Path, and agree in all parts that are TermContainer's
- Definition Classes
- StructuralElement
-
def
declare(b: ⇒ Unit): Unit
takes a argument and adds it to the _lazyBody
takes a argument and adds it to the _lazyBody
- Attributes
- protected
- Definition Classes
- RealizedTheory
-
def
declares(name: LocalName): Boolean
true iff a declaration for a name is present
true iff a declaration for a name is present
- Definition Classes
- ModuleOrLink
-
def
delete(name: LocalName): Option[Declaration]
delete a named declaration (does not have to exist)
delete a named declaration (does not have to exist)
- returns
the deleted declaration
- Definition Classes
- ModuleOrLink → MutableElementContainer
-
def
df: Option[Term]
- Definition Classes
- HasDefiniens
-
val
dfC: TermContainer
- Definition Classes
- Theory → HasDefiniens
-
def
dfNode: Seq[Node] with AbstractSeq[Node] with Serializable
- Definition Classes
- HasDefiniens
-
def
domain: List[LocalName]
the list of names of all declarations
the list of names of all declarations
- Definition Classes
- ModuleOrLink → ElementContainer
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
equivalentTo(that: StructuralElement): Boolean
logically equivalent: compares headerInfo, components, and declarations
logically equivalent: compares headerInfo, components, and declarations
- Definition Classes
- StructuralElement
-
val
feature: String
the kind of declaration, e.g., "constant"
the kind of declaration, e.g., "constant"
- Definition Classes
- Theory → ContentElement → StructuralElement
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
foreachComponent(f: (CPath, ComponentContainer) ⇒ Unit): Unit
recursively applies a function to all components in this element (in declaration order)
recursively applies a function to all components in this element (in declaration order)
- Definition Classes
- ContentElement
-
def
foreachDeclaration(f: (ContentElement) ⇒ Unit): Unit
recursively applies a function to all declarations in this element (in declaration order)
recursively applies a function to all declarations in this element (in declaration order)
- Definition Classes
- ContentElement
-
def
function(op: GlobalName, aTypesN: List[GlobalName], rTypeN: GlobalName)(fun: FunctionN): Unit
adds a rule for implementing a function symbol (argument and return types must have been added previously)
-
def
functionT[U, V](op: GlobalName, argType1: RepresentedRealizedType[U], rType: RepresentedRealizedType[V])(comp: (U) ⇒ V): Unit
typed variant, experimental, not used by ScalaExporter yet
-
def
get(name: LocalName): Declaration
- Definition Classes
- ElementContainer
-
def
getAllIncludes: List[IncludeData]
like getIncludes but also with includes of parametric theories and defined includes
like getIncludes but also with includes of parametric theories and defined includes
- Definition Classes
- AbstractTheory → ModuleOrLink
-
def
getAllIncludesWithSelf: List[IncludeData]
Get all transitive-reflexive inclusions.
Get all transitive-reflexive inclusions.
- Definition Classes
- ModuleOrLink
-
def
getAllIncludesWithoutMeta: List[IncludeData]
like getIncludesWithoutMeta but also with includes of parametric theories and their instantiations
like getIncludesWithoutMeta but also with includes of parametric theories and their instantiations
- Definition Classes
- AbstractTheory
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getComponent(k: ComponentKey): Option[ComponentContainer]
returns a specific component if present
returns a specific component if present
- Definition Classes
- StructuralElement
-
def
getComponentContext(k: ComponentKey): Context
like getComponent but returns the additional context (in addition to the context of the element) of the component, empty by default, override as needed unspecified if the component does not exist
like getComponent but returns the additional context (in addition to the context of the element) of the component, empty by default, override as needed unspecified if the component does not exist
- Definition Classes
- StructuralElement
-
def
getComponents: List[DeclarationComponent]
returns all term components of this elements
returns all term components of this elements
- Definition Classes
- Theory → StructuralElement
-
def
getConstants: List[Constant]
convenience method to obtain all constants
convenience method to obtain all constants
- Definition Classes
- AbstractTheory
-
def
getDeclarations: List[Declaration]
the list of declarations in narrative order, includes generated declarations
the list of declarations in narrative order, includes generated declarations
- Definition Classes
- ModuleOrLink → ElementContainer → ContentElement → StructuralElement
-
def
getDeclarationsBefore(n: LocalName): List[Declaration]
- Definition Classes
- ElementContainer
-
def
getDeclarationsElaborated: List[Declaration]
the list of declarations using elaborated declarations where possible these are: primitive elements: includes, constants other elements if they have not been fully elaborated
the list of declarations using elaborated declarations where possible these are: primitive elements: includes, constants other elements if they have not been fully elaborated
- Definition Classes
- ContainerElement
-
def
getDerivedDeclarations(f: String): List[DerivedDeclaration]
convenience method to obtain all derived declarations for a given feature
convenience method to obtain all derived declarations for a given feature
- Definition Classes
- AbstractTheory
-
def
getIncludes: List[MPath]
convenience method to obtain all included theories (including a possible meta-theory)
convenience method to obtain all included theories (including a possible meta-theory)
- Definition Classes
- AbstractTheory
-
def
getIncludesWithoutMeta: List[MPath]
convenience method to obtain all included theories (without a possible meta-theory)
convenience method to obtain all included theories (without a possible meta-theory)
- Definition Classes
- AbstractTheory
-
def
getInnerContext: Context
the context governing the body: meta-theory, parameters, and this theory
the context governing the body: meta-theory, parameters, and this theory
- Definition Classes
- AbstractTheory → ModuleOrLink
-
def
getMetaDataNode: NodeSeq
- Definition Classes
- HasMetaData
-
def
getMostSpecific(name: LocalName): Option[(Declaration, LocalName)]
- Definition Classes
- ModuleOrLink → ElementContainer
-
def
getNamedStructures: List[Structure]
convenience method to obtain all named structures
convenience method to obtain all named structures
- Definition Classes
- AbstractTheory
-
def
getO(name: LocalName): Option[Declaration]
retrieve a declaration
retrieve a declaration
- Definition Classes
- ModuleOrLink → ElementContainer
-
def
getO(name: String): Option[Declaration]
same as get(LocalName(name))
same as get(LocalName(name))
- Definition Classes
- ElementContainer
-
def
getOrigin: Origin
- Definition Classes
- StructuralElement
-
def
getPrimitiveDeclarations: List[Declaration]
the list of declarations in the order of addition, excludes generated declarations
the list of declarations in the order of addition, excludes generated declarations
- Definition Classes
- ContainerElement
-
def
getRealizedType(synType: GlobalName): RealizedType
look up the realized type for a given operator
look up the realized type for a given operator
- Attributes
- protected
-
def
getRealizees: List[IncludeData]
return all includes that are realizations
return all includes that are realizations
- Definition Classes
- AbstractTheory
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
headerInfo: HeaderInfo
header information of this elements includes the MMT types (e.g., domain, codomain of links) but not the logical types of constants
header information of this elements includes the MMT types (e.g., domain, codomain of links) but not the logical types of constants
- Definition Classes
- StructuralElement
-
def
headerNodes: Seq[Node]
common inner nodes: definiens (metadata is part of document)
common inner nodes: definiens (metadata is part of document)
- Definition Classes
- Theory → ModuleOrLink
-
def
init: Unit
creates the actual body of this class from the body
creates the actual body of this class from the body
- Definition Classes
- RealizedTheory → SemanticObject
-
def
innerNodes: NodeSeq
getPrimitiveDeclarations, with narrative structure
getPrimitiveDeclarations, with narrative structure
- Attributes
- protected
- Definition Classes
- ModuleOrLink
-
def
innerNodesElab: List[Node]
getDeclarationsElaborated, without narrative structure
getDeclarationsElaborated, without narrative structure
- Attributes
- protected
- Definition Classes
- ModuleOrLink
-
def
innerString: String
body as a string
body as a string
- Definition Classes
- ModuleOrLink
-
def
inverse(op: GlobalName, aTypesN: List[GlobalName], rTypeN: GlobalName)(fun: InvFunctionN): Unit
the partial inverse of an n-ary operator
-
def
inverse(op: GlobalName, aTypeN: GlobalName, rTypeN: GlobalName)(comp: (Any) ⇒ Option[Any]): Unit
the partial inverse of a unary operator
-
def
isDeclared(name: LocalName): Boolean
- Definition Classes
- ElementContainer
-
def
isEmpty: Boolean
true iff no declarations present
true iff no declarations present
- Definition Classes
- ModuleOrLink
-
def
isGenerated: Boolean
- Definition Classes
- StructuralElement
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
merge(that: StructuralElement): Unit
merge all properties of 'that' into 'this' except for components and declarations
merge all properties of 'that' into 'this' except for components and declarations
- Definition Classes
- StructuralElement
-
def
meta: Option[MPath]
the meta-theory
the meta-theory
- Definition Classes
- Theory → AbstractTheory
-
val
metaC: TermContainer
the container of the meta-theory
the container of the meta-theory
- Definition Classes
- Theory
-
val
metadata: MetaData
- Definition Classes
- HasMetaData
-
def
modulePath: MPath
path if seen as a module
path if seen as a module
- Definition Classes
- ModuleOrLink
-
lazy val
mpath: MPath
the MMT URI of this object, derived from its Scala name: scala://package?name
the MMT URI of this object, derived from its Scala name: scala://package?name
- Definition Classes
- SemanticObject
-
val
name: LocalName
local name relative to the parent element or namespace
local name relative to the parent element or namespace
- Definition Classes
- RealizedTheory → Module → ContentElement → NamedElement
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
outerString: String
header as a string (without definiens)
header as a string (without definiens)
- Definition Classes
- Theory → ModuleOrLink
-
val
paramC: ContextContainer
- Definition Classes
- Theory
-
def
parameters: Context
the parameters
the parameters
- Definition Classes
- Theory → AbstractTheory
-
val
parent: DPath
the containing knowledge item, a URL if none
the containing knowledge item, a URL if none
- Definition Classes
- RealizedTheory → Module → StructuralElement
-
var
parentDoc: Option[DPath]
- Definition Classes
- Module
-
def
path: MPath
the MMT URI of the element
the MMT URI of the element
- Definition Classes
- Module → ContentElement → StructuralElement
-
def
realizes(b: ⇒ Unit): Unit
- Attributes
- protected
-
def
reorder(ln: LocalName): Unit
moves a declaration to the end of its section (if the relDocHome of ln has changed, it is also moved to the new section) also moves all subsequent ln/X declarations (and updates their relDocHome)
moves a declaration to the end of its section (if the relDocHome of ln has changed, it is also moved to the new section) also moves all subsequent ln/X declarations (and updates their relDocHome)
- Definition Classes
- ModuleOrLink → MutableElementContainer
-
def
rule(r: SyntaxDrivenRule): Unit
adds a RuleConstant realizing r.head as r to this model
adds a RuleConstant realizing r.head as r to this model
- r
a BreadthRule for n-ary operators and an AbbrevRule for nullary operators
-
def
selfInclude: IncludeData
Get self inclusion.
Get self inclusion.
- Definition Classes
- AbstractTheory → ModuleOrLink
-
def
setOrigin(o: Origin): Unit
- Definition Classes
- StructuralElement
-
val
statements: HashMap[LocalName, Declaration]
the set of named statements, indexed by name if a statement has an alternativeName, it occurs twice in this map
the set of named statements, indexed by name if a statement has an alternativeName, it occurs twice in this map
- Attributes
- protected
- Definition Classes
- ModuleOrLink
-
def
streamInnerNodes(rh: RenderingHandler): Unit
- Definition Classes
- ModuleOrLink
-
def
superModule: Option[MPath]
- Definition Classes
- Module
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toNode(rh: RenderingHandler): Unit
overridden for streaming
-
def
toNode: Elem
XML representation
-
def
toNodeElab: Elem
- Definition Classes
- Theory
-
def
toString(): String
outerString, definiens, innerString
outerString, definiens, innerString
- Definition Classes
- ModuleOrLink → AnyRef → Any
-
def
toTerm: OMID
this element as a module expression
this element as a module expression
- Definition Classes
- Module → ModuleOrLink → ContentElement
- def translate(newNS: DPath, newName: LocalName, translator: Translator, context: Context): Theory
-
def
translateDf(translator: Translator, context: Context): TermContainer
- Definition Classes
- HasDefiniens
- def universe(synType: GlobalName)(semType: SemanticType): Unit
-
def
universe(rt: RealizedType): Unit
adds a rule for implementing a type
-
def
update(s: Declaration): Unit
updates a named declaration (preserving the order)
updates a named declaration (preserving the order)
- Definition Classes
- ModuleOrLink → MutableElementContainer
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()