		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Funscope-for-fundefs

Function scope for a list of function definitions.

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

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

Definitions and Theorems

Function: funscope-for-fundefs

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

Theorem: funscope-resultp-of-funscope-for-fundefs

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

Theorem: error-info-wfp-of-funscope-for-fundefs

(defthm error-info-wfp-of-funscope-for-fundefs
  (b* ((?funscope (funscope-for-fundefs fundefs)))
    (implies (reserrp funscope)
             (error-info-wfp funscope))))

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

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

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

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