Generate the fourth of the specialized matching predicates.
(deftreeops-gen-cst-list-list-conc-match grammar prefix print) → (mv events event-alist)
Function:
(defun deftreeops-gen-cst-list-list-conc-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-list-conc-match)) (declare (ignorable __function__)) (b* ((cst-list-list-conc-matchp (deftreeops-conc-match-pred prefix)) (cst-list-list-conc-matchp$ (add-suffix-to-fn cst-list-list-conc-matchp "$")) (cst-list-list-conc-matchp$-event (cons 'define (cons cst-list-list-conc-matchp$ (cons '((treess tree-list-listp) (conc concatenationp)) (cons ':returns (cons '(yes/no booleanp) (cons (cons 'and (cons '(tree-list-list-terminatedp treess) (cons (cons 'tree-list-list-match-concatenation-p (cons 'treess (cons 'conc (cons grammar 'nil)))) 'nil))) '(:hooks (:fix))))))))) (cst-list-list-conc-matchp-event (cons 'defmacro (cons cst-list-list-conc-matchp (cons '(treess conc) (cons '(declare (xargs :guard (common-lisp::stringp conc))) (cons (cons 'b* (cons (cons '((mv err conc rest) (parse-concatenation (string=>nats conc))) (cons (cons '(when err) (cons (cons 'er (cons 'hard (cons (cons 'quote (cons cst-list-list-conc-matchp 'nil)) '("~@0" err)))) 'nil)) (cons (cons '(when (consp rest)) (cons (cons 'er (cons 'hard (cons (cons 'quote (cons cst-list-list-conc-matchp 'nil)) '("Extra: ~s0" (nats=>string rest))))) 'nil)) '((conc (abstract-concatenation conc)))))) (cons (cons 'cons (cons (cons 'quote (cons cst-list-list-conc-matchp$ 'nil)) '((cons treess (cons (cons 'quote (cons conc 'nil)) 'nil))))) 'nil))) 'nil)))))) (table-event (cons 'table (cons 'acl2::macro-aliases-table (cons (cons 'quote (cons cst-list-list-conc-matchp 'nil)) (cons (cons 'quote (cons cst-list-list-conc-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-list-conc-matchp$ 'nil)) (cons (cons 'quote (cons cst-list-list-conc-matchp 'nil)) 'nil)))) 'nil)))) (mv (list* cst-list-list-conc-matchp$-event cst-list-list-conc-matchp-event table-event print-event?) (list (cons cst-list-list-conc-matchp$ cst-list-list-conc-matchp$-event) (cons cst-list-list-conc-matchp cst-list-list-conc-matchp-event))))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-cst-list-list-conc-match.events (b* (((mv ?events ?event-alist) (deftreeops-gen-cst-list-list-conc-match grammar prefix print))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-cst-list-list-conc-match.event-alist (b* (((mv ?events ?event-alist) (deftreeops-gen-cst-list-list-conc-match grammar prefix print))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)