1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
|
#|
Load this file into raw Lisp and it will understand bit-vector notation
#vxxx as illustrated below. Doing so is completely optional and, strictly
speaking, not sanctioned as legal ACL2 operation.
ACL2>(load "/proj/acl2/v2-5/acl2-sources/books/bdd/bit-vector-reader.lisp")
Loading /proj/acl2/v2-5/acl2-sources/books/bdd/bit-vector-reader.lisp
Finished loading /proj/acl2/v2-5/acl2-sources/books/bdd/bit-vector-reader.lisp
T
ACL2>#v01100
(NIL NIL T T NIL)
ACL2>(LP)
ACL2 Version 2.5. Level 1. Cbd "/v/hank/v87/kaufmann/".
Type :help for help.
ACL2 !>#v01100
(NIL NIL T T NIL)
ACL2 !>
|#
(defun bit-vector-reader (stream subchar arg)
;; We "unread" the vector character, and reread to get a symbol. Otherwise
;; the number following the vector character might be read as a leading zero
;; of an integer.
(declare (ignore subchar arg))
(unread-char #\v stream)
(let ((symbol (read stream t nil t)))
;; Get rid of the vector character, reverse, and list for NQTHM.
`(LIST ,@(map 'list #'(lambda (x)
(if (equal x #\1)
't
(if (equal x #\0)
'nil
(error "Non-binary digits in --> ~s."
symbol))))
(reverse (subseq (symbol-name symbol) 1))))))
(eval-when (load eval)
(progn
(set-dispatch-macro-character #\# #\v #'bit-vector-reader)
(let ((*readtable* *acl2-readtable*))
(set-dispatch-macro-character #\# #\v #'bit-vector-reader))))
|