		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-keyword

Parse a specified keyword.

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

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

This function is used to parse a keyword that appears in the list of tokens. There are other keywords that can appear within atomic-literal tokens, but those have already been assembled into the token by the lexer and will not be seen by this function.

Definitions and Theorems

Function: parse-keyword

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

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

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

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

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

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

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

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

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

Theorem: parsize-of-parse-keyword-<

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

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

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

Theorem: len-of-parse-keyword-<

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

Theorem: parse-keyword-of-str-fix-keyword

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

Theorem: parse-keyword-streqv-congruence-on-keyword

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

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

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

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

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

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

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

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

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