		Search-engine friendly clone of the ACL2 documentation.

Argument-partitioning

Vl-reorient-partitioned-args

Group arguments for instances after vl-partition-plainarglist.

Signature
(vl-reorient-partitioned-args lists n) → *
Arguments: lists — Guard (true-listp lists).; n — Guard (natp n).

We are given lists, which should be a vl-plainarglistlist-p formed by calling vl-partition-plainarglist, and n, the number of instances we are trying to generate. Note that every list in lists has length n.

At this point, the args are bundled up in a bad order. That is, to create the new instances, we want to have lists of the form

(arg1-slice1 arg2-slice1 arg3-slice1 ...) for the first instance,
(arg1-slice2 arg2-slice2 arg3-slice2 ...) for the second instance,
etc.

But instead, what vl-partition-plainarglist does is create lists of the slices, e.g.,

(arg1-slice1 arg1-slice2 arg1-slice3 ...)
(arg2-slice1 arg2-slice2 arg2-slice3 ...)
etc.

So our goal is simply to simply transpose this matrix and aggregate the data by slice, rather than by argument.

Definitions and Theorems

Function: vl-reorient-partitioned-args

(defun vl-reorient-partitioned-args (lists n)
  (declare (xargs :guard (and (true-listp lists) (natp n))))
  (declare (xargs :guard (all-have-len lists n)))
  (let ((__function__ 'vl-reorient-partitioned-args))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (cons (strip-cars lists)
            (vl-reorient-partitioned-args (strip-cdrs lists)
                                          (- n 1))))))

Theorem: vl-plainarglistlist-p-of-vl-reorient-partitioned-args

(defthm vl-plainarglistlist-p-of-vl-reorient-partitioned-args
 (implies
    (and (force (vl-plainarglistlist-p lists))
         (force (all-have-len lists n)))
    (vl-plainarglistlist-p (vl-reorient-partitioned-args lists n))))

Theorem: all-have-len-of-vl-reorient-partitioned-args

(defthm all-have-len-of-vl-reorient-partitioned-args
  (all-have-len (vl-reorient-partitioned-args lists n)
                (len lists)))

Theorem: len-of-vl-reorient-partitioned-args

(defthm len-of-vl-reorient-partitioned-args
  (equal (len (vl-reorient-partitioned-args lists n))
         (nfix n)))

Theorem: vl-reorient-partitioned-args-of-list-fix-lists

(defthm vl-reorient-partitioned-args-of-list-fix-lists
  (equal (vl-reorient-partitioned-args (list-fix lists)
                                       n)
         (vl-reorient-partitioned-args lists n)))

Theorem: vl-reorient-partitioned-args-list-equiv-congruence-on-lists

(defthm vl-reorient-partitioned-args-list-equiv-congruence-on-lists
  (implies (list-equiv lists lists-equiv)
           (equal (vl-reorient-partitioned-args lists n)
                  (vl-reorient-partitioned-args lists-equiv n)))
  :rule-classes :congruence)

Theorem: vl-reorient-partitioned-args-of-nfix-n

(defthm vl-reorient-partitioned-args-of-nfix-n
  (equal (vl-reorient-partitioned-args lists (nfix n))
         (vl-reorient-partitioned-args lists n)))

Theorem: vl-reorient-partitioned-args-nat-equiv-congruence-on-n

(defthm vl-reorient-partitioned-args-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-reorient-partitioned-args lists n)
                  (vl-reorient-partitioned-args lists n-equiv)))
  :rule-classes :congruence)