Packages

o

edu.cmu.cs.ls.keymaerax.parser

KeYmaeraXParser

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.

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

Linear Supertypes
Logging, TokenParser, Parser, (String) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. KeYmaeraXParser
  2. Logging
  3. TokenParser
  4. Parser
  5. Function1
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type TokenStream = List[Token]

    Lexer's token stream with first token at head.

    Lexer's token stream with first token at head.

    Definition Classes
    TokenParser

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

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

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

    Definition Classes
    KeYmaeraXParserParser → Function1
  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) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  9. val differentialProgramParser: (String) ⇒ DifferentialProgram
    Definition Classes
    KeYmaeraXParserParser
  10. val differentialProgramTokenParser: (TokenStream) ⇒ DifferentialProgram
    Definition Classes
    KeYmaeraXParserTokenParser
  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  13. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. val formulaParser: (String) ⇒ Formula
    Definition Classes
    KeYmaeraXParserParser
  15. val formulaTokenParser: (TokenStream) ⇒ Formula

    Parse the input token stream in the concrete syntax as a differential dynamic logic formula

    Parse the input token stream in the concrete syntax as a differential dynamic logic formula

    Definition Classes
    KeYmaeraXParserTokenParser
  16. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  19. val logger: Logger
    Attributes
    protected
    Definition Classes
    Logging
  20. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  21. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  23. def parse(input: TokenStream): Expression

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

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

    Definition Classes
    KeYmaeraXParserTokenParser
  24. val parser: Parser

    This default parser.

  25. lazy val printer: KeYmaeraXPrettyPrinter.type

    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
    KeYmaeraXParserParser
  26. val programParser: (String) ⇒ Program
    Definition Classes
    KeYmaeraXParserParser
  27. val programTokenParser: (TokenStream) ⇒ Program
    Definition Classes
    KeYmaeraXParserTokenParser
  28. def semanticAnalysis(e: Expression): Option[String]

    Semantic analysis of expressions after parsing, returning errors if any or None.

  29. def setAnnotationListener(listener: (Program, Formula) ⇒ Unit): Unit

    Register a listener for @annotations during the parse.

    Register a listener for @annotations during the parse.

    To do

    this design is suboptimal.

  30. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  31. val termParser: (String) ⇒ Term
    Definition Classes
    KeYmaeraXParserParser
  32. val termTokenParser: (TokenStream) ⇒ Term
    Definition Classes
    KeYmaeraXParserTokenParser
  33. def toString(): String
    Definition Classes
    Function1 → AnyRef → Any
  34. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  36. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from TokenParser

Inherited from Parser

Inherited from (String) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped