Packages

trait TacticParser extends (String) ⇒ BelleExpr

Parser interface for Bellerophon tactics of KeYmaera X. Provides a parser to read string inputs as a Bellerophon tactic. A parser is a function from input strings to Bellerophon expressions.

Parser: String => BelleExpr

Parsers are adjoint to printers, i.e., they reparse printed expressions as the original expressions but fail to parse syntactically ill-formed strings:

parser(printer(tactic)) == tactic
See also

Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer. Bellerophon: Tactical theorem proving for hybrid systems. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. Springer, 2017.

Linear Supertypes
(String) ⇒ BelleExpr, AnyRef, Any
Known Subclasses
BelleParser, DLBelleParser, DLMockBelleParser, DLTacticParser
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TacticParser
  2. Function1
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def apply(input: String, defs: Declaration): BelleExpr

    Parse the input string in the concrete syntax of Bellerophon tactics.

    Parse the input string in the concrete syntax of Bellerophon tactics.

    input

    the string to parse as a Bellerophon tactic.

    defs

    the definitions to elaborate variables/functions/predicates to their expected type.

    Exceptions thrown

    ParseException if input is not a well-formed Bellerophon tactic.

  2. abstract val expressionParser: Parser

    The expression parser for differential dynamic logic

  3. abstract val printer: (BelleExpr) ⇒ String

    A pretty-printer that can write the output that this parser reads

  4. abstract val tacticParser: (String) ⇒ BelleExpr

    Parse the input string in the concrete syntax as a Bellerophon tactic

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: (BelleExpr) ⇒ A): (String) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  5. final def apply(input: String): BelleExpr

    Parse the input string in the concrete syntax of Bellerophon tactics.

    Parse the input string in the concrete syntax of Bellerophon tactics.

    input

    the string to parse as a Bellerophon tactic.

    Definition Classes
    TacticParser → Function1
    Exceptions thrown

    ParseException if input is not a well-formed Bellerophon tactic.

  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) ⇒ String): (A) ⇒ BelleExpr
    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. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  19. def toString(): String
    Definition Classes
    Function1 → AnyRef → Any
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from (String) ⇒ BelleExpr

Inherited from AnyRef

Inherited from Any

Ungrouped