		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-code-for-concatenation

Generate code to parse an instance of an ABNF concatenation.

Signature
(defdefparse-gen-code-for-concatenation conc prefix group-table option-table repetition-table) → code
Arguments: conc — Guard (concatenationp conc).; prefix — Guard (common-lisp::symbolp prefix).; group-table — Guard (defdefparse-alt-symbol-alistp group-table).; option-table — Guard (defdefparse-alt-symbol-alistp option-table).; repetition-table — Guard (defdefparse-rep-symbol-alistp repetition-table).
Returns: code — Type (true-listp code).

A concatenation is parsed by parsing each repetition in order. We also generate a final b* binder that puts all the lists of trees from the repetiitons into a list of lists of trees for the concatenation.

Definitions and Theorems

Function: defdefparse-gen-code-for-concatenation-aux

(defun defdefparse-gen-code-for-concatenation-aux
       (conc index prefix group-table
             option-table repetition-table)
 (declare
  (xargs
     :guard (and (concatenationp conc)
                 (natp index)
                 (common-lisp::symbolp prefix)
                 (defdefparse-alt-symbol-alistp group-table)
                 (defdefparse-alt-symbol-alistp option-table)
                 (defdefparse-rep-symbol-alistp repetition-table))))
 (let ((__function__ 'defdefparse-gen-code-for-concatenation-aux))
   (declare (ignorable __function__))
   (b* (((when (endp conc)) (mv nil nil))
        ((mv code1 var)
         (defdefparse-gen-code-for-repetition
              (car conc)
              index prefix group-table
              option-table repetition-table))
        ((mv code2 vars)
         (defdefparse-gen-code-for-concatenation-aux
              (cdr conc)
              (1+ index)
              prefix group-table
              option-table repetition-table)))
     (mv (append code1 code2)
         (cons var vars)))))

Theorem: true-listp-of-defdefparse-gen-code-for-concatenation-aux.code

(defthm
      true-listp-of-defdefparse-gen-code-for-concatenation-aux.code
  (b* (((mv ?code ?vars)
        (defdefparse-gen-code-for-concatenation-aux
             conc index prefix group-table
             option-table repetition-table)))
    (true-listp code))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-defdefparse-gen-code-for-concatenation-aux.vars

(defthm
    symbol-listp-of-defdefparse-gen-code-for-concatenation-aux.vars
  (b* (((mv ?code ?vars)
        (defdefparse-gen-code-for-concatenation-aux
             conc index prefix group-table
             option-table repetition-table)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Function: defdefparse-gen-code-for-concatenation

(defun defdefparse-gen-code-for-concatenation
       (conc prefix group-table
             option-table repetition-table)
 (declare
  (xargs
     :guard (and (concatenationp conc)
                 (common-lisp::symbolp prefix)
                 (defdefparse-alt-symbol-alistp group-table)
                 (defdefparse-alt-symbol-alistp option-table)
                 (defdefparse-rep-symbol-alistp repetition-table))))
 (let ((__function__ 'defdefparse-gen-code-for-concatenation))
   (declare (ignorable __function__))
   (b* (((when (endp conc))
         (raise "Empty concatenation."))
        ((mv code vars)
         (defdefparse-gen-code-for-concatenation-aux
              conc 1 prefix group-table
              option-table repetition-table)))
     (append code
             (cons (cons 'treess
                         (cons (cons 'list vars) 'nil))
                   'nil)))))

Theorem: true-listp-of-defdefparse-gen-code-for-concatenation

(defthm true-listp-of-defdefparse-gen-code-for-concatenation
  (b* ((code (defdefparse-gen-code-for-concatenation
                  conc prefix group-table
                  option-table repetition-table)))
    (true-listp code))
  :rule-classes :rewrite)