		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-add-ident-objfun-file-scope

Add an identifier to the file scope of a disambiguation table, with object or function kind.

Signature
(dimb-add-ident-objfun-file-scope ident table) → new-table
Arguments: ident — Guard (identp ident).; table — Guard (dimb-tablep table).
Returns: new-table — Type (dimb-tablep new-table).

Unlike dimb-add-ident-objfun, this skips any block scopes, and directly updates the file scope at the bottom of the stack.

Definitions and Theorems

Function: dimb-add-ident-objfun-file-scope

(defun dimb-add-ident-objfun-file-scope (ident table)
  (declare (xargs :guard (and (identp ident)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-add-ident-objfun-file-scope))
    (declare (ignorable __function__))
    (b* (((when (endp table))
          (raise "Internal error: no scopes."))
         (table (dimb-table-fix table))
         (scope (car (last table)))
         (new-scope (acons (ident-fix ident)
                           (dimb-kind-objfun)
                           scope))
         (new-table (append (butlast table 1)
                            (list new-scope))))
      new-table)))

Theorem: dimb-tablep-of-dimb-add-ident-objfun-file-scope

(defthm dimb-tablep-of-dimb-add-ident-objfun-file-scope
  (b* ((new-table (dimb-add-ident-objfun-file-scope ident table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: dimb-add-ident-objfun-file-scope-of-ident-fix-ident

(defthm dimb-add-ident-objfun-file-scope-of-ident-fix-ident
  (equal (dimb-add-ident-objfun-file-scope (ident-fix ident)
                                           table)
         (dimb-add-ident-objfun-file-scope ident table)))

Theorem: dimb-add-ident-objfun-file-scope-ident-equiv-congruence-on-ident

(defthm
   dimb-add-ident-objfun-file-scope-ident-equiv-congruence-on-ident
  (implies
       (ident-equiv ident ident-equiv)
       (equal (dimb-add-ident-objfun-file-scope ident table)
              (dimb-add-ident-objfun-file-scope ident-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-add-ident-objfun-file-scope-of-dimb-table-fix-table

(defthm dimb-add-ident-objfun-file-scope-of-dimb-table-fix-table
 (equal
     (dimb-add-ident-objfun-file-scope ident (dimb-table-fix table))
     (dimb-add-ident-objfun-file-scope ident table)))

Theorem: dimb-add-ident-objfun-file-scope-dimb-table-equiv-congruence-on-table

(defthm
 dimb-add-ident-objfun-file-scope-dimb-table-equiv-congruence-on-table
 (implies
      (dimb-table-equiv table table-equiv)
      (equal (dimb-add-ident-objfun-file-scope ident table)
             (dimb-add-ident-objfun-file-scope ident table-equiv)))
 :rule-classes :congruence)