		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-line-comment

Lex a line comment during preprocessing.

Signature
(plex-line-comment first-pos ppstate) → (mv erp lexeme span new-ppstate)
Arguments: 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-line-comment, but it operates on preprocessor states instead of parser states, and it returns the content of the comment as part of the lexeme.

Collecting the content of the comment, i.e. the characters between // and new line (excluding both), requires some additional code here.

Definitions and Theorems

Function: plex-line-comment-loop

(defun plex-line-comment-loop (first-pos ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (positionp first-pos)
                             (ppstatep ppstate))))
 (let ((__function__ 'plex-line-comment-loop))
  (declare (ignorable __function__))
  (b* (((reterr)
        nil (irr-position)
        (irr-newline)
        ppstate)
       ((erp char pos ppstate)
        (pread-char ppstate)))
   (cond
    ((not char)
     (reterr-msg
      :where (position-to-msg pos)
      :expected "a character"
      :found (char-to-msg char)
      :extra
      (msg
       "The line comment starting at ~@1 ~
                                  never ends."
       (position-to-msg first-pos))))
    ((utf8-= char 10)
     (retok nil pos (newline-lf) ppstate))
    ((utf8-= char 13)
     (b* (((erp char2 pos2 ppstate)
           (pread-char ppstate)))
       (cond ((not char2)
              (retok nil pos (newline-cr) ppstate))
             ((utf8-= char2 10)
              (retok nil pos2 (newline-crlf) ppstate))
             (t (b* ((ppstate (punread-char ppstate)))
                  (retok nil pos (newline-lf)
                         ppstate))))))
    (t (b* (((erp content last-pos newline ppstate)
             (plex-line-comment-loop first-pos ppstate)))
         (retok (cons char content)
                last-pos newline ppstate)))))))

Theorem: nat-listp-of-plex-line-comment-loop.content

(defthm nat-listp-of-plex-line-comment-loop.content
  (b* (((mv acl2::?erp ?content
            ?last-pos ?newline ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (nat-listp content))
  :rule-classes :rewrite)

Theorem: positionp-of-plex-line-comment-loop.last-pos

(defthm positionp-of-plex-line-comment-loop.last-pos
  (b* (((mv acl2::?erp ?content
            ?last-pos ?newline ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: newlinep-of-plex-line-comment-loop.newline

(defthm newlinep-of-plex-line-comment-loop.newline
  (b* (((mv acl2::?erp ?content
            ?last-pos ?newline ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (newlinep newline))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-line-comment-loop.new-ppstate

(defthm ppstatep-of-plex-line-comment-loop.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?content
                     ?last-pos ?newline ?new-ppstate)
                 (plex-line-comment-loop first-pos ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-line-comment-loop-uncond

(defthm ppstate->size-of-plex-line-comment-loop-uncond
  (b* (((mv acl2::?erp ?content
            ?last-pos ?newline ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-line-comment-loop-cond

(defthm ppstate->size-of-plex-line-comment-loop-cond
  (b* (((mv acl2::?erp ?content
            ?last-pos ?newline ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)

Function: plex-line-comment

(defun plex-line-comment (first-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (positionp first-pos)
                              (ppstatep ppstate))))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp content last-pos newline ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (retok (make-plexeme-line-comment :content content
                                      :newline newline)
           (make-span :start first-pos
                      :end last-pos)
           ppstate)))

Theorem: plexemep-of-plex-line-comment.lexeme

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

Theorem: spanp-of-plex-line-comment.span

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

Theorem: ppstatep-of-plex-line-comment.new-ppstate

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

Theorem: ppstate->size-of-plex-line-comment-uncond

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

Theorem: ppstate->size-of-plex-line-comment-cond

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