Lex zero or more characters and escape sequences in a character constant.
(lex-*-c-char parstate) → (mv erp cchars closing-squote-pos new-parstate)
That is, lex a
This is called when we expect a character constant, after reading the opening single quote of a character constant. If successful, this reads up to and including the closing single quote, and returns the position of the latter, along with the sequence of characters and escape sequences.
We read the next character; it is an error if there is none. It is also an error if the character is a new-line. If the character is a single quote, we end the recursion and return. If the character is a backslah, we attempt to read an escape sequence, then we read zero or more additional characters and escape sequences, and we combine them with the escape sequence. In all other cases, we take the character as is, we read zero or more additional characters and escape sequences, and we combine them with the character.
Function:
(defun lex-*-c-char (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'lex-*-c-char)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-position) parstate) ((erp char pos parstate) (read-char parstate)) ((unless char) (reterr-msg :where (position-to-msg pos) :expected "an escape sequence or ~ any character other than ~ single quote or backslash or new-line" :found (char-to-msg char))) ((when (= char (char-code #\'))) (retok nil pos parstate)) ((when (= char 10)) (reterr-msg :where (position-to-msg pos) :expected "an escape sequence or ~ any character other than ~ single quote or backslash or new-line" :found (char-to-msg char))) ((erp cchar & parstate) (if (= char (char-code #\\)) (b* (((erp escape pos parstate) (lex-escape-sequence parstate)) (cchar (c-char-escape escape))) (retok cchar pos parstate)) (b* ((cchar (c-char-char char))) (retok cchar pos parstate)))) ((erp cchars closing-squote-pos parstate) (lex-*-c-char parstate))) (retok (cons cchar cchars) closing-squote-pos parstate))))
Theorem:
(defthm c-char-listp-of-lex-*-c-char.cchars (b* (((mv acl2::?erp ?cchars ?closing-squote-pos ?new-parstate) (lex-*-c-char parstate))) (c-char-listp cchars)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-*-c-char.closing-squote-pos (b* (((mv acl2::?erp ?cchars ?closing-squote-pos ?new-parstate) (lex-*-c-char parstate))) (positionp closing-squote-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-*-c-char.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?cchars ?closing-squote-pos ?new-parstate) (lex-*-c-char parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-*-c-char-uncond (b* (((mv acl2::?erp ?cchars ?closing-squote-pos ?new-parstate) (lex-*-c-char parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-*-c-char-cond (b* (((mv acl2::?erp ?cchars ?closing-squote-pos ?new-parstate) (lex-*-c-char parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (- (parsize parstate) (len cchars)))))) :rule-classes :linear)