Packages

package parser

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. case class BelleBinaryOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean) extends BelleOpSpec with Product with Serializable
  2. case class BelleBranchingOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Seq[BelleExpr]) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  3. case class BelleDefTacticOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (String, BelleExpr) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  4. case class BelleLetOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Expression, Expression, BelleExpr) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  5. sealed trait BelleOpSpec extends AnyRef

    Note

    Needs some work because the constructors for Belle expressions are far more diverse than the constructors for KeYmaera X expressions

  6. case class BelleRepeatOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (BelleExpr, Int, BelleType) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  7. case class BelleSaturatingOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (BelleExpr, BelleType) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  8. sealed abstract class BelleTerminal extends AnyRef
  9. case class BelleUSubstOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Seq[(BelleType, (RenUSubst) ⇒ BelleExpr)]) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
  10. case class BelleUnaryOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean) extends BelleOpSpec with Product with Serializable
  11. case class BelleUnitOpSpec[T, S](terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (T) ⇒ S) extends BelleOpSpec with Product with Serializable
  12. class DLBelleParser extends DLTacticParser

    Bellerophon tactic parser for Differential Dynamic Logic reads input strings in the concrete syntax of Bellerophon tactics for KeYmaera X.

    Bellerophon tactic parser for Differential Dynamic Logic reads input strings in the concrete syntax of Bellerophon tactics for KeYmaera X. It uses tacticProvider to map names and inputs to concrete tactic expressions.

    See also

    BelleParser

  13. class DLMockBelleParser extends DLTacticParser
  14. trait DLTacticParser extends TacticParser

    DL tactic parser with fastparse-compatible entry point.

  15. case class PosInBelleExpr(idxs: Seq[Int]) extends Product with Serializable

    Used to indicate the position in an expression.

    Used to indicate the position in an expression. Usually for error reporing purposes.

  16. class PositionException extends Exception
  17. case class PrinterException(msg: String) extends Exception with Product with Serializable
  18. trait TacticParser extends (String) ⇒ BelleExpr

    Parser interface for Bellerophon tactics of KeYmaera X.

    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.

Value Members

  1. object BRANCH_COMBINATOR extends BelleTerminal
  2. object BelleLexer extends (String) ⇒ List[BelleToken] with Logging

    A lexer for the Bellerophon tactics language.

  3. object BelleOpSpec
  4. object BelleParseException
  5. object BelleParser extends TacticParser with Logging

    The Bellerophon parser

    The Bellerophon parser

    See also

    DLBelleParser

  6. object BellePrettyPrinter extends (BelleExpr) ⇒ String

    A pretty-printer for the Bellerophon tactics language.

    A pretty-printer for the Bellerophon tactics language.

    Note

    Prefer this implementation over BelleExpr.prettyString.

  7. object CLOSE_PAREN extends BelleTerminal
  8. object COLON extends BelleTerminal
  9. object COMMA extends BelleTerminal
  10. object EOF extends BelleTerminal
  11. object OPEN_PAREN extends BelleTerminal
  12. object SEQ_COMBINATOR extends BelleTerminal

Ungrouped