		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-function-for-rulename

Generate a parsing function for a rule name.

Signature
(defdefparse-gen-function-for-rulename rulename order rules prefix group-table option-table repetition-table) → event
Arguments: rulename — Guard (common-lisp::stringp rulename).; order — Guard (pos-listp order).; rules — Guard (rulelistp rules).; 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 (pseudo-event-formp event).

The name is <prefix>-<R>, if <R> is the rule name. We look up the alternation that defines the rule name in the grammar, and we generate code to parse that, propagating errors, and returning a tree for the 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 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.

Definitions and Theorems

Function: defdefparse-gen-function-for-rulename

(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: pseudo-event-formp-of-defdefparse-gen-function-for-rulename

(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)