• Top

• Sv::vl-moddb.lisp

Vl-atts->svex

Signature

(vl-atts->svex x allowed-atts ss scopes) → (mv atts warnings)

Arguments

x — Guard (vl-atts-p x).

allowed-atts — Guard (string-listp allowed-atts).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

Returns

atts — Type (sv::attributes-p atts).

warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-atts->svex

(defun vl-atts->svex (x allowed-atts ss scopes)
 (declare (xargs :guard (and (vl-atts-p x)
                             (string-listp allowed-atts)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-atts->svex))
  (declare (ignorable __function__))
  (b*
   ((x (vl-atts-fix x))
    ((when (atom x)) (mv nil nil))
    ((unless (member-equal (caar x)
                           (string-list-fix allowed-atts)))
     (vl-atts->svex (cdr x)
                    allowed-atts ss scopes))
    ((mv val warnings)
     (if
      (cdar x)
      (b*
       (((mv vttree svex ?type size)
         (vl-expr-to-svex-untyped (cdar x)
                                  ss scopes))
        (svex
           (if size
               (sv::svex-concat size (sv::svex-lhsrewrite svex size)
                                (sv::svex-z))
             svex)))
       (mv svex (vttree->warnings vttree)))
      (mv nil nil)))
    ((wmv rest warnings)
     (vl-atts->svex (cdr x)
                    allowed-atts ss scopes)))
   (mv (cons (cons (caar x) val) rest)
       warnings))))

Theorem: attributes-p-of-vl-atts->svex.atts

(defthm attributes-p-of-vl-atts->svex.atts
  (b* (((mv ?atts ?warnings)
        (vl-atts->svex x allowed-atts ss scopes)))
    (sv::attributes-p atts))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-atts->svex.warnings

(defthm vl-warninglist-p-of-vl-atts->svex.warnings
  (b* (((mv ?atts ?warnings)
        (vl-atts->svex x allowed-atts ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-atts->svex-of-vl-atts-fix-x

(defthm vl-atts->svex-of-vl-atts-fix-x
  (equal (vl-atts->svex (vl-atts-fix x)
                        allowed-atts ss scopes)
         (vl-atts->svex x allowed-atts ss scopes)))

Theorem: vl-atts->svex-vl-atts-equiv-congruence-on-x

(defthm vl-atts->svex-vl-atts-equiv-congruence-on-x
  (implies (vl-atts-equiv x x-equiv)
           (equal (vl-atts->svex x allowed-atts ss scopes)
                  (vl-atts->svex x-equiv allowed-atts ss scopes)))
  :rule-classes :congruence)

Theorem: vl-atts->svex-of-string-list-fix-allowed-atts

(defthm vl-atts->svex-of-string-list-fix-allowed-atts
  (equal (vl-atts->svex x (string-list-fix allowed-atts)
                        ss scopes)
         (vl-atts->svex x allowed-atts ss scopes)))

Theorem: vl-atts->svex-string-list-equiv-congruence-on-allowed-atts

(defthm vl-atts->svex-string-list-equiv-congruence-on-allowed-atts
  (implies (str::string-list-equiv allowed-atts allowed-atts-equiv)
           (equal (vl-atts->svex x allowed-atts ss scopes)
                  (vl-atts->svex x allowed-atts-equiv ss scopes)))
  :rule-classes :congruence)

Theorem: vl-atts->svex-of-vl-scopestack-fix-ss

(defthm vl-atts->svex-of-vl-scopestack-fix-ss
  (equal (vl-atts->svex x allowed-atts (vl-scopestack-fix ss)
                        scopes)
         (vl-atts->svex x allowed-atts ss scopes)))

Theorem: vl-atts->svex-vl-scopestack-equiv-congruence-on-ss

(defthm vl-atts->svex-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-atts->svex x allowed-atts ss scopes)
                  (vl-atts->svex x allowed-atts ss-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-atts->svex-of-vl-elabscopes-fix-scopes

(defthm vl-atts->svex-of-vl-elabscopes-fix-scopes
  (equal (vl-atts->svex x allowed-atts
                        ss (vl-elabscopes-fix scopes))
         (vl-atts->svex x allowed-atts ss scopes)))

Theorem: vl-atts->svex-vl-elabscopes-equiv-congruence-on-scopes

(defthm vl-atts->svex-vl-elabscopes-equiv-congruence-on-scopes
  (implies (vl-elabscopes-equiv scopes scopes-equiv)
           (equal (vl-atts->svex x allowed-atts ss scopes)
                  (vl-atts->svex x allowed-atts ss scopes-equiv)))
  :rule-classes :congruence)