Add functions to a function table.
(add-funtypes fundefs funtab) → new-funtab
We first construct a function table for the function definitions, and then we use that to update the given function table, ensuring that the two tables have disjoint functions.
Function:
(defun add-funtypes (fundefs funtab) (declare (xargs :guard (and (fundef-listp fundefs) (funtablep funtab)))) (let ((__function__ 'add-funtypes)) (declare (ignorable __function__)) (b* ((funtab (funtable-fix funtab)) ((okf funtab1) (funtable-for-fundefs fundefs)) (overlap (intersect (omap::keys funtab1) (omap::keys funtab))) ((unless (emptyp overlap)) (reserrf (list :duplicate-functions overlap)))) (omap::update* funtab1 funtab))))
Theorem:
(defthm funtable-resultp-of-add-funtypes (b* ((new-funtab (add-funtypes fundefs funtab))) (funtable-resultp new-funtab)) :rule-classes :rewrite)
Theorem:
(defthm add-funtypes-of-fundef-list-fix-fundefs (equal (add-funtypes (fundef-list-fix fundefs) funtab) (add-funtypes fundefs funtab)))
Theorem:
(defthm add-funtypes-fundef-list-equiv-congruence-on-fundefs (implies (fundef-list-equiv fundefs fundefs-equiv) (equal (add-funtypes fundefs funtab) (add-funtypes fundefs-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm add-funtypes-of-funtable-fix-funtab (equal (add-funtypes fundefs (funtable-fix funtab)) (add-funtypes fundefs funtab)))
Theorem:
(defthm add-funtypes-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (add-funtypes fundefs funtab) (add-funtypes fundefs funtab-equiv))) :rule-classes :congruence)