		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Funtable-for-fundefs

Function table for a list of function definitions.

Signature
(funtable-for-fundefs fundefs) → funtab
Arguments: fundefs — Guard (fundef-listp fundefs).
Returns: funtab — Type (funtable-resultp funtab).

We go through the list and form a function table for the functions. It is an error if there are two functions with the same name.

Definitions and Theorems

Function: funtable-for-fundefs

(defun funtable-for-fundefs (fundefs)
  (declare (xargs :guard (fundef-listp fundefs)))
  (let ((__function__ 'funtable-for-fundefs))
    (declare (ignorable __function__))
    (b* (((when (endp fundefs)) nil)
         ((okf funtab)
          (funtable-for-fundefs (cdr fundefs)))
         (fundef (car fundefs))
         (fun (fundef->name fundef))
         ((when (consp (omap::assoc fun funtab)))
          (reserrf (list :duplicate-function fun))))
      (omap::update fun (funtype-for-fundef fundef)
                    funtab))))

Theorem: funtable-resultp-of-funtable-for-fundefs

(defthm funtable-resultp-of-funtable-for-fundefs
  (b* ((funtab (funtable-for-fundefs fundefs)))
    (funtable-resultp funtab))
  :rule-classes :rewrite)

Theorem: funtable-for-fundefs-of-fundef-list-fix-fundefs

(defthm funtable-for-fundefs-of-fundef-list-fix-fundefs
  (equal (funtable-for-fundefs (fundef-list-fix fundefs))
         (funtable-for-fundefs fundefs)))

Theorem: funtable-for-fundefs-fundef-list-equiv-congruence-on-fundefs

(defthm funtable-for-fundefs-fundef-list-equiv-congruence-on-fundefs
  (implies (fundef-list-equiv fundefs fundefs-equiv)
           (equal (funtable-for-fundefs fundefs)
                  (funtable-for-fundefs fundefs-equiv)))
  :rule-classes :congruence)