		Search-engine friendly clone of the ACL2 documentation.

Parser

Lex-rest-of-block-comment-fns

Mutually recursive part of block comment lexing.

Definitions and Theorems

Function: lex-rest-of-block-comment

(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 (nat-list-fix input))))
   (mv (abnf::make-tree-nonleaf
            :rulename? (abnf::rulename "rest-of-block-comment")
            :branches trees)
       input-after-trees))))

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

(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 (nat-list-fix input))))
   (mv
    (abnf::make-tree-nonleaf
      :rulename? (abnf::rulename "rest-of-block-comment-after-star")
      :branches trees)
    input-after-trees))))

Theorem: return-type-of-lex-rest-of-block-comment.tree

(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: return-type-of-lex-rest-of-block-comment.rest-input

(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: return-type-of-lex-rest-of-block-comment-after-star.tree

(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: return-type-of-lex-rest-of-block-comment-after-star.rest-input

(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: len-of-input-after-rest-of-block-comment-<=

(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: len-of-input-after-rest-of-block-comment-after-star-<=

(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: len-of-input-after-rest-of-block-comment-<

(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: len-of-input-after-rest-of-block-comment-after-star-<

(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)

Subtopics

Lex-rest-of-block-comment-after-star: Lex rule rest-of-block-comment-after-star.
Lex-rest-of-block-comment: Lex rule rest-of-block-comment.