		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-conc-info

Generate the information for a concatenation in the alternation that defines a rule name.

Signature
(deftreeops-gen-conc-info conc i discriminant-term check-conc-fn alt-singletonp rulename-upstring prefix) → info
Arguments: conc — Guard (concatenationp conc).; i — Indentifies the concatenation, starting from 1.
Guard (posp i).; discriminant-term — The discriminant term for the concatenation.; check-conc-fn — The check-conc-fn component of deftreeops-rulename-info.
Guard (common-lisp::symbolp check-conc-fn).; alt-singletonp — Whether the alternation that defines the rule name consists of a single concatenation or not.
Guard (booleanp alt-singletonp).; rulename-upstring — Rule name normalized in uppercase.
Guard (common-lisp::stringp rulename-upstring).; prefix — Guard (common-lisp::symbolp prefix).
Returns: info — Type (deftreeops-conc-infop info).

Definitions and Theorems

Function: deftreeops-gen-conc-info

(defun deftreeops-gen-conc-info
       (conc i discriminant-term check-conc-fn
             alt-singletonp rulename-upstring prefix)
 (declare
      (xargs :guard (and (concatenationp conc)
                         (posp i)
                         (common-lisp::symbolp check-conc-fn)
                         (booleanp alt-singletonp)
                         (common-lisp::stringp rulename-upstring)
                         (common-lisp::symbolp prefix))))
 (let ((__function__ 'deftreeops-gen-conc-info))
  (declare (ignorable __function__))
  (b*
   ((conc-singletonp (and (consp conc)
                          (not (consp (cdr conc)))))
    (matching-thm
        (and conc-singletonp
             (if alt-singletonp
                 (packn-pos (list prefix '-
                                  rulename-upstring '-conc-matching)
                            prefix)
               (packn-pos (list prefix '-
                                rulename-upstring '-conc
                                i '-matching)
                          prefix))))
    (check-conc-fn-equiv-thm
         (and check-conc-fn
              (packn-pos (list check-conc-fn '-
                               i '-iff-match-conc)
                         check-conc-fn)))
    (get-tree-list-list-fn
       (if alt-singletonp (packn-pos (list prefix '-
                                           rulename-upstring '-conc)
                                     prefix)
         (and check-conc-fn
              (packn-pos (list prefix '-
                               rulename-upstring '-conc
                               i)
                         prefix))))
    (rep-infos (and conc-singletonp
                    (deftreeops-gen-rep-info-list
                         conc i check-conc-fn alt-singletonp
                         rulename-upstring prefix)))
    (info (make-deftreeops-conc-info
               :conc conc
               :discriminant-term discriminant-term
               :check-conc-fn-equiv-thm check-conc-fn-equiv-thm
               :get-tree-list-list-fn get-tree-list-list-fn
               :matching-thm matching-thm
               :rep-infos rep-infos)))
   info)))

Theorem: deftreeops-conc-infop-of-deftreeops-gen-conc-info

(defthm deftreeops-conc-infop-of-deftreeops-gen-conc-info
  (b* ((info (deftreeops-gen-conc-info conc i discriminant-term
                                       check-conc-fn alt-singletonp
                                       rulename-upstring prefix)))
    (deftreeops-conc-infop info))
  :rule-classes :rewrite)