Grammar-parser-soundness
Soundness theorems for the parser of ABNF grammars.
If parse-grammar succeeds,
it returns a parse tree for the input rooted at rulelist:
Theorem: parse-treep-of-parse-grammar
(defthm parse-treep-of-parse-grammar
(let ((tree? (parse-grammar nats)))
(implies tree?
(parse-treep tree? (nat-list-fix nats)
*rulelist* *grammar*))))This is proved via two sets of theorems
for the parsing functions out of which parse-grammar is built:
- Input decomposition:
if parsing succeeds,
the string at the leaves of the returned tree(s)
consists of the consumed natural numbers in the input.
- Tree matching:
if parsing succeeds,
the returned tree(s) match(es) the syntactic entity
that the parsing function is meant to parse.
Subtopics
- Grammar-parser-tree-matching
- Tree matching theorems for the parser of ABNF grammars.
- Grammar-parser-input-decomposition
- Input decomposition theorems for the parser of ABNF grammars.
- Parse-treep-of-parse-grammar
- Top-level soundness theorem of the parser of ABNF grammars.
