Generate a parsing function for an ABNF option.
(defdefparse-gen-function-for-option alt order prefix group-table option-table repetition-table) → event
The name is retrieved from the alist for option parsing functions. We generate code to attempt to parse the alternation of the option, and returning a tree without rule name in case of success. If parsing the alternative fails, we succeed and return a tree without branches.
We also generate a linear rule about the remaining input. This is needed to prove the termination of recursive functions that call this function.
Since an option is always nullable, we do not generate the string inequality linear rule: see discussion in defdefparse-gen-function-for-rulename.
Function:
(defun defdefparse-gen-function-for-option (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-option)) (declare (ignorable __function__)) (b* ((parse-option (cdr (assoc-equal alt option-table))) (order (or order (integers-from-to 1 (len alt))))) (cons 'define (cons parse-option (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-option 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 (make-tree-nonleaf :rulename? nil :branches nil) (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-option '-<=) parse-option) '((<= (len rest-input) (len input)) :rule-classes :linear))) 'nil)))))))))))))))
Theorem:
(defthm pseudo-event-formp-of-defdefparse-gen-function-for-option (b* ((event (defdefparse-gen-function-for-option alt order prefix group-table option-table repetition-table))) (pseudo-event-formp event)) :rule-classes :rewrite)