author | wenzelm |
Thu, 06 Jun 2024 12:53:02 +0200 | |
changeset 80268 | 979f3893aa37 |
parent 78912 | ff4496b25197 |
permissions | -rw-r--r-- |
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 |
||
75405 | 9 |
import scala.util.parsing.combinator |
68845 | 10 |
import scala.util.parsing.input |
11 |
||
12 |
||
75393 | 13 |
object Thy_Element { |
68845 | 14 |
/* datatype element */ |
15 |
||
16 |
type Proof[A] = (List[Element[A]], A) |
|
75393 | 17 |
sealed case class Element[A](head: A, proof: Option[Proof[A]]) { |
68845 | 18 |
def iterator: Iterator[A] = |
19 |
Iterator(head) ++ |
|
20 |
(for { |
|
21 |
(prf, qed) <- proof.iterator |
|
22 |
b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed) |
|
23 |
} yield b) |
|
24 |
||
68846 | 25 |
def outline_iterator: Iterator[A] = |
26 |
proof match { |
|
27 |
case None => Iterator(head) |
|
28 |
case Some((_, qed)) => Iterator(head, qed) |
|
29 |
} |
|
30 |
||
69919 | 31 |
def proof_start: Option[A] = |
32 |
proof match { |
|
33 |
case None => None |
|
34 |
case Some((Nil, qed)) => Some(qed) |
|
35 |
case Some((start :: _, _)) => Some(start.head) |
|
36 |
} |
|
37 |
||
68845 | 38 |
def last: A = |
39 |
proof match { |
|
40 |
case None => head |
|
41 |
case Some((_, qed)) => qed |
|
42 |
} |
|
43 |
} |
|
44 |
||
45 |
def element[A](a: A, b: Proof[A]): Element[A] = Element(a, Some(b)) |
|
46 |
def atom[A](a: A): Element[A] = Element(a, None) |
|
47 |
||
48 |
||
49 |
/* parse elements */ |
|
50 |
||
68846 | 51 |
type Element_Command = Element[Command] |
52 |
||
78912
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
53 |
def parse_elements(commands: List[Command]): List[Element_Command] = { |
75393 | 54 |
case class Reader(in: List[Command]) extends input.Reader[Command] { |
68845 | 55 |
def first: Command = in.head |
56 |
def rest: Reader = Reader(in.tail) |
|
57 |
def pos: input.Position = input.NoPosition |
|
58 |
def atEnd: Boolean = in.isEmpty |
|
59 |
} |
|
60 |
||
75405 | 61 |
object Parsers extends combinator.Parsers { |
68845 | 62 |
type Elem = Command |
63 |
||
64 |
def command(pred: Command => Boolean): Parser[Command] = |
|
65 |
new Parser[Elem] { |
|
75393 | 66 |
def apply(in: Input) = { |
68845 | 67 |
if (in.atEnd) Failure("end of input", in) |
68 |
else { |
|
69 |
val command = in.first |
|
70 |
if (pred(command)) Success(command, in.rest) |
|
71 |
else Failure("bad input", in) |
|
72 |
} |
|
73 |
} |
|
74 |
} |
|
75 |
||
78912
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
76 |
def category(pred: String => Boolean, other: Boolean = false): Parser[Command] = |
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
77 |
command(_.span.is_keyword_kind(pred, other = other)) |
68845 | 78 |
|
68846 | 79 |
def theory_element: Parser[Element_Command] = |
78912
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
80 |
category(Keyword.theory_goal) ~ proof ^^ { case a ~ b => element(a, b) } |
68846 | 81 |
def proof_element: Parser[Element_Command] = |
78912
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
82 |
category(Keyword.proof_goal) ~ proof ^^ { case a ~ b => element(a, b) } | |
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
83 |
category(Keyword.proof_body, other = true) ^^ { case a => atom(a) } |
68845 | 84 |
def proof: Parser[Proof[Command]] = |
78912
ff4496b25197
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
wenzelm
parents:
75405
diff
changeset
|
85 |
rep(proof_element) ~ category(Keyword.qed) ^^ { case a ~ b => (a, b) } |
68845 | 86 |
|
68846 | 87 |
val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) } |
68845 | 88 |
|
68846 | 89 |
def apply: List[Element_Command] = |
68845 | 90 |
rep(theory_element | default_element)(Reader(commands)) match { |
91 |
case Success(result, rest) if rest.atEnd => result |
|
92 |
case bad => error(bad.toString) |
|
93 |
} |
|
94 |
} |
|
75405 | 95 |
Parsers.apply |
68845 | 96 |
} |
97 |
} |