Lex zero or more characters and escape sequences in a string literal.
(lex-*-s-char pstate) → (mv erp schars closing-dquote-pos new-pstate)
That is, lex a
This is called when we expect a string literal, after reading the opening double quote of a string literal. If successful, this reads up to and including the closing double 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 double 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-*-s-char (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-*-s-char)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate)) ((unless char) (reterr-msg :where (position-to-msg pos) :expected "an escape sequence or ~ any character other than ~ double quote or backslash" :found (char-to-msg char))) ((when (= char (char-code #\"))) (retok nil pos pstate)) ((when (= char 10)) (reterr-msg :where (position-to-msg pos) :expected "an escape sequence or ~ any character other than ~ double quote or backslash" :found (char-to-msg char))) ((erp schar & pstate) (if (= char (char-code #\\)) (b* (((erp escape pos pstate) (lex-escape-sequence pstate)) (schar (s-char-escape escape))) (retok schar pos pstate)) (b* ((schar (s-char-char char))) (retok schar pos pstate)))) ((erp schars closing-dquote-pos pstate) (lex-*-s-char pstate))) (retok (cons schar schars) closing-dquote-pos pstate))))
Theorem:
(defthm s-char-listp-of-lex-*-s-char.schars (b* (((mv acl2::?erp ?schars ?closing-dquote-pos ?new-pstate) (lex-*-s-char pstate))) (s-char-listp schars)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-*-s-char.closing-dquote-pos (b* (((mv acl2::?erp ?schars ?closing-dquote-pos ?new-pstate) (lex-*-s-char pstate))) (positionp closing-dquote-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-*-s-char.new-pstate (b* (((mv acl2::?erp ?schars ?closing-dquote-pos ?new-pstate) (lex-*-s-char pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-*-s-char-uncond (b* (((mv acl2::?erp ?schars ?closing-dquote-pos ?new-pstate) (lex-*-s-char pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-*-s-char-cond (b* (((mv acl2::?erp ?schars ?closing-dquote-pos ?new-pstate) (lex-*-s-char pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (- (parsize pstate) (len schars)))))) :rule-classes :linear)