		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-surjmaps

Process the surjmaps input.

Signature
(expdata-process-surjmaps surjmaps 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-surjmaps res-surjmaps updated-names-to-avoid) satisfying (typed-tuplep expdata-symbol-surjmap-alistp expdata-pos-surjmap-alistp symbol-listp result).

Starting from the empty alists for arg-surjmaps and res-surjmap, we repeatedly process each (arg/res-listk surjk) element, accumulating the processing results into arg-surjmaps and res-surjmaps. Then we reconstruct a possible larger arg-surjmaps 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 surjective mapping. If the final res-surjmaps is not empty, we similarly reconstruct a possibly larger res-surjmaps 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 surjective mapping.

Definitions and Theorems

Function: expdata-process-surjmaps-args

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

Theorem: expdata-symbol-surjmap-alistp-of-expdata-process-surjmaps-args

(defthm
     expdata-symbol-surjmap-alistp-of-expdata-process-surjmaps-args
 (implies
      (and (symbol-listp formals)
           (expdata-symbol-surjmap-alistp arg-surjmaps)
           (expdata-surjmapp surjmap-id))
      (b* ((new-arg-surjmaps (expdata-process-surjmaps-args
                                  formals arg-surjmaps surjmap-id)))
        (expdata-symbol-surjmap-alistp new-arg-surjmaps)))
 :rule-classes :rewrite)

Function: expdata-process-surjmaps-ress

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

Theorem: expdata-pos-surjmap-alistp-of-expdata-process-surjmaps-ress

(defthm expdata-pos-surjmap-alistp-of-expdata-process-surjmaps-ress
 (implies
  (and (posp j)
       (posp m)
       (expdata-pos-surjmap-alistp res-surjmaps)
       (expdata-surjmapp surjmap-id))
  (b*
   ((new-res-surjmaps
       (expdata-process-surjmaps-ress j m res-surjmaps surjmap-id)))
   (expdata-pos-surjmap-alistp new-res-surjmaps)))
 :rule-classes :rewrite)

Function: expdata-process-surjmaps

(defun expdata-process-surjmaps
       (surjmaps 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__ 'expdata-process-surjmaps))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (true-listp surjmaps))
     (er-soft+
      ctx t nil
      "The second input must be a true list, ~
                   but it is ~x0 instead."
      surjmaps))
    ((unless (>= (len surjmaps) 1))
     (er-soft+
      ctx t nil
      "The second input must be a non-empty list, ~
                   but it is ~x0 instead."
      surjmaps))
    ((er (list arg-surjmaps
               res-surjmaps names-to-avoid))
     (expdata-process-arg/res-list-surj-list
          surjmaps 1 old$ verify-guards$
          nil nil names-to-avoid ctx state))
    (surjname-id
        (expdata-fresh-defsurj-name-with-*s-suffix 'defsurj-identity
                                                   wrld))
    ((mv forth-image-id
         back-image-id back-of-forth-id
         oldp-guard-id newp-guard-id
         forth-guard-id back-guard-id
         forth-injective-id names-to-avoid)
     (expdata-fresh-defsurj-thm-names
          surjname-id
          verify-guards$ names-to-avoid wrld))
    (surjmap-id
         (make-expdata-surjmap :surjname surjname-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-injective forth-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-surjmaps (expdata-process-surjmaps-args
                       formals arg-surjmaps surjmap-id))
    (res-surjmaps
     (and
      res-surjmaps
      (expdata-process-surjmaps-ress 1 (number-of-results old$ wrld)
                                     res-surjmaps surjmap-id))))
   (value (list arg-surjmaps
                res-surjmaps names-to-avoid)))))