		Search-engine friendly clone of the ACL2 documentation.

Restrict-input-processing

Restrict-process-old

Process the old input.

Signature
(restrict-process-old old verify-guards ctx state) → (mv erp old state)
Returns: old — A symbolp that is the name of the target function of the transformation, denoted by the old input.

Definitions and Theorems

Function: restrict-process-old

(defun restrict-process-old (old verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'restrict-process-old))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((er old)
     (ensure-function-name-or-numbered-wildcard$
          old "The first input" t nil))
    (description (msg "The target function ~x0" old))
    ((er &)
     (ensure-function-is-logic-mode$ old description t nil))
    ((er &)
     (ensure-function-is-defined$ old description t nil))
    ((er &)
     (ensure-function-has-args$ old description t nil))
    ((er &)
     (ensure-function-number-of-results$ old 1 description t nil))
    ((er &)
     (ensure-function-no-stobjs$ old description t nil))
    (recursive (recursivep old nil wrld))
    ((er &)
     (if recursive
         (ensure-function-singly-recursive$ old description t nil)
       (value nil)))
    ((er &)
     (if recursive
         (ensure-function-known-measure$ old description t nil)
       (value nil)))
    ((er &)
     (if
      (eq verify-guards t)
      (ensure-function-is-guard-verified$
       old
       (msg
        "Since the :VERIFY-GUARDS input is T, ~
                          the target function ~x0"
        old)
       t nil)
      (value nil))))
   (value old))))