Convert MSB-first octal digits into an initial (not truncated, not extended) MSB-first vl-bitlist-p.
(vl-octal-digits-to-bitlist digits) → bits
Function:
(defun vl-octal-digits-to-bitlist (digits) (declare (xargs :guard (character-listp digits))) (let ((__function__ 'vl-octal-digits-to-bitlist)) (declare (ignorable __function__)) (if (atom digits) nil (append (case (car digits) (#\0 (list :vl-0val :vl-0val :vl-0val)) (#\1 (list :vl-0val :vl-0val :vl-1val)) (#\2 (list :vl-0val :vl-1val :vl-0val)) (#\3 (list :vl-0val :vl-1val :vl-1val)) (#\4 (list :vl-1val :vl-0val :vl-0val)) (#\5 (list :vl-1val :vl-0val :vl-1val)) (#\6 (list :vl-1val :vl-1val :vl-0val)) (#\7 (list :vl-1val :vl-1val :vl-1val)) ((#\x #\X) (list :vl-xval :vl-xval :vl-xval)) ((#\z #\Z #\?) (list :vl-zval :vl-zval :vl-zval)) (otherwise (progn$ (raise "Not an octal digit: ~x0.~%" (car digits)) (list :vl-0val :vl-0val :vl-0val)))) (vl-octal-digits-to-bitlist (cdr digits))))))
Theorem:
(defthm vl-bitlist-p-of-vl-octal-digits-to-bitlist (b* ((bits (vl-octal-digits-to-bitlist digits))) (vl-bitlist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-octal-digits-to-bitlist (equal (len (vl-octal-digits-to-bitlist x)) (* 3 (len x))))