		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-make-paramdecloverrides

Line up parameter arguments with parameter declarations.

Signature
(vl-make-paramdecloverrides formals actuals warnings ctx) → (mv successp warnings overrides)
Arguments: formals — In proper order, from the submodule.
Guard (vl-paramdecllist-p formals).; actuals — From the instance.
Guard (vl-paramargs-p actuals).; warnings — Warnings accumulator for the superior module.
Guard (vl-warninglist-p warnings).; ctx — Context for error messages.
Guard (vl-context-p ctx).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; overrides — Type (vl-paramdecloverridelist-p overrides).

Definitions and Theorems

Function: vl-make-paramdecloverrides

(defun vl-make-paramdecloverrides (formals actuals warnings ctx)
 (declare (xargs :guard (and (vl-paramdecllist-p formals)
                             (vl-paramargs-p actuals)
                             (vl-warninglist-p warnings)
                             (vl-context-p ctx))))
 (let ((__function__ 'vl-make-paramdecloverrides))
  (declare (ignorable __function__))
  (b*
   ((formals (vl-paramdecllist-fix formals))
    (ctx (vl-context-fix ctx))
    ((unless (uniquep (vl-paramdecllist->names formals)))
     (mv
      nil
      (fatal
       :type :vl-bad-instance
       :msg "~a0: parameters are not unique: ~&1."
       :args
       (list
            ctx
            (duplicated-members (vl-paramdecllist->names formals))))
      nil)))
   (vl-paramargs-case
    actuals
    (:vl-paramargs-named
     (b*
      ((actual-names (vl-namedparamvaluelist->names actuals.args))
       (formal-names
         (vl-paramdecllist->names (vl-nonlocal-paramdecls formals)))
       ((unless (uniquep actual-names))
        (mv
         nil
         (fatal
            :type :vl-bad-instance
            :msg
            "~a0: multiple occurrences of parameter arguments: ~&1."
            :args (list ctx (duplicated-members actual-names)))
         nil))
       (illegal-names (difference (mergesort actual-names)
                                  (mergesort formal-names)))
       ((when illegal-names)
        (mv
          nil
          (fatal :type :vl-bad-instance
                 :msg "~a0: parameter~s1 ~&2 ~s2."
                 :args (list ctx
                             (if (vl-plural-p illegal-names) "s" "")
                             illegal-names
                             (if (vl-plural-p illegal-names)
                                 "do not exist"
                               "does not exist")))
          nil))
       (overrides
           (vl-make-paramdecloverrides-named formals actuals.args)))
      (mv t (ok) overrides)))
    (:vl-paramargs-plain
     (b*
      ((num-formals (len (vl-nonlocal-paramdecls formals)))
       (num-actuals (len actuals.args))
       ((unless (<= num-actuals num-formals))
        (mv
         nil
         (fatal
          :type :vl-bad-instance
          :msg
          "~a0: too many parameter values: ~x1 (non-local) ~
                              parameter~s2, but is given ~x3 parameter argument~s4."
          :args (list ctx num-formals
                      (if (eql num-formals 1) "" "s")
                      num-actuals
                      (if (eql num-actuals 1) "" "s")))
         nil))
       (overrides
         (vl-make-paramdecloverrides-indexed formals actuals.args)))
      (mv t (ok) overrides)))))))

Theorem: booleanp-of-vl-make-paramdecloverrides.successp

(defthm booleanp-of-vl-make-paramdecloverrides.successp
  (b* (((mv ?successp ?warnings ?overrides)
        (vl-make-paramdecloverrides formals actuals warnings ctx)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-make-paramdecloverrides.warnings

(defthm vl-warninglist-p-of-vl-make-paramdecloverrides.warnings
  (b* (((mv ?successp ?warnings ?overrides)
        (vl-make-paramdecloverrides formals actuals warnings ctx)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-paramdecloverridelist-p-of-vl-make-paramdecloverrides.overrides

(defthm
 vl-paramdecloverridelist-p-of-vl-make-paramdecloverrides.overrides
 (b* (((mv ?successp ?warnings ?overrides)
       (vl-make-paramdecloverrides formals actuals warnings ctx)))
   (vl-paramdecloverridelist-p overrides))
 :rule-classes :rewrite)

Theorem: vl-make-paramdecloverrides-of-vl-paramdecllist-fix-formals

(defthm vl-make-paramdecloverrides-of-vl-paramdecllist-fix-formals
  (equal (vl-make-paramdecloverrides (vl-paramdecllist-fix formals)
                                     actuals warnings ctx)
         (vl-make-paramdecloverrides formals actuals warnings ctx)))

Theorem: vl-make-paramdecloverrides-vl-paramdecllist-equiv-congruence-on-formals

(defthm
 vl-make-paramdecloverrides-vl-paramdecllist-equiv-congruence-on-formals
 (implies
  (vl-paramdecllist-equiv formals formals-equiv)
  (equal
   (vl-make-paramdecloverrides formals actuals warnings ctx)
   (vl-make-paramdecloverrides formals-equiv actuals warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-make-paramdecloverrides-of-vl-paramargs-fix-actuals

(defthm vl-make-paramdecloverrides-of-vl-paramargs-fix-actuals
 (equal
      (vl-make-paramdecloverrides formals (vl-paramargs-fix actuals)
                                  warnings ctx)
      (vl-make-paramdecloverrides formals actuals warnings ctx)))

Theorem: vl-make-paramdecloverrides-vl-paramargs-equiv-congruence-on-actuals

(defthm
 vl-make-paramdecloverrides-vl-paramargs-equiv-congruence-on-actuals
 (implies
  (vl-paramargs-equiv actuals actuals-equiv)
  (equal
   (vl-make-paramdecloverrides formals actuals warnings ctx)
   (vl-make-paramdecloverrides formals actuals-equiv warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-make-paramdecloverrides-of-vl-warninglist-fix-warnings

(defthm vl-make-paramdecloverrides-of-vl-warninglist-fix-warnings
 (equal
   (vl-make-paramdecloverrides formals
                               actuals (vl-warninglist-fix warnings)
                               ctx)
   (vl-make-paramdecloverrides formals actuals warnings ctx)))

Theorem: vl-make-paramdecloverrides-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-make-paramdecloverrides-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
   (vl-make-paramdecloverrides formals actuals warnings ctx)
   (vl-make-paramdecloverrides formals actuals warnings-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-make-paramdecloverrides-of-vl-context-fix-ctx

(defthm vl-make-paramdecloverrides-of-vl-context-fix-ctx
 (equal
  (vl-make-paramdecloverrides formals
                              actuals warnings (vl-context-fix ctx))
  (vl-make-paramdecloverrides formals actuals warnings ctx)))

Theorem: vl-make-paramdecloverrides-vl-context-equiv-congruence-on-ctx

(defthm
      vl-make-paramdecloverrides-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal
   (vl-make-paramdecloverrides formals actuals warnings ctx)
   (vl-make-paramdecloverrides formals actuals warnings ctx-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-namedparamvaluelist->names: (vl-namedparamvaluelist->names x) maps vl-namedparamvalue->name across a list.
Vl-make-paramdecloverrides-indexed: Line up positional parameter arguments with parameter declarations.
Vl-find-namedparamvalue
Vl-paramdecloverride: Paired up parameter declaration with its override values from a module instance.
Vl-nonlocal-paramdecls: Filter parameter declarations, keeping only the non-local declarations.
Vl-paramdecloverridelist: A list of vl-paramdecloverride-p objects.