		Search-engine friendly clone of the ACL2 documentation.

Read-tty

Read a byte from the TTY.

Signature
(read-tty x86) → (mv byt x86)
Returns: x86 — Type (x86p x86), given (x86p x86).

This function reads a byte from the tty-in field of the x86 stobj by extracting and returning its car and writing the cdr to the tty-in field. If the tty-in field is empty (i.e. it is nil), this function returns nil and the x86 stobj is unmodified. Including tty-raw.lsp in raw lisp smashes this function to read from a TCP port instead.

Definitions and Theorems

Function: read-tty

(defun read-tty (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'read-tty))
    (declare (ignorable __function__))
    (b* ((buf (tty-in x86))
         ((when (null buf)) (mv nil x86))
         (byt (car buf))
         (x86 (!tty-in (cdr buf) x86)))
      (mv byt x86))))

Theorem: x86p-of-read-tty.x86

(defthm x86p-of-read-tty.x86
  (implies (x86p x86)
           (b* (((mv ?byt ?x86) (read-tty x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Theorem: unsigned-byte-p-8-non-nil-read-tty

(defthm unsigned-byte-p-8-non-nil-read-tty
  (implies (and (x86p x86)
                (mv-nth 0 (read-tty x86)))
           (unsigned-byte-p 8 (mv-nth 0 (read-tty x86)))))