		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-isomaps

Process the isomaps input.

Signature
(isodata-process-isomaps isomaps old$ verify-guards$ names-to-avoid ctx state) → (mv erp result state)
Arguments: old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A tuple (arg-isomaps res-isomaps update-names-to-avoid) satisfying (typed-tuplep isodata-symbol-isomap-alistp isodata-pos-isomap-alistp symbol-listp result).

Starting from the empty alists for arg-isomaps and res-isomap, we repeatedly process each (arg/res-listk isok) element, accumulating the processing results into arg-isomaps and res-isomaps. Then we reconstruct a possible larger arg-isomaps by going through the formal parameters of old in order, and associating them, in the new alist, with either the corresponding value in the old alist, or the identity isomorphic mapping. If the final res-isomaps is not empty, we similarly reconstruct a possibly larger res-isomaps by going through the integers from 1 to m in order, and associating them, in the new alist, with either the corresponding value in the old alist, or the identity isomorphic mapping.

Definitions and Theorems

Function: isodata-process-isomaps-args

(defun isodata-process-isomaps-args (formals arg-isomaps isomap-id)
 (declare
      (xargs :guard (and (symbol-listp formals)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-isomapp isomap-id))))
 (let ((__function__ 'isodata-process-isomaps-args))
  (declare (ignorable __function__))
  (b* (((when (endp formals)) nil)
       (pair (assoc-eq (car formals) arg-isomaps)))
   (if (consp pair)
       (cons pair
             (isodata-process-isomaps-args (cdr formals)
                                           arg-isomaps isomap-id))
    (acons (car formals)
           isomap-id
           (isodata-process-isomaps-args (cdr formals)
                                         arg-isomaps isomap-id))))))

Theorem: isodata-symbol-isomap-alistp-of-isodata-process-isomaps-args

(defthm isodata-symbol-isomap-alistp-of-isodata-process-isomaps-args
 (implies
  (and (symbol-listp formals)
       (isodata-symbol-isomap-alistp arg-isomaps)
       (isodata-isomapp isomap-id))
  (b*
   ((new-arg-isomaps
      (isodata-process-isomaps-args formals arg-isomaps isomap-id)))
   (isodata-symbol-isomap-alistp new-arg-isomaps)))
 :rule-classes :rewrite)

Function: isodata-process-isomaps-ress

(defun isodata-process-isomaps-ress (j m res-isomaps isomap-id)
 (declare (xargs :guard (and (posp j)
                             (posp m)
                             (isodata-pos-isomap-alistp res-isomaps)
                             (isodata-isomapp isomap-id))))
 (let ((__function__ 'isodata-process-isomaps-ress))
  (declare (ignorable __function__))
  (b* (((unless (mbt (and (posp j) (posp m))))
        nil)
       ((when (> j m)) nil)
       (pair (assoc j res-isomaps)))
   (if (consp pair)
       (cons pair
             (isodata-process-isomaps-ress (1+ j)
                                           m res-isomaps isomap-id))
    (acons
         j isomap-id
         (isodata-process-isomaps-ress (1+ j)
                                       m res-isomaps isomap-id))))))

Theorem: isodata-pos-isomap-alistp-of-isodata-process-isomaps-ress

(defthm isodata-pos-isomap-alistp-of-isodata-process-isomaps-ress
 (implies
   (and (posp j)
        (posp m)
        (isodata-pos-isomap-alistp res-isomaps)
        (isodata-isomapp isomap-id))
   (b*
    ((new-res-isomaps
          (isodata-process-isomaps-ress j m res-isomaps isomap-id)))
    (isodata-pos-isomap-alistp new-res-isomaps)))
 :rule-classes :rewrite)

Function: isodata-process-isomaps

(defun isodata-process-isomaps
       (isomaps old$
                verify-guards$ names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (booleanp verify-guards$)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'isodata-process-isomaps))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (true-listp isomaps))
     (er-soft+
      ctx t nil
      "The second input must be a true list, ~
                   but it is ~x0 instead."
      isomaps))
    ((unless (>= (len isomaps) 1))
     (er-soft+
      ctx t nil
      "The second input must be a non-empty list, ~
                   but it is ~x0 instead."
      isomaps))
    ((er (list arg-isomaps res-isomaps names-to-avoid))
     (isodata-process-arg/res-list-iso-list
          isomaps 1 old$ verify-guards$
          nil nil names-to-avoid ctx state))
    (isoname-id
         (isodata-fresh-defiso-name-with-*s-suffix 'defiso-identity
                                                   wrld))
    ((mv forth-image-id
         back-image-id back-of-forth-id
         forth-of-back-id oldp-guard-id
         newp-guard-id forth-guard-id
         back-guard-id forth-injective-id
         back-injective-id names-to-avoid)
     (isodata-fresh-defiso-thm-names
          isoname-id
          verify-guards$ names-to-avoid wrld))
    (isomap-id
         (make-isodata-isomap :isoname isoname-id
                              :localp t
                              :oldp '(lambda (x) 't)
                              :newp '(lambda (x) 't)
                              :forth '(lambda (x) x)
                              :back '(lambda (x) x)
                              :back-image back-image-id
                              :forth-image forth-image-id
                              :back-of-forth back-of-forth-id
                              :forth-of-back forth-of-back-id
                              :forth-injective forth-injective-id
                              :back-injective back-injective-id
                              :oldp-guard oldp-guard-id
                              :newp-guard newp-guard-id
                              :forth-guard forth-guard-id
                              :back-guard back-guard-id
                              :hints nil))
    (formals (formals old$ wrld))
    (arg-isomaps
       (isodata-process-isomaps-args formals arg-isomaps isomap-id))
    (res-isomaps
     (and
       res-isomaps
       (isodata-process-isomaps-ress 1 (number-of-results old$ wrld)
                                     res-isomaps isomap-id))))
   (value (list arg-isomaps
                res-isomaps names-to-avoid)))))