		Search-engine friendly clone of the ACL2 documentation.

Elaborate

Vl-design-elaborate-aux

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

Definitions and Theorems

Function: vl-design-elaborate-aux-fn

(defun vl-design-elaborate-aux-fn (x elabindex reclimit config)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (and (vl-design-p x)
                             (natp reclimit)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-design-elaborate-aux))
  (declare (ignorable __function__))
  (b* (((vl-design x) (vl-design-fix x)))
    (b*
     (((mv ok warnings udps elabindex)
       (vl-udplist-elaborate-fn x.udps elabindex reclimit config))
      ((mv ok1 warnings1 vardecls elabindex)
       (vl-vardecllist-elaborate-fn
            x.vardecls elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 taskdecls elabindex)
       (vl-taskdecllist-elaborate-fn
            x.taskdecls elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 fundecls elabindex)
       (vl-fundecllist-elaborate-fn
            x.fundecls elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 paramdecls elabindex)
       (vl-paramdecllist-elaborate-fn
            x.paramdecls elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 dpiimports elabindex)
       (vl-dpiimportlist-elaborate-fn
            x.dpiimports elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 typedefs elabindex)
       (vl-typedeflist-elaborate-fn
            x.typedefs elabindex reclimit config))
      (ok (and ok1 ok))
      (warnings (append-without-guard warnings1 warnings))
      ((mv ok1 warnings1 binds elabindex)
       (vl-bindlist-elaborate-fn x.binds 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-design x
                           :udps udps
                           :vardecls vardecls
                           :taskdecls taskdecls
                           :fundecls fundecls
                           :paramdecls paramdecls
                           :dpiimports dpiimports
                           :typedefs typedefs
                           :binds binds
                           :properties properties
                           :sequences sequences)
         elabindex)))))

Theorem: vl-warninglist-p-of-vl-design-elaborate-aux.warnings

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

Theorem: vl-design-p-of-vl-design-elaborate-aux.new-x

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

Theorem: vl-design-elaborate-aux-fn-of-vl-design-fix-x

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

Theorem: vl-design-elaborate-aux-fn-vl-design-equiv-congruence-on-x

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

Theorem: vl-design-elaborate-aux-fn-of-nfix-reclimit

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

Theorem: vl-design-elaborate-aux-fn-nat-equiv-congruence-on-reclimit

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

Theorem: vl-design-elaborate-aux-fn-of-vl-simpconfig-fix-config

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

Theorem: vl-design-elaborate-aux-fn-vl-simpconfig-equiv-congruence-on-config

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