		Search-engine friendly clone of the ACL2 documentation.

Execution

Init-for-loop

Initialize the execution of a for loop.

Signature
(init-for-loop name type from to env) → bound+env
Arguments: name — Guard (identifierp name).; type — Guard (typep type).; from — Guard (expr-valuep from).; to — Guard (expr-valuep to).; env — Guard (denvp env).
Returns: bound+env — Type (int+denv-resultp bound+env).

We ensure that the starting and ending expressions both have the declared type for the loop variable, which must be an integer type.

We use the starting expression's value to initialize a new constant with the name of the loop variable. Note that the loop variable is considered a constant inside the body of the loop, due to Leo's loop unrolling. We push a new scope with that constant.

We return the ending expressions' value, as an ACL2 integers, so that it can be used to eventually stop the loop iterations.

Definitions and Theorems

Function: init-for-loop

(defun init-for-loop (name type from to env)
 (declare (xargs :guard (and (identifierp name)
                             (typep type)
                             (expr-valuep from)
                             (expr-valuep to)
                             (denvp env))))
 (let ((__function__ 'init-for-loop))
  (declare (ignorable __function__))
  (b* (((unless (member-eq (type-kind type)
                           '(:unsigned :signed)))
        (reserrf (list :non-integer-loop-var-type (type-fix type))))
       ((okf from)
        (expr-value-to-value from env))
       ((unless (type-equiv (type-of-value from) type))
        (reserrf (list :mismatched-loop-type
                       :required (type-fix type)
                       :from-value from)))
       ((okf to) (expr-value-to-value to env))
       ((unless (type-equiv (type-of-value to) type))
        (reserrf (list :mismatched-loop-type
                       :required (type-fix type)
                       :from-value from)))
       (scope (init-vcscope-dinfo-loop name from))
       ((okf env)
        (push-vcscope-dinfo scope env))
       (bound (int-value-to-int to)))
    (make-int+denv :int bound :denv env))))

Theorem: int+denv-resultp-of-init-for-loop

(defthm int+denv-resultp-of-init-for-loop
  (b* ((bound+env (init-for-loop name type from to env)))
    (int+denv-resultp bound+env))
  :rule-classes :rewrite)

Theorem: init-for-loop-of-identifier-fix-name

(defthm init-for-loop-of-identifier-fix-name
  (equal (init-for-loop (identifier-fix name)
                        type from to env)
         (init-for-loop name type from to env)))

Theorem: init-for-loop-identifier-equiv-congruence-on-name

(defthm init-for-loop-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (init-for-loop name type from to env)
                  (init-for-loop name-equiv type from to env)))
  :rule-classes :congruence)

Theorem: init-for-loop-of-type-fix-type

(defthm init-for-loop-of-type-fix-type
  (equal (init-for-loop name (type-fix type)
                        from to env)
         (init-for-loop name type from to env)))

Theorem: init-for-loop-type-equiv-congruence-on-type

(defthm init-for-loop-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (init-for-loop name type from to env)
                  (init-for-loop name type-equiv from to env)))
  :rule-classes :congruence)

Theorem: init-for-loop-of-expr-value-fix-from

(defthm init-for-loop-of-expr-value-fix-from
  (equal (init-for-loop name type (expr-value-fix from)
                        to env)
         (init-for-loop name type from to env)))

Theorem: init-for-loop-expr-value-equiv-congruence-on-from

(defthm init-for-loop-expr-value-equiv-congruence-on-from
  (implies (expr-value-equiv from from-equiv)
           (equal (init-for-loop name type from to env)
                  (init-for-loop name type from-equiv to env)))
  :rule-classes :congruence)

Theorem: init-for-loop-of-expr-value-fix-to

(defthm init-for-loop-of-expr-value-fix-to
  (equal (init-for-loop name type from (expr-value-fix to)
                        env)
         (init-for-loop name type from to env)))

Theorem: init-for-loop-expr-value-equiv-congruence-on-to

(defthm init-for-loop-expr-value-equiv-congruence-on-to
  (implies (expr-value-equiv to to-equiv)
           (equal (init-for-loop name type from to env)
                  (init-for-loop name type from to-equiv env)))
  :rule-classes :congruence)

Theorem: init-for-loop-of-denv-fix-env

(defthm init-for-loop-of-denv-fix-env
  (equal (init-for-loop name type from to (denv-fix env))
         (init-for-loop name type from to env)))

Theorem: init-for-loop-denv-equiv-congruence-on-env

(defthm init-for-loop-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (init-for-loop name type from to env)
                  (init-for-loop name type from to env-equiv)))
  :rule-classes :congruence)