← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/vl/util/print.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/vl/util/print.lisp
34
34
(include-book "print-urlencode")
35
35
(include-book "print-htmlencode")
36
36
(include-book "cw-unformatted")
37
 
(include-book "std/strings/decimal" :dir :system)
 
37
(include-book "std/strings/pretty" :dir :system)
38
38
(local (include-book "arithmetic"))
39
39
(local (include-book "misc/assert" :dir :system))
40
40
(local (include-book "std/io/base" :dir :system))
63
63
 
64
64
(defsection vl-printedlist-p-util
65
65
  :extension vl-printedlist-p
66
 
  
 
66
 
67
67
  (local (in-theory (enable vl-printedlist-p)))
68
68
 
69
69
  (local (in-theory (e/d (repeated-revappend)
1523
1523
<p>Note: although other ACL2-style directives are not yet supported, we may
1524
1524
eventually extend the printer to allow them.</p>")
1525
1525
 
1526
 
(define vl-ppr-escape-slashes
1527
 
  :parents (vl-basic-fmt)
1528
 
  :short "This is basically like acl2::prin1-with-slashes, but we put the
1529
 
characters into the accumulator in reverse order instead of printing them."
1530
 
  ((x          stringp)
1531
 
   (n          natp)
1532
 
   (xl         (eql xl (length x)))
1533
 
   (slash-char characterp)
1534
 
   (col        natp)
1535
 
   acc)
1536
 
  :guard (<= n xl)
1537
 
  :returns (mv (col-prime natp :rule-classes :type-prescription)
1538
 
               (acc-prime character-listp :hyp (character-listp acc)))
1539
 
  :measure (nfix (- (nfix xl) (nfix n)))
1540
 
  :verbosep t
1541
 
  (b* ((n   (lnfix n))
1542
 
       (col (lnfix col))
1543
 
       ((when (mbe :logic (zp (- (nfix xl) (nfix n)))
1544
 
                   :exec (eql n xl)))
1545
 
        (mv col acc))
1546
 
       ((the character char)
1547
 
        (mbe :logic (char-fix (char x n))
1548
 
             :exec (char x n)))
1549
 
       ((the character slash-char)
1550
 
        (mbe :logic (char-fix slash-char)
1551
 
             :exec slash-char)))
1552
 
    (vl-ppr-escape-slashes x
1553
 
                           (the unsigned-byte (+ 1 n))
1554
 
                           xl
1555
 
                           slash-char
1556
 
                           (if (eql char #\Newline)
1557
 
                               0
1558
 
                             (the unsigned-byte (+ 1 col)))
1559
 
                           (if (or (eql char #\\)
1560
 
                                   (eql char slash-char))
1561
 
                               (list* char #\\ acc)
1562
 
                             (cons char acc))))
1563
 
  :hooks ((:fix :hints(("Goal"
1564
 
                        ;; The expansion heuristics stupidly don't want to open
1565
 
                        ;; up calls that have fixes in them.
1566
 
                        :expand ((:free (x n xl slash-char col)
1567
 
                                  (vl-ppr-escape-slashes x n xl slash-char col acc)))))))
1568
 
  ///
1569
 
  (defthm vl-printedlist-p-of-vl-ppr-escape-slashes
1570
 
    (implies (vl-printedlist-p acc)
1571
 
             (vl-printedlist-p
1572
 
              (mv-nth 1 (vl-ppr-escape-slashes x n xl slash-char col acc))))))
1573
 
 
1574
 
(define vl-ppr-explode-symbol-aux
1575
 
  :parents (vl-ppr-explode-symbol)
1576
 
  :short "Write the characters for a symbol name, adding bars if necessary."
1577
 
  ((name stringp   "Name of a symbol or package.")
1578
 
   (col  natp)
1579
 
   acc)
1580
 
  :returns (mv (new-col natp :rule-classes :type-prescription)
1581
 
               (acc     character-listp :hyp (character-listp acc)))
1582
 
  (b* ((name (string-fix name))
1583
 
       (col  (lnfix col))
1584
 
       (len  (length name))
1585
 
       ((when (acl2::may-need-slashes-fn name 10))
1586
 
        (b* (((mv col acc)
1587
 
              (vl-ppr-escape-slashes name 0 len #\| (+ 1 col) (cons #\| acc))))
1588
 
          (mv (+ 1 col) (cons #\| acc)))))
1589
 
    (mv (+ (lnfix col) len)
1590
 
        (str::revappend-chars name acc)))
1591
 
  :verbosep t
1592
 
  :prepwork
1593
 
  ((local (in-theory (disable acl2::may-need-slashes-fn))))
1594
 
  ///
1595
 
  (defthm vl-printedlist-p-of-vl-ppr-explode-symbol-aux
1596
 
    (implies (vl-printedlist-p acc)
1597
 
             (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-symbol-aux name col acc))))))
1598
 
 
1599
 
 
1600
 
(define vl-ppr-explode-symbol
1601
 
  :parents (vl-basic-fmt)
1602
 
  :short "Print a symbol."
1603
 
  ((x   symbolp "The symbol we want to explode.")
1604
 
   (pkg symbolp "A symbol in the current package we are printing from.")
1605
 
   (col natp    "Current column we're at.")
1606
 
   (acc))
1607
 
  :returns (mv (new-col natp :rule-classes :type-prescription)
1608
 
               (acc     character-listp :hyp (character-listp acc)))
1609
 
  (b* ((x     (mbe :logic (acl2::symbol-fix x) :exec x))
1610
 
       (pkg   (mbe :logic (acl2::symbol-fix pkg) :exec pkg))
1611
 
       (col   (lnfix col))
1612
 
       (xname (symbol-name x))
1613
 
       (xpkg  (symbol-package-name x))
1614
 
       ((when (or (equal xpkg xname)
1615
 
                  (equal (intern-in-package-of-symbol xname pkg) x)))
1616
 
        (vl-ppr-explode-symbol-aux xname col acc))
1617
 
       ((when (equal xpkg "KEYWORD"))
1618
 
        (vl-ppr-explode-symbol-aux xname (+ 1 col) (cons #\: acc)))
1619
 
       ((mv col acc) (vl-ppr-explode-symbol-aux xpkg col acc))
1620
 
       (col          (+ 2 col))
1621
 
       (acc          (list* #\: #\: acc)))
1622
 
    (vl-ppr-explode-symbol-aux xname col acc))
1623
 
  ///
1624
 
  (defthm vl-printedlist-p-of-vl-ppr-explode-symbol
1625
 
    (implies (vl-printedlist-p acc)
1626
 
             (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-symbol x pkg col acc))))))
1627
 
 
1628
 
(define vl-ppr-explode-string
1629
 
  :parents (vl-basic-fmt)
1630
 
  :short "Print a string."
1631
 
  ((x stringp)
1632
 
   (col natp)
1633
 
   acc)
1634
 
  :returns (mv (new-col natp :rule-classes :type-prescription)
1635
 
               (acc character-listp :hyp (character-listp acc)))
1636
 
  (b* ((x   (string-fix x))
1637
 
       (col (lnfix col))
1638
 
       ((mv col acc)
1639
 
        (vl-ppr-escape-slashes x 0 (length x) #\" (+ 1 col) (cons #\" acc))))
1640
 
    (mv (+ 1 col) (cons #\" acc)))
1641
 
  ///
1642
 
  (defthm vl-printedlist-p-of-vl-ppr-explode-string
1643
 
    (implies (vl-printedlist-p acc)
1644
 
             (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-string x col acc))))))
1645
 
 
1646
 
(define vl-ppr-explode-atom
1647
 
  :parents (vl-basic-fmt)
1648
 
  ((x atom)
1649
 
   (pkg symbolp)
1650
 
   (base print-base-p)
1651
 
   (col natp)
1652
 
   acc)
1653
 
  :hooks ((:fix :args ((pkg symbolp) (col natp))))
1654
 
  :returns (mv (new-col natp :rule-classes :type-prescription)
1655
 
               (acc character-listp :hyp (character-listp acc)))
1656
 
  (b* ((col (lnfix col))
1657
 
       ((when (symbolp x))
1658
 
        (vl-ppr-explode-symbol x pkg col acc))
1659
 
       ((when (stringp x))
1660
 
        (vl-ppr-explode-string x col acc))
1661
 
       ((when (acl2-numberp x))
1662
 
        (let* ((explode (explode-atom x base))
1663
 
               (len     (len explode)))
1664
 
          (mv (+ col len) (revappend explode acc))))
1665
 
       ((when (characterp x))
1666
 
        (case x
1667
 
          (#\Space   (mv (+ col 7) (str::revappend-chars "#\\Space" acc)))
1668
 
          (#\Newline (mv (+ col 9) (str::revappend-chars "#\\Newline" acc)))
1669
 
          (#\Tab     (mv (+ col 5) (str::revappend-chars "#\\Tab" acc)))
1670
 
          (#\Rubout  (mv (+ col 8) (str::revappend-chars "#\\Rubout" acc)))
1671
 
          (#\Page    (mv (+ col 6) (str::revappend-chars "#\\Page" acc)))
1672
 
          (otherwise (mv (+ col 3) (list* x #\\ #\# acc))))))
1673
 
    (raise "Bad atom: ~x0." x)
1674
 
    (mv (+ col 10) (str::revappend-chars "<bad atom>" acc)))
1675
 
  ///
1676
 
  (defthm vl-printedlist-p-of-vl-ppr-explode-atom
1677
 
    (implies (vl-printedlist-p acc)
1678
 
             (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-atom x pkg base col acc))))))
1679
 
 
1680
 
 
1681
 
(define vl-stupid-ppr1
1682
 
  :parents (vl-basic-fmt)
1683
 
  :short "Barbaric pretty-printer."
1684
 
  ((x                      "Any ACL2 object.")
1685
 
   (pkg      symbolp       "Home package we're printing from.")
1686
 
   (base     print-base-p  "Numeric base for printing numbers.")
1687
 
   (rmargin  natp          "Right margin for line wrapping.")
1688
 
   (in-listp booleanp      "Are we currently in a list?")
1689
 
   (col      natp          "Current column number.")
1690
 
   (acc))
1691
 
  :hooks ((:fix :args ((pkg symbolp)
1692
 
                       (rmargin natp)
1693
 
                       (in-listp booleanp)
1694
 
                       (col natp))))
1695
 
  :returns (mv (new-col natp :rule-classes :type-prescription)
1696
 
               (new-acc character-listp :hyp (character-listp acc)))
1697
 
  :verify-guards nil
1698
 
  (b* ((col     (lnfix col))
1699
 
       (rmargin (lnfix rmargin))
1700
 
       ((when (atom x))
1701
 
        (vl-ppr-explode-atom x pkg base col acc))
1702
 
       ((mv col acc)
1703
 
        (if in-listp
1704
 
            (vl-stupid-ppr1 (car x) pkg base rmargin nil col acc)
1705
 
          (vl-stupid-ppr1 (car x) pkg base rmargin nil (+ 1 col) (cons #\( acc))))
1706
 
       ((when (not (cdr x)))
1707
 
        (mv (+ 1 (lnfix col)) (if in-listp acc (cons #\) acc))))
1708
 
       ;; "Maybe break"
1709
 
       ((mv col acc) (if (< col rmargin)
1710
 
                         (mv col acc)
1711
 
                       (mv 0 (cons #\Newline acc))))
1712
 
       ((when (consp (cdr x)))
1713
 
        ;; Successive elements of a list, no dots.
1714
 
        (b* (((mv col acc)
1715
 
              (vl-stupid-ppr1 (cdr x) pkg base rmargin t (+ 1 col) (cons #\Space acc))))
1716
 
          (mv (+ 1 (lnfix col))
1717
 
              (if in-listp acc (cons #\) acc)))))
1718
 
 
1719
 
       ;; End element, need a dot.
1720
 
       (col (+ 3 col))
1721
 
       (acc (list* #\Space #\. #\Space acc))
1722
 
 
1723
 
       ;; "Maybe break"
1724
 
       ((mv col acc) (if (< col rmargin)
1725
 
                         (mv col acc)
1726
 
                       (mv 0 (cons #\Newline acc))))
1727
 
 
1728
 
       ((mv col acc)
1729
 
        (vl-stupid-ppr1 (cdr x) pkg base rmargin t col acc)))
1730
 
 
1731
 
    (mv (+ 1 (lnfix col))
1732
 
        (if in-listp acc (cons #\) acc))))
1733
 
  ///
1734
 
  (defthm vl-printedlist-p-of-vl-stupid-ppr1
1735
 
    (implies (vl-printedlist-p acc)
1736
 
             (vl-printedlist-p (mv-nth 1 (vl-stupid-ppr1 x pkg base rmargin in-listp col acc)))))
1737
 
 
1738
 
  (verify-guards vl-stupid-ppr1))
1739
 
 
 
1526
 
 
1527
 
 
1528
 
 
1529
 
 
1530
;; (define vl-ppr-escape-slashes
 
1531
;;   :parents (vl-basic-fmt)
 
1532
;;   :short "This is basically like acl2::prin1-with-slashes, but we put the
 
1533
;; characters into the accumulator in reverse order instead of printing them."
 
1534
;;   ((x          stringp)
 
1535
;;    (n          natp)
 
1536
;;    (xl         (eql xl (length x)))
 
1537
;;    (slash-char characterp)
 
1538
;;    (col        natp)
 
1539
;;    acc)
 
1540
;;   :guard (<= n xl)
 
1541
;;   :returns (mv (col-prime natp :rule-classes :type-prescription)
 
1542
;;                (acc-prime character-listp :hyp (character-listp acc)))
 
1543
;;   :measure (nfix (- (nfix xl) (nfix n)))
 
1544
;;   :verbosep t
 
1545
;;   (b* ((n   (lnfix n))
 
1546
;;        (col (lnfix col))
 
1547
;;        ((when (mbe :logic (zp (- (nfix xl) (nfix n)))
 
1548
;;                    :exec (eql n xl)))
 
1549
;;         (mv col acc))
 
1550
;;        ((the character char)
 
1551
;;         (mbe :logic (char-fix (char x n))
 
1552
;;              :exec (char x n)))
 
1553
;;        ((the character slash-char)
 
1554
;;         (mbe :logic (char-fix slash-char)
 
1555
;;              :exec slash-char)))
 
1556
;;     (vl-ppr-escape-slashes x
 
1557
;;                            (the unsigned-byte (+ 1 n))
 
1558
;;                            xl
 
1559
;;                            slash-char
 
1560
;;                            (if (eql char #\Newline)
 
1561
;;                                0
 
1562
;;                              (the unsigned-byte (+ 1 col)))
 
1563
;;                            (if (or (eql char #\\)
 
1564
;;                                    (eql char slash-char))
 
1565
;;                                (list* char #\\ acc)
 
1566
;;                              (cons char acc))))
 
1567
;;   :hooks ((:fix :hints(("Goal"
 
1568
;;                         ;; The expansion heuristics stupidly don't want to open
 
1569
;;                         ;; up calls that have fixes in them.
 
1570
;;                         :expand ((:free (x n xl slash-char col)
 
1571
;;                                   (vl-ppr-escape-slashes x n xl slash-char col acc)))))))
 
1572
;;   ///
 
1573
;;   (defthm vl-printedlist-p-of-vl-ppr-escape-slashes
 
1574
;;     (implies (vl-printedlist-p acc)
 
1575
;;              (vl-printedlist-p
 
1576
;;               (mv-nth 1 (vl-ppr-escape-slashes x n xl slash-char col acc))))))
 
1577
 
 
1578
;; (define vl-ppr-explode-symbol-aux
 
1579
;;   :parents (vl-ppr-explode-symbol)
 
1580
;;   :short "Write the characters for a symbol name, adding bars if necessary."
 
1581
;;   ((name stringp   "Name of a symbol or package.")
 
1582
;;    (col  natp)
 
1583
;;    acc)
 
1584
;;   :returns (mv (new-col natp :rule-classes :type-prescription)
 
1585
;;                (acc     character-listp :hyp (character-listp acc)))
 
1586
;;   (b* ((name (string-fix name))
 
1587
;;        (col  (lnfix col))
 
1588
;;        (len  (length name))
 
1589
;;        ((when (acl2::may-need-slashes-fn name 10))
 
1590
;;         (b* (((mv col acc)
 
1591
;;               (vl-ppr-escape-slashes name 0 len #\| (+ 1 col) (cons #\| acc))))
 
1592
;;           (mv (+ 1 col) (cons #\| acc)))))
 
1593
;;     (mv (+ (lnfix col) len)
 
1594
;;         (str::revappend-chars name acc)))
 
1595
;;   :verbosep t
 
1596
;;   :prepwork
 
1597
;;   ((local (in-theory (disable acl2::may-need-slashes-fn))))
 
1598
;;   ///
 
1599
;;   (defthm vl-printedlist-p-of-vl-ppr-explode-symbol-aux
 
1600
;;     (implies (vl-printedlist-p acc)
 
1601
;;              (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-symbol-aux name col acc))))))
 
1602
 
 
1603
 
 
1604
;; (define vl-ppr-explode-symbol
 
1605
;;   :parents (vl-basic-fmt)
 
1606
;;   :short "Print a symbol."
 
1607
;;   ((x   symbolp "The symbol we want to explode.")
 
1608
;;    (pkg symbolp "A symbol in the current package we are printing from.")
 
1609
;;    (col natp    "Current column we're at.")
 
1610
;;    (acc))
 
1611
;;   :returns (mv (new-col natp :rule-classes :type-prescription)
 
1612
;;                (acc     character-listp :hyp (character-listp acc)))
 
1613
;;   (b* ((x     (mbe :logic (acl2::symbol-fix x) :exec x))
 
1614
;;        (pkg   (mbe :logic (acl2::symbol-fix pkg) :exec pkg))
 
1615
;;        (col   (lnfix col))
 
1616
;;        (xname (symbol-name x))
 
1617
;;        (xpkg  (symbol-package-name x))
 
1618
;;        ((when (or (equal xpkg xname)
 
1619
;;                   (equal (intern-in-package-of-symbol xname pkg) x)))
 
1620
;;         (vl-ppr-explode-symbol-aux xname col acc))
 
1621
;;        ((when (equal xpkg "KEYWORD"))
 
1622
;;         (vl-ppr-explode-symbol-aux xname (+ 1 col) (cons #\: acc)))
 
1623
;;        ((mv col acc) (vl-ppr-explode-symbol-aux xpkg col acc))
 
1624
;;        (col          (+ 2 col))
 
1625
;;        (acc          (list* #\: #\: acc)))
 
1626
;;     (vl-ppr-explode-symbol-aux xname col acc))
 
1627
;;   ///
 
1628
;;   (defthm vl-printedlist-p-of-vl-ppr-explode-symbol
 
1629
;;     (implies (vl-printedlist-p acc)
 
1630
;;              (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-symbol x pkg col acc))))))
 
1631
 
 
1632
;; (define vl-ppr-explode-string
 
1633
;;   :parents (vl-basic-fmt)
 
1634
;;   :short "Print a string."
 
1635
;;   ((x stringp)
 
1636
;;    (col natp)
 
1637
;;    acc)
 
1638
;;   :returns (mv (new-col natp :rule-classes :type-prescription)
 
1639
;;                (acc character-listp :hyp (character-listp acc)))
 
1640
;;   (b* ((x   (string-fix x))
 
1641
;;        (col (lnfix col))
 
1642
;;        ((mv col acc)
 
1643
;;         (vl-ppr-escape-slashes x 0 (length x) #\" (+ 1 col) (cons #\" acc))))
 
1644
;;     (mv (+ 1 col) (cons #\" acc)))
 
1645
;;   ///
 
1646
;;   (defthm vl-printedlist-p-of-vl-ppr-explode-string
 
1647
;;     (implies (vl-printedlist-p acc)
 
1648
;;              (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-string x col acc))))))
 
1649
 
 
1650
;; (define vl-ppr-explode-atom
 
1651
;;   :parents (vl-basic-fmt)
 
1652
;;   ((x atom)
 
1653
;;    (pkg symbolp)
 
1654
;;    (base print-base-p)
 
1655
;;    (col natp)
 
1656
;;    acc)
 
1657
;;   :hooks ((:fix :args ((pkg symbolp) (col natp))))
 
1658
;;   :returns (mv (new-col natp :rule-classes :type-prescription)
 
1659
;;                (acc character-listp :hyp (character-listp acc)))
 
1660
;;   (b* ((col (lnfix col))
 
1661
;;        ((when (symbolp x))
 
1662
;;         (vl-ppr-explode-symbol x pkg col acc))
 
1663
;;        ((when (stringp x))
 
1664
;;         (vl-ppr-explode-string x col acc))
 
1665
;;        ((when (acl2-numberp x))
 
1666
;;         (let* ((explode (explode-atom x base))
 
1667
;;                (len     (len explode)))
 
1668
;;           (mv (+ col len) (revappend explode acc))))
 
1669
;;        ((when (characterp x))
 
1670
;;         (case x
 
1671
;;           (#\Space   (mv (+ col 7) (str::revappend-chars "#\\Space" acc)))
 
1672
;;           (#\Newline (mv (+ col 9) (str::revappend-chars "#\\Newline" acc)))
 
1673
;;           (#\Tab     (mv (+ col 5) (str::revappend-chars "#\\Tab" acc)))
 
1674
;;           (#\Rubout  (mv (+ col 8) (str::revappend-chars "#\\Rubout" acc)))
 
1675
;;           (#\Page    (mv (+ col 6) (str::revappend-chars "#\\Page" acc)))
 
1676
;;           (otherwise (mv (+ col 3) (list* x #\\ #\# acc))))))
 
1677
;;     (raise "Bad atom: ~x0." x)
 
1678
;;     (mv (+ col 10) (str::revappend-chars "<bad atom>" acc)))
 
1679
;;   ///
 
1680
;;   (defthm vl-printedlist-p-of-vl-ppr-explode-atom
 
1681
;;     (implies (vl-printedlist-p acc)
 
1682
;;              (vl-printedlist-p (mv-nth 1 (vl-ppr-explode-atom x pkg base col acc))))))
 
1683
 
 
1684
 
 
1685
;; (define vl-stupid-ppr1
 
1686
;;   :parents (vl-basic-fmt)
 
1687
;;   :short "Barbaric pretty-printer."
 
1688
;;   ((x                      "Any ACL2 object.")
 
1689
;;    (pkg      symbolp       "Home package we're printing from.")
 
1690
;;    (base     print-base-p  "Numeric base for printing numbers.")
 
1691
;;    (rmargin  natp          "Right margin for line wrapping.")
 
1692
;;    (in-listp booleanp      "Are we currently in a list?")
 
1693
;;    (col      natp          "Current column number.")
 
1694
;;    (acc))
 
1695
;;   :hooks ((:fix :args ((pkg symbolp)
 
1696
;;                        (rmargin natp)
 
1697
;;                        (in-listp booleanp)
 
1698
;;                        (col natp))))
 
1699
;;   :returns (mv (new-col natp :rule-classes :type-prescription)
 
1700
;;                (new-acc character-listp :hyp (character-listp acc)))
 
1701
;;   :verify-guards nil
 
1702
;;   (b* ((col     (lnfix col))
 
1703
;;        (rmargin (lnfix rmargin))
 
1704
;;        ((when (atom x))
 
1705
;;         (vl-ppr-explode-atom x pkg base col acc))
 
1706
;;        ((mv col acc)
 
1707
;;         (if in-listp
 
1708
;;             (vl-stupid-ppr1 (car x) pkg base rmargin nil col acc)
 
1709
;;           (vl-stupid-ppr1 (car x) pkg base rmargin nil (+ 1 col) (cons #\( acc))))
 
1710
;;        ((when (not (cdr x)))
 
1711
;;         (mv (+ 1 (lnfix col)) (if in-listp acc (cons #\) acc))))
 
1712
;;        ;; "Maybe break"
 
1713
;;        ((mv col acc) (if (< col rmargin)
 
1714
;;                          (mv col acc)
 
1715
;;                        (mv 0 (cons #\Newline acc))))
 
1716
;;        ((when (consp (cdr x)))
 
1717
;;         ;; Successive elements of a list, no dots.
 
1718
;;         (b* (((mv col acc)
 
1719
;;               (vl-stupid-ppr1 (cdr x) pkg base rmargin t (+ 1 col) (cons #\Space acc))))
 
1720
;;           (mv (+ 1 (lnfix col))
 
1721
;;               (if in-listp acc (cons #\) acc)))))
 
1722
 
 
1723
;;        ;; End element, need a dot.
 
1724
;;        (col (+ 3 col))
 
1725
;;        (acc (list* #\Space #\. #\Space acc))
 
1726
 
 
1727
;;        ;; "Maybe break"
 
1728
;;        ((mv col acc) (if (< col rmargin)
 
1729
;;                          (mv col acc)
 
1730
;;                        (mv 0 (cons #\Newline acc))))
 
1731
 
 
1732
;;        ((mv col acc)
 
1733
;;         (vl-stupid-ppr1 (cdr x) pkg base rmargin t col acc)))
 
1734
 
 
1735
;;     (mv (+ 1 (lnfix col))
 
1736
;;         (if in-listp acc (cons #\) acc))))
 
1737
;;   ///
 
1738
;;   (defthm vl-printedlist-p-of-vl-stupid-ppr1
 
1739
;;     (implies (vl-printedlist-p acc)
 
1740
;;              (vl-printedlist-p (mv-nth 1 (vl-stupid-ppr1 x pkg base rmargin in-listp col acc)))))
 
1741
 
 
1742
;;   (verify-guards vl-stupid-ppr1))
1740
1743
 
1741
1744
(define vl-skip-ws
1742
1745
  :parents (vl-basic-fmt)
1862
1865
         (implies (character-listp x)
1863
1866
                  (true-listp x))))
1864
1867
 
 
1868
 
 
1869
 
 
1870
(define vl-fmt-tilde-x-column ((rchars   character-listp)
 
1871
                               (orig-col natp))
 
1872
  ;; Horrible stupid function used in vl-stupid-ppr1.  The str::pretty function
 
1873
  ;; doesn't tell us the final column number.  This just looks at the
 
1874
  ;; (backwards) characters to figure it out.
 
1875
  :returns (col natp)
 
1876
  (cond ((atom rchars)
 
1877
         (lnfix orig-col))
 
1878
        ((chareqv (car rchars) #\Newline)
 
1879
         0)
 
1880
        (t
 
1881
         (+ 1 (vl-fmt-tilde-x-column (cdr rchars) orig-col)))))
 
1882
 
1865
1883
(define vl-fmt-tilde-x (x &key (ps 'ps))
1866
1884
  :parents (vl-basic-fmt)
1867
1885
  (b* ((rchars  (vl-ps->rchars))
1871
1889
       (htmlp   (vl-ps->htmlp))
1872
1890
       (tabsize (vl-ps->tabsize))
1873
1891
       (rmargin (vl-ps->autowrap-col))
 
1892
 
 
1893
       (config (str::make-printconfig :flat-right-margin   (max 40 (floor rmargin 2))
 
1894
                                      :hard-right-margin   (max 77 rmargin)
 
1895
                                      :print-base          base
 
1896
                                      :print-radix         nil
 
1897
                                      :home-package        pkg
 
1898
                                      :print-lowercase     nil))
 
1899
 
 
1900
       (x-rchars (str::revappend-pretty x nil :config config :col col))
1874
1901
       ((unless htmlp)
1875
 
        (mv-let (col rchars)
1876
 
                (vl-stupid-ppr1 x pkg base rmargin nil col rchars)
1877
 
                (vl-ps-seq
1878
 
                 (vl-ps-update-col col)
1879
 
                 (vl-ps-update-rchars rchars))))
1880
 
       ;; Else, we need to HTML-encode the printing of X.  Rather than
1881
 
       ;; complicate all the ppr functions with htmlp, we just do the normal
1882
 
       ;; printing then HTML-encode the resulting character list.  This is kind
1883
 
       ;; of horrifyingly inefficient.  On the other hand, it's still linear
1884
 
       ;; and shouldn't be THAT bad...
1885
 
       (temp         nil)
1886
 
       ((mv & temp)  (vl-stupid-ppr1 x pkg base rmargin nil col temp))
1887
 
       (temp         (reverse temp))
1888
 
       ((mv col rchars) (vl-html-encode-chars-aux temp col tabsize rchars)))
1889
 
      (vl-ps-seq
1890
 
       (vl-ps-update-col col)
1891
 
       (vl-ps-update-rchars rchars))))
 
1902
        (vl-ps-seq
 
1903
         ;; One option would be to append the new-rchars onto rchars.  Cost: N
 
1904
         ;; conses.  Another option would be to implode new-rchars into a
 
1905
         ;; string, then cons that string onto rchars.  Cost: implode and one
 
1906
         ;; cons.  I think I'll go with the second option because it seems like
 
1907
         ;; it should be nicer to the garbage collector.
 
1908
         (vl-ps-update-rchars (cons (str::rchars-to-string x-rchars) rchars))
 
1909
         (vl-ps-update-col    (vl-fmt-tilde-x-column x-rchars col))))
 
1910
 
 
1911
       ;; HTML mode.  We're going to html encode the new-rchars.
 
1912
       ((mv col rchars)
 
1913
        (vl-html-encode-chars-aux (reverse x-rchars) col tabsize rchars)))
 
1914
    (vl-ps-seq
 
1915
     (vl-ps-update-col col)
 
1916
     (vl-ps-update-rchars rchars))))
 
1917
 
 
1918
(local
 
1919
 (encapsulate
 
1920
   ()
 
1921
   (defun test-vl-fmt-tilde-x (x)
 
1922
     (with-local-ps
 
1923
       (vl-print "Hello ")
 
1924
       (vl-fmt-tilde-x x)
 
1925
       (vl-print ", World")))
 
1926
   (assert! (equal (test-vl-fmt-tilde-x '(a))
 
1927
                   "Hello (A), World"))
 
1928
   (assert! (equal (test-vl-fmt-tilde-x '(a b))
 
1929
                   "Hello (A B), World"))
 
1930
   (assert! (equal (test-vl-fmt-tilde-x
 
1931
                    (repeat 10 ':foo)) "Hello (:FOO :FOO
 
1932
            :FOO :FOO
 
1933
            :FOO :FOO
 
1934
            :FOO :FOO
 
1935
            :FOO :FOO), World"))))
1892
1936
 
1893
1937
(define vl-fmt-tilde-s (x &key (ps 'ps))
1894
1938
  :parents (vl-basic-fmt)
1933
1977
 
1934
1978
 
1935
1979
 
1936
 
 
1937
1980
(define vl-fmt-print-space (&key (ps 'ps))
1938
1981
  :parents (vl-basic-fmt)
1939
1982