		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Funscope-to-funtable

Turn a function scope into a function table.

Signature
(funscope-to-funtable funscope) → funtab
Arguments: funscope — Guard (funscopep funscope).
Returns: funtab — Type (funtablep funtab).

We turn the function information values of the omap into function types. They keys of the omap are unchanged.

See funenv-to-funtable for more explanation on the purpose of this computation.

Definitions and Theorems

Function: funscope-to-funtable

(defun funscope-to-funtable (funscope)
  (declare (xargs :guard (funscopep funscope)))
  (let ((__function__ 'funscope-to-funtable))
    (declare (ignorable __function__))
    (b* ((funscope (funscope-fix funscope))
         ((when (omap::emptyp funscope)) nil)
         ((mv name funinfo)
          (omap::head funscope))
         (funtab (funscope-to-funtable (omap::tail funscope))))
      (omap::update name (funinfo-to-funtype funinfo)
                    funtab))))

Theorem: funtablep-of-funscope-to-funtable

(defthm funtablep-of-funscope-to-funtable
  (b* ((funtab (funscope-to-funtable funscope)))
    (funtablep funtab))
  :rule-classes :rewrite)

Theorem: in-of-funscope-to-funtable

(defthm in-of-funscope-to-funtable
  (iff (omap::assoc fun (funscope-to-funtable funscope))
       (omap::assoc fun (funscope-fix funscope))))

Theorem: consp-of-assoc-of-funscope-to-funtable

(defthm consp-of-assoc-of-funscope-to-funtable
  (equal (consp (omap::assoc fun (funscope-to-funtable funscope)))
         (consp (omap::assoc fun (funscope-fix funscope)))))

Theorem: keys-of-funscope-to-funtable

(defthm keys-of-funscope-to-funtable
  (equal (omap::keys (funscope-to-funtable funscope))
         (omap::keys (funscope-fix funscope))))

Theorem: funscope-to-funtable-of-update

(defthm funscope-to-funtable-of-update
 (implies
      (and (identifierp fun)
           (funinfop info)
           (funscopep funscope))
      (equal (funscope-to-funtable (omap::update fun info funscope))
             (omap::update fun (funinfo-to-funtype info)
                           (funscope-to-funtable funscope)))))

Theorem: funscope-to-funtable-of-funscope-fix-funscope

(defthm funscope-to-funtable-of-funscope-fix-funscope
  (equal (funscope-to-funtable (funscope-fix funscope))
         (funscope-to-funtable funscope)))

Theorem: funscope-to-funtable-funscope-equiv-congruence-on-funscope

(defthm funscope-to-funtable-funscope-equiv-congruence-on-funscope
  (implies (funscope-equiv funscope funscope-equiv)
           (equal (funscope-to-funtable funscope)
                  (funscope-to-funtable funscope-equiv)))
  :rule-classes :congruence)