Generate the information for a rule name.
(deftreeops-gen-rulename-info rulename alt prefix) → info
Function:
(defun deftreeops-gen-rulename-info (rulename alt prefix) (declare (xargs :guard (and (rulenamep rulename) (alternationp alt) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-rulename-info)) (declare (ignorable __function__)) (b* ((rulename-string (rulename->get rulename)) (rulename-upstring (str::upcase-string rulename-string)) (nonleaf-thm (packn-pos (list prefix '- rulename-upstring '-nonleaf) prefix)) (rulename-thm (packn-pos (list prefix '- rulename-upstring '-rulename) prefix)) (match-thm (packn-pos (list prefix '- rulename-upstring '-branches-match-alt) prefix)) (concs-thm (packn-pos (list prefix '- rulename-upstring '-concs) prefix)) ((mv terms alt-kind) (deftreeops-gen-discriminant-terms alt)) (terms-or-nils (or terms (repeat (len alt) nil))) (alt-singletonp (and (consp alt) (endp (cdr alt)))) (conc-equivs-thm (and (not alt-singletonp) terms (packn-pos (list prefix '- rulename-upstring '-conc-equivs) prefix))) (check-conc-fn (and (not alt-singletonp) terms (= alt-kind 1) (packn-pos (list prefix '- rulename-upstring '-conc?) prefix))) (conc-infos (deftreeops-gen-conc-info-list alt terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix)) (info (make-deftreeops-rulename-info :alt alt :nonleaf-thm nonleaf-thm :rulename-thm rulename-thm :match-thm match-thm :concs-thm concs-thm :conc-equivs-thm conc-equivs-thm :alt-kind alt-kind :check-conc-fn check-conc-fn :conc-infos conc-infos))) info)))
Theorem:
(defthm deftreeops-rulename-infop-of-deftreeops-gen-rulename-info (b* ((info (deftreeops-gen-rulename-info rulename alt prefix))) (deftreeops-rulename-infop info)) :rule-classes :rewrite)