Packages

sealed trait Context[+T <: Expression] extends (Expression) ⇒ Formula

Convenience wrapper around contexts such as f(.) or p(.) or C{_} to make it easy to instantiate their arguments.

T

the type/kind of expression that this context is representing.

Example:
  1. Split a formula at a position into subformula and its context, then instantiate this context with other subformulas:

    val parser = KeYmaeraXParser
    val f = parser("x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1")
    // split f into context ctx and subformula g such that f is ctx{g}
    val (ctx,g) = Context.at(f, PosInExpr(1::1::Nil))
    println(f + " is the same as " + ctx(g))
    // put another formula h in in place of g
    val h = parser("x^2>y")
    // x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x^2>y)
    val result = ctx(h)
    println(result)
Linear Supertypes
(Expression) ⇒ Formula, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Context
  2. Function1
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def apply(e: Expression): Formula

    Return the result of instantiating this context with argument e.

    Return the result of instantiating this context with argument e. That is filling the respective dot placeholder of this context with expression e.

    Definition Classes
    Context → Function1
  2. abstract def ctx: T

    the expression of type T representing this context.

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 andThen[A](g: (Formula) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  5. def apply(c: Context[Formula]): Context[Formula]

    Return the result of instantiating this context with an argument c which is itself again a context.

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Formula
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  11. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def isDifferentialProgramContext: Boolean

    True if this context has a DotProgram so expects a program as argument

  15. def isFormulaContext: Boolean

    True if this context has a DotFormula so expects a formula as argument

  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  17. def isProgramContext: Boolean

    True if this context has a DotProgram so expects a program as argument

  18. def isTermContext: Boolean

    True if this context has a DotTerm so expects a term as argument

  19. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  23. def toString(): String
    Definition Classes
    Context → Function1 → AnyRef → Any
  24. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  25. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from (Expression) ⇒ Formula

Inherited from AnyRef

Inherited from Any

Ungrouped