Correctness theorems for the parser of ABNF grammars.
The correctness of the parser consists of two parts:
(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).
(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.