		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-user-lambda

Recognize untranslated lambda expressions that are valid for evaluation.

Signature
(check-user-lambda x wrld) → (mv lambd/message stobjs-out)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: lambd/message — A pseudo-termp or msgp.; stobjs-out — A symbol-listp.

An untranslated lambda expression is a lambda expression as entered by the user. This function checks whether xis a true list of exactly three elements, whose first element is the symbol lambda, whose second element is a list of legal variable symbols without duplicates, and whose third element is an untranslated term that is valid for evaluation.

If the check succeeds, the translated lambda expression is returned, along with the stobjs-out list of the body of the lambda expression (see check-user-term for an explanation of the stobjs-out list of a term). Otherwise, a possibly structured error message is returned (printable with ~@), along with nil as stobjs-out list.

The check-user-lambda function does not terminate if check-user-term does not terminate.

Definitions and Theorems

Function: check-user-lambda

(defun check-user-lambda (x wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'check-user-lambda))
    (declare (ignorable __function__))
    (b* (((unless (true-listp x))
          (mv (msg "~x0 is not a true list." x)
              nil))
         ((unless (= (len x) 3))
          (mv (msg "~x0 does not consist of exactly three elements."
                   x)
              nil))
         ((unless (eq (first x) 'lambda))
          (mv (msg "~x0 does not start with LAMBDA." x)
              nil))
         ((unless (arglistp (second x)))
          (mv (msg "~x0 does not have valid formal parameters."
                   x)
              nil))
         ((mv term/message stobjs-out)
          (check-user-term (third x) wrld))
         ((when (msgp term/message))
          (mv (msg "~x0 does not have a valid body.  ~@1"
                   x term/message)
              nil)))
      (mv (cons 'lambda
                (cons (second x)
                      (cons term/message 'nil)))
          stobjs-out))))