		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-vardecl-atts-begin

Signature
(vl-pp-vardecl-atts-begin x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-atts-p x).

Definitions and Theorems

Function: vl-pp-vardecl-atts-begin-fn

(defun vl-pp-vardecl-atts-begin-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-atts-p x)))
 (let ((__function__ 'vl-pp-vardecl-atts-begin))
  (declare (ignorable __function__))
  (b*
   ((x (vl-atts-fix x))
    ((unless x) ps)
    (x (vl-remove-keys (vl-pp-vardecl-special-atts)
                       x))
    ((unless x) ps)
    ((when (and (tuplep 1 x)
                (equal (caar x) "VL_FOR")))
     (b*
      ((str (cdar x))
       (strval
        (and
            str
            (vl-expr-case
                 str
                 :vl-literal (vl-value-case str.val
                                            :vl-string str.val.value
                                            :otherwise nil)
                 :otherwise nil))))
      (if (not strval)
          (prog2$ (raise "Expected FROM to contain a string.")
                  ps)
        (vl-ps-seq (vl-println "")
                   (vl-progindent)
                   (vl-ps-span "vl_cmt" (vl-print "/* For ")
                               (vl-print-str strval)
                               (vl-println " */")))))))
   (vl-ps-seq (vl-println "")
              (vl-progindent)
              (vl-pp-atts x)
              (vl-println "")))))

Theorem: vl-pp-vardecl-atts-begin-fn-of-vl-atts-fix-x

(defthm vl-pp-vardecl-atts-begin-fn-of-vl-atts-fix-x
  (equal (vl-pp-vardecl-atts-begin-fn (vl-atts-fix x)
                                      ps)
         (vl-pp-vardecl-atts-begin-fn x ps)))

Theorem: vl-pp-vardecl-atts-begin-fn-vl-atts-equiv-congruence-on-x

(defthm vl-pp-vardecl-atts-begin-fn-vl-atts-equiv-congruence-on-x
  (implies (vl-atts-equiv x x-equiv)
           (equal (vl-pp-vardecl-atts-begin-fn x ps)
                  (vl-pp-vardecl-atts-begin-fn x-equiv ps)))
  :rule-classes :congruence)