		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-*-definition

Parse a *definition.

Signature
(parse-*-definition token input) → (mv trees next-token rest-input)
Arguments: token — Guard (abnf::tree-optionp token).; input — Guard (abnf::tree-listp input).
Returns: trees — Type (abnf::tree-list-resultp trees).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

Definitions and Theorems

Function: parse-*-definition

(defun parse-*-definition (token input)
  (declare (xargs :guard (and (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (let ((__function__ 'parse-*-definition))
    (declare (ignorable __function__))
    (b* (((mv tree token-after-definition
              input-after-definition)
          (parse-definition token input))
         ((when (reserrp tree))
          (mv nil (abnf::tree-option-fix token)
              (abnf::tree-list-fix input)))
         ((pok trees)
          (parse-*-definition token-after-definition
                              input-after-definition)))
      (mv (cons tree trees) token input))))

Theorem: tree-list-resultp-of-parse-*-definition.trees

(defthm tree-list-resultp-of-parse-*-definition.trees
  (b* (((mv ?trees ?next-token ?rest-input)
        (parse-*-definition token input)))
    (abnf::tree-list-resultp trees))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-*-definition.next-token

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

Theorem: tree-listp-of-parse-*-definition.rest-input

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

Theorem: parsize-of-parse-*-definition-<=

(defthm parsize-of-parse-*-definition-<=
  (b* (((mv ?trees ?next-token ?rest-input)
        (parse-*-definition token input)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parse-*-definition-of-tree-option-fix-token

(defthm parse-*-definition-of-tree-option-fix-token
  (equal (parse-*-definition (abnf::tree-option-fix token)
                             input)
         (parse-*-definition token input)))

Theorem: parse-*-definition-tree-option-equiv-congruence-on-token

(defthm parse-*-definition-tree-option-equiv-congruence-on-token
  (implies (abnf::tree-option-equiv token token-equiv)
           (equal (parse-*-definition token input)
                  (parse-*-definition token-equiv input)))
  :rule-classes :congruence)

Theorem: parse-*-definition-of-tree-list-fix-input

(defthm parse-*-definition-of-tree-list-fix-input
  (equal (parse-*-definition token (abnf::tree-list-fix input))
         (parse-*-definition token input)))

Theorem: parse-*-definition-tree-list-equiv-congruence-on-input

(defthm parse-*-definition-tree-list-equiv-congruence-on-input
  (implies (abnf::tree-list-equiv input input-equiv)
           (equal (parse-*-definition token input)
                  (parse-*-definition token input-equiv)))
  :rule-classes :congruence)