		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-group-macro

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

Signature
(defdefparse-gen-group-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-group-macro

(defun defdefparse-gen-group-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-group-macro))
  (declare (ignorable __function__))
  (b* ((macro-name (packn-pos (list 'defparse- name '-group)
                              pkg-wit)))
   (cons
    'defmacro
    (cons
     macro-name
     (cons
      '(group &key order)
      (cons
       (cons
        'b*
        (cons
         (cons
          '((mv err tree rest)
            (parse-group (string=>nats group)))
          (cons
           (cons
            '(when err)
            (cons
              (cons 'er
                    (cons 'hard
                          (cons (cons 'quote (cons macro-name 'nil))
                                '("~@0" err))))
              'nil))
           (cons
            (cons
             '(when (consp rest))
             (cons
              (cons
                 'er
                 (cons 'hard
                       (cons (cons 'quote (cons macro-name 'nil))
                             '("Extra: ~s0." (nats=>string rest)))))
              'nil))
            '((alt (abstract-group/option tree))))))
         (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-group
                         (cons (cons 'quote (cons alt 'nil))
                               (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)))
       'nil)))))))

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

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