		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-add-ord

Add an ordinary identifier to the validation table.

Signature
(valid-add-ord 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).

We pass the information to associate to the identifier.

The identifier is always added to the first (i.e. innermost, i.e. current) scope. We check the existence of at least one scope; recall that there must be always a file scope.

If the identifier is already present in the current scope, its information is overwritten, but we only call this function after checking that this overwriting is acceptable, i.e. when it ``refines'' the validation information for the identifier. We could consider adding a guard to this function that characterizes the acceptable overwriting.

Definitions and Theorems

Function: valid-add-ord

(defun valid-add-ord (ident info table)
  (declare (xargs :guard (and (identp ident)
                              (valid-ord-infop info)
                              (valid-tablep table))))
  (let ((__function__ 'valid-add-ord))
    (declare (ignorable __function__))
    (b* (((unless (> (valid-table-num-scopes table) 0))
          (raise "Internal error: no scopes in validation table.")
          (valid-table-fix table))
         (scopes (valid-table->scopes table))
         (scope (car 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 (cons new-scope (cdr scopes))))
      (change-valid-table table
                          :scopes new-scopes))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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