		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-string-literal

Lex a string literal during preprocessing.

Signature
(plex-string-literal eprefix? first-pos ppstate) → (mv erp lexeme span new-ppstate)
Arguments: eprefix? — Guard (eprefix-optionp eprefix?).; 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-string-literal, but it operates on preprocessor states instead of parser states.

Definitions and Theorems

Function: plex-string-literal

(defun plex-string-literal (eprefix? first-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (eprefix-optionp eprefix?)
                              (positionp first-pos)
                              (ppstatep ppstate))))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp schars closing-dquote-pos ppstate)
        (plex-*-s-char ppstate))
       (span (make-span :start first-pos
                        :end closing-dquote-pos)))
    (retok (plexeme-string (stringlit eprefix? schars))
           span ppstate)))

Theorem: plexemep-of-plex-string-literal.lexeme

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

Theorem: spanp-of-plex-string-literal.span

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

Theorem: ppstatep-of-plex-string-literal.new-ppstate

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

Theorem: ppstate->size-of-plex-string-literal-uncond

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

Theorem: ppstate->size-of-plex-string-literal-cond

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