		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-process-static

Process the static input.

Signature
(parteval-process-static static old$ verify-guards$ ctx state) → (mv erp static$ state)
Arguments: old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: static$ — A symbol-alistp from y1, ..., ym to the translated c1, ..., cm.

Definitions and Theorems

Function: parteval-process-static

(defun parteval-process-static
       (static old$ verify-guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (booleanp verify-guards$))))
 (let ((__function__ 'parteval-process-static))
   (declare (ignorable __function__))
   (b* (((er &)
         (ensure-doublet-list$ static "The second input" t nil))
        (alist (doublets-to-alist static))
        (y1...ym (strip-cars alist))
        (description (msg "The list ~x0 of static parameters"
                          y1...ym))
        ((when (null y1...ym))
         (er-soft+ ctx t nil
                   "~@0 must not be empty." description))
        ((er &)
         (ensure-list-has-no-duplicates$ y1...ym description t nil))
        ((er &)
         (ensure-value-is-symbol-list$ y1...ym description t nil))
        ((er &)
         (ensure-list-subset$ y1...ym (formals old$ (w state))
                              description t nil))
        (c1...cm (strip-cdrs alist))
        ((er c1...cm$)
         (parteval-process-static-terms
              c1...cm
              y1...ym old$ verify-guards$ ctx state))
        (static$ (pairlis$ y1...ym c1...cm$)))
     (value static$))))