Packages

trait DLTacticParser extends TacticParser

DL tactic parser with fastparse-compatible entry point.

Linear Supertypes
TacticParser, (String) ⇒ BelleExpr, AnyRef, Any
Known Subclasses
DLBelleParser, DLMockBelleParser
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DLTacticParser
  2. TacticParser
  3. Function1
  4. AnyRef
  5. 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.

    Definition Classes
    TacticParser
    Exceptions thrown

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

  2. abstract val expressionParser: Parser

    The expression parser for differential dynamic logic

    The expression parser for differential dynamic logic

    Definition Classes
    TacticParser
  3. abstract val printer: (BelleExpr) ⇒ String

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

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

    Definition Classes
    TacticParser
  4. abstract def setDefTactics(defs: Map[String, DefTactic]): Unit

    Sets the defined tactics to be used during parsing.

  5. abstract def setDefs(defs: Declaration): Unit

    Sets the definitions to be used during parsing.

  6. abstract def tactic[_](implicit arg0: P[Any]): P[BelleExpr]

    Parses a dL Bellerophon tactic.

  7. abstract val tacticParser: (String) ⇒ BelleExpr

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

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

    Definition Classes
    TacticParser

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 TacticParser

Inherited from (String) ⇒ BelleExpr

Inherited from AnyRef

Inherited from Any

Ungrouped