Lex a string literal.
(lex-stringlit eprefix? first-pos pstate) → (mv erp lexeme span new-pstate)
This is called when we expect a string literal, after the opening double quote, and the prefix before that if present, have already been read. We read zero or more characters and escape sequences. In the process of reading those characters and escape sequences, we read up to the closing double quote (see lex-*-s-char), whose position we use as the ending one of the span we return. The starting position of the span is passed to this function as input.
Function:
(defun lex-stringlit (eprefix? first-pos pstate) (declare (xargs :guard (and (eprefix-optionp eprefix?) (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-stringlit)) (declare (ignorable __function__)) (b* (((reterr) (irr-lexeme) (irr-span) (irr-parstate)) ((erp schars closing-dquote-pos pstate) (lex-*-s-char pstate)) (span (make-span :start first-pos :end closing-dquote-pos))) (retok (lexeme-token (token-string (stringlit eprefix? schars))) span pstate))))
Theorem:
(defthm lexemep-of-lex-stringlit.lexeme (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-stringlit eprefix? first-pos pstate))) (lexemep lexeme)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-lex-stringlit.span (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-stringlit eprefix? first-pos pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-stringlit.new-pstate (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-stringlit eprefix? first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-stringlit-uncond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-stringlit eprefix? first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-stringlit-cond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-stringlit eprefix? first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)