		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-update-ext

Update the externals map with an identifier.

Signature
(valid-update-ext ident type uid table) → new-table
Arguments: ident — Guard (identp ident).; type — Guard (typep type).; uid — Guard (uidp uid).; table — Guard (valid-tablep table).
Returns: new-table — Type (valid-tablep new-table).

If no entry exists for the identifier, add a new valid-ext-info. If an entry does exist, update the declared-in field to include the name of the current translation unit.

When an existing entry already exists, type compatibility is not checked, nor is the UID. Instead, the caller should check compatibility and ensure a proper UID before updating.

Definitions and Theorems

Function: valid-update-ext

(defun valid-update-ext (ident type uid table)
 (declare (xargs :guard (and (identp ident)
                             (typep type)
                             (uidp uid)
                             (valid-tablep table))))
 (b*
  (((valid-table table) table)
   (info? (valid-lookup-ext ident table))
   (new-info
    (valid-ext-info-option-case
     info?
     :some
     (change-valid-ext-info
      info?
      :declared-in (insert table.filepath
                           (valid-ext-info->declared-in info?.val)))
     :none
     (make-valid-ext-info :type type
                          :declared-in (insert table.filepath nil)
                          :uid uid)))
   (new-externals (omap::update (ident-fix ident)
                                new-info table.externals)))
  (change-valid-table table
                      :externals new-externals)))

Theorem: valid-tablep-of-valid-update-ext

(defthm valid-tablep-of-valid-update-ext
  (b* ((new-table (valid-update-ext ident type uid table)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: valid-update-ext-of-ident-fix-ident

(defthm valid-update-ext-of-ident-fix-ident
  (equal (valid-update-ext (ident-fix ident)
                           type uid table)
         (valid-update-ext ident type uid table)))

Theorem: valid-update-ext-ident-equiv-congruence-on-ident

(defthm valid-update-ext-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (valid-update-ext ident type uid table)
                  (valid-update-ext ident-equiv type uid table)))
  :rule-classes :congruence)

Theorem: valid-update-ext-of-type-fix-type

(defthm valid-update-ext-of-type-fix-type
  (equal (valid-update-ext ident (type-fix type)
                           uid table)
         (valid-update-ext ident type uid table)))

Theorem: valid-update-ext-type-equiv-congruence-on-type

(defthm valid-update-ext-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (valid-update-ext ident type uid table)
                  (valid-update-ext ident type-equiv uid table)))
  :rule-classes :congruence)

Theorem: valid-update-ext-of-uid-fix-uid

(defthm valid-update-ext-of-uid-fix-uid
  (equal (valid-update-ext ident type (uid-fix uid)
                           table)
         (valid-update-ext ident type uid table)))

Theorem: valid-update-ext-uid-equiv-congruence-on-uid

(defthm valid-update-ext-uid-equiv-congruence-on-uid
  (implies (uid-equiv uid uid-equiv)
           (equal (valid-update-ext ident type uid table)
                  (valid-update-ext ident type uid-equiv table)))
  :rule-classes :congruence)

Theorem: valid-update-ext-of-valid-table-fix-table

(defthm valid-update-ext-of-valid-table-fix-table
  (equal (valid-update-ext ident type uid (valid-table-fix table))
         (valid-update-ext ident type uid table)))

Theorem: valid-update-ext-valid-table-equiv-congruence-on-table

(defthm valid-update-ext-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-update-ext ident type uid table)
                  (valid-update-ext ident type uid table-equiv)))
  :rule-classes :congruence)