		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-code-for-repetition

Generate code to parse an instance of an ABNF repetition.

Signature
(defdefparse-gen-code-for-repetition rep index prefix group-table option-table repetition-table) → (mv code var)
Arguments: rep — Guard (repetitionp rep).; index — Guard (natp index).; 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).; var — Type (common-lisp::symbolp var).

A repetition is part of a concatenation, and a concatenation (see defdefparse-gen-code-for-concatenation) is parsed by parsing each of its repetitions; the results of parsing the repetitions must be put together to yield the result of parsing the concatenation. The result of parsing each repetition is bound to a different variable, called trees<index> where <index> is a numeric index that starts with 1 and is incremented as we go through the concatenation. The index is passed to this code generation function, which generates b* binders and also returns the variable name.

If the repetition is in the alist, its parsing function is retrieved from there and we generate code to bind its result to trees<index>. We also propagate any error.

If the repetition is not in the alist, it must be a singleton repetition (this is what we support for now), in which case we generate code to parse the element, and we put the resulting tree into a singleton list if successful. Note that we propagate the error when parsing the element, i.e. we pass t as the check-error-p flag.

Definitions and Theorems

Function: defdefparse-gen-code-for-repetition

(defun defdefparse-gen-code-for-repetition
       (rep index prefix group-table
            option-table repetition-table)
 (declare
  (xargs
     :guard (and (repetitionp rep)
                 (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-repetition))
  (declare (ignorable __function__))
  (b*
   ((trees-index (add-suffix 'trees
                             (str::nat-to-dec-string index)))
    (parse-repetition-fn? (cdr (assoc-equal rep repetition-table)))
    ((when parse-repetition-fn?)
     (mv
      (cons
       (cons (cons 'mv (cons trees-index '(input)))
             (cons (cons parse-repetition-fn? '(input))
                   'nil))
       (cons
           (cons (cons 'when
                       (cons (cons 'reserrp (cons trees-index 'nil))
                             'nil))
                 (cons (cons 'mv
                             (cons (cons 'reserrf-push
                                         (cons trees-index 'nil))
                                   '(input)))
                       'nil))
           'nil))
      trees-index))
    ((repetition rep) rep)
    ((when (equal rep.range
                  (make-repeat-range :min 1
                                     :max (nati-finite 1))))
     (mv (append (defdefparse-gen-code-for-element
                      rep.element
                      t prefix group-table option-table)
                 (cons (cons trees-index '((list tree)))
                       'nil))
         trees-index)))
   (prog2$ (raise "Repetition ~x0 not supported yet." rep)
           (mv nil nil)))))

Theorem: true-listp-of-defdefparse-gen-code-for-repetition.code

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

Theorem: symbolp-of-defdefparse-gen-code-for-repetition.var

(defthm symbolp-of-defdefparse-gen-code-for-repetition.var
  (b* (((mv ?code ?var)
        (defdefparse-gen-code-for-repetition
             rep index prefix group-table
             option-table repetition-table)))
    (common-lisp::symbolp var))
  :rule-classes :rewrite)