		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-function-for-group

Generate a parsing function for an ABNF group.

Signature
(defdefparse-gen-function-for-group alt order prefix group-table option-table repetition-table) → event
Arguments: alt — Guard (alternationp alt).; order — Guard (pos-listp order).; 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: event — Type (pseudo-event-formp event).

The name is retrieved from the alist for group parsing functions. We generate code to attempt to parse the alternation of the group, propagating errors, and returning a tree without rule name in case of success.

We also generate linear rules about the remaining input. These are needed to prove the termination of recursive functions that call this function.

If the alternation is nullable, we should not generate the strict inequality linear rule: see discussion in defdefparse-gen-function-for-rulename. However, for now we do not support that here, i.e. we implicitly assume that the alternation is not nullable.

Definitions and Theorems

Function: defdefparse-gen-function-for-group

(defun defdefparse-gen-function-for-group
       (alt order prefix group-table
            option-table repetition-table)
 (declare
  (xargs
     :guard (and (alternationp alt)
                 (pos-listp order)
                 (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-function-for-group))
  (declare (ignorable __function__))
  (b* ((parse-group (cdr (assoc-equal alt group-table)))
       (order (or order (integers-from-to 1 (len alt)))))
   (cons
    'define
    (cons
     parse-group
     (cons
      '((input nat-listp))
      (cons
       ':returns
       (cons
        '(mv (tree tree-resultp)
             (rest-input nat-listp))
        (cons
         ':short
         (cons
          (str::cat "Parse a @('"
                    (pretty-print-element (element-group alt))
                    "').")
          (cons
           (cons
            'b*
            (cons
               (cons (cons '(mv treess input)
                           (cons (defdefparse-gen-code-for-alternation
                                      alt order prefix group-table
                                      option-table repetition-table)
                                 'nil))
                     '(((when (reserrp treess))
                        (mv (reserrf-push treess)
                            (nat-list-fix input)))))
               '((mv (make-tree-nonleaf :rulename? nil
                                        :branches treess)
                     input))))
           (cons
            ':hooks
            (cons
             '(:fix)
             (cons
              '///
              (cons
               (cons
                   'defret
                   (cons (packn-pos (list 'len-of- parse-group '-<=)
                                    parse-group)
                         '((<= (len rest-input) (len input))
                           :rule-classes :linear)))
               (cons
                (cons
                  'defret
                  (cons (packn-pos (list 'len-of- parse-group '-<)
                                   parse-group)
                        '((implies (not (reserrp tree))
                                   (< (len rest-input) (len input)))
                          :rule-classes :linear)))
                'nil))))))))))))))))

Theorem: pseudo-event-formp-of-defdefparse-gen-function-for-group

(defthm pseudo-event-formp-of-defdefparse-gen-function-for-group
  (b* ((event (defdefparse-gen-function-for-group
                   alt order prefix group-table
                   option-table repetition-table)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)