		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rulename-info

Generate the information for a rule name.

Signature
(deftreeops-gen-rulename-info rulename alt prefix) → info
Arguments: rulename — Guard (rulenamep rulename).; alt — The alternation that define rulename.
Guard (alternationp alt).; prefix — Guard (common-lisp::symbolp prefix).
Returns: info — Type (deftreeops-rulename-infop info).

Definitions and Theorems

Function: deftreeops-gen-rulename-info

(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: deftreeops-rulename-infop-of-deftreeops-gen-rulename-info

(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)