		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function/macro/lambda

Cause an error if a value is not the name of an existing function, the name of an existing macro, or a lambda expression.

Signature
(ensure-function/macro/lambda x description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — nil or error-erp.; val — A tuple (fn stobjs-in stobjs-out new-description) consisting of a pseudo-termfnp, a symbol-listp, a symbol-listp, and a msgp if erp is nil, otherwise error-val.

If x is the name of a function, return x itself, along with its stobjs-in and stobjs-out lists. If x is the name of a macro, return the translation of the lambda expression (lambda (x1 ... xn) (x x1 ... xn)), where x1, ..., xn are the required arguments of x, along with the stobjs-in and stobjs-out lists of the lambda expression (see below). If x is a lambda expression, return its translation, along with the stobjs-in and stobjs-out lists of the lambda expression (see below).

In each of the above cases, also return a new description of x, based on whether x is a function, macro, or lambda expression. The new description can be passed to error-checking functions to check additional conditions on the function, macro, or lambda expression.

The stobjs-in list of a lambda expression is calculated in the same way as the stobjs-in list of a function, using compute-stobj-flags on the lambda expression's formals (instead of the function's formal). The stobjs-out list of a lambda expression is returned by check-user-lambda.

If the translation of a lambda expression fails, the error message returned by check-user-lambda is incorporated into a larger error message. Since the message returned starts with the lambda expression, it can be incorporated into the larger message without capitalization concerns.

Definitions and Theorems

Function: ensure-function/macro/lambda

(defun
 ensure-function/macro/lambda
 (x description
    error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (msgp description)))
 (let
  ((__function__ 'ensure-function/macro/lambda))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state)))
   (cond
    ((function-namep x wrld)
     (value (list x (stobjs-in x wrld)
                  (stobjs-out x wrld)
                  (msg "~@0, which is the function ~x1,"
                       description x))))
    ((macro-namep x wrld)
     (b*
      ((args (macro-required-args x wrld))
       (ulambda (cons 'lambda
                      (cons args (cons (cons x args) 'nil))))
       ((mv tlambda stobjs-out)
        (check-user-lambda ulambda wrld))
       (stobjs-in (compute-stobj-flags args t wrld)))
      (value
       (list
        tlambda stobjs-in stobjs-out
        (msg
         "~@0, which is the lambda expression ~x1 ~
                          denoted by the macro ~x2,"
         description ulambda x)))))
    ((symbolp x)
     (er-soft+
      ctx error-erp error-val
      "~@0 must be a function name, a macro name, ~
             or a lambda expression.  ~
             The symbol ~x1 is not the name of a function or macro."
      description x))
    (t
     (b*
      (((mv tlambda/msg stobjs-out)
        (check-user-lambda x wrld))
       ((when (msgp tlambda/msg))
        (er-soft+
         ctx error-erp error-val
         "~@0 must be a function name, a macro name, ~
                     or a lambda expression.  ~
                     Since ~x1 is not a symbol, ~
                     it must be a lambda expression.  ~
                     ~@2"
         description x tlambda/msg))
       (tlambda tlambda/msg)
       (stobjs-in (compute-stobj-flags (lambda-formals tlambda)
                                       t wrld)))
      (value (list tlambda stobjs-in stobjs-out
                   (msg "~@0, which is the lambda expression ~x1,"
                        description x)))))))))

Subtopics

Ensure-function/macro/lambda$: Call ensure-function/macro/lambda with ctx and state as the last two arguments.