		Search-engine friendly clone of the ACL2 documentation.

Elaborate

Vl-clkdecl-elaborate

Signature
(vl-clkdecl-elaborate x elabindex &key (reclimit 'reclimit) (config 'config)) → (mv ok warnings new-x new-elabindex)
Arguments: x — Guard (vl-clkdecl-p x).; reclimit — Guard (natp reclimit).; config — Guard (vl-simpconfig-p config).
Returns: warnings — Type (vl-warninglist-p warnings).; new-x — Type (vl-clkdecl-p new-x).

Definitions and Theorems

Function: vl-clkdecl-elaborate-fn

(defun vl-clkdecl-elaborate-fn (x elabindex reclimit config)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (vl-clkdecl-p x)
                              (natp reclimit)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-clkdecl-elaborate))
    (declare (ignorable __function__))
    (b* (((vl-clkdecl x) (vl-clkdecl-fix x)))
      (b* (((mv ok warnings event elabindex)
            (vl-evatomlist-elaborate-fn
                 x.event elabindex reclimit config))
           ((mv ok1 warnings1 iskew elabindex)
            (vl-maybe-clkskew-elaborate-fn
                 x.iskew elabindex reclimit config))
           (ok (and ok1 ok))
           (warnings (append-without-guard warnings1 warnings))
           ((mv ok1 warnings1 oskew elabindex)
            (vl-maybe-clkskew-elaborate-fn
                 x.oskew elabindex reclimit config))
           (ok (and ok1 ok))
           (warnings (append-without-guard warnings1 warnings))
           ((mv ok1 warnings1 clkassigns elabindex)
            (vl-clkassignlist-elaborate-fn
                 x.clkassigns elabindex reclimit config))
           (ok (and ok1 ok))
           (warnings (append-without-guard warnings1 warnings))
           ((mv ok1 warnings1 properties elabindex)
            (vl-propertylist-elaborate-fn
                 x.properties elabindex reclimit config))
           (ok (and ok1 ok))
           (warnings (append-without-guard warnings1 warnings))
           ((mv ok1 warnings1 sequences elabindex)
            (vl-sequencelist-elaborate-fn
                 x.sequences elabindex reclimit config))
           (ok (and ok1 ok))
           (warnings (append-without-guard warnings1 warnings)))
        (mv ok warnings
            (change-vl-clkdecl x
                               :event event
                               :iskew iskew
                               :oskew oskew
                               :clkassigns clkassigns
                               :properties properties
                               :sequences sequences)
            elabindex)))))

Theorem: vl-warninglist-p-of-vl-clkdecl-elaborate.warnings

(defthm vl-warninglist-p-of-vl-clkdecl-elaborate.warnings
  (b* (((mv ?ok ?warnings ?new-x ?new-elabindex)
        (vl-clkdecl-elaborate-fn x elabindex reclimit config)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-clkdecl-p-of-vl-clkdecl-elaborate.new-x

(defthm vl-clkdecl-p-of-vl-clkdecl-elaborate.new-x
  (b* (((mv ?ok ?warnings ?new-x ?new-elabindex)
        (vl-clkdecl-elaborate-fn x elabindex reclimit config)))
    (vl-clkdecl-p new-x))
  :rule-classes :rewrite)

Theorem: vl-clkdecl-elaborate-fn-of-vl-clkdecl-fix-x

(defthm vl-clkdecl-elaborate-fn-of-vl-clkdecl-fix-x
  (equal (vl-clkdecl-elaborate-fn (vl-clkdecl-fix x)
                                  elabindex reclimit config)
         (vl-clkdecl-elaborate-fn x elabindex reclimit config)))

Theorem: vl-clkdecl-elaborate-fn-vl-clkdecl-equiv-congruence-on-x

(defthm vl-clkdecl-elaborate-fn-vl-clkdecl-equiv-congruence-on-x
 (implies
  (vl-clkdecl-equiv x x-equiv)
  (equal
       (vl-clkdecl-elaborate-fn x elabindex reclimit config)
       (vl-clkdecl-elaborate-fn x-equiv elabindex reclimit config)))
 :rule-classes :congruence)

Theorem: vl-clkdecl-elaborate-fn-of-nfix-reclimit

(defthm vl-clkdecl-elaborate-fn-of-nfix-reclimit
  (equal (vl-clkdecl-elaborate-fn x elabindex (nfix reclimit)
                                  config)
         (vl-clkdecl-elaborate-fn x elabindex reclimit config)))

Theorem: vl-clkdecl-elaborate-fn-nat-equiv-congruence-on-reclimit

(defthm vl-clkdecl-elaborate-fn-nat-equiv-congruence-on-reclimit
 (implies
  (acl2::nat-equiv reclimit reclimit-equiv)
  (equal
       (vl-clkdecl-elaborate-fn x elabindex reclimit config)
       (vl-clkdecl-elaborate-fn x elabindex reclimit-equiv config)))
 :rule-classes :congruence)

Theorem: vl-clkdecl-elaborate-fn-of-vl-simpconfig-fix-config

(defthm vl-clkdecl-elaborate-fn-of-vl-simpconfig-fix-config
  (equal
       (vl-clkdecl-elaborate-fn x elabindex
                                reclimit (vl-simpconfig-fix config))
       (vl-clkdecl-elaborate-fn x elabindex reclimit config)))

Theorem: vl-clkdecl-elaborate-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
   vl-clkdecl-elaborate-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
       (vl-clkdecl-elaborate-fn x elabindex reclimit config)
       (vl-clkdecl-elaborate-fn x elabindex reclimit config-equiv)))
 :rule-classes :congruence)