		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-symbol-among

Parse a symbol among the ones in a specified list.

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

As with keywords, this is consistent with the fact that the rule symbol does not appear on the right hand side of any rule other than the rule token.

This function is used to parse a symbol that appears in the list of tokens. There is a small number of other symbols that can appear within identifier or 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-symbol-among-aux

(defun parse-symbol-among-aux (nats strings)
  (declare (xargs :guard (and (nat-listp nats)
                              (string-listp strings))))
  (let ((__function__ 'parse-symbol-among-aux))
    (declare (ignorable __function__))
    (and (consp strings)
         (or (equal (string=>nats (str-fix (car strings)))
                    (nat-list-fix nats))
             (parse-symbol-among-aux nats (cdr strings))))))

Theorem: booleanp-of-parse-symbol-among-aux

(defthm booleanp-of-parse-symbol-among-aux
  (b* ((yes/no (parse-symbol-among-aux nats strings)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: parse-symbol-among-aux-of-nat-list-fix-nats

(defthm parse-symbol-among-aux-of-nat-list-fix-nats
  (equal (parse-symbol-among-aux (nat-list-fix nats)
                                 strings)
         (parse-symbol-among-aux nats strings)))

Theorem: parse-symbol-among-aux-nat-list-equiv-congruence-on-nats

(defthm parse-symbol-among-aux-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (parse-symbol-among-aux nats strings)
                  (parse-symbol-among-aux nats-equiv strings)))
  :rule-classes :congruence)

Theorem: parse-symbol-among-aux-of-string-list-fix-strings

(defthm parse-symbol-among-aux-of-string-list-fix-strings
 (equal (parse-symbol-among-aux nats (str::string-list-fix strings))
        (parse-symbol-among-aux nats strings)))

Theorem: parse-symbol-among-aux-string-list-equiv-congruence-on-strings

(defthm
     parse-symbol-among-aux-string-list-equiv-congruence-on-strings
  (implies (str::string-list-equiv strings strings-equiv)
           (equal (parse-symbol-among-aux nats strings)
                  (parse-symbol-among-aux nats strings-equiv)))
  :rule-classes :congruence)

Function: parse-symbol-among

(defun parse-symbol-among (symbols token input)
  (declare (xargs :guard (and (string-listp symbols)
                              (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (declare (xargs :guard (subsetp-equal symbols *symbols*)))
  (let ((__function__ 'parse-symbol-among))
    (declare (ignorable __function__))
    (b* ((tree (check-token-root "symbol" token))
         ((when (reserrp tree))
          (perr (reserrf-push tree)))
         (fringe (abnf::tree->string tree))
         ((unless (nat-listp fringe))
          (perr :impossible))
         ((unless (parse-symbol-among-aux fringe symbols))
          (perr (list :required
                      :one-of (str::string-list-fix symbols)
                      :found tree)))
         (tree (abnf::tree-leafterm fringe))
         ((mv token input) (parse-token input)))
      (mv tree token input))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: parse-symbol-among-of-string-list-fix-symbols

(defthm parse-symbol-among-of-string-list-fix-symbols
  (equal (parse-symbol-among (str::string-list-fix symbols)
                             token input)
         (parse-symbol-among symbols token input)))

Theorem: parse-symbol-among-string-list-equiv-congruence-on-symbols

(defthm parse-symbol-among-string-list-equiv-congruence-on-symbols
  (implies (str::string-list-equiv symbols symbols-equiv)
           (equal (parse-symbol-among symbols token input)
                  (parse-symbol-among symbols-equiv token input)))
  :rule-classes :congruence)

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

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

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

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

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

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

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

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