		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-undefined

Process the :undefined input.

Signature
(isodata-process-undefined undefined old$ ctx state) → (mv erp undefined$ state)
Arguments: old$ — Guard (symbolp old$).
Returns: undefined$ — Either :base-case-then, or :base-case-else, or a pseudo-termp.

Definitions and Theorems

Function: isodata-process-undefined

(defun isodata-process-undefined (undefined old$ ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbolp old$)))
  (let ((__function__ 'isodata-process-undefined))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         (stobjs-out (acl2::stobjs-out+ old$ (w state)))
         (m (len stobjs-out))
         ((when (eq :auto undefined))
          (value (if (< 1 m)
                     (cons 'mv stobjs-out)
                   (car stobjs-out))))
         ((when (member-eq undefined
                           '(:base-case-then :base-case-else)))
          (value undefined))
         ((er (list term stobjs-out))
          (ensure-value-is-untranslated-term$
               undefined "The :UNDEFINED input" t nil))
         (description
              (msg "The term ~x0 that denotes the undefined value"
                   undefined))
         ((er &)
          (ensure-term-free-vars-subset$ term (formals old$ wrld)
                                         description t nil))
         ((er &)
          (ensure-term-logic-mode$ term description t nil))
         ((er &)
          (ensure-function/lambda/term-number-of-results$
               stobjs-out m description t nil))
         ((er &)
          (ensure-term-no-stobjs$ stobjs-out description t nil))
         ((er &)
          (ensure-term-does-not-call$ term old$ description t nil)))
      (value term))))