		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-arguments

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

Definitions and Theorems

Function: vl-pp-arguments-fn

(defun vl-pp-arguments-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-arguments-p x)))
 (let ((__function__ 'vl-pp-arguments))
  (declare (ignorable __function__))
  (without-mimicking-linebreaks
   (b*
    ((namedp (vl-arguments-case x :vl-arguments-named))
     (args (vl-arguments-case
                x
                :vl-arguments-named (vl-arguments-named->args x)
                :vl-arguments-plain (vl-arguments-plain->args x)))
     (force-newlinep (longer-than-p 5 args))
     ((when namedp)
      (vl-ps-seq (if (vl-arguments-named->starp x)
                     (vl-ps-seq (vl-print ".*")
                                (cond ((atom args) ps)
                                      ((not force-newlinep)
                                       (vl-println? ", "))
                                      (t (vl-println ","))))
                   ps)
                 (vl-pp-namedarglist args force-newlinep)))
     ((when (and (consp args)
                 (not (consp (cdr args)))
                 (not (vl-plainarg->expr (car args)))))
      (if
       (vl-plainarg->portname (car args))
       (b*
        ((namedarg
          (make-vl-namedarg :name (vl-plainarg->portname (car args))
                            :expr nil
                            :atts (vl-plainarg->atts (car args)))))
        (cw
         "; Warning: horrible corner case in vl-pp-arguments, ~
                   printing named.~%")
        (vl-pp-namedarglist (list namedarg)
                            force-newlinep))
       (progn$
        (raise
         "Trying to print a plain argument list, of length 1, which ~
                   contains a \"blank\" entry.  But there is actually no way ~
                   to express this in Verilog.")
        ps))))
    (vl-pp-plainarglist args force-newlinep)))))

Theorem: vl-pp-arguments-fn-of-vl-arguments-fix-x

(defthm vl-pp-arguments-fn-of-vl-arguments-fix-x
  (equal (vl-pp-arguments-fn (vl-arguments-fix x)
                             ps)
         (vl-pp-arguments-fn x ps)))

Theorem: vl-pp-arguments-fn-vl-arguments-equiv-congruence-on-x

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