Lex a block comment.
This is called when we expect a block comment,
after we have read the initial
Following the mutually recursive rules of the grammar,
we have two mutually recursive loop functions,
which scan through the characters
until the end of the comment is reached,
or until the end of file is reached
(in which case it is an error).
In case of success, we retutn a comment lexeme,
which currently contains no information
(but that may change in the future).
The span of the comment is calculated from
the first position (of the
Function:
(defun lex-rest-of-block-comment (first-pos pstate) (declare (xargs :guard (and (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-rest-of-block-comment)) (declare (ignorable __function__)) (b* (((reterr) (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate))) (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)))) ((= char (char-code #\*)) (lex-rest-of-block-comment-after-star first-pos pstate)) (t (lex-rest-of-block-comment first-pos pstate))))))
Function:
(defun lex-rest-of-block-comment-after-star (first-pos pstate) (declare (xargs :guard (and (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-rest-of-block-comment-after-star)) (declare (ignorable __function__)) (b* (((reterr) (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate))) (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)))) ((= char (char-code #\/)) (retok pos pstate)) ((= char (char-code #\*)) (lex-rest-of-block-comment-after-star first-pos pstate)) (t (lex-rest-of-block-comment first-pos pstate))))))
Theorem:
(defthm return-type-of-lex-rest-of-block-comment.last-pos (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment first-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment.new-pstate (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment-after-star.last-pos (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment-after-star first-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment-after-star.new-pstate (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment-after-star first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-rest-of-block-comment-uncond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-resto-of-block-comment-after-star-uncond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment-after-star first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-rest-of-block-comment-cond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-resto-of-block-comment-after-star-cond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-rest-of-block-comment-after-star first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Function:
(defun lex-block-comment (first-pos pstate) (declare (xargs :guard (and (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-block-comment)) (declare (ignorable __function__)) (b* (((reterr) (irr-lexeme) (irr-span) (irr-parstate)) ((erp last-pos pstate) (lex-rest-of-block-comment first-pos pstate))) (retok (lexeme-comment) (make-span :start first-pos :end last-pos) pstate))))
Theorem:
(defthm lexemep-of-lex-block-comment.lexeme (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-block-comment first-pos pstate))) (lexemep lexeme)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-lex-block-comment.span (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-block-comment first-pos pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-block-comment.new-pstate (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-block-comment first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-block-comment-uncond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-block-comment first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-block-comment-cond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-block-comment first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)