Generate all the events.
(deftreeops-gen-everything grammar rules prefix call) → event
Function:
(defun deftreeops-gen-everything (grammar rules prefix call) (declare (xargs :guard (and (common-lisp::symbolp grammar) (rulelistp rules) (common-lisp::symbolp prefix) (pseudo-event-formp call)))) (let ((__function__ 'deftreeops-gen-everything)) (declare (ignorable __function__)) (b* ((matchers (deftreeops-gen-matchers grammar prefix)) ((mv rulename-infos rulename-events) (deftreeops-gen-all-rulename-infos+events rules prefix)) ((mv numrange-infos numrange-events) (deftreeops-gen-all-numrange-infos+events rules prefix)) (table-value (make-deftreeops-table-value :rulename-info-alist rulename-infos :numrange-info-alist numrange-infos)) (event (cons 'defsection (cons (add-suffix grammar "-TREE-OPERATIONS") (cons ':parents (cons (cons grammar 'nil) (cons ':short (cons (str::cat "Tree operations specialized to @(tsee " (str::downcase-string (symbol-name grammar)) ").") (append matchers (append rulename-events (append numrange-events (cons (deftreeops-table-add call table-value) 'nil)))))))))))) event)))
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-everything (b* ((event (deftreeops-gen-everything grammar rules prefix call))) (pseudo-event-formp event)) :rule-classes :rewrite)