Packages

package parser

Parser & Pretty-Printer for Differential Dynamic Logic

Defines the concrete syntax of differential dynamic logic as used in KeYmaera X. Provides a parser to read string and file inputs with differential dynamic logic. Conversely provides a pretty-printer to format differential dynamic logic expression data structure as human readable concrete syntax.

PrettyPrinter: Expression => String
Parser: String => Expression

Usage Overview

The default pretty-printer for the concrete syntax in KeYmaera X is in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter. The corresponding parser for the concrete syntax in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser. Also see Grammar of KeYmaera X Syntax

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)
Printing Differential Dynamic Logic

edu.cmu.cs.ls.keymaerax.parser.PrettyPrinter defines the interface for all differential dynamic logic pretty printers in KeYmaera X.

PrettyPrinter: Expression => String

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter implements the pretty-printer for the concrete syntax of differential dynamic logic used in KeYmaera X. A pretty-printer is essentially a function from differential dynamic logic expressions to strings.

Printing formulas to strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter.apply:

val pp = KeYmaeraXPrettyPrinter
// "x < -y"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> [x:=1;]x>=0"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)
Printing Fully Parenthesized Forms

Fully parenthesized strings are obtained using the edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter printer:

val pp = FullPrettyPrinter
// "x < -(y)"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> ([x:=1;](x>=0))"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)

The fully-parenthesized pretty printer corresponding to a pretty printer can also be obtained using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrinter.fullPrinter

Parsing Differential Dynamic Logic

edu.cmu.cs.ls.keymaerax.parser.Parser defines the interface for all differential dynamic logic parsers in KeYmaera X.

Parser: String => Expression

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser implements the parser for the concrete syntax of differential dynamic logic used in KeYmaera X. A parser is essentially a function from input string to differential dynamic logic expressions.

Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:

val parser = KeYmaeraXParser
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")

The parser parses any dL expression, so will also accept terms or programs from strings, which will lead to appropriate types:

val parser = KeYmaeraXParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms
val term0 = parser("x+5")
val term1 = parser("x^2-2*x+7")
val term2 = parser("x*y/3+(x-1)^2+5*z")
// programs
val prog0 = parser("x:=1;")
val prog1 = parser("x:=1;x:=5;x:=-1;")
val prog2 = parser("x:=1;{{x'=5}++x:=0;}")
Parsing Only Formulas of Differential Dynamic Logic

The parser that only parses formulas is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.formulaParser

// the formula parser only accepts formulas
val parser = KeYmaeraXParser.formulaParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms will cause exceptions
try { parser("x+5") } catch {case e: ParseException => println("Rejected")}
// programs will cause exceptions
try { parser("x:=1;") } catch {case e: ParseException => println("Rejected")}

Similarly, a parser that only parses terms is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.termParser and a parser that only parses programs is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.programParser

Parsing Pretty-Printed Strings

Corresponding parsers and pretty-printers match with one another. Parsing a pretty-printed expression results in the original expression again:

parse(print(e)) == e

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser and are inverses in this sense. The converse print(parse(s)) == s is not quite the case, because there can be minor spacing and superfluous parentheses differences. The following slightly weaker form still holds:

parse(print(parse(s))) == parse(s)

Parsing the pretty-print of an expression with compatible printers and parsers always gives the original expression back:

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val fml = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
// something like "true -> [x:=1;]x>=0" modulo spacing
val print = pp(fml)
val reparse = parser(print)
if (fml == reparse) println("Print and reparse successful") else println("Discrepancy")
Pretty-Printing Parsed Strings

It can be quite helpful to print an expression that has been parsed to check how it got parsed:

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)
println("Original: " + input)
println("Can differ slightly by spacing and parentheses")

Recall that the default pretty printer uses compact parentheses and braces. That is, it only prints them when necessary to disambiguate. For storage purposes and disambiguation it can be better to use fully parenthesized printouts, which is what edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter achieves:

val parser = KeYmaeraXParser
val pp = FullPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
// (((x)^(2)>=0)&(x < 44))->([{x:=2;}{{x'=1&x<=10}}](x>=1))
println("Printed:  " + print)
println("Original: " + input)
Pretty-Printing Sequents

Sequents can be pretty-printed using the default pretty printer via edu.cmu.cs.ls.keymaerax.core.Sequent.prettyString

val parser = KeYmaeraXParser
val sequent = Sequent(IndexedSeq(parse("x<22"), parse("x>0")), IndexedSeq(parse("[x:=x+1;]x<23")))
println("Printed:  " + sequent.prettyString)
See also

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser

Grammar of Differential Dynamic Logic

"Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015."

Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. parser
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class :+[A](tail: Stack[A], top: A) extends Stack[A] with Product with Serializable

    A stack tail :+ top with top on the top of tail

  2. trait BasePrettyPrinter extends PrettyPrinter

    Common base functionality for KeYmaera X Pretty Printers.

  3. trait BinaryNotation extends OpNotation

    Notational specification for binary operators of arity 2

  4. case class BinaryOpSpec[T <: Expression](op: Terminal, prec: Int, assoc: BinaryNotation, kind: (Kind, Kind), const: (String, T, T) ⇒ T) extends OpSpec with Product with Serializable

    Binary operator notation specification with a constructor and expected argument kinds.

  5. case class ExternalEvidence() extends Evidence with Product with Serializable
  6. class KeYmaeraXArchivePrinter extends (ParsedArchiveEntry) ⇒ String

    Prints a KeYmaera X archive.

    Prints a KeYmaera X archive.

    Format example:

    ArchiveEntry "Entry 1".
      Functions. ... End.
      ProgramVariables. ... End.
      Problem. ... End.
      Tactic "Proof 1". ... End.
      Tactic "Proof 2". ... End.
    End.
    Lemma "Entry 2". ... End.

    Created by smitsch on 01/04/18.

  7. class KeYmaeraXPrecedencePrinter extends KeYmaeraXSkipPrinter

    Precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    Precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    To do

    Augment with ensuring postconditions that check correct reparse non-recursively.

    See also

    Grammar

  8. class KeYmaeraXPrinter extends BasePrettyPrinter

    Vanilla: KeYmaera X Printer formats differential dynamic logic expressions in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    Vanilla: KeYmaera X Printer formats differential dynamic logic expressions in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    Example:
    1. Printing formulas to strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter.apply:

      val pp = KeYmaeraXPrettyPrinter
      // "x < -y"
      val fml0 = Less(Variable("x"),Neg(Variable("y")))
      val fml0str = pp(fml0)
      // "true -> [x:=1;]x>=0"
      val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
      val fml1str = pp(fml1)
    To do

    Augment with ensuring postconditions that check correct reparse non-recursively.

    See also

    Grammar

  9. abstract class KeYmaeraXSkipPrinter extends KeYmaeraXPrinter

    KeYmaera X Printer base class formatting based on parentheses skipping decisions.

  10. class KeYmaeraXWeightedPrettyPrinter extends KeYmaeraXPrecedencePrinter

    Weighted precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according and extra space weighted according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    Weighted precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according and extra space weighted according to the concrete syntax of differential dynamic logic with explicit statement end ; operator.

    See also

    Grammar

  11. sealed abstract class LexerMode extends AnyRef

    LexerModes corresponds to file types.

  12. sealed trait Location extends Serializable

    The location where a Terminal is located in an input stream.

    The location where a Terminal is located in an input stream.

    Note

    Serializable to make sure sbt test allows Location in ParseException errors.

  13. trait NullaryNotation extends OpNotation

    Notational specification for nullary operators of arity 0

  14. sealed trait OpNotation extends AnyRef

    Operator associativity notational specification

  15. trait OpSpec extends Ordered[OpSpec]

    Operator notation specification with precedence and associativity.

    Operator notation specification with precedence and associativity.

    To do

    Could add spacing weight information to determine how much spacing is added around an operator. Alternatively, spacing weight can be inferred from the prec numerics and how far they are apart.

  16. case class ParseException(msg: String, loc: Location, found: String, expect: String, after: String, state: String, cause: Throwable = null) extends ProverException with Product with Serializable

    Indicates a parse error at the given location, with the context information state.

    Indicates a parse error at the given location, with the context information state.

    See also

    ProverException.getContext

  17. trait Parser extends (String) ⇒ Expression

    Parser interface for KeYmaera X.

    Parser interface for KeYmaera X. Provides a parser to read string and file inputs with differential dynamic logic. A parser is essentially a function from input string to differential dynamic logic expressions.

    Parser: String => Expression
  18. trait PrettyPrinter extends (Expression) ⇒ String

    Pretty-Printer interface for KeYmaera X.

    Pretty-Printer interface for KeYmaera X. A pretty-printer formats the differential dynamic logic expression data structure as human readable concrete syntax. A pretty-printer is essentially a function from differential dynamic logic expressions to strings.

    PrettyPrinter: Expression => String
    See also

    edu.cmu.cs.ls.keymaerax.core.PrettyPrinter

  19. case class ProofEvidence() extends Evidence with Product with Serializable
  20. case class Region(line: Int, column: Int, endLine: Int, endColumn: Int) extends Location with Product with Serializable
  21. sealed trait Stack[+A] extends AnyRef

    Stack with top on the right.

    Stack with top on the right. For example the stack Bottom :+ a3 :+ a2 +: a1 has element a1 on the top, then a2 as the top of the tail.

  22. class StringConverter extends AnyRef
  23. case class SuffixRegion(line: Int, column: Int) extends Location with Product with Serializable

    Like a region, but extends until the end of the input.

    Like a region, but extends until the end of the input.

    line

    The starting line.

    column

    The ending line.

  24. sealed abstract class Terminal extends AnyRef

    Terminal symbols of the differential dynamic logic grammar.

  25. trait TernaryNotation extends OpNotation

    Notational specification for ternary operators of arity 3

  26. case class TernaryOpSpec[T <: Expression](op: Terminal, op2: Terminal, op3: Terminal, prec: Int, assoc: TernaryNotation, kind: (Kind, Kind, Kind), const: (String, T, T, T) ⇒ T) extends OpSpec with Product with Serializable

    Ternary operator notation specification with one terminal per operand, with constructor and expected argument kinds.

  27. trait TokenParser extends AnyRef
  28. trait UnaryNotation extends OpNotation

    Notational specification for unary operators of arity 1

  29. case class UnaryOpSpec[T <: Expression](op: Terminal, prec: Int, assoc: UnaryNotation, kind: Kind, const: (String, T) ⇒ T) extends OpSpec with Product with Serializable

    Unary operator notation specification with a constructor and expected argument kind.

  30. case class UnitOpSpec(op: Terminal, prec: Int, const: (String) ⇒ Expression) extends OpSpec with Product with Serializable

    Nullary operator notation specification with a constructor.

Value Members

  1. final def checkInput(requirement: Boolean, message: ⇒ Any, loc: ⇒ Location, state: ⇒ String): Unit

    Check input for requirement being true, throwing a ParseException if false.

    Check input for requirement being true, throwing a ParseException if false. This method is a require coming from the parser that cannot be disabled. Blame is on the user input.

    requirement

    the expression to test for being true

    message

    a String explaining what is expected.

    loc

    the location where the parse error occurred.

    state

    information about the parser state in which the parse error occurred.

    Annotations
    @inline()
    See also

    scala.Predef.require()

  2. object AtomicBinaryFormat extends BinaryNotation

    Atomic operators of arity 0 within syntactic category with 2 arguments from lower category

  3. object AtomicFormat extends NullaryNotation

    Atomic operators of arity 0 within syntactic category

  4. object AxiomFileMode extends LexerMode
  5. object BinaryOpSpec extends Serializable
  6. object Bottom extends Stack[Nothing]

    The empty stack bottom

  7. object EOF extends Terminal

    End Of Stream

  8. object ExpressionMode extends LexerMode
  9. object FullPrettyPrinter extends BasePrettyPrinter

    Fully-parenthesized pretty printer in full form with full parentheses.

    Fully-parenthesized pretty printer in full form with full parentheses.

    Example:
    1. Fully parenthesized strings are obtained using the edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter printer:

      val pp = FullPrettyPrinter
      // "x < -(y)"
      val fml0 = Less(Variable("x"),Neg(Variable("y")))
      val fml0str = pp(fml0)
      // "true -> ([x:=1;](x>=0))"
      val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
      val fml1str = pp(fml1)
    See also

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrinter.fullPrinter

  10. object FullPrettyPrinter0 extends KeYmaeraXPrinter

    Fully parenthesized pretty printer that is functionally equivalent to FullPrettyPrinter

  11. object KeYmaera3PrettyPrinter extends KeYmaeraXPrecedencePrinter

    Differential Dynamic Logic pretty printer in concrete KeYmaera 3 notation.

  12. object KeYmaeraXArchiveParser

    Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers.

    Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers. An archive contains at least one entry combining a model in the .kyx format and a (partial) proof tactic in .kyt format.

    Format example:

    ArchiveEntry "Entry 1".
      Functions. ... End.
      ProgramVariables. ... End.
      Problem. ... End.
      Tactic "Proof 1". ... End.
      Tactic "Proof 2". ... End.
    End.
    ArchiveEntry "Entry 2". ... End.
  13. object KeYmaeraXAxiomParser extends (String) ⇒ List[(String, Formula)] with Logging

    Parse an axiom string to a list of named formulas that are to be used as axioms in a theory.

    Parse an axiom string to a list of named formulas that are to be used as axioms in a theory. Created by nfulton on 6/11/15.

  14. object KeYmaeraXExtendedLemmaParser extends (String) ⇒ (Option[String], List[Sequent], List[Evidence]) with Logging

    Lemma format is as follows:

    Lemma format is as follows:

    Sequent.
      Formula: <<formula>>
      ...
      ==>
      Formula: <<formula>>
      ...
    Sequent.
      ...
    End.
    Tool.
      <<key>> """"<<value>>""""
      ...
    End.

    Created by smitsch on 7/03/15. Modified by nfulton on 12/16/15 -- Lemmas are now more general.

  15. object KeYmaeraXLexer extends (String) ⇒ List[Token] with Logging

    Lexer for KeYmaera X turns string into list of tokens.

  16. object KeYmaeraXNoContractPrettyPrinter extends KeYmaeraXPrecedencePrinter

    KeYmaera X Pretty Printer without contract checking

    KeYmaera X Pretty Printer without contract checking

    See also

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrecedencePrinter

  17. object KeYmaeraXParser extends Parser with TokenParser with Logging

    KeYmaera X parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.

    KeYmaera X parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.

    Example:
    1. Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:

      val parser = KeYmaeraXParser
      val fml0 = parser("x!=5")
      val fml1 = parser("x>0 -> [x:=x+1;]x>1")
      val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
    See also

    Grammar

    edu.cmu.cs.ls.keymaerax.parser

  18. object KeYmaeraXPrettyPrinter extends KeYmaeraXPrecedencePrinter

    Default KeYmaera X Pretty Printer formats differential dynamic logic expressions

    Default KeYmaera X Pretty Printer formats differential dynamic logic expressions

    See also

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrecedencePrinter

  19. object LeftAssociative extends BinaryNotation

    Left-associative infix operators of arity 2, i.e.

    Left-associative infix operators of arity 2, i.e. x-y-z=(x-y)-z

  20. object LemmaFileMode extends LexerMode
  21. object LexException
  22. object MixedBinary extends BinaryNotation

    Mixed binary operators of arity 2

  23. object NonAssociative extends BinaryNotation

    Non-associative infix operators of arity 2, i.e.

    Non-associative infix operators of arity 2, i.e. explicit parentheses a<->(b<->c)

  24. object OpSpec

    Differential Dynamic Logic's concrete syntax: operator notation specifications.

    Differential Dynamic Logic's concrete syntax: operator notation specifications.

    Note

    Subtleties: sPower right associative to ensure x23 == x(23) instead of (x2)3. sPower < sNeg to ensure -x2 == -(x2) instead of (-x)^2. NUMBER lexer does not contain - sign to enable x-5 to be parsed. Parser will make up for this, respecting binary versus unary operators. sEquiv nonassociative to ensure that p()<->q()<->r() does not parse since binding unclear. sAnd and sOr are right-associative to simplify stable position ordering during sequent decomposition.

  25. object ParseException extends Serializable
  26. object ParserHelper
  27. object PostfixFormat extends UnaryNotation

    Unary postfix operators of arity 1 within syntactic category

  28. object PrefixFormat extends UnaryNotation

    Unary prefix operators of arity 1 within syntactic category

  29. object ProblemFileMode extends LexerMode
  30. object RightAssociative extends BinaryNotation

    Right-associative infix operators of arity 2, i.e.

    Right-associative infix operators of arity 2, i.e. xyz=x(yz)

  31. object StringConverter

    Implicit conversions from strings into core data structures.

    Implicit conversions from strings into core data structures. Created by smitsch on 1/8/15.

  32. object TernaryOpSpec extends Serializable
  33. object TernaryPrefixFormat extends TernaryNotation

    Ternary operators with a terminal before each operand, like if P then a else b

  34. object UnaryOpSpec extends Serializable
  35. object UnitOpSpec extends Serializable
  36. object UnknownLocation extends Location

Inherited from AnyRef

Inherited from Any

Ungrouped