Lex a line comment.
This is called when we expect a line comment,
after reading the initial
We read characters in a loop until
either we find a new-line character (success)
or we find end of file (failure).
In case of success, we return
a lexeme that currently contains no information
(but that may change in the future),
and a span calculated from
the position of the first
Function:
(defun lex-line-comment-loop (first-pos pstate) (declare (xargs :guard (and (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-line-comment-loop)) (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 line comment starting at ~@1 ~ never ends." (position-to-msg first-pos)))) ((= char 10) (retok pos pstate)) (t (lex-line-comment-loop first-pos pstate))))))
Theorem:
(defthm positionp-of-lex-line-comment-loop.last-pos (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-line-comment-loop first-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-line-comment-loop.new-pstate (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-line-comment-loop first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-line-comment-loop-uncond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-line-comment-loop first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-line-comment-loop-cond (b* (((mv acl2::?erp ?last-pos ?new-pstate) (lex-line-comment-loop first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Function:
(defun lex-line-comment (first-pos pstate) (declare (xargs :guard (and (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-line-comment)) (declare (ignorable __function__)) (b* (((reterr) (irr-lexeme) (irr-span) (irr-parstate)) ((erp last-pos pstate) (lex-line-comment-loop first-pos pstate))) (retok (lexeme-comment) (make-span :start first-pos :end last-pos) pstate))))
Theorem:
(defthm lexemep-of-lex-line-comment.lexeme (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-line-comment first-pos pstate))) (lexemep lexeme)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-lex-line-comment.span (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-line-comment first-pos pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-line-comment.new-pstate (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-line-comment first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-line-comment-uncond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-line-comment first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-line-comment-cond (b* (((mv acl2::?erp ?lexeme ?span ?new-pstate) (lex-line-comment first-pos pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)