68845
|
1 |
/* Title: Pure/Thy/thy_element.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Theory elements: statements with optional proof.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
import scala.util.parsing.combinator.Parsers
|
|
10 |
import scala.util.parsing.input
|
|
11 |
|
|
12 |
|
|
13 |
object Thy_Element
|
|
14 |
{
|
|
15 |
/* datatype element */
|
|
16 |
|
|
17 |
type Proof[A] = (List[Element[A]], A)
|
|
18 |
sealed case class Element[A](head: A, proof: Option[Proof[A]])
|
|
19 |
{
|
|
20 |
def iterator: Iterator[A] =
|
|
21 |
Iterator(head) ++
|
|
22 |
(for {
|
|
23 |
(prf, qed) <- proof.iterator
|
|
24 |
b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
|
|
25 |
} yield b)
|
|
26 |
|
68846
|
27 |
def outline_iterator: Iterator[A] =
|
|
28 |
proof match {
|
|
29 |
case None => Iterator(head)
|
|
30 |
case Some((_, qed)) => Iterator(head, qed)
|
|
31 |
}
|
|
32 |
|
69919
|
33 |
def proof_start: Option[A] =
|
|
34 |
proof match {
|
|
35 |
case None => None
|
|
36 |
case Some((Nil, qed)) => Some(qed)
|
|
37 |
case Some((start :: _, _)) => Some(start.head)
|
|
38 |
}
|
|
39 |
|
68845
|
40 |
def last: A =
|
|
41 |
proof match {
|
|
42 |
case None => head
|
|
43 |
case Some((_, qed)) => qed
|
|
44 |
}
|
|
45 |
}
|
|
46 |
|
|
47 |
def element[A](a: A, b: Proof[A]): Element[A] = Element(a, Some(b))
|
|
48 |
def atom[A](a: A): Element[A] = Element(a, None)
|
|
49 |
|
|
50 |
|
|
51 |
/* parse elements */
|
|
52 |
|
68846
|
53 |
type Element_Command = Element[Command]
|
|
54 |
|
|
55 |
def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] =
|
68845
|
56 |
{
|
|
57 |
case class Reader(in: List[Command]) extends input.Reader[Command]
|
|
58 |
{
|
|
59 |
def first: Command = in.head
|
|
60 |
def rest: Reader = Reader(in.tail)
|
|
61 |
def pos: input.Position = input.NoPosition
|
|
62 |
def atEnd: Boolean = in.isEmpty
|
|
63 |
}
|
|
64 |
|
|
65 |
object Parser extends Parsers
|
|
66 |
{
|
|
67 |
type Elem = Command
|
|
68 |
|
|
69 |
def command(pred: Command => Boolean): Parser[Command] =
|
|
70 |
new Parser[Elem] {
|
|
71 |
def apply(in: Input) =
|
|
72 |
{
|
|
73 |
if (in.atEnd) Failure("end of input", in)
|
|
74 |
else {
|
|
75 |
val command = in.first
|
|
76 |
if (pred(command)) Success(command, in.rest)
|
|
77 |
else Failure("bad input", in)
|
|
78 |
}
|
|
79 |
}
|
|
80 |
}
|
|
81 |
|
|
82 |
def category(pred: String => Boolean, other: Boolean): Parser[Command] =
|
|
83 |
command(_.span.is_kind(keywords, pred, other))
|
|
84 |
|
68846
|
85 |
def theory_element: Parser[Element_Command] =
|
68845
|
86 |
category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
|
68846
|
87 |
def proof_element: Parser[Element_Command] =
|
68845
|
88 |
category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
|
|
89 |
category(Keyword.proof_body, true) ^^ { case a => atom(a) }
|
|
90 |
def proof: Parser[Proof[Command]] =
|
|
91 |
rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
|
|
92 |
|
68846
|
93 |
val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }
|
68845
|
94 |
|
68846
|
95 |
def apply: List[Element_Command] =
|
68845
|
96 |
rep(theory_element | default_element)(Reader(commands)) match {
|
|
97 |
case Success(result, rest) if rest.atEnd => result
|
|
98 |
case bad => error(bad.toString)
|
|
99 |
}
|
|
100 |
}
|
|
101 |
Parser.apply
|
|
102 |
}
|
|
103 |
}
|