Quelle thy_element.scala Sprache: Scala

/*  Title:      Pure/Thy/thy_element.ML
    Author:     Makarius

Theory elements: statements with optional proof.
*/

package isabelle

import scala.util.parsing.combinator
import scala.util.parsing.input

object Thy_Element {
  /* datatype element */

  type Proof[A] = (List[Element[A]], A)
  sealed case class Element[A](head: A, proof: Option[Proof[A]]) {
    def iterator: Iterator[A] =
      Iterator(head) ++
        (for {
          (prf, qed) <- proof.iterator
          b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
        } yield b)

    def outline_iterator: Iterator[A] =
      proof match {
        case None => Iterator(head)
        case Some((_, qed)) => Iterator(head, qed)
      }

    def proof_start: Option[A] =
      proof match {
        case None => None
        case Some((Nil, qed)) => Some(qed)
        case Some((start :: _, _)) => Some(start.head)
      }

    def last: A =
      proof match {
        case None => head
        case Some((_, qed)) => qed
      }
  }

  def element[A](a: A, b: Proof[A]): Element[A] = Element(a, Some(b))
  def atom[A](a: A): Element[A] = Element(a, None)

  /* parse elements */

  type Element_Command = Element[Command]

  def parse_elements(commands: List[Command]): List[Element_Command] = {
    case class Reader(in: List[Command]) extends input.Reader[Command] {
      def first: Command = in.head
      def rest: Reader = Reader(in.tail)
      def pos: input.Position = input.NoPosition
      def atEnd: Boolean = in.isEmpty
    }

    object Parsers extends combinator.Parsers {
      type Elem = Command

      def command(pred: Command => Boolean): Parser[Command] =
        new Parser[Elem] {
          def apply(in: Input) = {
            if (in.atEnd) Failure("end of input", in)
            else {
              val command = in.first
              if (pred(command)) Success(command, in.rest)
              else Failure("bad input", in)
            }
          }
        }

      def category(pred: String => Boolean, other: Boolean = false): Parser[Command] =
        command(_.span.is_keyword_kind(pred, other = other))

      def theory_element: Parser[Element_Command] =
        category(Keyword.theory_goal) ~ proof ^^ { case a ~ b => element(a, b) }
      def proof_element: Parser[Element_Command] =
        category(Keyword.proof_goal) ~ proof ^^ { case a ~ b => element(a, b) } |
        category(Keyword.proof_body, other = true) ^^ { case a => atom(a) }
      def proof: Parser[Proof[Command]] =
        rep(proof_element) ~ category(Keyword.qed) ^^ { case a ~ b => (a, b) }

      val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }

      def apply: List[Element_Command] =
        rep(theory_element | default_element)(Reader(commands)) match {
          case Success(result, rest) if rest.atEnd => result
          case bad => error(bad.toString)
        }
    }
    Parsers.apply
  }
}

quality94%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.