		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Init-scope

Initialize the variable scope for a function call.

Signature
(init-scope formals actuals) → result
Arguments: formals — Guard (param-declon-listp formals).; actuals — Guard (value-listp actuals).
Returns: result — Type (scope-resultp result).

We go through formal parameters and actual arguments, pairing them up into the scope. We return an error if they do not match in number or types, or if there are repeated parameters. Before the comparison, we adjust the parameter types and we perform array-to-pointer conversion on the argument types.

Prior to storing each actual, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: init-scope

(defun init-scope (formals actuals)
  (declare (xargs :guard (and (param-declon-listp formals)
                              (value-listp actuals))))
  (let ((__function__ 'init-scope))
    (declare (ignorable __function__))
    (b* ((formals (param-declon-list-fix formals))
         (actuals (value-list-fix actuals))
         ((when (endp formals))
          (if (endp actuals)
              nil
            (error (list :init-scope
                         :extra-actuals actuals))))
         ((when (endp actuals))
          (error (list :init-scope
                       :extra-formals formals)))
         (scope (init-scope (cdr formals)
                            (cdr actuals)))
         ((when (errorp scope)) scope)
         (formal (car formals))
         (actual (car actuals))
         ((mv name tyname)
          (param-declon-to-ident+tyname formal))
         (formal-type (adjust-type (tyname-to-type tyname)))
         (actual-type (apconvert-type (type-of-value actual)))
         ((unless (equal formal-type actual-type))
          (error (list :formal-actual-mistype
                       :name name
                       :formal formal-type
                       :actual actual-type))))
      (if (omap::assoc name scope)
          (error (list :init-scope
                       :duplicate-param name))
        (omap::update name
                      (remove-flexible-array-member actual)
                      scope)))))

Theorem: scope-resultp-of-init-scope

(defthm scope-resultp-of-init-scope
  (b* ((result (init-scope formals actuals)))
    (scope-resultp result))
  :rule-classes :rewrite)

Theorem: init-scope-of-param-declon-list-fix-formals

(defthm init-scope-of-param-declon-list-fix-formals
  (equal (init-scope (param-declon-list-fix formals)
                     actuals)
         (init-scope formals actuals)))

Theorem: init-scope-param-declon-list-equiv-congruence-on-formals

(defthm init-scope-param-declon-list-equiv-congruence-on-formals
  (implies (param-declon-list-equiv formals formals-equiv)
           (equal (init-scope formals actuals)
                  (init-scope formals-equiv actuals)))
  :rule-classes :congruence)

Theorem: init-scope-of-value-list-fix-actuals

(defthm init-scope-of-value-list-fix-actuals
  (equal (init-scope formals (value-list-fix actuals))
         (init-scope formals actuals)))

Theorem: init-scope-value-list-equiv-congruence-on-actuals

(defthm init-scope-value-list-equiv-congruence-on-actuals
  (implies (value-list-equiv actuals actuals-equiv)
           (equal (init-scope formals actuals)
                  (init-scope formals actuals-equiv)))
  :rule-classes :congruence)