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.  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

   DLBelleParser → TacticParser

6.  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.

7.  def argList[_, A](p: ⇒ P[A])(implicit arg0: P[Any]): P[List[A]]
8.  def argument[_](argInfo: ArgInfo)(implicit arg0: P[Any]): P[Seq[Any]]
9.  def argumentInterior[_](argInfo: ArgInfo)(implicit arg0: P[Any]): P[Seq[Any]]
10.  def argumentList[_](isStart: Boolean, args: List[ArgInfo], numPosArgs: Int)(implicit arg0: P[Any]): P[(List[Seq[Any]], List[PositionLocator])]
11.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

12.  def at[_](implicit arg0: P[Any]): P[BelleExpr]
13.  def atomicTactic[_](implicit arg0: P[Any]): P[BelleExpr]
14.  def baseTac[_](implicit arg0: P[Any]): P[BelleExpr]
15.  def baseVariable[_](implicit arg0: P[Any]): P[BaseVariable]
16.  val belleParser: (String) ⇒ BelleExpr

    Parse the input string in the concrete syntax as a differential dynamic logic expression

17.  def blank[_](implicit arg0: P[Any]): P[Unit]

    Explicit nonempty whitespace terminal from expParser.

18.  def branchTac[_](implicit arg0: P[Any]): P[BelleExpr]
19.  def builtinTactic[_](implicit arg0: P[Any]): P[BelleExpr]
20.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

21.  def compose[A](g: (A) ⇒ String): (A) ⇒ BelleExpr

    Definition Classes

    Function1

    Annotations

    @unspecialized()

22.  def eitherTac[_](implicit arg0: P[Any]): P[BelleExpr]
23.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

24.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

25.  def escapedPositionExpression[_](implicit arg0: P[Any]): P[(Expression, PosInExpr)]
26.  def escapedString[_](implicit arg0: P[Any]): P[String]
27.  def expression[_](implicit arg0: P[Any]): P[Expression]

    expression: Parses a dL expression from expParser.

28.  val expressionParser: Parser

    The expression parser for differential dynamic logic

    The expression parser for differential dynamic logic

    Definition Classes

    DLBelleParser → TacticParser

29.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

30.  def formula[_](implicit arg0: P[Any]): P[Formula]

    formula: Parses a dL formula from expParser.

31.  def fullTactic[_](implicit arg0: P[Any]): P[BelleExpr]
32.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

33.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

34.  def ident[_](implicit arg0: P[Any]): P[(String, Option[Int])]

    parse an identifier from expParser

35.  def integer[_](implicit arg0: P[Any]): P[Int]
36.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

37.  def locator[_](implicit arg0: P[Any]): P[PositionLocator]
38.  def natural[_](implicit arg0: P[Any]): P[Int]
39.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

40.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

41.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

42.  def number[_](implicit arg0: P[Any]): P[Number]

    parse a number literal from expParser

43.  def optionTac[_](implicit arg0: P[Any]): P[BelleExpr]
44.  def parenTac[_](implicit arg0: P[Any]): P[BelleExpr]
45.  def partialTac[_](implicit arg0: P[Any]): P[BelleExpr]
46.  def posInExpr[_](implicit arg0: P[Any]): P[PosInExpr]
47.  def position[_](implicit arg0: P[Any]): P[Position]
48.  def positionLocator[_](implicit arg0: P[Any]): P[PositionLocator]
49.  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

    DLBelleParser → TacticParser

50.  def program[_](implicit arg0: P[Any]): P[Program]

    program: Parses a dL program from expParser.

51.  def repTac[_](implicit arg0: P[Any]): P[BelleExpr]
52.  def searchLocator[_](implicit arg0: P[Any]): P[PositionLocator]
53.  def seqTac[_](implicit arg0: P[Any]): P[BelleExpr]
54.  def setDefTactics(defs: Map[String, DefTactic]): Unit

    Sets the defined tactics to be used during parsing.

    Sets the defined tactics to be used during parsing.

    Definition Classes

    DLBelleParser → DLTacticParser

55.  def setDefs(defs: Declaration): Unit

    Sets the definitions to be used when parsing tactic expressions.

    Sets the definitions to be used when parsing tactic expressions. Expected to be set before apply or tactic are used.

    Definition Classes

    DLBelleParser → DLTacticParser

56.  def shape[_](implicit arg0: P[Any]): P[(String, (Expression, PosInExpr))]
57.  def string[_](implicit arg0: P[Any]): P[String]
58.  def substPair[_](implicit arg0: P[Any]): P[SubstitutionPair]
59.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

60.  def tactic[_](implicit arg0: P[Any]): P[BelleExpr]

    tactic: Parses a dL Bellerophon tactic.

    tactic: Parses a dL Bellerophon tactic.

    Definition Classes

    DLBelleParser → DLTacticParser

61.  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

    DLBelleParser → TacticParser

62.  def tacticSymbol[_](implicit arg0: P[Any]): P[String]
63.  def term[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]

    term: Parses a dL term from expParser.

64.  def toString(): String

    Definition Classes

    Function1 → AnyRef → Any

65.  def usingTac[_](implicit arg0: P[Any]): P[BelleExpr]
66.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

67.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

68.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )