Generate a parsing function for an ABNF group.
(defdefparse-gen-function-for-group alt order prefix group-table option-table repetition-table) → 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.
Function:
(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:
(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)