Lex a character constant.
(lex-character-constant cprefix? first-pos pstate) → (mv erp lexeme span new-pstate)
This is called when we expect a character constant, after the opening single quote, and the prefix before that if present, have already been read. So we read zero or more characters and escape sequences, and ensure that there is at least one (according to the grammar). In the process of reading those characters and escape sequences, we read up to the closing single quote (see lex-*-c-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-character-constant (cprefix? first-pos pstate) (declare (xargs :guard (and (cprefix-optionp cprefix?) (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-character-constant)) (declare (ignorable __function__)) (b* (((reterr) (irr-lexeme) (irr-span) (irr-parstate)) ((erp cchars closing-squote-pos pstate) (lex-*-c-char pstate)) (span (make-span :start first-pos :end closing-squote-pos)) ((unless cchars) (reterr-msg :where (position-to-msg closing-squote-pos) :expected "one or more characters and escape sequences" :found "none"))) (retok (lexeme-token (token-const (const-char (cconst cprefix? cchars)))) span pstate))))
Theorem:
(defthm lexemep-of-lex-character-constant.lexeme (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-character-constant cprefix? first-pos pstate))) (lexemep lexeme)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-lex-character-constant.span (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-character-constant cprefix? first-pos pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-character-constant.new-pstate (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-character-constant cprefix? first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-character-constant-uncond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-character-constant cprefix? first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-character-constant-cond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-character-constant cprefix? first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)