		Search-engine friendly clone of the ACL2 documentation.

Execution

End-of-for-loop-p

Check if a for loop has ended.

Signature
(end-of-for-loop-p name bound env) → yes/no
Arguments: name — Guard (identifierp name).; bound — Guard (integerp bound).; env — Guard (denvp env).
Returns: yes/no — Type (booleanp yes/no).

This is used in exec-for-loop-iterations, to check whether the iterations end. We retrieve the value of the named loop variable, and compare it with the bound: the loop has ended if the value is greater than or equal to the bound. If the loop variable does not exist, or is not integer, we return nil; however, none of this will ever happen in well-formed computation states, which we plan to prove formally.

Definitions and Theorems

Function: end-of-for-loop-p

(defun end-of-for-loop-p (name bound env)
  (declare (xargs :guard (and (identifierp name)
                              (integerp bound)
                              (denvp env))))
  (let ((__function__ 'end-of-for-loop-p))
    (declare (ignorable __function__))
    (b* ((info (get-var/const-dinfo name env))
         ((unless info) nil)
         (val (var/const-dinfo->value info))
         ((unless (int-valuep val)) nil)
         (int (int-value-to-int val)))
      (>= int (ifix bound)))))

Theorem: booleanp-of-end-of-for-loop-p

(defthm booleanp-of-end-of-for-loop-p
  (b* ((yes/no (end-of-for-loop-p name bound env)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: end-of-for-loop-p-of-identifier-fix-name

(defthm end-of-for-loop-p-of-identifier-fix-name
  (equal (end-of-for-loop-p (identifier-fix name)
                            bound env)
         (end-of-for-loop-p name bound env)))

Theorem: end-of-for-loop-p-identifier-equiv-congruence-on-name

(defthm end-of-for-loop-p-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (end-of-for-loop-p name bound env)
                  (end-of-for-loop-p name-equiv bound env)))
  :rule-classes :congruence)

Theorem: end-of-for-loop-p-of-ifix-bound

(defthm end-of-for-loop-p-of-ifix-bound
  (equal (end-of-for-loop-p name (ifix bound)
                            env)
         (end-of-for-loop-p name bound env)))

Theorem: end-of-for-loop-p-int-equiv-congruence-on-bound

(defthm end-of-for-loop-p-int-equiv-congruence-on-bound
  (implies (acl2::int-equiv bound bound-equiv)
           (equal (end-of-for-loop-p name bound env)
                  (end-of-for-loop-p name bound-equiv env)))
  :rule-classes :congruence)

Theorem: end-of-for-loop-p-of-denv-fix-env

(defthm end-of-for-loop-p-of-denv-fix-env
  (equal (end-of-for-loop-p name bound (denv-fix env))
         (end-of-for-loop-p name bound env)))

Theorem: end-of-for-loop-p-denv-equiv-congruence-on-env

(defthm end-of-for-loop-p-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (end-of-for-loop-p name bound env)
                  (end-of-for-loop-p name bound env-equiv)))
  :rule-classes :congruence)