		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-param-declon

Check a parameter declaration.

Signature
(check-param-declon param vartab tagenv) → new-vartab
Arguments: param — Guard (param-declonp param).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: new-vartab — Type (var-table-resultp new-vartab).

The variable table passed as input is the one engendered by the parameter declarations that precede this one. We check the components of the parameter declaration and we check that the parameter can be added to the variable table; the latter check fails if there is a duplicate parameter. Each parameter is considered defined in the variable table. Note that we regard each declaration as defining the variable, because no multiple declarations of the same parameter are allowed. We adjust the type [C:6.7.6.3/7]. We also ensure that the (adjusted) type is complete [C:6.7.6.3/4]. If all checks succeed, we return the variable table updated with the parameter, with the adjusted type.

Definitions and Theorems

Function: check-param-declon

(defun check-param-declon (param vartab tagenv)
 (declare (xargs :guard (and (param-declonp param)
                             (var-tablep vartab)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-param-declon))
   (declare (ignorable __function__))
   (b*
    (((mv var tyname)
      (param-declon-to-ident+tyname param))
     ((okf type)
      (check-tyname tyname tagenv))
     ((okf &) (check-ident var))
     (type (adjust-type type))
     ((unless (type-completep type))
      (reserrf
           (list :param-type-incomplete (param-declon-fix param)))))
    (var-table-add-var var type (var-defstatus-defined)
                       vartab))))

Theorem: var-table-resultp-of-check-param-declon

(defthm var-table-resultp-of-check-param-declon
  (b* ((new-vartab (check-param-declon param vartab tagenv)))
    (var-table-resultp new-vartab))
  :rule-classes :rewrite)

Theorem: check-param-declon-of-param-declon-fix-param

(defthm check-param-declon-of-param-declon-fix-param
  (equal (check-param-declon (param-declon-fix param)
                             vartab tagenv)
         (check-param-declon param vartab tagenv)))

Theorem: check-param-declon-param-declon-equiv-congruence-on-param

(defthm check-param-declon-param-declon-equiv-congruence-on-param
  (implies (param-declon-equiv param param-equiv)
           (equal (check-param-declon param vartab tagenv)
                  (check-param-declon param-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-param-declon-of-var-table-fix-vartab

(defthm check-param-declon-of-var-table-fix-vartab
  (equal (check-param-declon param (var-table-fix vartab)
                             tagenv)
         (check-param-declon param vartab tagenv)))

Theorem: check-param-declon-var-table-equiv-congruence-on-vartab

(defthm check-param-declon-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-param-declon param vartab tagenv)
                  (check-param-declon param vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-param-declon-of-tag-env-fix-tagenv

(defthm check-param-declon-of-tag-env-fix-tagenv
  (equal (check-param-declon param vartab (tag-env-fix tagenv))
         (check-param-declon param vartab tagenv)))

Theorem: check-param-declon-tag-env-equiv-congruence-on-tagenv

(defthm check-param-declon-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-param-declon param vartab tagenv)
                  (check-param-declon param vartab tagenv-equiv)))
  :rule-classes :congruence)