Generate a parsing function for a rule name.
(defdefparse-gen-function-for-rulename rulename order rules prefix group-table option-table repetition-table) → event
The name is
We also generate linear rules about the remaining input. These are needed to prove the termination of recursive functions that call this function.
If every concatenation in the alternation that defines the rule name is nullable (i.e. can expand to the empty string of natural numbers), then the strict inequality linear rule should not be generated; otherwise, it should be generated. For now we do a very simple and partial test for nullability, namely whether the alternation consists of a single concatenation of a single repetition with `*`: clearly, this is nullable. We will extend this eventually; the ABNF library should eventually contain operations to determine whether grammar rules are nullable, using the well-known algorithms found in the literature.
Function:
(defun defdefparse-gen-function-for-rulename (rulename order rules prefix group-table option-table repetition-table) (declare (xargs :guard (and (common-lisp::stringp rulename) (pos-listp order) (rulelistp rules) (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-rulename)) (declare (ignorable __function__)) (b* ((parse-rulename (packn-pos (list prefix '- (str::upcase-string rulename)) prefix)) (alt (lookup-rulename (rulename rulename) rules)) (order (or order (integers-from-to 1 (len alt)))) (nullablep (and (consp alt) (not (consp (cdr alt))) (b* ((conc (car alt))) (and (consp conc) (not (consp (cdr conc))) (b* ((rep (car conc))) (equal (repetition->range rep) (make-repeat-range :min 0 :max (nati-infinity))))))))) (cons 'define (cons parse-rulename (cons '((input nat-listp)) (cons ':returns (cons '(mv (tree tree-resultp) (rest-input nat-listp)) (cons ':short (cons (str::cat "Parse a @('" rulename "').") (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))))) (cons (cons 'mv (cons (cons 'make-tree-nonleaf (cons ':rulename? (cons (cons 'rulename (cons rulename 'nil)) '(:branches treess)))) '(input))) 'nil))) (cons ':hooks (cons '(:fix) (cons '/// (cons (cons 'defret (cons (packn-pos (list 'len-of- parse-rulename '-<=) parse-rulename) '((<= (len rest-input) (len input)) :rule-classes :linear))) (and (not nullablep) (cons (cons 'defret (cons (packn-pos (list 'len-of- parse-rulename '-<) parse-rulename) '((implies (not (reserrp tree)) (< (len rest-input) (len input))) :rule-classes :linear))) 'nil)))))))))))))))))
Theorem:
(defthm pseudo-event-formp-of-defdefparse-gen-function-for-rulename (b* ((event (defdefparse-gen-function-for-rulename rulename order rules prefix group-table option-table repetition-table))) (pseudo-event-formp event)) :rule-classes :rewrite)