Packages

o

edu.cmu.cs.ls.keymaerax.parser

KeYmaeraXArchiveParser

object KeYmaeraXArchiveParser extends KeYmaeraXArchiveParserBase

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 possibly a (partial) proof tactic.

Format example:

ArchiveEntry "Entry 1".
  Description "optional description text".
  ProgramVariables ... End.
  Definitions ... End.
  Problem ... End.
  Tactic "Proof 1" ... End.
  Tactic "Proof 2" ... End.
End.
ArchiveEntry "Entry 2". ... End.
See also

Wiki

DLArchiveParser

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. KeYmaeraXArchiveParser
  2. KeYmaeraXArchiveParserBase
  3. ArchiveParser
  4. Function1
  5. AnyRef
  6. 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
    KeYmaeraXArchiveParserBase

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: (List[ParsedArchiveEntry]) ⇒ A): (String) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  5. final def apply(input: String): List[ParsedArchiveEntry]
    Definition Classes
    ArchiveParser → 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) ⇒ List[ParsedArchiveEntry]
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  9. def convert(t: Tactic, defs: Declaration): (String, String, BelleExpr)
    Attributes
    protected
    Definition Classes
    KeYmaeraXArchiveParserKeYmaeraXArchiveParserBase
  10. def convert(entry: ArchiveEntry, text: String, parseTactics: Boolean): ParsedArchiveEntry
    Definition Classes
    KeYmaeraXArchiveParserBase
  11. def doParse(input: String, parseTactics: Boolean): List[ParsedArchiveEntry]

    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. Skips parsing tactics if parseTactics is false. Requires KeYmaeraXPrettyPrinter setup if parseTactics is true.

    Attributes
    protected
    Definition Classes
    KeYmaeraXArchiveParserBaseArchiveParser
  12. def elaborateEntry(entry: ArchiveEntry): ArchiveEntry

    Elaborates problem, annotations, and annotations in definitions in the entry according to the entry-specific and inherited definitions listed in entry.

    Elaborates problem, annotations, and annotations in definitions in the entry according to the entry-specific and inherited definitions listed in entry.

    Definition Classes
    KeYmaeraXArchiveParserBase
  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  15. def exprParser: Parser

    The expression parser used in this archive parser.

    The expression parser used in this archive parser.

    Definition Classes
    KeYmaeraXArchiveParserBaseArchiveParser
  16. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. def getEntry(name: String, content: String, parseTactics: Boolean = true): Option[ParsedArchiveEntry]

    Reads a specific entry from the archive.

    Reads a specific entry from the archive.

    Definition Classes
    ArchiveParser
  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  20. def isExercise(model: String): Boolean

    Indicates whether or not the model represents an exercise.

    Indicates whether or not the model represents an exercise.

    Definition Classes
    ArchiveParser
  21. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  22. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  23. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. def parse(input: TokenStream, text: String, parseTactics: Boolean): List[ParsedArchiveEntry]

    Parses the input token stream (lexed from text); skips tactic parsing if parseTactics is false.

    Parses the input token stream (lexed from text); skips tactic parsing if parseTactics is false.

    Definition Classes
    KeYmaeraXArchiveParserBase
  26. final def parse(input: String, parseTactics: Boolean): List[ParsedArchiveEntry]
    Definition Classes
    ArchiveParser
  27. final def parse(input: String): List[ParsedArchiveEntry]
    Definition Classes
    ArchiveParser
  28. def parseAsExpandedFormula(input: String): Formula

    Returns the first entry in input as a formula with all definitions fully expanded.

    Returns the first entry in input as a formula with all definitions fully expanded.

    Definition Classes
    ArchiveParser
  29. def parseAsFormula(in: InputStream): Formula

    Returns the first entry in in as formula.

    Returns the first entry in in as formula.

    Definition Classes
    ArchiveParser
  30. def parseAsFormula(input: String): Formula

    Returns the first entry in input as formula.

    Returns the first entry in input as formula.

    Definition Classes
    ArchiveParser
  31. def parseFromFile(file: String): List[ParsedArchiveEntry]

    Parses an archive from the source at path file.

    Parses an archive from the source at path file. Use file#entry to refer to a specific entry in the file.

    Definition Classes
    ArchiveParser
  32. def parseProblem(input: String, parseTactics: Boolean = true): ParsedArchiveEntry

    Parses a single entry.

    Parses a single entry.

    Definition Classes
    ArchiveParser
  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. def tacticParser: TacticParser

    The tactic parser used in this archive parser.

    The tactic parser used in this archive parser.

    Definition Classes
    KeYmaeraXArchiveParserBaseArchiveParser
  35. def toString(): String
    Definition Classes
    Function1 → AnyRef → Any
  36. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  37. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  38. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from ArchiveParser

Inherited from (String) ⇒ List[ParsedArchiveEntry]

Inherited from AnyRef

Inherited from Any

Ungrouped