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)