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* (((mv matchers matchers-event-alist) (deftreeops-gen-matchers grammar prefix)) ((mv numrange-infos numrange-events numrange-event-alist) (deftreeops-gen-all-numrange-infos+events rules prefix)) ((mv charval-infos charval-events charval-event-alist) (deftreeops-gen-all-charval-infos+events rules prefix)) ((mv rulename-infos rulename-events rulename-event-alist) (deftreeops-gen-all-rulename-infos+events rules charval-infos prefix)) (event-alist (append matchers-event-alist numrange-event-alist charval-event-alist rulename-event-alist)) (table-value (make-deftreeops-table-value :rulename-info-alist rulename-infos :numrange-info-alist numrange-infos :charval-info-alist charval-infos :event-alist event-alist :call call)) (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 numrange-events (append charval-events (append rulename-events (cons (deftreeops-table-add grammar 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)