		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 newline (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) 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 ppstate))
    ((utf8-= char 13)
     (b* (((erp char2 pos2 ppstate)
           (pread-char ppstate)))
       (cond ((not char2) (retok nil pos ppstate))
             ((utf8-= char2 10)
              (retok nil pos2 ppstate))
             (t (b* ((ppstate (punread-char ppstate)))
                  (retok nil pos ppstate))))))
    (t (b* (((erp content last-pos ppstate)
             (plex-line-comment-loop first-pos ppstate)))
         (retok (cons char content)
                last-pos 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 ?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 ?new-ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (positionp last-pos))
  :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 ?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 ?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 ?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 ppstate)
        (plex-line-comment-loop first-pos ppstate)))
    (retok (plexeme-line-comment content)
           (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)