Raise a syntax error if axioms (or anything else) follow a theorem.
Chris Pressey
1 year, 1 month ago
| 118 | 118 |
|
| 119 | 119 |
// This is a comment.
|
| 120 | 120 |
axiom inv(A) = A // This is also a comment.
|
| 121 | |
===> ok
|
|
121 |
|
|
122 |
===> ok
|
|
123 |
|
|
124 |
A comment may not be the very last thing in the document though.
|
|
125 |
They do need to end with a newline character.
|
|
126 |
|
|
127 |
// This is a comment.
|
|
128 |
axiom inv(A) = A // This is also a comment.
|
|
129 |
???>
|
|
130 |
|
|
131 |
A theorem may be followed only by another theorem or the end of the
|
|
132 |
document. A theorem may not be followed by, e.g., an axiom.
|
|
133 |
|
|
134 |
axiom inv(A) = A.
|
|
135 |
theorem inv(A) = A proof A = A inv(A) = A qed.
|
|
136 |
axiom dec(A) = A.
|
|
137 |
???>
|
| 122 | 138 |
|
| 123 | 139 |
### Check Eqthy Document
|
| 124 | 140 |
|
| 37 | 37 |
axioms.append(self.axiom())
|
| 38 | 38 |
while self.scanner.on('theorem'):
|
| 39 | 39 |
theorems.append(self.theorem())
|
| 40 | |
if not (axioms or theorems):
|
|
40 |
if (not axioms) and (not theorems):
|
| 41 | 41 |
raise EqthySyntaxError(
|
| 42 | 42 |
self.scanner.filename,
|
| 43 | 43 |
self.scanner.line_number,
|
| 44 | 44 |
"Eqthy document is empty"
|
| 45 | 45 |
)
|
|
46 |
self.scanner.check_eof()
|
| 46 | 47 |
return Document(axioms=axioms, theorems=theorems)
|
| 47 | 48 |
|
| 48 | 49 |
def axiom(self) -> Axiom:
|
| 38 | 38 |
self.line_number += self.token.count('\n')
|
| 39 | 39 |
return True
|
| 40 | 40 |
|
| 41 | |
def scan(self) -> None:
|
|
41 |
def consume_whitespace(self) -> None:
|
| 42 | 42 |
self.scan_pattern(r'[ \t\n\r]*', 'whitespace')
|
| 43 | 43 |
while self.scan_pattern(r'\/\/.*?[\n\r]', 'comment'):
|
| 44 | 44 |
self.scan_pattern(r'[ \t\n\r]*', 'whitespace')
|
| 45 | 45 |
if self.pos >= len(self.text):
|
| 46 | 46 |
self.token = None
|
| 47 | 47 |
self.type = 'EOF'
|
|
48 |
|
|
49 |
def scan(self) -> None:
|
|
50 |
self.consume_whitespace()
|
|
51 |
if self.type == 'EOF':
|
| 48 | 52 |
return
|
| 49 | 53 |
if self.scan_pattern(r'\,|\@|\+|\:|\<|\>|\{|\}|\[|\]|\^', 'operator'):
|
| 50 | 54 |
return
|
|
| 73 | 77 |
def on_type(self, type: str) -> bool:
|
| 74 | 78 |
return self.type == type
|
| 75 | 79 |
|
| 76 | |
def check_type(self, type: str) -> None:
|
| 77 | |
if not self.type == type:
|
| 78 | |
self.syntax_error("Expected {}, but found '{}'".format(self.type, self.token))
|
|
80 |
def check_eof(self) -> None:
|
|
81 |
self.consume_whitespace()
|
|
82 |
if self.type != 'EOF':
|
|
83 |
self.syntax_error("Expected end of document, but found '{}' ({})".format(self.token, self.type))
|
| 79 | 84 |
|
| 80 | 85 |
def consume(self, token: str) -> bool:
|
| 81 | 86 |
if self.token == token:
|