		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::empty 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::in fun (funscope-to-funtable funscope))
             (omap::in fun (funscope-fix funscope))))

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

(defthm
     consp-of-in-of-funscope-to-funtable
     (equal (consp (omap::in fun (funscope-to-funtable funscope)))
            (consp (omap::in 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)