8 |
8 |
9 import scala.util.parsing.combinator.Parsers |
9 import scala.util.parsing.combinator.Parsers |
10 import scala.util.parsing.input |
10 import scala.util.parsing.input |
11 |
11 |
12 |
12 |
13 object Thy_Element |
13 object Thy_Element { |
14 { |
|
15 /* datatype element */ |
14 /* datatype element */ |
16 |
15 |
17 type Proof[A] = (List[Element[A]], A) |
16 type Proof[A] = (List[Element[A]], A) |
18 sealed case class Element[A](head: A, proof: Option[Proof[A]]) |
17 sealed case class Element[A](head: A, proof: Option[Proof[A]]) { |
19 { |
|
20 def iterator: Iterator[A] = |
18 def iterator: Iterator[A] = |
21 Iterator(head) ++ |
19 Iterator(head) ++ |
22 (for { |
20 (for { |
23 (prf, qed) <- proof.iterator |
21 (prf, qed) <- proof.iterator |
24 b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed) |
22 b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed) |
50 |
48 |
51 /* parse elements */ |
49 /* parse elements */ |
52 |
50 |
53 type Element_Command = Element[Command] |
51 type Element_Command = Element[Command] |
54 |
52 |
55 def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] = |
53 def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] = { |
56 { |
54 case class Reader(in: List[Command]) extends input.Reader[Command] { |
57 case class Reader(in: List[Command]) extends input.Reader[Command] |
|
58 { |
|
59 def first: Command = in.head |
55 def first: Command = in.head |
60 def rest: Reader = Reader(in.tail) |
56 def rest: Reader = Reader(in.tail) |
61 def pos: input.Position = input.NoPosition |
57 def pos: input.Position = input.NoPosition |
62 def atEnd: Boolean = in.isEmpty |
58 def atEnd: Boolean = in.isEmpty |
63 } |
59 } |
64 |
60 |
65 object Parser extends Parsers |
61 object Parser extends Parsers { |
66 { |
|
67 type Elem = Command |
62 type Elem = Command |
68 |
63 |
69 def command(pred: Command => Boolean): Parser[Command] = |
64 def command(pred: Command => Boolean): Parser[Command] = |
70 new Parser[Elem] { |
65 new Parser[Elem] { |
71 def apply(in: Input) = |
66 def apply(in: Input) = { |
72 { |
|
73 if (in.atEnd) Failure("end of input", in) |
67 if (in.atEnd) Failure("end of input", in) |
74 else { |
68 else { |
75 val command = in.first |
69 val command = in.first |
76 if (pred(command)) Success(command, in.rest) |
70 if (pred(command)) Success(command, in.rest) |
77 else Failure("bad input", in) |
71 else Failure("bad input", in) |