		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Var-table-add-var

Add a variable to (the innermost scope of) a variable table.

Signature
(var-table-add-var var type defstatus vartab) → new-vartab
Arguments: var — Guard (identp var).; type — Guard (typep type).; defstatus — Guard (var-defstatusp defstatus).; vartab — Guard (var-tablep vartab).
Returns: new-vartab — Type (var-table-resultp new-vartab).

Besides the type of the variable, we also pass a variable definition status to this ACL2 function, which says whether the variable declaration that we are processing constitutes a definition, a tentative definition, or neither. This variable definition status is determined by the specifics of the declaration, including where it occurs (block scope or file scope).

We look up the variable in the variable table. If it is not found, we add it, with the definition status given. If it is found, it must have the same type as the given type, otherwise it is an error. The given definition status is combined with the one in the table, as follows [C17:6.9.2]:

If the one in the table is undefined, and the one in the declaration is also undefined, it remains undefined in the table.
If the one in the table is undefined, and the one in the declaration is defined or tentatively defined, the latter replaces the former in the table.
If the one in the table is tentatively defined, and the one in the declaration is undefined or tentatively defined, it remains tentatively defined in the table.
If the one in the table is tentatively defined, and the one in the declaration is defined, the latter replaces the former in the table.
If the one in the table is defined, and the one in the declaration is undefined or tentatively defined, it remains defined in the table.
If the one in the table is defined, and the one in the declaration is defined, it is an error, because there cannot be two definitions [C17:6.9/5].

Definitions and Theorems

Function: var-table-add-var

(defun var-table-add-var (var type defstatus vartab)
 (declare (xargs :guard (and (identp var)
                             (typep type)
                             (var-defstatusp defstatus)
                             (var-tablep vartab))))
 (let ((__function__ 'var-table-add-var))
   (declare (ignorable __function__))
   (b* ((var (ident-fix var))
        (vartab (var-table-fix vartab))
        (varscope (car vartab))
        (var-info (omap::assoc var varscope))
        ((when (not (consp var-info)))
         (b* ((info (make-var-sinfo :type type
                                    :defstatus defstatus))
              (new-varscope (omap::update var info varscope)))
           (cons new-varscope (cdr vartab))))
        (info (cdr var-info))
        ((unless (type-equiv type (var-sinfo->type info)))
         (reserrf (list :different-type-var var)))
        (tabdefstatus (var-sinfo->defstatus info))
        ((when (or (and (var-defstatus-case tabdefstatus :undefined)
                        (var-defstatus-case defstatus :undefined))
                   (and (var-defstatus-case tabdefstatus :tentative)
                        (var-defstatus-case defstatus :undefined))
                   (and (var-defstatus-case tabdefstatus :tentative)
                        (var-defstatus-case defstatus :tentative))
                   (and (var-defstatus-case tabdefstatus :defined)
                        (var-defstatus-case defstatus :undefined))
                   (and (var-defstatus-case tabdefstatus :defined)
                        (var-defstatus-case defstatus :tentative))))
         vartab)
        ((when (or (and (var-defstatus-case tabdefstatus :undefined)
                        (var-defstatus-case defstatus :tentative))
                   (and (var-defstatus-case tabdefstatus :undefined)
                        (var-defstatus-case defstatus :defined))
                   (and (var-defstatus-case tabdefstatus :tentative)
                        (var-defstatus-case defstatus :defined))))
         (b* ((new-info (change-var-sinfo info
                                          :defstatus defstatus))
              (new-varscope (omap::update var new-info varscope)))
           (cons new-varscope (cdr vartab)))))
     (assert* (and (var-defstatus-case tabdefstatus :defined)
                   (var-defstatus-case defstatus :defined))
              (reserrf (list :duplicate-var-def var))))))

Theorem: var-table-resultp-of-var-table-add-var

(defthm var-table-resultp-of-var-table-add-var
  (b* ((new-vartab (var-table-add-var var type defstatus vartab)))
    (var-table-resultp new-vartab))
  :rule-classes :rewrite)

Theorem: var-table-add-var-of-ident-fix-var

(defthm var-table-add-var-of-ident-fix-var
  (equal (var-table-add-var (ident-fix var)
                            type defstatus vartab)
         (var-table-add-var var type defstatus vartab)))

Theorem: var-table-add-var-ident-equiv-congruence-on-var

(defthm var-table-add-var-ident-equiv-congruence-on-var
  (implies
       (ident-equiv var var-equiv)
       (equal (var-table-add-var var type defstatus vartab)
              (var-table-add-var var-equiv type defstatus vartab)))
  :rule-classes :congruence)

Theorem: var-table-add-var-of-type-fix-type

(defthm var-table-add-var-of-type-fix-type
  (equal (var-table-add-var var (type-fix type)
                            defstatus vartab)
         (var-table-add-var var type defstatus vartab)))

Theorem: var-table-add-var-type-equiv-congruence-on-type

(defthm var-table-add-var-type-equiv-congruence-on-type
  (implies
       (type-equiv type type-equiv)
       (equal (var-table-add-var var type defstatus vartab)
              (var-table-add-var var type-equiv defstatus vartab)))
  :rule-classes :congruence)

Theorem: var-table-add-var-of-var-defstatus-fix-defstatus

(defthm var-table-add-var-of-var-defstatus-fix-defstatus
  (equal (var-table-add-var var type (var-defstatus-fix defstatus)
                            vartab)
         (var-table-add-var var type defstatus vartab)))

Theorem: var-table-add-var-var-defstatus-equiv-congruence-on-defstatus

(defthm
      var-table-add-var-var-defstatus-equiv-congruence-on-defstatus
  (implies
       (var-defstatus-equiv defstatus defstatus-equiv)
       (equal (var-table-add-var var type defstatus vartab)
              (var-table-add-var var type defstatus-equiv vartab)))
  :rule-classes :congruence)

Theorem: var-table-add-var-of-var-table-fix-vartab

(defthm var-table-add-var-of-var-table-fix-vartab
  (equal (var-table-add-var var
                            type defstatus (var-table-fix vartab))
         (var-table-add-var var type defstatus vartab)))

Theorem: var-table-add-var-var-table-equiv-congruence-on-vartab

(defthm var-table-add-var-var-table-equiv-congruence-on-vartab
  (implies
       (var-table-equiv vartab vartab-equiv)
       (equal (var-table-add-var var type defstatus vartab)
              (var-table-add-var var type defstatus vartab-equiv)))
  :rule-classes :congruence)