		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-process-static-terms

Process the c1, ..., cm parts of the static input.

Signature
(parteval-process-static-terms cj...cm yj...ym old$ verify-guards$ ctx state) → (mv erp cj...cm$ state)
Arguments: cj...cm — List (c1 ... cm) initially, then a tail of that in the recursive calls.
Guard (true-listp cj...cm).; yj...ym — Guard (symbol-listp yj...ym).; old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: cj...cm$ — The pseudo-term-listp list of terms cj...cm, in translated form.

Definitions and Theorems

Function: parteval-process-static-terms

(defun parteval-process-static-terms
       (cj...cm yj...ym old$ verify-guards$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp cj...cm)
                             (symbol-listp yj...ym)
                             (symbolp old$)
                             (booleanp verify-guards$))))
 (declare (xargs :guard (equal (len cj...cm) (len yj...ym))))
 (let ((__function__ 'parteval-process-static-terms))
  (declare (ignorable __function__))
  (b*
   (((when (endp cj...cm)) (value nil))
    (yj (car yj...ym))
    (cj (car cj...cm))
    (description
         (msg "The term ~x0 assigned to the static parameter ~x1"
              cj yj))
    ((er (list cj$ stobjs-out))
     (ensure-value-is-untranslated-term$ cj description t nil))
    ((er &)
     (ensure-term-ground$ cj$ description t nil))
    ((er &)
     (ensure-term-logic-mode$ cj$ description t nil))
    ((er &)
     (ensure-function/lambda/term-number-of-results$
          stobjs-out 1 description t nil))
    ((er &)
     (ensure-term-no-stobjs$ stobjs-out description t nil))
    ((er &)
     (if verify-guards$
      (ensure-term-guard-verified-exec-fns$
       cj$
       (msg
        "Since either the :VERIFY-GUARDS input is T, ~
                          or it is (perhaps by default) :AUTO ~
                          and the target function ~x0 is guard-verified, ~@1"
        old$ (msg-downcase-first description))
       t nil)
      (value :this-is-irrelevant)))
    ((er &)
     (ensure-term-does-not-call$ cj$ old$ description t nil))
    (cj+1...cm (cdr cj...cm))
    (yj+1...ym (cdr yj...ym))
    ((er cj+1...cm$)
     (parteval-process-static-terms cj+1...cm yj+1...ym
                                    old$ verify-guards$ ctx state)))
   (value (cons cj$ cj+1...cm$)))))