Lex a character constant.
(lex-cconst 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-cconst (cprefix? first-pos pstate) (declare (xargs :guard (and (cprefix-optionp cprefix?) (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-cconst)) (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-cconst.lexeme (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-cconst cprefix? first-pos pstate))) (lexemep lexeme)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-lex-cconst.span (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-cconst cprefix? first-pos pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-cconst.new-pstate (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-cconst cprefix? first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-cconst-uncond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-cconst cprefix? first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-cconst-cond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-cconst cprefix? first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)