		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-rulename-macro

Generate the defparse-name-rulename macro described in the defdefparse user documentation.

Signature
(defdefparse-gen-rulename-macro name pkg-wit grammar prefix group-table-name option-table-name repetition-table-name) → event
Arguments: name — Guard (common-lisp::symbolp name).; pkg-wit — Guard (common-lisp::symbolp pkg-wit).; grammar — Guard (common-lisp::symbolp grammar).; prefix — Guard (common-lisp::symbolp prefix).; group-table-name — Guard (common-lisp::symbolp group-table-name).; option-table-name — Guard (common-lisp::symbolp option-table-name).; repetition-table-name — Guard (common-lisp::symbolp repetition-table-name).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defdefparse-gen-rulename-macro

(defun defdefparse-gen-rulename-macro
       (name pkg-wit grammar prefix group-table-name
             option-table-name repetition-table-name)
 (declare
  (xargs :guard (and (common-lisp::symbolp name)
                     (common-lisp::symbolp pkg-wit)
                     (common-lisp::symbolp grammar)
                     (common-lisp::symbolp prefix)
                     (common-lisp::symbolp group-table-name)
                     (common-lisp::symbolp option-table-name)
                     (common-lisp::symbolp repetition-table-name))))
 (let ((__function__ 'defdefparse-gen-rulename-macro))
  (declare (ignorable __function__))
  (b* ((macro-name (packn-pos (list 'defparse- name '-rulename)
                              pkg-wit)))
   (cons
    'defmacro
    (cons
     macro-name
     (cons
      '(rulename &key order)
      (cons
       (cons
        'cons
        (cons
         ''make-event
         (cons
          (cons
           'cons
           (cons
            (cons
             'cons
             (cons
              ''defdefparse-gen-function-for-spec
              (cons
               (cons
                'cons
                (cons
                 '(cons 'defdefparse-function-spec-rulename
                        (cons rulename
                              (cons (cons 'quote (cons order 'nil))
                                    'nil)))
                 (cons
                  (cons
                   'cons
                   (cons
                    (cons 'quote (cons grammar 'nil))
                    (cons
                     (cons
                      'cons
                      (cons
                       (cons
                        'cons
                        (cons
                         ''quote
                         (cons
                          (cons
                              'cons
                              (cons (cons 'quote (cons prefix 'nil))
                                    '('nil)))
                          'nil)))
                       (cons
                        (cons
                         'cons
                         (cons
                          (cons 'quote
                                (cons group-table-name 'nil))
                          (cons
                           (cons
                            'cons
                            (cons
                             (cons 'quote
                                   (cons option-table-name 'nil))
                             (cons
                              (cons
                               'cons
                               (cons
                                (cons
                                  'quote
                                  (cons repetition-table-name 'nil))
                                '('nil)))
                              'nil)))
                           'nil)))
                        'nil)))
                     'nil)))
                  'nil)))
               'nil)))
            '('nil)))
          'nil)))
       'nil)))))))

Theorem: pseudo-event-formp-of-defdefparse-gen-rulename-macro

(defthm pseudo-event-formp-of-defdefparse-gen-rulename-macro
  (b* ((event (defdefparse-gen-rulename-macro
                   name pkg-wit grammar prefix
                   group-table-name option-table-name
                   repetition-table-name)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)