		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-old

Process the old input.

Signature
(expdata-process-old old predicate 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: expdata-process-old

(defun expdata-process-old (old predicate verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'expdata-process-old))
  (declare (ignorable __function__))
  (b*
   (((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-no-stobjs$ old$ description t nil))
    ((er &)
     (if
      (eq predicate t)
      (ensure-function-number-of-results$ old$ 1 description t nil)
      (value nil)))
    (recursive (recursivep old$ nil (w state)))
    ((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 recursive (ensure-function-not-in-termination-thm$
                        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$))))