		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-matchers

Generate the specialized matching predicates.

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

(defun deftreeops-gen-matchers (grammar prefix print)
 (declare (xargs :guard (and (common-lisp::symbolp grammar)
                             (common-lisp::symbolp prefix)
                             (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-matchers))
  (declare (ignorable __function__))
  (b*
   (((mv cst-match-events cst-match-event-alist)
     (deftreeops-gen-cst-match grammar prefix print))
    ((mv cst-list-elem-match-events
         cst-list-elem-match-event-alist)
     (deftreeops-gen-cst-list-elem-match grammar prefix print))
    ((mv cst-list-rep-match-events
         cst-list-rep-match-event-alist)
     (deftreeops-gen-cst-list-rep-match grammar prefix print))
    ((mv cst-list-list-conc-match-events
         cst-list-list-conc-match-event-alist)
     (deftreeops-gen-cst-list-list-conc-match grammar prefix print))
    ((mv cst-list-list-alt-match-events
         cst-list-list-alt-match-event-alist)
     (deftreeops-gen-cst-list-list-alt-match grammar prefix print)))
   (mv (append cst-match-events
               cst-list-elem-match-events
               cst-list-rep-match-events
               cst-list-list-conc-match-events
               cst-list-list-alt-match-events)
       (append cst-match-event-alist
               cst-list-elem-match-event-alist
               cst-list-rep-match-event-alist
               cst-list-list-conc-match-event-alist
               cst-list-list-alt-match-event-alist)))))

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

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

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

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