		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 bad-instance-fatalp warnings) → (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).; bad-instance-fatalp — Guard (booleanp bad-instance-fatalp).; warnings — Warnings accumulator for the superior module.
Guard (vl-warninglist-p warnings).
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 bad-instance-fatalp warnings)
 (declare (xargs :guard (and (vl-paramdecllist-p formals)
                             (vl-paramargs-p actuals)
                             (booleanp bad-instance-fatalp)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-make-paramdecloverrides))
  (declare (ignorable __function__))
  (b*
   ((formals (vl-paramdecllist-fix formals))
    ((unless (uniquep (vl-paramdecllist->names formals)))
     (mv
      nil
      (fatal
       :type :vl-paramdecl-names-not-unique
       :msg "parameters are not unique: ~&1."
       :args
       (list
            nil
            (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-instance-paramargs-duplicates
            :msg "multiple occurrences of parameter arguments: ~&1."
            :args (list nil (duplicated-members actual-names)))
         nil))
       (illegal-names (difference (mergesort actual-names)
                                  (mergesort formal-names)))
       (warnings
         (if illegal-names
           (warn :type :vl-instance-paramargs-nonexistent
                 :msg "parameter~s1 ~&2 ~s3."
                 :args (list nil
                             (if (vl-plural-p illegal-names) "s" "")
                             illegal-names
                             (if (vl-plural-p illegal-names)
                                 "do not exist"
                               "does not exist"))
                 :fatalp bad-instance-fatalp)
           warnings))
       (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-instance-paramargs-wrong-arity
          :msg
          "too many parameter values: ~x1 (non-local) ~
                              parameter~s2, but is given ~x3 parameter argument~s4."
          :args (list nil 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 bad-instance-fatalp warnings)))
    (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 bad-instance-fatalp warnings)))
    (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 bad-instance-fatalp warnings)))
   (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 bad-instance-fatalp warnings)
   (vl-make-paramdecloverrides
        formals
        actuals bad-instance-fatalp warnings)))

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 bad-instance-fatalp warnings)
   (vl-make-paramdecloverrides
        formals-equiv
        actuals bad-instance-fatalp warnings)))
 :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)
                                  bad-instance-fatalp warnings)
      (vl-make-paramdecloverrides
           formals
           actuals bad-instance-fatalp warnings)))

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 bad-instance-fatalp warnings)
   (vl-make-paramdecloverrides formals actuals-equiv
                               bad-instance-fatalp warnings)))
 :rule-classes :congruence)

Theorem: vl-make-paramdecloverrides-of-bool-fix-bad-instance-fatalp

(defthm vl-make-paramdecloverrides-of-bool-fix-bad-instance-fatalp
 (equal
    (vl-make-paramdecloverrides formals actuals
                                (acl2::bool-fix bad-instance-fatalp)
                                warnings)
    (vl-make-paramdecloverrides
         formals
         actuals bad-instance-fatalp warnings)))

Theorem: vl-make-paramdecloverrides-iff-congruence-on-bad-instance-fatalp

(defthm
   vl-make-paramdecloverrides-iff-congruence-on-bad-instance-fatalp
 (implies
  (iff bad-instance-fatalp
       bad-instance-fatalp-equiv)
  (equal
   (vl-make-paramdecloverrides formals
                               actuals bad-instance-fatalp warnings)
   (vl-make-paramdecloverrides formals actuals
                               bad-instance-fatalp-equiv warnings)))
 :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 bad-instance-fatalp
                                 (vl-warninglist-fix warnings))
     (vl-make-paramdecloverrides
          formals
          actuals bad-instance-fatalp warnings)))

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 bad-instance-fatalp warnings)
   (vl-make-paramdecloverrides formals actuals
                               bad-instance-fatalp warnings-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.