		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-character-constant

Lex a character constant during preprocessing.

Signature
(plex-character-constant cprefix? first-pos ppstate) → (mv erp lexeme span new-ppstate)
Arguments: cprefix? — Guard (cprefix-optionp cprefix?).; first-pos — Guard (positionp first-pos).; ppstate — Guard (ppstatep ppstate).
Returns: lexeme — Type (plexemep lexeme).; span — Type (spanp span).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is the same as lex-character-constant, but it operates on preprocessor states instead of parser states.

Definitions and Theorems

Function: plex-character-constant

(defun plex-character-constant (cprefix? first-pos ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (cprefix-optionp cprefix?)
                             (positionp first-pos)
                             (ppstatep ppstate))))
 (let ((__function__ 'plex-character-constant))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp cchars closing-squote-pos ppstate)
        (plex-*-c-char ppstate))
       (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 (plexeme-char (cconst cprefix? cchars))
           span ppstate))))

Theorem: plexemep-of-plex-character-constant.lexeme

(defthm plexemep-of-plex-character-constant.lexeme
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-character-constant cprefix? first-pos ppstate)))
    (plexemep lexeme))
  :rule-classes :rewrite)

Theorem: spanp-of-plex-character-constant.span

(defthm spanp-of-plex-character-constant.span
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-character-constant cprefix? first-pos ppstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-character-constant.new-ppstate

(defthm ppstatep-of-plex-character-constant.new-ppstate
  (implies
       (ppstatep ppstate)
       (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
             (plex-character-constant cprefix? first-pos ppstate)))
         (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-character-constant-uncond

(defthm ppstate->size-of-plex-character-constant-uncond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-character-constant cprefix? first-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-character-constant-cond

(defthm ppstate->size-of-plex-character-constant-cond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-character-constant cprefix? first-pos ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)