Packages

t

info.kwarc.mmt.lf

SolutionRules

trait SolutionRules extends LFRealizationInScala

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SolutionRules
  2. LFRealizationInScala
  3. RealizationInScala
  4. RealizedTheory
  5. SemanticObject
  6. Theory
  7. AbstractTheory
  8. Module
  9. ModuleOrLink
  10. HasDefiniens
  11. ContainerElement
  12. MutableElementContainer
  13. ElementContainer
  14. ContentElement
  15. StructuralElement
  16. NamedElement
  17. Content
  18. ClientProperties
  19. HasMetaData
  20. AnyRef
  21. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract val _domain: TheoryScala

    the modelled theory

    the modelled theory

    Definition Classes
    RealizationInScala

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def _assert(name: String, term: () ⇒ Term, assertion: (Term) ⇒ Boolean): Unit
    Definition Classes
    RealizationInScala
  5. lazy val _name: LocalName

    the name of the modelled theory

    the name of the modelled theory

    Definition Classes
    RealizationInScala
  6. lazy val _path: MPath

    the MMT URI of the modelled theory

    the MMT URI of the modelled theory

    Definition Classes
    RealizationInScala
  7. def _test(controller: Controller, log: (String) ⇒ Unit): Unit
    Definition Classes
    RealizationInScala
  8. 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
    ModuleOrLinkMutableElementContainer
  9. 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
  10. def asDocument: Document

    the narrative structure

    the narrative structure

    Definition Classes
    ModuleOrLink
  11. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  12. lazy val clientProperty: ListMap[URI, Any]
    Definition Classes
    ClientProperties
  13. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  14. 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
  15. 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
  16. 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
  17. 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
    ModuleOrLinkMutableElementContainer
  18. def df: Option[Term]
    Definition Classes
    HasDefiniens
  19. val dfC: TermContainer
    Definition Classes
    TheoryHasDefiniens
  20. def dfNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Definition Classes
    HasDefiniens
  21. def domain: List[LocalName]

    the list of names of all declarations

    the list of names of all declarations

    Definition Classes
    ModuleOrLinkElementContainer
  22. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  23. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  24. def equivalentTo(that: StructuralElement): Boolean

    logically equivalent: compares headerInfo, components, and declarations

    logically equivalent: compares headerInfo, components, and declarations

    Definition Classes
    StructuralElement
  25. val feature: String

    the kind of declaration, e.g., "constant"

    the kind of declaration, e.g., "constant"

    Definition Classes
    TheoryContentElementStructuralElement
  26. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  27. 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
  28. 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
  29. 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)

    adds a rule for implementing a function symbol (argument and return types must have been added previously)

    Definition Classes
    RealizationInScala
  30. def functionT[U, V](op: GlobalName, argType1: RepresentedRealizedType[U], rType: RepresentedRealizedType[V])(comp: (U) ⇒ V): Unit

    typed variant, experimental, not used by ScalaExporter yet

    typed variant, experimental, not used by ScalaExporter yet

    Definition Classes
    RealizationInScala
  31. def get(name: LocalName): Declaration
    Definition Classes
    ElementContainer
  32. 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
    AbstractTheoryModuleOrLink
  33. def getAllIncludesWithSelf: List[IncludeData]

    Get all transitive-reflexive inclusions.

    Get all transitive-reflexive inclusions.

    Definition Classes
    ModuleOrLink
  34. 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
  35. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  36. def getComponent(k: ComponentKey): Option[ComponentContainer]

    returns a specific component if present

    returns a specific component if present

    Definition Classes
    StructuralElement
  37. 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
  38. def getComponents: List[DeclarationComponent]

    returns all term components of this elements

    returns all term components of this elements

    Definition Classes
    TheoryStructuralElement
  39. def getConstants: List[Constant]

    convenience method to obtain all constants

    convenience method to obtain all constants

    Definition Classes
    AbstractTheory
  40. 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
    ModuleOrLinkElementContainerContentElementStructuralElement
  41. def getDeclarationsBefore(n: LocalName): List[Declaration]
    Definition Classes
    ElementContainer
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
    AbstractTheoryModuleOrLink
  47. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  48. def getMostSpecific(name: LocalName): Option[(Declaration, LocalName)]
    Definition Classes
    ModuleOrLinkElementContainer
  49. def getNamedStructures: List[Structure]

    convenience method to obtain all named structures

    convenience method to obtain all named structures

    Definition Classes
    AbstractTheory
  50. def getO(name: LocalName): Option[Declaration]

    retrieve a declaration

    retrieve a declaration

    Definition Classes
    ModuleOrLinkElementContainer
  51. def getO(name: String): Option[Declaration]

    same as get(LocalName(name))

    same as get(LocalName(name))

    Definition Classes
    ElementContainer
  52. def getOrigin: Origin
    Definition Classes
    StructuralElement
  53. 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
  54. 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
    Definition Classes
    RealizationInScala
  55. def getRealizees: List[IncludeData]

    return all includes that are realizations

    return all includes that are realizations

    Definition Classes
    AbstractTheory
  56. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  57. 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
  58. def headerNodes: Seq[Node]

    common inner nodes: definiens (metadata is part of document)

    common inner nodes: definiens (metadata is part of document)

    Definition Classes
    TheoryModuleOrLink
  59. 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
    RealizedTheorySemanticObject
  60. def innerNodes: NodeSeq

    getPrimitiveDeclarations, with narrative structure

    getPrimitiveDeclarations, with narrative structure

    Attributes
    protected
    Definition Classes
    ModuleOrLink
  61. def innerNodesElab: List[Node]

    getDeclarationsElaborated, without narrative structure

    getDeclarationsElaborated, without narrative structure

    Attributes
    protected
    Definition Classes
    ModuleOrLink
  62. def innerString: String

    body as a string

    body as a string

    Definition Classes
    ModuleOrLink
  63. def inverse(op: GlobalName, aTypesN: List[GlobalName], rTypeN: GlobalName)(fun: InvFunctionN): Unit

    the partial inverse of an n-ary operator

    the partial inverse of an n-ary operator

    Definition Classes
    RealizationInScala
  64. def inverse(op: GlobalName, aTypeN: GlobalName, rTypeN: GlobalName)(comp: (Any) ⇒ Option[Any]): Unit

    the partial inverse of a unary operator

    the partial inverse of a unary operator

    Definition Classes
    RealizationInScala
  65. def isDeclared(name: LocalName): Boolean
    Definition Classes
    ElementContainer
  66. def isEmpty: Boolean

    true iff no declarations present

    true iff no declarations present

    Definition Classes
    ModuleOrLink
  67. def isGenerated: Boolean
    Definition Classes
    StructuralElement
  68. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  69. 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
  70. def meta: Option[MPath]

    the meta-theory

    the meta-theory

    Definition Classes
    TheoryAbstractTheory
  71. val metaC: TermContainer

    the container of the meta-theory

    the container of the meta-theory

    Definition Classes
    Theory
  72. val metadata: MetaData
    Definition Classes
    HasMetaData
  73. def modulePath: MPath

    path if seen as a module

    path if seen as a module

    Definition Classes
    ModuleOrLink
  74. 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
  75. val name: LocalName

    local name relative to the parent element or namespace

    local name relative to the parent element or namespace

    Definition Classes
    RealizedTheoryModuleContentElementNamedElement
  76. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  77. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  78. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  79. def outerString: String

    header as a string (without definiens)

    header as a string (without definiens)

    Definition Classes
    TheoryModuleOrLink
  80. val paramC: ContextContainer
    Definition Classes
    Theory
  81. def parameters: Context

    the parameters

    the parameters

    Definition Classes
    TheoryAbstractTheory
  82. val parent: DPath

    the containing knowledge item, a URL if none

    the containing knowledge item, a URL if none

    Definition Classes
    RealizedTheoryModuleStructuralElement
  83. var parentDoc: Option[DPath]
    Definition Classes
    Module
  84. def path: MPath

    the MMT URI of the element

    the MMT URI of the element

    Definition Classes
    ModuleContentElementStructuralElement
  85. def realizes(b: ⇒ Unit): Unit
    Attributes
    protected
    Definition Classes
    RealizationInScala
  86. 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
    ModuleOrLinkMutableElementContainer
  87. 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

    Definition Classes
    RealizationInScala
  88. def selfInclude: IncludeData

    Get self inclusion.

    Get self inclusion.

    Definition Classes
    AbstractTheoryModuleOrLink
  89. def setOrigin(o: Origin): Unit
    Definition Classes
    StructuralElement
  90. def solve_binary_left(op: GlobalName, argType1N: GlobalName, argType2N: GlobalName, rTypeN: GlobalName)(invert: (Any, Any) ⇒ Option[Any]): Unit
  91. def solve_binary_right(op: GlobalName, argType1N: GlobalName, argType2N: GlobalName, rTypeN: GlobalName)(invert: (Any, Any) ⇒ Option[Any]): Unit
  92. def solve_unary(op: GlobalName, argTypeN: GlobalName, rTypeN: GlobalName)(invert: (Any) ⇒ Option[Any]): Unit
  93. 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
  94. def streamInnerNodes(rh: RenderingHandler): Unit
    Definition Classes
    ModuleOrLink
  95. def superModule: Option[MPath]
    Definition Classes
    Module
  96. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  97. def toNode(rh: RenderingHandler): Unit

    overridden for streaming

    overridden for streaming

    Definition Classes
    TheoryContent
  98. def toNode: Elem

    XML representation

    XML representation

    Definition Classes
    TheoryContent
  99. def toNodeElab: Elem
    Definition Classes
    Theory
  100. def toString(): String

    outerString, definiens, innerString

    outerString, definiens, innerString

    Definition Classes
    ModuleOrLink → AnyRef → Any
  101. def toTerm: OMID

    this element as a module expression

    this element as a module expression

    Definition Classes
    ModuleModuleOrLinkContentElement
  102. def translate(newNS: DPath, newName: LocalName, translator: Translator, context: Context): Theory
    Definition Classes
    TheoryModule
  103. def translateDf(translator: Translator, context: Context): TermContainer
    Definition Classes
    HasDefiniens
  104. val under: List[GlobalName]

    the HOAS apply operators in applications

    the HOAS apply operators in applications

    Definition Classes
    LFRealizationInScalaRealizationInScala
  105. def universe(synType: GlobalName)(semType: SemanticType): Unit
    Definition Classes
    RealizationInScala
  106. def universe(rt: RealizedType): Unit

    adds a rule for implementing a type

    adds a rule for implementing a type

    Definition Classes
    RealizationInScala
  107. def update(s: Declaration): Unit

    updates a named declaration (preserving the order)

    updates a named declaration (preserving the order)

    Definition Classes
    ModuleOrLinkMutableElementContainer
  108. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  109. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  110. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from LFRealizationInScala

Inherited from RealizationInScala

Inherited from RealizedTheory

Inherited from SemanticObject

Inherited from Theory

Inherited from AbstractTheory

Inherited from Module

Inherited from ModuleOrLink

Inherited from HasDefiniens

Inherited from ContainerElement[Declaration]

Inherited from ElementContainer[Declaration]

Inherited from ContentElement

Inherited from StructuralElement

Inherited from NamedElement

Inherited from Content

Inherited from ClientProperties

Inherited from HasMetaData

Inherited from AnyRef

Inherited from Any

Ungrouped