		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-initer

Check an initializer.

Signature
(check-initer initer funtab vartab tagenv constp) → type
Arguments: initer — Guard (initerp initer).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).; constp — Guard (booleanp constp).
Returns: type — Type (init-type-resultp type).

If the initializer is a single expression, we ensure that it is a well-formed pure or call expression, and we return the type as a single initialization type.

If the initializer is a list of expressions, for now we require them to be pure expressions, and we return their types as a list initialization type.

The parameter constp passed to this ACL2 function is a flag indicating whether the initializer must be constant or not.

Definitions and Theorems

Function: check-initer

(defun check-initer (initer funtab vartab tagenv constp)
 (declare (xargs :guard (and (initerp initer)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv)
                             (booleanp constp))))
 (let ((__function__ 'check-initer))
  (declare (ignorable __function__))
  (initer-case
    initer :single
    (b* (((okf type)
          (check-expr-call-or-pure initer.get funtab vartab tagenv))
         ((when (and constp (not (expr-constp initer.get))))
          (reserrf (list :not-constant
                         :single initer.get))))
      (init-type-single type))
    :list
    (b* (((okf types)
          (check-expr-pure-list initer.get vartab tagenv))
         ((when (and constp
                     (not (expr-list-constp initer.get))))
          (reserrf (list :not-constant
                         :multi initer.get))))
      (init-type-list types)))))

Theorem: init-type-resultp-of-check-initer

(defthm init-type-resultp-of-check-initer
  (b* ((type (check-initer initer funtab vartab tagenv constp)))
    (init-type-resultp type))
  :rule-classes :rewrite)

Theorem: check-initer-of-initer-fix-initer

(defthm check-initer-of-initer-fix-initer
  (equal (check-initer (initer-fix initer)
                       funtab vartab tagenv constp)
         (check-initer initer funtab vartab tagenv constp)))

Theorem: check-initer-initer-equiv-congruence-on-initer

(defthm check-initer-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (check-initer initer funtab vartab tagenv constp)
                  (check-initer initer-equiv
                                funtab vartab tagenv constp)))
  :rule-classes :congruence)

Theorem: check-initer-of-fun-table-fix-funtab

(defthm check-initer-of-fun-table-fix-funtab
  (equal (check-initer initer (fun-table-fix funtab)
                       vartab tagenv constp)
         (check-initer initer funtab vartab tagenv constp)))

Theorem: check-initer-fun-table-equiv-congruence-on-funtab

(defthm check-initer-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (check-initer initer funtab vartab tagenv constp)
                  (check-initer initer
                                funtab-equiv vartab tagenv constp)))
  :rule-classes :congruence)

Theorem: check-initer-of-var-table-fix-vartab

(defthm check-initer-of-var-table-fix-vartab
  (equal (check-initer initer funtab (var-table-fix vartab)
                       tagenv constp)
         (check-initer initer funtab vartab tagenv constp)))

Theorem: check-initer-var-table-equiv-congruence-on-vartab

(defthm check-initer-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-initer initer funtab vartab tagenv constp)
                  (check-initer initer
                                funtab vartab-equiv tagenv constp)))
  :rule-classes :congruence)

Theorem: check-initer-of-tag-env-fix-tagenv

(defthm check-initer-of-tag-env-fix-tagenv
  (equal (check-initer initer
                       funtab vartab (tag-env-fix tagenv)
                       constp)
         (check-initer initer funtab vartab tagenv constp)))

Theorem: check-initer-tag-env-equiv-congruence-on-tagenv

(defthm check-initer-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-initer initer funtab vartab tagenv constp)
                  (check-initer initer
                                funtab vartab tagenv-equiv constp)))
  :rule-classes :congruence)

Theorem: check-initer-of-bool-fix-constp

(defthm check-initer-of-bool-fix-constp
  (equal (check-initer initer funtab
                       vartab tagenv (acl2::bool-fix constp))
         (check-initer initer funtab vartab tagenv constp)))

Theorem: check-initer-iff-congruence-on-constp

(defthm check-initer-iff-congruence-on-constp
  (implies (iff constp constp-equiv)
           (equal (check-initer initer funtab vartab tagenv constp)
                  (check-initer initer
                                funtab vartab tagenv constp-equiv)))
  :rule-classes :congruence)