• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
      • Grammar-parser
        • Grammar-parser-implementation
          • Parse-grammar-from-file
          • Parse-ichar2
          • Parse-ichar
          • Parse-in-either-range
          • Parse-*-in-either-range
          • Parse-bit
          • Parse-equal-/-equal-slash
          • Parse-wsp
          • Parse-*digit-star-*digit
          • Parse-hexdig
          • Parse-cwsp
          • Parse-concatenation
          • Parse-case-insensitive-string
          • Parse-alpha
          • Parse-dot-1*bit
          • Parse-case-sensitive-string
          • Parse-bin/dec/hex-val
          • Parse-alpha/digit/dash
          • Parse-rule
          • Parse-repeat
          • Parse-cnl
          • Parse-sp
          • Parse-rule-/-*cwsp-cnl
          • Parse-element
          • Parse-dec-val
          • Parse-bin-val
          • Parse-alternation
          • Parse-*cwsp-cnl
          • Parse-*bit
          • Parse-wsp/vchar
          • Parse-quoted-string
          • Parse-prose-val
          • Parse-hex-val
          • Parse-grammar
          • Parse-elements
          • Parse-defined-as
          • Parse-dash-1*hexdig
          • Parse-comment
          • Parse-char-val
          • Parse-1*bit
          • Parse-rulename
          • Parse-num-val
          • Parse-htab
          • Parse-hex-val-rest
          • Parse-dot-1*hexdig
          • Parse-dot-1*digit
          • Parse-digit
          • Parse-dec-val-rest
          • Parse-dash-1*digit
          • Parse-dash-1*bit
          • Parse-crlf
          • Parse-cr
          • Parse-conc-rest-comp
          • Parse-cnl-wsp
          • Parse-bin-val-rest
          • Parse-alt-rest-comp
          • Parse-*cwsp
          • Parse-vchar
          • Parse-rulelist
          • Parse-option
          • Parse-group
          • Parse-1*-dot-1*hexdig
          • Parse-1*-dot-1*digit
          • Parse-1*-dot-1*bit
          • Parse-*-rule-/-*cwsp-cnl
          • Parse-*-alpha/digit/dash
          • Parse-lf
          • Parse-dquote
          • Parse-1*hexdig
          • Parse-1*cwsp
          • Parse-?repeat
          • Parse-*-dot-1*hexdig
          • Parse-*-dot-1*digit
          • Parse-*-dot-1*bit
          • Parse-repetition
          • Parse-1*digit
          • Parse-?%i
          • Parse-*wsp/vchar
          • Parse-*hexdig
          • Parse-*digit
          • Parse-alt-rest
          • Parse-conc-rest
          • *grammar-parser-error-msg*
        • Grammar-parser-correctness
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Constructor-utilities
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Pfcs
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Grammar-parser-implementation

Parse-grammar-from-file

Parse a file into an ABNF grammar.

Signature

(parse-grammar-from-file filename state) → (mv tree? state)

Arguments

filename — Guard (common-lisp::stringp filename).

Returns

tree? — Type (tree-optionp tree?).

The ABNF language consists of sequences of ASCII codes, as shown by theorem ascii-only-*grammar*. ASCII codes are octets (i.e. 8-bit bytes). Thus, instead of parsing sequences of natural numbers, we can parse sequences of characters (which are isomorphic to octets), by converting the characters to the corresponding octets. The characters can be read from a file.

This function parses the characters from a file into a grammar. If parsing fails, nil is returned. If reading the characters from the file fails, nil is returned.

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 by calling set-buffer-file-coding-system with dos, and saving the file. If the file is put under a version control system, it should be forced to be treated as a text file with CRLF end-of-line (e.g. see the .gitattributes file in this directory) to avoid turning carriage returns and line feeds into just line feeds across Windows and Unix platforms.

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.

Definitions and Theorems

Function: parse-grammar-from-file

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

Theorem: tree-optionp-of-parse-grammar-from-file.tree?

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