		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-mimic-linestart

Mechanism to try to indent expressions like the user had done.

Signature
(vl-mimic-linestart atts &key (attname '"VL_LINESTART") (ps 'ps)) → ps
Arguments: atts — Guard (vl-atts-p atts).; attname — Guard (stringp attname).

See in particular parse-expressions, which annotates certain expressions with a VL_LINESTART attribute that indicates that the expression was the first thing on a new line, and gives the column number that the expression was found on.

This function should be called when we are ready to insert a newline but only if one was present in the original source code. If the attributes indicate that there was a newline here, we insert a newline and indent appropriately.

Definitions and Theorems

Function: vl-mimic-linestart-fn

(defun vl-mimic-linestart-fn (atts attname ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (vl-atts-p atts)
                              (stringp attname))))
  (let ((__function__ 'vl-mimic-linestart))
    (declare (ignorable __function__))
    (b* (((unless atts) ps)
         (look (assoc-equal (string-fix attname)
                            (vl-atts-fix atts)))
         ((unless look) ps)
         ((unless (vl-ps->mimic-linebreaks-p))
          ps)
         (indent (if (and (vl-expr-p (cdr look))
                          (vl-expr-resolved-p (cdr look))
                          (<= 0 (vl-resolved->val (cdr look))))
                     (vl-resolved->val (cdr look))
                   0))
         (indent (max indent (vl-ps->autowrap-ind))))
      (vl-ps-seq (vl-println "")
                 (vl-indent indent)))))

Theorem: vl-mimic-linestart-fn-of-vl-atts-fix-atts

(defthm vl-mimic-linestart-fn-of-vl-atts-fix-atts
  (equal (vl-mimic-linestart-fn (vl-atts-fix atts)
                                attname ps)
         (vl-mimic-linestart-fn atts attname ps)))

Theorem: vl-mimic-linestart-fn-vl-atts-equiv-congruence-on-atts

(defthm vl-mimic-linestart-fn-vl-atts-equiv-congruence-on-atts
  (implies (vl-atts-equiv atts atts-equiv)
           (equal (vl-mimic-linestart-fn atts attname ps)
                  (vl-mimic-linestart-fn atts-equiv attname ps)))
  :rule-classes :congruence)

Theorem: vl-mimic-linestart-fn-of-str-fix-attname

(defthm vl-mimic-linestart-fn-of-str-fix-attname
  (equal (vl-mimic-linestart-fn atts (str-fix attname)
                                ps)
         (vl-mimic-linestart-fn atts attname ps)))

Theorem: vl-mimic-linestart-fn-streqv-congruence-on-attname

(defthm vl-mimic-linestart-fn-streqv-congruence-on-attname
  (implies (streqv attname attname-equiv)
           (equal (vl-mimic-linestart-fn atts attname ps)
                  (vl-mimic-linestart-fn atts attname-equiv ps)))
  :rule-classes :congruence)