		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-function-for-repetition

Generate a parsing function for an ABNF repetition.

Signature
(defdefparse-gen-function-for-repetition rep prefix group-table option-table repetition-table) → event
Arguments: rep — Guard (repetitionp rep).; 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 (acl2::maybe-pseudo-event-formp event).

This is only used for repetitions whose repeat prefix is *, i.e. zero or more (i.e. this is all we support for now). The name is retrieved from the alist for repetition parsing functions. We generate a recursive function that repeatedly attempts to parse the underlying element. Note that we set the check-error-p flag to nil here, because we don't want the error to be returned, we just want to stop the recursion.

Definitions and Theorems

Function: defdefparse-gen-function-for-repetition

(defun defdefparse-gen-function-for-repetition
       (rep prefix group-table
            option-table repetition-table)
 (declare
  (xargs
     :guard (and (repetitionp rep)
                 (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-repetition))
  (declare (ignorable __function__))
  (b* ((parse-repetition (cdr (assoc-equal rep repetition-table)))
       ((repetition rep) rep)
       ((unless (equal rep.range
                       (make-repeat-range :min 0
                                          :max (nati-infinity))))
        (raise "Repetition ~x0 currently not supported."
               rep)))
   (cons
    'define
    (cons
     parse-repetition
     (cons
      '((input nat-listp))
      (cons
       ':returns
       (cons
        '(mv (trees tree-listp)
             (rest-input nat-listp))
        (cons
         ':short
         (cons
          (str::cat "Parse a @('"
                    (pretty-print-repetition rep)
                    "').")
          (cons
           (cons
            'b*
            (cons
             (append
              (defdefparse-gen-code-for-element
                   rep.element
                   nil prefix group-table option-table)
              (cons
                  '((when (reserrp tree)) (mv nil input))
                  (cons (cons '(mv trees input)
                              (cons (cons parse-repetition '(input))
                                    'nil))
                        'nil)))
             '((mv (cons tree trees) input))))
           (cons
            ':measure
            (cons
             '(len input)
             (cons
              ':hints
              (cons
               '(("Goal" :in-theory (enable o< o-finp)))
               (cons
                ':hooks
                (cons
                 '(:fix)
                 (cons
                  '///
                  (cons
                   (cons
                    'defret
                    (cons
                         (packn-pos (list 'len-of- parse-repetition)
                                    parse-repetition)
                         '((<= (len rest-input) (len input))
                           :rule-classes :linear
                           :hints (("Goal" :induct t)))))
                   'nil)))))))))))))))))))

Theorem: maybe-pseudo-event-formp-of-defdefparse-gen-function-for-repetition

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