		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Parse-grammar*

Parse a sequence of natural numbers as an ABNF grammar.

Signature
(parse-grammar* nats) → result
Arguments: nats — Guard (nat-listp nats).
Returns: result — Type (or (tree-setp result) (equal result :infinite)).

This is a declaratively defined, non-executable parser for the ABNF language itself (parse-grammar is a verified executable parser). It turns text (represented as a sequence of natural numbers) with ABNF grammar rules (defining the concrete syntax of some language) into parse trees; the parse trees can be abstracted to lists of rules in the ABNF abstract syntax.

This function may return more than one parse tree, because the rulelist rule in [RFC:4] is ambiguous. For example, the string `rulename defined-as alternation c-nl WSP c-nl' can be parsed in two different ways (see the theorem below):

As a rulelist consisting of just a rule whose elements has `c-nl WSP' as *c-wsp.
As a rulelist consisting of a rule whose elements has `' (i.e. the empty string) as *c-wsp, followed by a (*c-wsp c-nl) with WSP as *c-wsp.

This ambiguity only concerns blank space and comments, so it does not affect the abstract syntax and the semantics.

It remains to be proved that this function always returns a finite set of trees, never :infinite.

Definitions and Theorems

Function: parse-grammar*

(defun parse-grammar* (nats)
       (declare (xargs :guard (nat-listp nats)))
       (parse nats *rulelist* *grammar*))

Theorem: return-type-of-parse-grammar*

(defthm return-type-of-parse-grammar*
        (b* ((result (parse-grammar* nats)))
            (or (tree-setp result)
                (equal result :infinite)))
        :rule-classes :rewrite)

Theorem: rulelist-ambiguous-example

(defthm
 rulelist-ambiguous-example
 (b*
  ((string (list *rulename* *defined-as*
                 *alternation* *c-nl* *wsp* *c-nl*))
   (tree-rulename (tree-leafrule *rulename*))
   (tree-defined-as (tree-leafrule *defined-as*))
   (tree-alternation (tree-leafrule *alternation*))
   (tree-c-nl (tree-leafrule *c-nl*))
   (tree-wsp (tree-leafrule *wsp*))
   (tree-c-nl-wsp (tree-nonleaf nil
                                (list (list tree-c-nl)
                                      (list tree-wsp))))
   (tree-c-wsp-1 (tree-nonleaf *c-wsp* (list (list tree-c-nl-wsp))))
   (tree-c-wsp-2 (tree-nonleaf *c-wsp* (list (list tree-wsp))))
   (tree-elements-1 (tree-nonleaf *elements*
                                  (list (list tree-alternation)
                                        (list tree-c-wsp-1))))
   (tree-elements-2
        (tree-nonleaf *elements*
                      (list (list tree-alternation) nil)))
   (tree-rule-1 (tree-nonleaf *rule*
                              (list (list tree-rulename)
                                    (list tree-defined-as)
                                    (list tree-elements-1)
                                    (list tree-c-nl))))
   (tree-rule-/-*cwsp-cnl-1
        (tree-nonleaf nil (list (list tree-rule-1))))
   (tree-rulelist-1
        (tree-nonleaf *rulelist*
                      (list (list tree-rule-/-*cwsp-cnl-1))))
   (tree-rule-2 (tree-nonleaf *rule*
                              (list (list tree-rulename)
                                    (list tree-defined-as)
                                    (list tree-elements-2)
                                    (list tree-c-nl))))
   (tree-rule-/-*cwsp-cnl-2
        (tree-nonleaf nil (list (list tree-rule-2))))
   (tree-*cwsp-cnl (tree-nonleaf nil
                                 (list (list tree-c-wsp-2)
                                       (list tree-c-nl))))
   (tree-rule-/-*cwsp-cnl-3
        (tree-nonleaf nil (list (list tree-*cwsp-cnl))))
   (tree-rulelist-2
        (tree-nonleaf *rulelist*
                      (list (list tree-rule-/-*cwsp-cnl-2
                                  tree-rule-/-*cwsp-cnl-3)))))
  (and (stringp string)
       (treep tree-rulelist-1)
       (treep tree-rulelist-2)
       (tree-match-element-p tree-rulelist-1
                             (element-rulename *rulelist*)
                             *grammar*)
       (tree-match-element-p tree-rulelist-2
                             (element-rulename *rulelist*)
                             *grammar*)
       (not (equal tree-rulelist-1 tree-rulelist-2))
       (equal (tree->string tree-rulelist-1)
              string)
       (equal (tree->string tree-rulelist-2)
              string))))