		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-operator

Parse a specified operator.

Signature
(parse-operator operator token input) → (mv tree next-token rest-input)
Arguments: operator — Guard (stringp operator).; 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 operator. We return it as a leaf tree as the first result, because this is how an operator occurs in the CSTs of the syntactic grammar. In other words, the operator rulename does not appear in any CST returned by the parser.

This is consistent with the fact that the rule for operator does not appear on the right hand side of any rule other than the rule token.

Definitions and Theorems

Function: parse-operator

(defun parse-operator (operator token input)
 (declare (xargs :guard (and (stringp operator)
                             (abnf::tree-optionp token)
                             (abnf::tree-listp input))))
 (declare (xargs :guard (member-equal operator *operators*)))
 (let ((__function__ 'parse-operator))
   (declare (ignorable __function__))
   (b*
     ((tree (check-token-root "operator" token))
      ((when (reserrp tree))
       (perr (reserrf-push tree)))
      ((unless (equal (abnf::tree->string tree)
                      (string=>nats (str-fix operator))))
       (perr (list :required (str-fix operator)
                   :found (abnf::tree-option-fix token))))
      (tree (abnf::tree-leafterm (string=>nats (str-fix operator))))
      ((mv token input) (parse-token input)))
     (mv tree token input))))

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

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

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

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

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

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

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

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

Theorem: parsize-of-parse-operator-<

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

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

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

Theorem: len-of-parse-operator-<

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

Theorem: parse-operator-of-str-fix-operator

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

Theorem: parse-operator-streqv-congruence-on-operator

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

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

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

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

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

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

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

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

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