		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Get-funtype

Look up a function in a function table.

Signature
(get-funtype name funtab) → funty?
Arguments: name — Guard (identifierp name).; funtab — Guard (funtablep funtab).
Returns: funty? — Type (funtype-resultp funty?).

The lookup is by name. If a function is found, we return its type. Otherwise we return an error.

Definitions and Theorems

Function: get-funtype

(defun get-funtype (name funtab)
 (declare (xargs :guard (and (identifierp name)
                             (funtablep funtab))))
 (let ((__function__ 'get-funtype))
  (declare (ignorable __function__))
  (b* ((pair (omap::assoc (identifier-fix name)
                          (funtable-fix funtab))))
    (if (consp pair)
        (cdr pair)
      (reserrf (list :function-not-found (identifier-fix name)))))))

Theorem: funtype-resultp-of-get-funtype

(defthm funtype-resultp-of-get-funtype
  (b* ((funty? (get-funtype name funtab)))
    (funtype-resultp funty?))
  :rule-classes :rewrite)

Theorem: get-funtype-of-identifier-fix-name

(defthm get-funtype-of-identifier-fix-name
  (equal (get-funtype (identifier-fix name)
                      funtab)
         (get-funtype name funtab)))

Theorem: get-funtype-identifier-equiv-congruence-on-name

(defthm get-funtype-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-funtype name funtab)
                  (get-funtype name-equiv funtab)))
  :rule-classes :congruence)

Theorem: get-funtype-of-funtable-fix-funtab

(defthm get-funtype-of-funtable-fix-funtab
  (equal (get-funtype name (funtable-fix funtab))
         (get-funtype name funtab)))

Theorem: get-funtype-funtable-equiv-congruence-on-funtab

(defthm get-funtype-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (get-funtype name funtab)
                  (get-funtype name funtab-equiv)))
  :rule-classes :congruence)