		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-add-ord-file-scope

Add an ordinary identifier to the file scope of a validation table.

Signature
(valid-add-ord-file-scope ident info table) → new-table
Arguments: ident — Guard (identp ident).; info — Guard (valid-ord-infop info).; table — Guard (valid-tablep table).
Returns: new-table — Type (valid-tablep new-table).

Unlike valid-add-ord, this skips any block scopes, and directly updates the file scope at the bottom of the stack. It is used in some situations.

As in valid-add-ord, we update the externals map if info indicates external linkage.

Definitions and Theorems

Function: valid-add-ord-file-scope

(defun valid-add-ord-file-scope (ident info table)
 (declare (xargs :guard (and (identp ident)
                             (valid-ord-infop info)
                             (valid-tablep table))))
 (let ((__function__ 'valid-add-ord-file-scope))
  (declare (ignorable __function__))
  (b*
   ((scopes (valid-table->scopes table))
    ((when (endp scopes))
     (raise "Internal error: no scopes.")
     (irr-valid-table))
    (scope (car (last scopes)))
    (ord-scope (valid-scope->ord scope))
    (new-ord-scope (acons (ident-fix ident)
                          (valid-ord-info-fix info)
                          ord-scope))
    (new-scope (change-valid-scope scope
                                   :ord new-ord-scope))
    (new-scopes (append (butlast scopes 1)
                        (list new-scope)))
    (table (change-valid-table table
                               :scopes new-scopes)
)
    (table
     (valid-ord-info-case
      info
      :objfun
      (linkage-case
         info.linkage
         :external (valid-update-ext ident info.type info.uid table)
         :otherwise table)
      :otherwise table)
))
   table)))

Theorem: valid-tablep-of-valid-add-ord-file-scope

(defthm valid-tablep-of-valid-add-ord-file-scope
  (b* ((new-table (valid-add-ord-file-scope ident info table)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: valid-add-ord-file-scope-of-ident-fix-ident

(defthm valid-add-ord-file-scope-of-ident-fix-ident
  (equal (valid-add-ord-file-scope (ident-fix ident)
                                   info table)
         (valid-add-ord-file-scope ident info table)))

Theorem: valid-add-ord-file-scope-ident-equiv-congruence-on-ident

(defthm valid-add-ord-file-scope-ident-equiv-congruence-on-ident
 (implies (ident-equiv ident ident-equiv)
          (equal (valid-add-ord-file-scope ident info table)
                 (valid-add-ord-file-scope ident-equiv info table)))
 :rule-classes :congruence)

Theorem: valid-add-ord-file-scope-of-valid-ord-info-fix-info

(defthm valid-add-ord-file-scope-of-valid-ord-info-fix-info
  (equal (valid-add-ord-file-scope ident (valid-ord-info-fix info)
                                   table)
         (valid-add-ord-file-scope ident info table)))

Theorem: valid-add-ord-file-scope-valid-ord-info-equiv-congruence-on-info

(defthm
   valid-add-ord-file-scope-valid-ord-info-equiv-congruence-on-info
 (implies (valid-ord-info-equiv info info-equiv)
          (equal (valid-add-ord-file-scope ident info table)
                 (valid-add-ord-file-scope ident info-equiv table)))
 :rule-classes :congruence)

Theorem: valid-add-ord-file-scope-of-valid-table-fix-table

(defthm valid-add-ord-file-scope-of-valid-table-fix-table
  (equal
       (valid-add-ord-file-scope ident info (valid-table-fix table))
       (valid-add-ord-file-scope ident info table)))

Theorem: valid-add-ord-file-scope-valid-table-equiv-congruence-on-table

(defthm
     valid-add-ord-file-scope-valid-table-equiv-congruence-on-table
 (implies (valid-table-equiv table table-equiv)
          (equal (valid-add-ord-file-scope ident info table)
                 (valid-add-ord-file-scope ident info table-equiv)))
 :rule-classes :congruence)