Packages

case class Context(variables: VarDecl*) extends Obj with ElementContainer[VarDecl] with DefaultLookup[VarDecl] with Product with Serializable

An MMT context as a list of variable declarations VarDecl.

Being a list especially implies that there is an **order of the entries**. For example, this is important when using the Context in an OMBINDC to represent a lambda term: (λxy. x + y) will be represented as OMBINDC whose context has VarDecl entries "x", "y" in that order.
Another situation where order is important is when later VarDecl declarations refer to previous ones.

Note that variables is not necessarily meant in a strict sense of only variables, namely a context can also include declarations of a whole theory and all of its (transitively) included theories by use of IncludeVarDecl. There is an helper apply method on the companion object of Context: scala Context(MPath(/* ... */))

variables

The context's variables

Source
Context.scala
Linear Supertypes
Serializable, Serializable, Product, Equals, DefaultLookup[VarDecl], ElementContainer[VarDecl], Obj, HashEquality[Obj], ShortURIPrinter, BaseType, Content, ClientProperties, HasMetaData, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Context
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. DefaultLookup
  7. ElementContainer
  8. Obj
  9. HashEquality
  10. ShortURIPrinter
  11. BaseType
  12. Content
  13. ClientProperties
  14. HasMetaData
  15. AnyRef
  16. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Context(variables: VarDecl*)

    variables

    The context's variables

Type Members

  1. type ThisType = Context

    the type of this instance

    the type of this instance

    This is needed to provide sharper return types for inductive functions, e.g., substitution returns Term if applied to Term, Context if applied to Context, etc.

    Definition Classes
    Context → Obj

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(that: Context): Context

    concatenate contexts

  4. def ++(v: VarDecl): Context

    add variable at the end

  5. def ++(p: MPath): Context

    add a theory inclusion at the end

  6. def /(args: List[Term]): Option[Substitution]

    returns

    substitution that maps variables according to args, None if lengths do not match

  7. def /!(args: List[Term]): Substitution
  8. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def ^(sub: Substitution): ThisType

    applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier

    applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier

    Definition Classes
    Obj
  10. def ^?(sub: Substitution): ThisType

    optimized version of substitution defined in terms of SmartSubstitutionApplier

    optimized version of substitution defined in terms of SmartSubstitutionApplier

    Definition Classes
    Obj
  11. def ^^(sub: Substitution)(implicit sa: SubstitutionApplier): ThisType

    convenience method that applies substitution by relegating to a SubstitutionApplier

    convenience method that applies substitution by relegating to a SubstitutionApplier

    This has the effect that o ^^ sub becomes an infix notation for substitution if an implicit SubstitutionApplier is available.

    Definition Classes
    Obj
  12. def after(name: LocalName): Context

    returns

    the suffix after and excluding the variable

  13. def alpha(that: Context): Option[Substitution]

    if c1 and c2 have the same length, then (c1 alpha c2 : c1 -> c2) is the substitution mapping corresponding variables

    if c1 and c2 have the same length, then (c1 alpha c2 : c1 -> c2) is the substitution mapping corresponding variables

    This substitution can be used to alpha-rename c1-objects to c2-objects.

  14. def apply(name: LocalName): VarDecl

    look up a variable by name, throws LookupError if not declared

  15. def asDeclarations(home: Term): List[Declaration]
  16. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  17. def before(name: LocalName): Context

    returns

    the prefix up to and excluding the variable

  18. lazy val clientProperty: ListMap[URI, Any]
    Definition Classes
    ClientProperties
  19. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  20. def copyFrom(o: Obj): Unit

    replaces metadata of this with pointer to those of o

    replaces metadata of this with pointer to those of o

    o

    the original object call o2.copyFrom(o1) after transforming o1 into o2 in order to preserve metadata

    Definition Classes
    Obj
  21. def declsInContext: Iterator[(Context, VarDecl)]

    returns

    an iterator over all declarations in their respective context

  22. def domain: List[LocalName]
    Definition Classes
    DefaultLookup
  23. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  25. lazy val freeVars: List[LocalName]

    the free variables of this object in any order

    the free variables of this object in any order

    Definition Classes
    Obj
  26. def get(name: LocalName): VarDecl
    Definition Classes
    ElementContainer
  27. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  28. def getDeclarations: List[VarDecl]
    Definition Classes
    Context → ElementContainer
  29. def getDeclarationsBefore(n: LocalName): List[VarDecl]
    Definition Classes
    ElementContainer
  30. def getDomain: List[DomainElement]

    returns

    domain of this context, flattening nested ComplexTheories and ComplexMorphisms Due to ComplexMorphism's, names may erroneously be defined but not declared.

  31. def getIncludes: List[MPath]

    all theories directly included into this context

  32. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  33. def getMostSpecific(name: LocalName): Option[(VarDecl, LocalName)]
    Definition Classes
    DefaultLookup
  34. def getO(name: LocalName): Option[VarDecl]
    Definition Classes
    DefaultLookup
  35. def getO(name: String): Option[VarDecl]

    same as get(LocalName(name))

    same as get(LocalName(name))

    Definition Classes
    ElementContainer
  36. def governingPath: Option[ContentPath]

    the governing path required by Content is the head, if any

    the governing path required by Content is the head, if any

    Definition Classes
    Obj
  37. lazy val hash: Int

    the hash code

    the hash code

    Definition Classes
    HashEquality
  38. def hasheq(that: HashEquality[Obj]): Boolean

    this hasheq that is the same as this == that, but fails immediately if false

    this hasheq that is the same as this == that, but fails immediately if false

    Definition Classes
    HashEquality
  39. def hashneq(that: HashEquality[Obj]): Boolean

    this hasheq that is the same as this == that, but fails immediately if false

    this hasheq that is the same as this == that, but fails immediately if false

    Definition Classes
    HashEquality
  40. def head: None.type
    Definition Classes
    Context → Obj
  41. def id: Substitution

    the identity substitution of this context

  42. def index(name: LocalName): Option[Int]

    returns

    the de Bruijn index of the variable, starting from 0

  43. def isDeclared(name: LocalName): Boolean
    Definition Classes
    ElementContainer
  44. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  45. def length: Int
  46. def mapTerms(f: (Context, Term) ⇒ Term): Context

    applies a function to the type/definiens of all variables (in the respective context)

    applies a function to the type/definiens of all variables (in the respective context)

    returns

    the resulting context

  47. def mapVarDecls[A](f: (Context, VarDecl) ⇒ A): List[A]

    applies a function to each VarDecl, each time in the respective context

    applies a function to each VarDecl, each time in the respective context

    returns

    the list of results

  48. def mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Attributes
    protected
    Definition Classes
    Obj
  49. val metadata: MetaData
    Definition Classes
    HasMetaData
  50. def minimalSubContext(req: List[LocalName]): Context

    the subcontext whose variables occur (transitively closed) in the given variables

    the subcontext whose variables occur (transitively closed) in the given variables

    if context |- t, then also context.minimalSubContext(t.freeVars) |- t

  51. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  52. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  53. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  54. def subobject(pos: Position): (Context, Obj)

    returns the subobject at a given position and its context

    returns the subobject at a given position and its context

    Definition Classes
    Obj
  55. def subobjects: List[(Context, Obj)]

    all direct subobjects of this object with their context (excluding any outer context of this object)

    all direct subobjects of this object with their context (excluding any outer context of this object)

    Definition Classes
    Context → Obj
  56. def subobjectsNoContext(os: List[Obj]): List[(Context, Obj)]

    auxiliary function for subobjects in the absence of binding

    auxiliary function for subobjects in the absence of binding

    Attributes
    protected
    Definition Classes
    Obj
  57. def substitute(sub: Substitution)(implicit sa: SubstitutionApplier): Context

    substitutes in all variable declarations except for the previously declared variables if |- G ++ H and |- sub : G -> G' then |- G' ++ (H ^ sub)

    substitutes in all variable declarations except for the previously declared variables if |- G ++ H and |- sub : G -> G' then |- G' ++ (H ^ sub)

    Definition Classes
    Context → Obj
  58. def subsumes(that: Context): Boolean

    true if that is a subcontext (inclusion substitution) of this one

  59. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  60. def toCML: Node
    Definition Classes
    Obj
  61. def toCMLQVars(implicit qvars: Context): Elem
    Definition Classes
    Context → Obj
  62. def toNode: Elem

    prints to OpenMath

    prints to OpenMath

    Definition Classes
    Context → Obj → Content
  63. def toNode(rh: RenderingHandler): Unit

    by default, this prints out toNode

    by default, this prints out toNode

    potentially large StructuralElements should override it with a memory-efficient implementation

    Definition Classes
    Content
  64. def toOBJNode: Elem

    prints to OpenMath (with OMOBJ wrapper)

    prints to OpenMath (with OMOBJ wrapper)

    Definition Classes
    Obj
  65. def toPartialSubstitution: Substitution

    returns this as a substitutions using those variables that have a definiens

  66. def toStr(implicit shortURIs: Boolean): String

    configurable string representation

    configurable string representation

    shortURIs

    print OMS without namespace, theory

    Definition Classes
    Context → ShortURIPrinter
  67. def toString(): String

    defaults to toStr(false)

    defaults to toStr(false)

    Definition Classes
    ShortURIPrinter → AnyRef → Any
  68. def toSubstitution: Option[Substitution]

    returns this as a substitution if all variables have a definiens

  69. val variables: VarDecl*
  70. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  71. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  72. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from DefaultLookup[VarDecl]

Inherited from ElementContainer[VarDecl]

Inherited from Obj

Inherited from HashEquality[Obj]

Inherited from ShortURIPrinter

Inherited from BaseType

Inherited from Content

Inherited from ClientProperties

Inherited from HasMetaData

Inherited from AnyRef

Inherited from Any

Ungrouped