		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-symbol

Parse a specified symbol.

Signature
(parse-symbol symbol token input) → (mv tree next-token rest-input)
Arguments: symbol — Guard (stringp symbol).; 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).

This is used to check the presence of an expected symbol.

For more details see parse-symbol-among.

Definitions and Theorems

Function: parse-symbol

(defun parse-symbol (symbol token input)
  (declare (xargs :guard (and (stringp symbol)
                              (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (declare (xargs :guard (member-equal symbol *symbols*)))
  (let ((__function__ 'parse-symbol))
    (declare (ignorable __function__))
    (parse-symbol-among (list symbol)
                        token input)))

Theorem: tree-resultp-of-parse-symbol.tree

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

Theorem: tree-optionp-of-parse-symbol.next-token

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

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

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

Theorem: parsize-of-parse-symbol-<=

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

Theorem: parsize-of-parse-symbol-<

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

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

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

Theorem: len-of-parse-symbol-<

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

Theorem: parse-symbol-of-str-fix-symbol

(defthm parse-symbol-of-str-fix-symbol
  (equal (parse-symbol (str-fix symbol)
                       token input)
         (parse-symbol symbol token input)))

Theorem: parse-symbol-streqv-congruence-on-symbol

(defthm parse-symbol-streqv-congruence-on-symbol
  (implies (acl2::streqv symbol symbol-equiv)
           (equal (parse-symbol symbol token input)
                  (parse-symbol symbol-equiv token input)))
  :rule-classes :congruence)

Theorem: parse-symbol-of-tree-option-fix-token

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

Theorem: parse-symbol-tree-option-equiv-congruence-on-token

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

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

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

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

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