		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-token

Parse a token.

Signature
(parse-token input) → (mv tree? rest-input)
Arguments: input — Guard (abnf::tree-listp input).
Returns: tree? — Type (abnf::tree-optionp tree?).; rest-input — Type (abnf::tree-listp rest-input).

This is used to obtain the next token in the input, if any.

Definitions and Theorems

Function: parse-token

(defun parse-token (input)
  (declare (xargs :guard (abnf::tree-listp input)))
  (let ((__function__ 'parse-token))
    (declare (ignorable __function__))
    (b* (((when (atom input)) (mv nil nil))
         (input (abnf::tree-list-fix input)))
      (mv (car input) (cdr input)))))

Theorem: tree-optionp-of-parse-token.tree?

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

Theorem: tree-listp-of-parse-token.rest-input

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

Theorem: len-of-parse-token-<=

(defthm len-of-parse-token-<=
  (b* (((mv ?tree? ?rest-input)
        (parse-token input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-parse-token-<

(defthm len-of-parse-token-<
  (b* (((mv ?tree? ?rest-input)
        (parse-token input)))
    (implies tree? (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: parse-token-of-tree-list-fix-input

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

Theorem: parse-token-tree-list-equiv-congruence-on-input

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