		Search-engine friendly clone of the ACL2 documentation.

Restrict-input-processing

Restrict-process-restriction

Process the restriction input.

Signature
(restrict-process-restriction restriction old verify-guards ctx state) → (mv erp restriction state)
Arguments: old — Guard (symbolp old).; verify-guards — Guard (booleanp verify-guards).
Returns: restriction — A pseudo-termp that is the translation of restriction.

Definitions and Theorems

Function: restrict-process-restriction

(defun restrict-process-restriction
       (restriction old verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (booleanp verify-guards))))
 (let ((__function__ 'restrict-process-restriction))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (restriction (if (equal restriction ':guard)
                     (guard old nil wrld)
                   restriction))
    ((er (list term stobjs-out))
     (ensure-value-is-untranslated-term$
          restriction "The second input" t nil))
    (description
         (msg "The term ~x0 that denotes the restricting predicate"
              restriction))
    ((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 1 description t nil))
    ((er &)
     (ensure-term-no-stobjs$ stobjs-out description t nil))
    ((er &)
     (if
      (eq verify-guards t)
      (ensure-term-guard-verified-exec-fns$
       term
       (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 &)
     (ensure-term-does-not-call$ term old description t nil)))
   (value term))))