		Search-engine friendly clone of the ACL2 documentation.

Execution

Init-vcscope-dinfo-call

Initialize the dynamic information about a variable and constant scope, for a function call.

Signature
(init-vcscope-dinfo-call params args) → vcscope-info
Arguments: params — Guard (funparam-listp params).; args — Guard (value-listp args).
Returns: vcscope-info — Type (vcscope-dinfo-resultp vcscope-info).

This calculates the initial scope in the frame for the call. We go through the parameters of the called function and the arguments passed to the call, and we ensure they agree in number and types. We stop with an error if there are duplicate parameters.

For now we treat public and private parameters as just variables, and we treat constant and const parameters as just constants. We may extend this in the future.

Definitions and Theorems

Function: init-vcscope-dinfo-call

(defun init-vcscope-dinfo-call (params args)
 (declare (xargs :guard (and (funparam-listp params)
                             (value-listp args))))
 (let ((__function__ 'init-vcscope-dinfo-call))
  (declare (ignorable __function__))
  (b* (((when (endp params))
        (if (endp args)
            nil
          (reserrf (list :extra-args (value-list-fix args)))))
       ((when (endp args))
        (reserrf (list :extra-params (funparam-list-fix params))))
       ((funparam param) (car params))
       (arg (car args))
       ((unless (equal (type-of-value arg) param.type))
        (reserrf (list :type-mismatch
                       param.name param.type (value-fix arg))))
       (constp (or (var/const-sort-case param.sort :constant)
                   (var/const-sort-case param.sort :const)))
       (info (make-var/const-dinfo :value arg
                                   :constp constp))
       ((okf scope)
        (init-vcscope-dinfo-call (cdr params)
                                 (cdr args)))
       ((when (get-var/const-dinfo-from-scope param.name scope))
        (reserrf (list :duplicate-param param.name)))
       (scope (add-var/const-dinfo-to-scope param.name info scope)))
    scope)))

Theorem: vcscope-dinfo-resultp-of-init-vcscope-dinfo-call

(defthm vcscope-dinfo-resultp-of-init-vcscope-dinfo-call
  (b* ((vcscope-info (init-vcscope-dinfo-call params args)))
    (vcscope-dinfo-resultp vcscope-info))
  :rule-classes :rewrite)

Theorem: init-vcscope-dinfo-call-of-funparam-list-fix-params

(defthm init-vcscope-dinfo-call-of-funparam-list-fix-params
  (equal (init-vcscope-dinfo-call (funparam-list-fix params)
                                  args)
         (init-vcscope-dinfo-call params args)))

Theorem: init-vcscope-dinfo-call-funparam-list-equiv-congruence-on-params

(defthm
   init-vcscope-dinfo-call-funparam-list-equiv-congruence-on-params
  (implies (funparam-list-equiv params params-equiv)
           (equal (init-vcscope-dinfo-call params args)
                  (init-vcscope-dinfo-call params-equiv args)))
  :rule-classes :congruence)

Theorem: init-vcscope-dinfo-call-of-value-list-fix-args

(defthm init-vcscope-dinfo-call-of-value-list-fix-args
  (equal (init-vcscope-dinfo-call params (value-list-fix args))
         (init-vcscope-dinfo-call params args)))

Theorem: init-vcscope-dinfo-call-value-list-equiv-congruence-on-args

(defthm init-vcscope-dinfo-call-value-list-equiv-congruence-on-args
  (implies (value-list-equiv args args-equiv)
           (equal (init-vcscope-dinfo-call params args)
                  (init-vcscope-dinfo-call params args-equiv)))
  :rule-classes :congruence)