		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-unparam-actualkey

Signature
(vl-unparam-actualkey x inst-ss mod-ss) → actualkey
Arguments: x — Guard (vl-paramdecl-p x).; inst-ss — instantiating context.
Guard (vl-scopestack-p inst-ss).; mod-ss — instantiated module context.
Guard (vl-scopestack-p mod-ss).

Definitions and Theorems

Function: vl-unparam-actualkey

(defun vl-unparam-actualkey (x inst-ss mod-ss)
 (declare (xargs :guard (and (vl-paramdecl-p x)
                             (vl-scopestack-p inst-ss)
                             (vl-scopestack-p mod-ss))))
 (let ((__function__ 'vl-unparam-actualkey))
  (declare (ignorable __function__))
  (b* (((vl-paramdecl x)))
   (vl-paramtype-case
    x.type :vl-implicitvalueparam
    (and x.type.default
         (vl-expr-strip x.type.default))
    :vl-explicitvalueparam
    (and x.type.default
         (vl-expr-strip x.type.default))
    :vl-typeparam
    (b* (((unless x.type.default)
          (raise "no default on type parameter ~x0~%" x))
         (has-usertypes (vl-datatype-has-usertypes x.type.default))
         ((unless has-usertypes)
          (vl-datatype-strip x.type.default)))
     (vl-datatype-case
      x.type.default :vl-usertype
      (b* (((mv err trace ?context tail)
            (vl-follow-scopeexpr x.type.default.name
                                 (if x.overriddenp inst-ss mod-ss)))
           ((when err)
            (raise "Error resolving type name: ~x0~%" err))
           ((vl-hidstep step) (car trace))
           (scopekey (vl-scopestack->hashkey step.ss))
           (newtypename (make-vl-scopeexpr-end :hid tail)))
       (hons
          (vl-datatype-strip (change-vl-usertype x.type.default
                                                 :name newtypename))
          scopekey))
      :otherwise
      (b* ((scopekey (vl-scopestack->hashkey
                          (if x.overriddenp inst-ss mod-ss))))
        (hons (vl-datatype-strip x.type.default)
              scopekey))))))))

Theorem: vl-unparam-actualkey-of-vl-paramdecl-fix-x

(defthm vl-unparam-actualkey-of-vl-paramdecl-fix-x
  (equal (vl-unparam-actualkey (vl-paramdecl-fix x)
                               inst-ss mod-ss)
         (vl-unparam-actualkey x inst-ss mod-ss)))

Theorem: vl-unparam-actualkey-vl-paramdecl-equiv-congruence-on-x

(defthm vl-unparam-actualkey-vl-paramdecl-equiv-congruence-on-x
  (implies (vl-paramdecl-equiv x x-equiv)
           (equal (vl-unparam-actualkey x inst-ss mod-ss)
                  (vl-unparam-actualkey x-equiv inst-ss mod-ss)))
  :rule-classes :congruence)

Theorem: vl-unparam-actualkey-of-vl-scopestack-fix-inst-ss

(defthm vl-unparam-actualkey-of-vl-scopestack-fix-inst-ss
  (equal (vl-unparam-actualkey x (vl-scopestack-fix inst-ss)
                               mod-ss)
         (vl-unparam-actualkey x inst-ss mod-ss)))

Theorem: vl-unparam-actualkey-vl-scopestack-equiv-congruence-on-inst-ss

(defthm
     vl-unparam-actualkey-vl-scopestack-equiv-congruence-on-inst-ss
  (implies (vl-scopestack-equiv inst-ss inst-ss-equiv)
           (equal (vl-unparam-actualkey x inst-ss mod-ss)
                  (vl-unparam-actualkey x inst-ss-equiv mod-ss)))
  :rule-classes :congruence)

Theorem: vl-unparam-actualkey-of-vl-scopestack-fix-mod-ss

(defthm vl-unparam-actualkey-of-vl-scopestack-fix-mod-ss
  (equal (vl-unparam-actualkey x inst-ss (vl-scopestack-fix mod-ss))
         (vl-unparam-actualkey x inst-ss mod-ss)))

Theorem: vl-unparam-actualkey-vl-scopestack-equiv-congruence-on-mod-ss

(defthm
      vl-unparam-actualkey-vl-scopestack-equiv-congruence-on-mod-ss
  (implies (vl-scopestack-equiv mod-ss mod-ss-equiv)
           (equal (vl-unparam-actualkey x inst-ss mod-ss)
                  (vl-unparam-actualkey x inst-ss mod-ss-equiv)))
  :rule-classes :congruence)