		Search-engine friendly clone of the ACL2 documentation.

Defmapping-input-processing

Defmapping-process-function

Process one of the input functions (i.e. doma, domb, alpha, or beta).

Signature
(defmapping-process-function function position guard-thms$ ctx state) → (mv erp result state)
Arguments: function — The doma, domb, alpha, or beta input to defmapping.; position — Position of the input in the ordered inputs to defmapping.
Guard (member position '(2 3 4 5)).; guard-thms$ — Guard (booleanp guard-thms$).
Returns: result — A tuple (function$ arity numres) satisfying (typed-tuplep pseudo-termfnp natp posp).

Return either the input unchanged (if it is a function name) or its translation (if it is a lambda expression). Also return the arity and the number of results.

Definitions and Theorems

Function: defmapping-process-function

(defun defmapping-process-function
       (function position guard-thms$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (member position '(2 3 4 5))
                             (booleanp guard-thms$))))
 (let ((__function__ 'defmapping-process-function))
  (declare (ignorable __function__))
  (b*
   (((er (list fn/lambda
               stobjs-in stobjs-out description))
     (ensure-function/macro/lambda$
          function
          (msg "The ~n0 input" (list position))
          t nil))
    ((er &)
     (ensure-function/lambda-logic-mode$
          fn/lambda description t nil))
    ((er &)
     (ensure-function/lambda-closed$ fn/lambda description t nil))
    ((unless guard-thms$)
     (value (list fn/lambda (len stobjs-in)
                  (len stobjs-out))))
    ((er &)
     (ensure-function/lambda-guard-verified-exec-fns$
      fn/lambda
      (msg
        "Since the :GUARD-THMS input is (perhaps by default) T, ~@0"
        (msg-downcase-first description))
      t nil)))
   (value (list fn/lambda (len stobjs-in)
                (len stobjs-out))))))