		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-arg/res-list-surj

Process an (arg/res-list surj) component of the surjmaps input.

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

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

Definitions and Theorems

Function: expdata-process-arg/res-list-surj-add-args

(defun expdata-process-arg/res-list-surj-add-args
       (args surjmap arg-surjmaps)
 (declare
  (xargs :guard (and (symbol-listp args)
                     (expdata-surjmapp surjmap)
                     (expdata-symbol-surjmap-alistp arg-surjmaps))))
 (let ((__function__ 'expdata-process-arg/res-list-surj-add-args))
   (declare (ignorable __function__))
   (cond ((endp args) arg-surjmaps)
         (t (expdata-process-arg/res-list-surj-add-args
                 (cdr args)
                 surjmap
                 (acons (car args)
                        surjmap arg-surjmaps))))))

Theorem: expdata-symbol-surjmap-alistp-of-expdata-process-arg/res-list-surj-add-args

(defthm
 expdata-symbol-surjmap-alistp-of-expdata-process-arg/res-list-surj-add-args
 (implies (and (symbol-listp args)
               (expdata-surjmapp surjmap)
               (expdata-symbol-surjmap-alistp arg-surjmaps))
          (b* ((new-arg-surjmaps (expdata-process-arg/res-list-surj-add-args
                                      args surjmap arg-surjmaps)))
            (expdata-symbol-surjmap-alistp new-arg-surjmaps)))
 :rule-classes :rewrite)

Function: expdata-process-arg/res-list-surj-add-ress

(defun expdata-process-arg/res-list-surj-add-ress
       (ress surjmap res-surjmaps)
 (declare
     (xargs :guard (and (pos-listp ress)
                        (expdata-surjmapp surjmap)
                        (expdata-pos-surjmap-alistp res-surjmaps))))
 (let ((__function__ 'expdata-process-arg/res-list-surj-add-ress))
   (declare (ignorable __function__))
   (cond ((endp ress) res-surjmaps)
         (t (expdata-process-arg/res-list-surj-add-ress
                 (cdr ress)
                 surjmap
                 (acons (car ress)
                        surjmap res-surjmaps))))))

Theorem: expdata-pos-surjmap-alistp-of-expdata-process-arg/res-list-surj-add-ress

(defthm
 expdata-pos-surjmap-alistp-of-expdata-process-arg/res-list-surj-add-ress
 (implies (and (pos-listp ress)
               (expdata-surjmapp surjmap)
               (expdata-pos-surjmap-alistp res-surjmaps))
          (b* ((new-res-surjmaps (expdata-process-arg/res-list-surj-add-ress
                                      ress surjmap res-surjmaps)))
            (expdata-pos-surjmap-alistp new-res-surjmaps)))
 :rule-classes :rewrite)

Function: expdata-process-arg/res-list-surj

(defun expdata-process-arg/res-list-surj
       (arg/res-list-surj k old$ verify-guards$ arg-surjmaps
                          res-surjmaps names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare
     (xargs :guard (and (posp k)
                        (symbolp old$)
                        (booleanp verify-guards$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (symbol-listp names-to-avoid))))
 (let ((__function__ 'expdata-process-arg/res-list-surj))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-tuple$ arg/res-list-surj 2
                    (msg "The ~n0 component of the second input"
                         (list k))
                    t nil))
    (arg/res-list (first arg/res-list-surj))
    (surj (second arg/res-list-surj))
    ((er (list args ress))
     (expdata-process-arg/res-list arg/res-list k old$ ctx state))
    (arg-overlap (intersection-eq args (strip-cars arg-surjmaps)))
    ((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-surjmaps)))
    ((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 surjmap names-to-avoid))
     (expdata-process-surj surj k old$ verify-guards$
                           names-to-avoid ctx state))
    (arg-surjmaps (expdata-process-arg/res-list-surj-add-args
                       args surjmap arg-surjmaps))
    (res-surjmaps (expdata-process-arg/res-list-surj-add-ress
                       ress surjmap res-surjmaps)))
   (value (list arg-surjmaps
                res-surjmaps names-to-avoid)))))