Generate a parsing function for an ABNF repetition.
(defdefparse-gen-function-for-repetition rep prefix group-table option-table repetition-table) → event
This is only used for repetitions whose repeat prefix is
Function:
(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 ':hooks (cons '(:fix) (cons ':measure (cons '(len input) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of- parse-repetition) parse-repetition) '((<= (len rest-input) (len input)) :rule-classes :linear))) 'nil)))))))))))))))))
Theorem:
(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)