		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-cst-list-rep-match

Generate the third of the specialized matching predicates.

Signature
(deftreeops-gen-cst-list-rep-match grammar prefix print) → (mv events event-alist)
Arguments: grammar — Guard (common-lisp::symbolp grammar).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).
Returns: events — Type (pseudo-event-form-listp events).; event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-cst-list-rep-match

(defun deftreeops-gen-cst-list-rep-match (grammar prefix print)
 (declare (xargs :guard (and (common-lisp::symbolp grammar)
                             (common-lisp::symbolp prefix)
                             (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-cst-list-rep-match))
  (declare (ignorable __function__))
  (b*
   ((cst-list-rep-matchp (deftreeops-rep-match-pred prefix))
    (cst-list-rep-matchp$
         (add-suffix-to-fn cst-list-rep-matchp "$"))
    (cst-list-rep-matchp$-event
     (cons
      'define
      (cons
       cst-list-rep-matchp$
       (cons
        '((trees tree-listp) (rep repetitionp))
        (cons
         ':returns
         (cons
          '(yes/no booleanp)
          (cons
           (cons
            'and
            (cons
                 '(tree-list-terminatedp trees)
                 (cons (cons 'tree-list-match-repetition-p
                             (cons 'trees
                                   (cons 'rep (cons grammar 'nil))))
                       'nil)))
           '(:hooks (:fix)))))))))
    (cst-list-rep-matchp-event
     (cons
      'defmacro
      (cons
       cst-list-rep-matchp
       (cons
        '(trees rep)
        (cons
         '(declare (xargs :guard (common-lisp::stringp rep)))
         (cons
          (cons
           'b*
           (cons
            (cons
             '((mv err rep rest)
               (parse-repetition (string=>nats rep)))
             (cons
              (cons
               '(when err)
               (cons
                (cons
                  'er
                  (cons 'hard
                        (cons (cons 'quote
                                    (cons cst-list-rep-matchp 'nil))
                              '("~@0" err))))
                'nil))
              (cons
               (cons
                '(when (consp rest))
                (cons
                 (cons
                  'er
                  (cons 'hard
                        (cons (cons 'quote
                                    (cons cst-list-rep-matchp 'nil))
                              '("Extra: ~s0" (nats=>string rest)))))
                 'nil))
               '((rep (abstract-repetition rep))))))
            (cons
             (cons 'cons
                   (cons (cons 'quote
                               (cons cst-list-rep-matchp$ 'nil))
                         '((cons trees
                                 (cons (cons 'quote (cons rep 'nil))
                                       'nil)))))
             'nil)))
          'nil))))))
    (table-event
     (cons 'table
           (cons 'acl2::macro-aliases-table
                 (cons (cons 'quote
                             (cons cst-list-rep-matchp 'nil))
                       (cons (cons 'quote
                                   (cons cst-list-rep-matchp$ 'nil))
                             'nil)))))
    (print-event?
     (and
      (evmac-input-print->= print :result)
      (cons
       (cons
            'cw-event
            (cons '"Function ~x0 and macro ~x1.~%"
                  (cons (cons 'quote
                              (cons cst-list-rep-matchp$ 'nil))
                        (cons (cons 'quote
                                    (cons cst-list-rep-matchp 'nil))
                              'nil))))
       'nil))))
   (mv (list* cst-list-rep-matchp$-event
              cst-list-rep-matchp-event
              table-event print-event?)
       (list (cons cst-list-rep-matchp$
                   cst-list-rep-matchp$-event)
             (cons cst-list-rep-matchp
                   cst-list-rep-matchp-event))))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-cst-list-rep-match.events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-cst-list-rep-match.events
 (b* (((mv ?events ?event-alist)
       (deftreeops-gen-cst-list-rep-match grammar prefix print)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-cst-list-rep-match.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-cst-list-rep-match.event-alist
 (b* (((mv ?events ?event-alist)
       (deftreeops-gen-cst-list-rep-match grammar prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)