		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-arg/res-list-iso

Process an (arg/res-list iso) component of the isomaps input.

Signature
(isodata-process-arg/res-list-iso arg/res-list-iso k old$ verify-guards$ arg-isomaps res-isomaps names-to-avoid ctx state) → (mv erp result state)
Arguments: arg/res-list-iso — The (arg/res-listk isok) component of isomaps.; k — The k in (arg/res-listk isok).
Guard (posp k).; old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A tuple (arg-isomaps res-isomaps updated-names-to-avoid) satisfying (typed-tuplep isodata-symbol-isomap-alistp isodata-pos-isomap-alistp symbol-listp result).

The arg-isomaps and res-isomaps inputs are obtained by having previously called this function on (arg/res-list1 iso1), ..., (arg/res-listk-1 isok-1) in turn. When we call this function on (arg/res-listk isok), we extend arg-isomaps and res-isomaps with the information in (arg/res-listk isok). As we do that, we check that the arguments of old in arg/res-listk are not already keys in arg-isomaps: if any of them did, it would mean that it is already present in one of (arg/res-list1 iso1), ..., (arg/res-listk-1 isok-1), violating the disjointness requirement. Similarly, we check that the result indices in arg/res-listk are not already keys in res-isomaps: if any of them did, it would mean that the same result is already present in one of (arg/res-list1 iso1), ..., (arg/res-listk-1 isok-1), violating the disjointness requirement.

Definitions and Theorems

Function: isodata-process-arg/res-list-iso-add-args

(defun isodata-process-arg/res-list-iso-add-args
       (args isomap arg-isomaps)
 (declare
    (xargs :guard (and (symbol-listp args)
                       (isodata-isomapp isomap)
                       (isodata-symbol-isomap-alistp arg-isomaps))))
 (let ((__function__ 'isodata-process-arg/res-list-iso-add-args))
   (declare (ignorable __function__))
   (cond ((endp args) arg-isomaps)
         (t (isodata-process-arg/res-list-iso-add-args
                 (cdr args)
                 isomap
                 (acons (car args)
                        isomap arg-isomaps))))))

Theorem: isodata-symbol-isomap-alistp-of-isodata-process-arg/res-list-iso-add-args

(defthm
 isodata-symbol-isomap-alistp-of-isodata-process-arg/res-list-iso-add-args
 (implies (and (symbol-listp args)
               (isodata-isomapp isomap)
               (isodata-symbol-isomap-alistp arg-isomaps))
          (b* ((new-arg-isomaps (isodata-process-arg/res-list-iso-add-args
                                     args isomap arg-isomaps)))
            (isodata-symbol-isomap-alistp new-arg-isomaps)))
 :rule-classes :rewrite)

Function: isodata-process-arg/res-list-iso-add-ress

(defun isodata-process-arg/res-list-iso-add-ress
       (ress isomap res-isomaps)
  (declare
       (xargs :guard (and (pos-listp ress)
                          (isodata-isomapp isomap)
                          (isodata-pos-isomap-alistp res-isomaps))))
  (let ((__function__ 'isodata-process-arg/res-list-iso-add-ress))
    (declare (ignorable __function__))
    (cond ((endp ress) res-isomaps)
          (t (isodata-process-arg/res-list-iso-add-ress
                  (cdr ress)
                  isomap
                  (acons (car ress)
                         isomap res-isomaps))))))

Theorem: isodata-pos-isomap-alistp-of-isodata-process-arg/res-list-iso-add-ress

(defthm
 isodata-pos-isomap-alistp-of-isodata-process-arg/res-list-iso-add-ress
 (implies (and (pos-listp ress)
               (isodata-isomapp isomap)
               (isodata-pos-isomap-alistp res-isomaps))
          (b* ((new-res-isomaps (isodata-process-arg/res-list-iso-add-ress
                                     ress isomap res-isomaps)))
            (isodata-pos-isomap-alistp new-res-isomaps)))
 :rule-classes :rewrite)

Function: isodata-process-arg/res-list-iso

(defun isodata-process-arg/res-list-iso
       (arg/res-list-iso k old$ verify-guards$ arg-isomaps
                         res-isomaps names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (posp k)
                         (symbolp old$)
                         (booleanp verify-guards$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (symbol-listp names-to-avoid))))
 (let ((__function__ 'isodata-process-arg/res-list-iso))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-tuple$ arg/res-list-iso 2
                    (msg "The ~n0 component of the second input"
                         (list k))
                    t nil))
    (arg/res-list (first arg/res-list-iso))
    (iso (second arg/res-list-iso))
    ((er (list args ress))
     (isodata-process-arg/res-list arg/res-list k old$ ctx state))
    (arg-overlap (intersection-eq args (strip-cars arg-isomaps)))
    ((when arg-overlap)
     (er-soft+
      ctx t nil
      "The ~n0 component of the second input includes ~&1, ~
                   which are also present in the preceding components. ~
                   This violates the disjointness requirement."
      (list k)
      arg-overlap))
    (res-overlap (intersection$ ress (strip-cars res-isomaps)))
    ((when res-overlap)
     (er-soft+
      ctx t nil
      "The ~n0 component of the second input includes ~
                   the ~s1 ~&2, ~
                   which ~s3 also present in the preceding components. ~
                   This violates the disjointness requirement."
      (list k)
      (if (= (len res-overlap) 1)
          "result with index"
        "results with indices")
      res-overlap
      (if (= (len res-overlap) 1)
          "is"
        "are")))
    ((er (list isomap names-to-avoid))
     (isodata-process-iso iso k old$ verify-guards$
                          names-to-avoid ctx state))
    (arg-isomaps (isodata-process-arg/res-list-iso-add-args
                      args isomap arg-isomaps))
    (res-isomaps (isodata-process-arg/res-list-iso-add-ress
                      ress isomap res-isomaps)))
   (value (list arg-isomaps
                res-isomaps names-to-avoid)))))