Generate the first of the specialized matching predicates.
(deftreeops-gen-cst-match grammar prefix) → events
Function:
(defun deftreeops-gen-cst-match (grammar prefix) (declare (xargs :guard (and (common-lisp::symbolp grammar) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-cst-match)) (declare (ignorable __function__)) (b* ((cst-matchp (deftreeops-match-pred prefix)) (cst-matchp$ (add-suffix-to-fn cst-matchp "$"))) (cons (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)))))))) (cons (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))))) (cons (cons 'table (cons 'acl2::macro-aliases-table (cons (cons 'quote (cons cst-matchp 'nil)) (cons (cons 'quote (cons cst-matchp$ 'nil)) 'nil)))) 'nil))))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-cst-match (b* ((events (deftreeops-gen-cst-match grammar prefix))) (pseudo-event-form-listp events)) :rule-classes :rewrite)