		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-struct-component-declarations

Parse a struct-component-declarations.

Signature
(parse-struct-component-declarations token input) → (mv tree next-token rest-input)
Arguments: token — Guard (abnf::tree-optionp token).; input — Guard (abnf::tree-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

Definitions and Theorems

Function: parse-struct-component-declarations

(defun parse-struct-component-declarations (token input)
 (declare (xargs :guard (and (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (let ((__function__ 'parse-struct-component-declarations))
  (declare (ignorable __function__))
  (b* (((pok< tree)
        (parse-struct-component-declaration token input))
       ((pok trees)
        (parse-*-comma-struct-component-declaration token input)))
   (if
    (token-stringp "," token)
    (b* (((pok ctree)
          (parse-symbol "," token input)))
     (mv
      (abnf::make-tree-nonleaf
       :rulename? (abnf::rulename "struct-component-declarations")
       :branches
       (list
        (list tree)
        trees
        (list
          (abnf::make-tree-nonleaf :rulename? nil
                                   :branches (list (list ctree))))))
      token input))
    (mv
     (abnf::make-tree-nonleaf
         :rulename? (abnf::rulename "struct-component-declarations")
         :branches
         (list (list tree)
               trees
               (list (abnf::make-tree-nonleaf :rulename? nil
                                              :branches nil))))
     token input)))))

Theorem: tree-resultp-of-parse-struct-component-declarations.tree

(defthm tree-resultp-of-parse-struct-component-declarations.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-struct-component-declarations token input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-struct-component-declarations.next-token

(defthm
     tree-optionp-of-parse-struct-component-declarations.next-token
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-struct-component-declarations token input)))
    (abnf::tree-optionp next-token))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-struct-component-declarations.rest-input

(defthm tree-listp-of-parse-struct-component-declarations.rest-input
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-struct-component-declarations token input)))
    (abnf::tree-listp rest-input))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-struct-component-declarations-<=

(defthm parsize-of-parse-struct-component-declarations-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-struct-component-declarations token input)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parsize-of-parse-struct-component-declarations-<

(defthm parsize-of-parse-struct-component-declarations-<
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-struct-component-declarations token input)))
    (implies (not (reserrp tree))
             (< (parsize next-token rest-input)
                (parsize token input))))
  :rule-classes :linear)

Theorem: parse-struct-component-declarations-of-tree-option-fix-token

(defthm parse-struct-component-declarations-of-tree-option-fix-token
 (equal
  (parse-struct-component-declarations (abnf::tree-option-fix token)
                                       input)
  (parse-struct-component-declarations token input)))

Theorem: parse-struct-component-declarations-tree-option-equiv-congruence-on-token

(defthm
 parse-struct-component-declarations-tree-option-equiv-congruence-on-token
 (implies
    (abnf::tree-option-equiv token token-equiv)
    (equal (parse-struct-component-declarations token input)
           (parse-struct-component-declarations token-equiv input)))
 :rule-classes :congruence)

Theorem: parse-struct-component-declarations-of-tree-list-fix-input

(defthm parse-struct-component-declarations-of-tree-list-fix-input
  (equal (parse-struct-component-declarations
              token (abnf::tree-list-fix input))
         (parse-struct-component-declarations token input)))

Theorem: parse-struct-component-declarations-tree-list-equiv-congruence-on-input

(defthm
 parse-struct-component-declarations-tree-list-equiv-congruence-on-input
 (implies
    (abnf::tree-list-equiv input input-equiv)
    (equal (parse-struct-component-declarations token input)
           (parse-struct-component-declarations token input-equiv)))
 :rule-classes :congruence)