		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rep-info

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

Signature
(deftreeops-gen-rep-info rep i check-conc-fn alt-singletonp rulename-upstring prefix) → info
Arguments: rep — Guard (repetitionp rep).; i — Indentifies the concatenation that this repetition is part of, starting from 1.
Guard (posp i).; 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-rep-infop info).

Definitions and Theorems

Function: deftreeops-gen-rep-info

(defun deftreeops-gen-rep-info
       (rep i check-conc-fn
            alt-singletonp rulename-upstring prefix)
 (declare
      (xargs :guard (and (repetitionp rep)
                         (posp i)
                         (common-lisp::symbolp check-conc-fn)
                         (booleanp alt-singletonp)
                         (common-lisp::stringp rulename-upstring)
                         (common-lisp::symbolp prefix))))
 (let ((__function__ 'deftreeops-gen-rep-info))
  (declare (ignorable __function__))
  (b*
   ((matching-thm
     (and
         (equal (repetition->range rep)
                (make-repeat-range :min 1
                                   :max (nati-finite 1)))
         (if alt-singletonp
             (packn-pos (list prefix '-
                              rulename-upstring '-conc-rep-matching)
                        prefix)
           (packn-pos (list prefix '-
                            rulename-upstring '-conc
                            i '-rep-matching)
                      prefix))))
    (get-tree-list-fn
         (and (equal (repetition->range rep)
                     (make-repeat-range :min 1
                                        :max (nati-finite 1)))
              (if alt-singletonp
                  (packn-pos (list prefix '-
                                   rulename-upstring '-conc-rep)
                             prefix)
                (and check-conc-fn
                     (packn-pos (list prefix '-
                                      rulename-upstring '-conc
                                      i '-rep)
                                prefix)))))
    (get-tree-fn (and get-tree-list-fn
                      (or alt-singletonp
                          (element-case (repetition->element rep)
                                        :rulename))
                      (packn-pos (list get-tree-list-fn '-elem)
                                 get-tree-list-fn))))
   (make-deftreeops-rep-info :matching-thm matching-thm
                             :get-tree-list-fn get-tree-list-fn
                             :get-tree-fn get-tree-fn))))

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

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