Parse a file into an ABNF grammar.
The ABNF language consists of sequences of ASCII codes,
as shown by theorem
This function parses the characters from a file into a grammar.
If parsing fails,
Thus, a language definition in ABNF can be put into a file
(e.g. copied and pasted from an RFC)
and parsed with this function.
Note that in ABNF lines are terminated by a carriage return and line feed,
so the file must follow that convention.
On Unix systems (e.g. Linux and macOS),
this can be accomplished by writing the file in Emacs,
setting the buffer's end-of-line to carriage return and line feed
If parsing succeeds, it returns a correct parse tree for the contents of the file as a list of ABNF rules, according to the concrete syntax rules.
(defun parse-grammar-from-file (filename state) (declare (xargs :stobjs (state))) (declare (xargs :guard (common-lisp::stringp filename))) (b* (((mv chars state) (read-file-characters filename state)) ((unless (character-listp chars)) (mv (hard-error 'abnf "ABNF Grammar File Reading Error." nil) state)) (nats (chars=>nats chars)) (tree? (parse-grammar nats)) ((unless tree?) (mv (hard-error 'abnf "ABNF Grammar File Parsing Error." nil) state))) (mv tree? state)))
(defthm tree-optionp-of-parse-grammar-from-file.tree? (b* (((mv ?tree? acl2::?state) (parse-grammar-from-file filename state))) (tree-optionp tree?)) :rule-classes :rewrite)