		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-override-parameter-value

Try to override an arbitrary parameter with its final value.

Signature
(vl-override-parameter-value decl value ss warnings ctx) → (mv okp warnings new-value)
Arguments: decl — Some parameter from the submodule.
Guard (vl-paramdecl-p decl).; value — Final value to override the parameter with.
Guard (vl-paramvalue-p value).; ss — Scopestack.
Guard (vl-scopestack-p ss).; warnings — Warnings accumulator for the submodule.
Guard (vl-warninglist-p warnings).; ctx — Context for error messages.
Guard (vl-context-p ctx).
Returns: okp — Type (booleanp okp).; warnings — Type (vl-warninglist-p warnings).; new-value — On success, the new value to use for this parameter.
Type (vl-paramvalue-p new-value).

Definitions and Theorems

Function: vl-override-parameter-value

(defun vl-override-parameter-value (decl value ss warnings ctx)
 (declare (xargs :guard (and (vl-paramdecl-p decl)
                             (vl-paramvalue-p value)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings)
                             (vl-context-p ctx))))
 (let ((__function__ 'vl-override-parameter-value))
   (declare (ignorable __function__))
   (b* ((decl (vl-paramdecl-fix decl))
        (value (vl-paramvalue-fix value))
        ((when (vl-paramvalue-datatype-p value))
         (vl-override-parameter-with-type decl value warnings ctx)))
     (vl-override-parameter-with-expr decl value ss warnings ctx))))

Theorem: booleanp-of-vl-override-parameter-value.okp

(defthm booleanp-of-vl-override-parameter-value.okp
  (b* (((mv ?okp ?warnings ?new-value)
        (vl-override-parameter-value decl value ss warnings ctx)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-override-parameter-value.warnings

(defthm vl-warninglist-p-of-vl-override-parameter-value.warnings
  (b* (((mv ?okp ?warnings ?new-value)
        (vl-override-parameter-value decl value ss warnings ctx)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-paramvalue-p-of-vl-override-parameter-value.new-value

(defthm vl-paramvalue-p-of-vl-override-parameter-value.new-value
  (b* (((mv ?okp ?warnings ?new-value)
        (vl-override-parameter-value decl value ss warnings ctx)))
    (vl-paramvalue-p new-value))
  :rule-classes :rewrite)

Theorem: vl-override-parameter-value-of-vl-paramdecl-fix-decl

(defthm vl-override-parameter-value-of-vl-paramdecl-fix-decl
  (equal (vl-override-parameter-value (vl-paramdecl-fix decl)
                                      value ss warnings ctx)
         (vl-override-parameter-value decl value ss warnings ctx)))

Theorem: vl-override-parameter-value-vl-paramdecl-equiv-congruence-on-decl

(defthm
  vl-override-parameter-value-vl-paramdecl-equiv-congruence-on-decl
 (implies
  (vl-paramdecl-equiv decl decl-equiv)
  (equal
    (vl-override-parameter-value decl value ss warnings ctx)
    (vl-override-parameter-value decl-equiv value ss warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-value-of-vl-paramvalue-fix-value

(defthm vl-override-parameter-value-of-vl-paramvalue-fix-value
  (equal (vl-override-parameter-value decl (vl-paramvalue-fix value)
                                      ss warnings ctx)
         (vl-override-parameter-value decl value ss warnings ctx)))

Theorem: vl-override-parameter-value-vl-paramvalue-equiv-congruence-on-value

(defthm
 vl-override-parameter-value-vl-paramvalue-equiv-congruence-on-value
 (implies
  (vl-paramvalue-equiv value value-equiv)
  (equal
    (vl-override-parameter-value decl value ss warnings ctx)
    (vl-override-parameter-value decl value-equiv ss warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-value-of-vl-scopestack-fix-ss

(defthm vl-override-parameter-value-of-vl-scopestack-fix-ss
 (equal
      (vl-override-parameter-value decl value (vl-scopestack-fix ss)
                                   warnings ctx)
      (vl-override-parameter-value decl value ss warnings ctx)))

Theorem: vl-override-parameter-value-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-override-parameter-value-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
    (vl-override-parameter-value decl value ss warnings ctx)
    (vl-override-parameter-value decl value ss-equiv warnings ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-value-of-vl-warninglist-fix-warnings

(defthm vl-override-parameter-value-of-vl-warninglist-fix-warnings
  (equal (vl-override-parameter-value
              decl
              value ss (vl-warninglist-fix warnings)
              ctx)
         (vl-override-parameter-value decl value ss warnings ctx)))

Theorem: vl-override-parameter-value-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-override-parameter-value-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
    (vl-override-parameter-value decl value ss warnings ctx)
    (vl-override-parameter-value decl value ss warnings-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-override-parameter-value-of-vl-context-fix-ctx

(defthm vl-override-parameter-value-of-vl-context-fix-ctx
  (equal (vl-override-parameter-value
              decl
              value ss warnings (vl-context-fix ctx))
         (vl-override-parameter-value decl value ss warnings ctx)))

Theorem: vl-override-parameter-value-vl-context-equiv-congruence-on-ctx

(defthm
     vl-override-parameter-value-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal
    (vl-override-parameter-value decl value ss warnings ctx)
    (vl-override-parameter-value decl value ss warnings ctx-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-convert-parameter-value-to-explicit-type: Alter the expression given to an explicitly typed parameter so that it has the correct type.
Vl-override-parameter-with-expr: Try to override a parameter with a new expression.
Vl-override-parameter-with-type: Try to override a parameter with a new datatype.
Vl-paramdecl-final-value