		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-process-domain

Process the :domain input.

Signature
(tailrec-process-domain domain old$ combine q r variant$ verify-guards$ verbose ctx state) → (mv erp domain$ state)
Arguments: old$ — Guard (symbolp old$).; combine — Guard (pseudo-termp combine).; q — Guard (symbolp q).; r — Guard (symbolp r).; variant$ — Guard (tailrec-variantp variant$).; verify-guards$ — Guard (booleanp verify-guards$).; verbose — Guard (booleanp verbose).
Returns: domain$ — A pseudo-termfnp that is the predicate denoted by domain.

If successful, return: the input itself, if it is a function name; the translated lambda expression denoted by the input, if the input is a macro name; the translation of the input, if the input is a lambda expression; the inferred function name or the default translated lambda expression that holds for every value, if the input is :auto.

Definitions and Theorems

Function: tailrec-process-domain

(defun tailrec-process-domain
       (domain old$ combine q r variant$
               verify-guards$ verbose ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp combine)
                             (symbolp q)
                             (symbolp r)
                             (tailrec-variantp variant$)
                             (booleanp verify-guards$)
                             (booleanp verbose))))
 (let ((__function__ 'tailrec-process-domain))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((when (eq domain :auto))
     (value
          (tailrec-infer-domain combine q r variant$ verbose wrld)))
    (description "The :DOMAIN input")
    ((er (list fn/lambda
               stobjs-in stobjs-out description))
     (cond
      ((function-namep domain wrld)
       (value (list domain (stobjs-in domain wrld)
                    (stobjs-out domain wrld)
                    (msg "~@0, which is the function ~x1,"
                         description domain))))
      ((macro-namep domain wrld)
       (b*
        ((args (macro-required-args domain wrld))
         (ulambda (cons 'lambda
                        (cons args (cons (cons domain args) 'nil))))
         ((mv tlambda stobjs-out)
          (check-user-lambda ulambda wrld))
         (stobjs-in (compute-stobj-flags args t nil wrld)))
        (value
         (list
          tlambda stobjs-in stobjs-out
          (msg
           "~@0, which is the lambda expression ~x1 ~
                              denoted by the macro ~x2,"
           description ulambda domain)))))
      ((symbolp domain)
       (er-soft+
        ctx t nil
        "~@0 must be :AUTO, ~
                                    a function name, ~
                                    a macro name, ~
                                    or a lambda expression.  ~
                                    The symbol ~x1 is not :AUTO or ~
                                    the name of a function or macro."
        description domain))
      (t
       (b*
        (((mv tlambda/msg stobjs-out)
          (check-user-lambda domain wrld))
         ((when (msgp tlambda/msg))
          (er-soft+
           ctx t nil
           "~@0 must be :AUTO, ~
                                  a function name, ~
                                  a macro name, ~
                                  or a lambda expression.  ~
                                  Since ~x1 is not a symbol, ~
                                  it must be a lambda expression.  ~
                                  ~@2"
           description domain tlambda/msg))
         (tlambda tlambda/msg)
         (stobjs-in (compute-stobj-flags (lambda-formals tlambda)
                                         t nil wrld)))
        (value (list tlambda stobjs-in stobjs-out
                     (msg "~@0, which is the lambda expression ~x1,"
                          description domain)))))))
    ((er &)
     (ensure-function/lambda-logic-mode$
          fn/lambda description t nil))
    ((er &)
     (ensure-function/lambda-arity$ stobjs-in 1 description t nil))
    ((er &)
     (ensure-function/lambda/term-number-of-results$
          stobjs-out 1 description t nil))
    ((er &)
     (ensure-function/lambda-no-stobjs$
          stobjs-in stobjs-out description t nil))
    ((er &)
     (ensure-function/lambda-closed$ fn/lambda description t nil))
    ((er &)
     (if verify-guards$
      (ensure-function/lambda-guard-verified-exec-fns$
       fn/lambda
       (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 nil)))
    ((er &)
     (if
      (symbolp fn/lambda)
      (ensure-symbol-different$ fn/lambda old$
                                (msg "the target function ~x0" old$)
                                description t nil)
      (ensure-term-does-not-call$ (lambda-body fn/lambda)
                                  old$ description t nil))))
   (value fn/lambda))))