		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-block-comment

Lex a block comment during preprocessing.

Signature
(plex-block-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-block-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 */ (excluding both), requires some additional code here. Note that plex-rest-of-block-comment-after-star is always called just after a * has been read; the addition of that * to the content is deferred until it is established that the * is not part of the closing */; see the comments interspersed with the code.

Definitions and Theorems

Function: plex-rest-of-block-comment

(defun plex-rest-of-block-comment (first-pos ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (positionp first-pos)
                             (ppstatep ppstate))))
 (let ((__function__ 'plex-rest-of-block-comment))
  (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 block comment starting at ~@1 ~
                                    never ends."
       (position-to-msg first-pos))))
    ((utf8-= char (char-code #\*))
     (plex-rest-of-block-comment-after-star first-pos ppstate))
    (t (b* (((erp content last-pos ppstate)
             (plex-rest-of-block-comment first-pos ppstate)))
         (retok (cons char content)
                last-pos ppstate)))))))

Function: plex-rest-of-block-comment-after-star

(defun plex-rest-of-block-comment-after-star (first-pos ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (positionp first-pos)
                             (ppstatep ppstate))))
 (let ((__function__ 'plex-rest-of-block-comment-after-star))
  (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 block comment starting at ~@1 ~
                                    never ends."
       (position-to-msg first-pos))))
    ((utf8-= char (char-code #\/))
     (retok nil pos ppstate))
    ((utf8-= char (char-code #\*))
     (b*
      (((erp content last-pos ppstate)
        (plex-rest-of-block-comment-after-star first-pos ppstate)))
      (retok (cons (char-code #\*) content)
             last-pos ppstate)))
    (t (b* (((erp content last-pos ppstate)
             (plex-rest-of-block-comment first-pos ppstate)))
         (retok (list* (char-code #\*) char content)
                last-pos ppstate)))))))

Theorem: return-type-of-plex-rest-of-block-comment.content

(defthm return-type-of-plex-rest-of-block-comment.content
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment first-pos ppstate)))
    (nat-listp content))
  :rule-classes :rewrite)

Theorem: return-type-of-plex-rest-of-block-comment.last-pos

(defthm return-type-of-plex-rest-of-block-comment.last-pos
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment first-pos ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: return-type-of-plex-rest-of-block-comment.new-ppstate

(defthm return-type-of-plex-rest-of-block-comment.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp
                     ?content ?last-pos ?new-ppstate)
                 (plex-rest-of-block-comment first-pos ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: return-type-of-plex-rest-of-block-comment-after-star.content

(defthm return-type-of-plex-rest-of-block-comment-after-star.content
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment-after-star first-pos ppstate)))
    (nat-listp content))
  :rule-classes :rewrite)

Theorem: return-type-of-plex-rest-of-block-comment-after-star.last-pos

(defthm
      return-type-of-plex-rest-of-block-comment-after-star.last-pos
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment-after-star first-pos ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: return-type-of-plex-rest-of-block-comment-after-star.new-ppstate

(defthm
   return-type-of-plex-rest-of-block-comment-after-star.new-ppstate
 (implies
   (ppstatep ppstate)
   (b* (((mv acl2::?erp
             ?content ?last-pos ?new-ppstate)
         (plex-rest-of-block-comment-after-star first-pos ppstate)))
     (ppstatep new-ppstate)))
 :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-rest-of-block-comment-uncond

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

Theorem: ppstate->size-of-plex-resto-of-block-comment-after-star-uncond

(defthm
     ppstate->size-of-plex-resto-of-block-comment-after-star-uncond
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment-after-star first-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-plex-rest-of-block-comment-cond

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

Theorem: ppstate->size-of-plex-resto-of-block-comment-after-star-cond

(defthm ppstate->size-of-plex-resto-of-block-comment-after-star-cond
  (b* (((mv acl2::?erp
            ?content ?last-pos ?new-ppstate)
        (plex-rest-of-block-comment-after-star first-pos ppstate)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)

Function: plex-block-comment

(defun plex-block-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-rest-of-block-comment first-pos ppstate)))
    (retok (plexeme-block-comment content)
           (make-span :start first-pos
                      :end last-pos)
           ppstate)))

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

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

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

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

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

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

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

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

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

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