Grammar-parser

Grammar-parser-correctness

Correctness theorems for the parser of ABNF grammars.

The correctness of the parser consists of two parts:

Soundness: 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*))))
```
That is, the parser recognizes only grammars (i.e. lists of rules).
Completeness: for every terminated tree rooted at rulelist that satisfies the disambiguating restrictions, parse-grammar succeeds on the string at the leaves of the tree and returns that tree:
Theorem: parse-grammar-when-tree-match
```
(defthm parse-grammar-when-tree-match
  (implies
       (and (tree-match-element-p tree (element-rulename *rulelist*)
                                  *grammar*)
            (tree-terminatedp tree)
            (tree-rulelist-restriction-p tree))
       (equal (parse-grammar (tree->string tree))
              (tree-fix tree))))
```
That is, the parser recognizes all grammars (i.e. lists of rules) whose trees satisfy the disambiguating restrictions.

Some of these proofs apply to the Seq parsing primitives. Those proofs should be eventually moved with the parsing primitives.

Subtopics

Grammar-parser-completeness: Completeness theorems for the parser of ABNF grammars.
Grammar-parser-soundness: Soundness theorems for the parser of ABNF grammars.