[acl2/acl2] f47e15: Print non-Boolean masks on a separate line

0 views
Skip to first unread message

GitHub

unread,
Jan 9, 2017, 12:22:56 PM1/9/17
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: f47e15f004ec18d873529404e1ae7704dbaa765a
https://github.com/acl2/acl2/commit/f47e15f004ec18d873529404e1ae7704dbaa765a
Author: Keshav Kini <kesha...@oracle.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Print non-Boolean masks on a separate line

When printing `svex-env-p` values using `svtv-print-alist-readable`,
every 4vec value which has some non-Boolean component (i.e. is not a
2vec) is (before this commit) displayed with a comment off to the
right giving a "non-Boolean mask", which is a bitvector showing which
bits are either X or Z, i.e. not a Boolean value 0 or 1.

This commit moves the non-Boolean mask to a separate line and aligns
it with the upper and lower components of the 4vec. With the new
positioning, it's easier to visually compare the non-Boolean mask with
the 4vec's components, as well as with other nearby values of the same
bit width.

Also, this change makes it far less likely for the pretty-printed
svex-env-p value to run into word wrapping issues. Formerly, due to
the spacing used, the non-Boolean mask would commonly (in my
experience) be wrapped to the next line if the 4vec was 32 bits or
wider and had a non-Boolean MSB. Now it shouldn't need to wrap until
it's around 160 bits wide, assuming the default right margin of around
77 columns.

Before:

```lisp
(FOO #ux1_FFFF ;; non-Boolean mask: #ux1_-
FFFF
. #ux0)
```

After:

```lisp
(FOO #ux1_FFFF
. #ux0)
;;; non-Boolean mask: #ux1_FFFF
```


Commit: 3cbaafc18c04cf5750e8a4e274e9b939050cd225
https://github.com/acl2/acl2/commit/3cbaafc18c04cf5750e8a4e274e9b939050cd225
Author: Keshav Kini <kesha...@oracle.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Right-align the three values for a non-2vec

Before:

```lisp
((RES #uxFCFA
. #uxCA0))
;;; non-Boolean mask: #uxF05A
```

After:

```lisp
((RES #uxFCFA
. #uxCA0))
;;; non-Boolean mask: #uxF05A
```


Commit: 991df11a980d0f335d98d6b96dffa82c92e461ca
https://github.com/acl2/acl2/commit/991df11a980d0f335d98d6b96dffa82c92e461ca
Author: Keshav Kini <kesha...@oracle.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Oops, I guess mask could need padding

For example, (str::hexify (logxor #ux-10 #uxF)) is "#ux-1", which
would need one character of padding to align with "#ux-10". Though I
doubt people are trying to eyeball bitwise comparisons of negative
integer literals... (?)


Commit: 96fbcbf6fa861f1b53413cc9eb58e52b3823cc3f
https://github.com/acl2/acl2/commit/96fbcbf6fa861f1b53413cc9eb58e52b3823cc3f
Author: solswords <ssw...@gmail.com>
Date: 2017-01-09 (Mon, 09 Jan 2017)

Changed paths:
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
Merge pull request #681 from kini/svex-env-printing

Improve formatting of non-Boolean masks


Compare: https://github.com/acl2/acl2/compare/84222b2b85b4...96fbcbf6fa86

GitHub

unread,
Jan 9, 2017, 12:47:22 PM1/9/17
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages