Mutually recursive part of block comment lexing.
Function:
(defun lex-rest-of-block-comment (input) (declare (xargs :guard (nat-listp input))) (let ((__function__ 'lex-rest-of-block-comment)) (declare (ignorable __function__)) (b* (((mv trees input-after-trees) (b* (((mv tree-star+rest input-after-star+rest) (b* (((mv tree-star input-after-star) (abnf::parse-ichars "*" input)) ((when (reserrp tree-star)) (mv (reserrf "problem lexing \"*\"") input)) ((mv tree-rest input-after-rest) (lex-rest-of-block-comment-after-star input-after-star)) ((when (reserrp tree-rest)) (mv (reserrf "problem lexing rest-of-block-comment-after-star") input))) (mv (list (list tree-star) (list tree-rest)) input-after-rest))) ((unless (reserrp tree-star+rest)) (mv tree-star+rest input-after-star+rest)) ((mv tree-not-star+rest input-after-not-star+rest) (b* (((mv tree-not-star input-after-not-star) (lex-not-star input)) ((when (reserrp tree-not-star)) (mv (reserrf "problem lexing not-star") input)) ((mv tree-rest input-after-rest) (lex-rest-of-block-comment input-after-not-star)) ((when (reserrp tree-rest)) (mv (reserrf "problem lexing rest-of-block-comment") input))) (mv (list (list tree-not-star) (list tree-rest)) input-after-rest)))) (mv tree-not-star+rest input-after-not-star+rest))) ((when (reserrp trees)) (mv trees (acl2::nat-list-fix input)))) (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "rest-of-block-comment") :branches trees) input-after-trees))))
Function:
(defun lex-rest-of-block-comment-after-star (input) (declare (xargs :guard (nat-listp input))) (let ((__function__ 'lex-rest-of-block-comment-after-star)) (declare (ignorable __function__)) (b* (((mv trees input-after-trees) (b* (((mv tree-slash input-after-slash) (abnf::parse-ichars "/" input)) ((unless (reserrp tree-slash)) (mv (list (list tree-slash)) input-after-slash)) ((mv tree-star+rest input-after-star+rest) (b* (((mv tree-star input-after-star) (abnf::parse-ichars "*" input)) ((when (reserrp tree-star)) (mv (reserrf "problem lexing \"*\"") input)) ((mv tree-rest input-after-rest) (lex-rest-of-block-comment-after-star input-after-star)) ((when (reserrp tree-rest)) (mv (reserrf "problem lexing rest-of-block-comment-after-star") input))) (mv (list (list tree-star) (list tree-rest)) input-after-rest))) ((unless (reserrp tree-star+rest)) (mv tree-star+rest input-after-star+rest)) ((mv tree-not-star-or-slash+rest input-after-not-star-or-slash+rest) (b* (((mv tree-not-star-or-slash input-after-not-star-or-slash) (lex-not-star-or-slash input)) ((when (reserrp tree-not-star-or-slash)) (mv (reserrf "problem lexing not-star-or-slash") input)) ((mv tree-rest input-after-rest) (lex-rest-of-block-comment input-after-not-star-or-slash)) ((when (reserrp tree-rest)) (mv (reserrf "problem lexing rest-of-block-comment") input))) (mv (list (list tree-not-star-or-slash) (list tree-rest)) input-after-rest)))) (mv tree-not-star-or-slash+rest input-after-not-star-or-slash+rest))) ((when (reserrp trees)) (mv trees (acl2::nat-list-fix input)))) (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "rest-of-block-comment-after-star") :branches trees) input-after-trees))))
Theorem:
(defthm return-type-of-lex-rest-of-block-comment.tree (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment input))) (abnf::tree-resultp tree)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment.rest-input (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment-after-star.tree (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment-after-star input))) (abnf::tree-resultp tree)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-lex-rest-of-block-comment-after-star.rest-input (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment-after-star input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-input-after-rest-of-block-comment-<= (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm len-of-input-after-rest-of-block-comment-after-star-<= (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment-after-star input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm len-of-input-after-rest-of-block-comment-< (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment input))) (implies (not (reserrp tree)) (< (len rest-input) (len input)))) :rule-classes :linear)
Theorem:
(defthm len-of-input-after-rest-of-block-comment-after-star-< (b* (((mv ?tree ?rest-input) (lex-rest-of-block-comment-after-star input))) (implies (not (reserrp tree)) (< (len rest-input) (len input)))) :rule-classes :linear)