(to-parstate$ parstate) → *
Function:
(defun to-parstate$-chars-read (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp n))) (let ((__function__ 'to-parstate$-chars-read)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (i (1- n)) ((unless (< i (parstate->chars-length parstate))) (raise "Internal error: chars-read index ~x0 out of bound ~x1." i (parstate->chars-length parstate)))) (cons (parstate->char i parstate) (to-parstate$-chars-read (1- n) parstate)))))
Theorem:
(defthm char+position-listp-of-to-parstate$-chars-read (b* ((chars (to-parstate$-chars-read n parstate))) (char+position-listp chars)) :rule-classes :rewrite)
Function:
(defun to-parstate$-chars-unread (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp n))) (let ((__function__ 'to-parstate$-chars-unread)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (i (+ (parstate->chars-read parstate) (- (parstate->chars-unread parstate) n))) ((unless (>= i 0)) (raise "Internal error: chars-unread index ~x0 is negative." i)) ((unless (< i (parstate->chars-length parstate))) (raise "Internal error: chars-unread index ~x0 out of bound ~x1." i (parstate->chars-length parstate)))) (cons (parstate->char i parstate) (to-parstate$-chars-unread (1- n) parstate)))))
Theorem:
(defthm char+position-listp-of-to-parstate$-chars-unread (b* ((chars (to-parstate$-chars-unread n parstate))) (char+position-listp chars)) :rule-classes :rewrite)
Function:
(defun to-parstate$-tokens-read (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp n))) (let ((__function__ 'to-parstate$-tokens-read)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (i (1- n)) ((unless (< i (parstate->tokens-length parstate))) (raise "Internal error: tokens-read index ~x0 out of bound ~x1." i (parstate->tokens-length parstate)))) (cons (parstate->token i parstate) (to-parstate$-tokens-read (1- n) parstate)))))
Theorem:
(defthm token+span-listp-of-to-parstate$-tokens-read (b* ((tokens (to-parstate$-tokens-read n parstate))) (token+span-listp tokens)) :rule-classes :rewrite)
Function:
(defun to-parstate$-tokens-unread (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp n))) (let ((__function__ 'to-parstate$-tokens-unread)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (i (+ (parstate->tokens-read parstate) (- (parstate->tokens-unread parstate) n))) ((unless (>= i 0)) (raise "Internal error: tokens-unread index ~x0 is negative." i)) ((unless (< i (parstate->tokens-length parstate))) (raise "Internal error: tokens-unread index ~x0 out of bound ~x1." i (parstate->tokens-length parstate)))) (cons (parstate->token i parstate) (to-parstate$-tokens-unread (1- n) parstate)))))
Theorem:
(defthm token+span-listp-of-to-parstate$-tokens-unread (b* ((tokens (to-parstate$-tokens-unread n parstate))) (token+span-listp tokens)) :rule-classes :rewrite)
Function:
(defun to-parstate$ (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard t)) (let ((__function__ 'to-parstate$)) (declare (ignorable __function__)) (make-parstate$ :bytes (parstate->bytes parstate) :position (parstate->position parstate) :chars-read (to-parstate$-chars-read (parstate->chars-read parstate) parstate) :chars-unread (to-parstate$-chars-unread (parstate->chars-unread parstate) parstate) :tokens-read (to-parstate$-tokens-read (parstate->tokens-read parstate) parstate) :tokens-unread (to-parstate$-tokens-unread (parstate->tokens-unread parstate) parstate) :gcc (parstate->gcc parstate))))