		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Restrict-vars

Restrict the variables in the local state to a specified set.

Signature
(restrict-vars vars cstate) → new-cstate
Arguments: vars — Guard (identifier-setp vars).; cstate — Guard (cstatep cstate).
Returns: new-cstate — Type (cstatep new-cstate).

This is used when a block is exited: any new variable declared in the block is discarded, by retaining only the variables present in the local state before the block; any of the retained variables must retain their values from the block (i.e. the block may modify them).

Definitions and Theorems

Function: restrict-vars

(defun restrict-vars (vars cstate)
  (declare (xargs :guard (and (identifier-setp vars)
                              (cstatep cstate))))
  (let ((__function__ 'restrict-vars))
    (declare (ignorable __function__))
    (b* ((lstate (cstate->local cstate))
         (new-lstate (omap::restrict (identifier-set-fix vars)
                                     lstate)))
      (change-cstate cstate
                     :local new-lstate))))

Theorem: cstatep-of-restrict-vars

(defthm cstatep-of-restrict-vars
  (b* ((new-cstate (restrict-vars vars cstate)))
    (cstatep new-cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-restrict-vars

(defthm error-info-wfp-of-restrict-vars
  (b* ((?new-cstate (restrict-vars vars cstate)))
    (implies (reserrp new-cstate)
             (error-info-wfp new-cstate))))

Theorem: restrict-vars-of-identifier-set-fix-vars

(defthm restrict-vars-of-identifier-set-fix-vars
  (equal (restrict-vars (identifier-set-fix vars)
                        cstate)
         (restrict-vars vars cstate)))

Theorem: restrict-vars-identifier-set-equiv-congruence-on-vars

(defthm restrict-vars-identifier-set-equiv-congruence-on-vars
  (implies (identifier-set-equiv vars vars-equiv)
           (equal (restrict-vars vars cstate)
                  (restrict-vars vars-equiv cstate)))
  :rule-classes :congruence)

Theorem: restrict-vars-of-cstate-fix-cstate

(defthm restrict-vars-of-cstate-fix-cstate
  (equal (restrict-vars vars (cstate-fix cstate))
         (restrict-vars vars cstate)))

Theorem: restrict-vars-cstate-equiv-congruence-on-cstate

(defthm restrict-vars-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (restrict-vars vars cstate)
                  (restrict-vars vars cstate-equiv)))
  :rule-classes :congruence)