Generate the information and events for all the rulenames in a grammar.
(deftreeops-gen-all-rulename-infos+events rules charval-infos prefix) → (mv rulename-infos rulename-events)
We generate the events in an order that keeps analogous events together and avoids forward references.
Function:
(defun deftreeops-gen-all-rulename-infos+events (rules charval-infos prefix) (declare (xargs :guard (and (rulelistp rules) (deftreeops-charval-info-alistp charval-infos) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-all-rulename-infos+events)) (declare (ignorable __function__)) (b* ((infos (deftreeops-gen-rulename-info-alist rules prefix)) ((mv nonleaf-thm-events rulename-thm-events match-thm-events concs-thm-events conc-equivs-thm-events check-conc-fn-events get-tree-list-list-fn-events conc-matching-thm-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events) (deftreeops-gen-rulename-alist-events infos charval-infos prefix)) (events (append nonleaf-thm-events rulename-thm-events match-thm-events concs-thm-events conc-matching-thm-events rep-matching-thm-events conc-equivs-thm-events check-conc-fn-events get-tree-list-list-fn-events get-tree-list-fn-events get-tree-fn-events))) (mv infos events))))
Theorem:
(defthm deftreeops-rulename-info-alistp-of-deftreeops-gen-all-rulename-infos+events.rulename-infos (b* (((mv ?rulename-infos ?rulename-events) (deftreeops-gen-all-rulename-infos+events rules charval-infos prefix))) (deftreeops-rulename-info-alistp rulename-infos)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-all-rulename-infos+events.rulename-events (b* (((mv ?rulename-infos ?rulename-events) (deftreeops-gen-all-rulename-infos+events rules charval-infos prefix))) (pseudo-event-form-listp rulename-events)) :rule-classes :rewrite)