		Search-engine friendly clone of the ACL2 documentation.

Execution

Init-vcscope-dinfo-loop

Initialize the dynamic information about a variable and constant scope, for a loop.

Signature
(init-vcscope-dinfo-loop name val) → vcscope-info
Arguments: name — Guard (identifierp name).; val — Guard (valuep val).
Returns: vcscope-info — Type (vcscope-dinfop vcscope-info).

This scope consists of just the loop variable, which is marked as a constant because, due to loop unrolling, loop variables are considered constants in the loop bodies.

Definitions and Theorems

Function: init-vcscope-dinfo-loop

(defun init-vcscope-dinfo-loop (name val)
  (declare (xargs :guard (and (identifierp name) (valuep val))))
  (let ((__function__ 'init-vcscope-dinfo-loop))
    (declare (ignorable __function__))
    (b* ((info (make-var/const-dinfo :value val
                                     :constp t)))
      (omap::update (identifier-fix name)
                    info nil))))

Theorem: vcscope-dinfop-of-init-vcscope-dinfo-loop

(defthm vcscope-dinfop-of-init-vcscope-dinfo-loop
  (b* ((vcscope-info (init-vcscope-dinfo-loop name val)))
    (vcscope-dinfop vcscope-info))
  :rule-classes :rewrite)

Theorem: init-vcscope-dinfo-loop-of-identifier-fix-name

(defthm init-vcscope-dinfo-loop-of-identifier-fix-name
  (equal (init-vcscope-dinfo-loop (identifier-fix name)
                                  val)
         (init-vcscope-dinfo-loop name val)))

Theorem: init-vcscope-dinfo-loop-identifier-equiv-congruence-on-name

(defthm init-vcscope-dinfo-loop-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (init-vcscope-dinfo-loop name val)
                  (init-vcscope-dinfo-loop name-equiv val)))
  :rule-classes :congruence)

Theorem: init-vcscope-dinfo-loop-of-value-fix-val

(defthm init-vcscope-dinfo-loop-of-value-fix-val
  (equal (init-vcscope-dinfo-loop name (value-fix val))
         (init-vcscope-dinfo-loop name val)))

Theorem: init-vcscope-dinfo-loop-value-equiv-congruence-on-val

(defthm init-vcscope-dinfo-loop-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (init-vcscope-dinfo-loop name val)
                  (init-vcscope-dinfo-loop name val-equiv)))
  :rule-classes :congruence)