		Search-engine friendly clone of the ACL2 documentation.

Grammar-parser-soundness

Parse-treep-of-parse-grammar

Top-level soundness theorem of the parser of ABNF grammars.

If parse-grammar succeeds, it returns a parse tree for the input rooted at rulelist. This is proved from the input decomposition theorem and tree matching theorem for rulelist, and the fact that parse-grammar fails if there is extra input.

An alternative formulation is to avoid nat-list-fix but include the hypothesis that the input satisfies nat-listp.

Definitions and Theorems

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*))))