		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-cst-match

Generate the first of the specialized matching predicates.

Signature
(deftreeops-gen-cst-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-match

(defun deftreeops-gen-cst-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-match))
  (declare (ignorable __function__))
  (b*
   ((cst-matchp (deftreeops-match-pred prefix))
    (cst-matchp$ (add-suffix-to-fn cst-matchp "$"))
    (cst-matchp$-event
     (cons
      'define
      (cons
       cst-matchp$
       (cons
        '((tree treep) (elem elementp))
        (cons
         ':returns
         (cons
          '(yes/no booleanp)
          (cons
           (cons
            'and
            (cons
                '(tree-terminatedp tree)
                (cons (cons 'tree-match-element-p
                            (cons 'tree
                                  (cons 'elem (cons grammar 'nil))))
                      'nil)))
           '(:hooks (:fix)))))))))
    (cst-matchp-event
     (cons
      'defmacro
      (cons
       cst-matchp
       (cons
        '(tree elem)
        (cons
         '(declare (xargs :guard (common-lisp::stringp elem)))
         (cons
          (cons
           'b*
           (cons
            (cons
             '((mv err elem rest)
               (parse-element (string=>nats elem)))
             (cons
              (cons
               '(when err)
               (cons
                (cons
                    'er
                    (cons 'hard
                          (cons (cons 'quote (cons cst-matchp 'nil))
                                '("~@0" err))))
                'nil))
              (cons
               (cons
                '(when (consp rest))
                (cons
                 (cons
                  'er
                  (cons 'hard
                        (cons (cons 'quote (cons cst-matchp 'nil))
                              '("Extra: ~s0" (nats=>string rest)))))
                 'nil))
               '((elem (abstract-element elem))))))
            (cons
             (cons
                  'cons
                  (cons (cons 'quote (cons cst-matchp$ 'nil))
                        '((cons tree
                                (cons (cons 'quote (cons elem 'nil))
                                      'nil)))))
             'nil)))
          'nil))))))
    (table-event
       (cons 'table
             (cons 'acl2::macro-aliases-table
                   (cons (cons 'quote (cons cst-matchp 'nil))
                         (cons (cons 'quote (cons cst-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-matchp$ 'nil))
                          (cons (cons 'quote (cons cst-matchp 'nil))
                                'nil))))
        'nil))))
   (mv (list* cst-matchp$-event cst-matchp-event
              table-event print-event?)
       (list (cons cst-matchp$ cst-matchp$-event)
             (cons cst-matchp cst-matchp-event))))))

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

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

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

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