		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-symbol

Attempts to eat the named symbol, returning either the list of remaining tokens or a reserr.

Signature
(parse-symbol symbol tokens) → tokens-after-symbol-or-reserr
Arguments: symbol — Guard (stringp symbol).; tokens — Guard (abnf::tree-listp tokens).
Returns: tokens-after-symbol-or-reserr — Type (abnf::tree-list-resultp tokens-after-symbol-or-reserr).

parse-symbol does not build any AST on its own, since there is no Yul AST node class whose surface syntax can consist solely of a single symbol.

In this context, symbol is a nonterminal in the ABNF grammar for Yul, and its alternatives are terminal symbols. See grammar-new.abnf.

Parsing a symbol as a concrete syntax tree means we look for a nonleaf tree where the rulename is "symbol" and the leafterm has the bytes (ASCII codes) of the terminal symbol's string.

Definitions and Theorems

Function: parse-symbol

(defun parse-symbol (symbol tokens)
 (declare (xargs :guard (and (stringp symbol)
                             (abnf::tree-listp tokens))))
 (let ((__function__ 'parse-symbol))
  (declare (ignorable __function__))
  (if
   (not (member-equal symbol *yul-symbols*))
   (prog2$
    (er
      hard? 'top-level
      (string-append
           "parse-symbol called on something not in *yul-symbols*: "
           symbol))
    (reserrf (cons "program logic error" tokens)))
   (b*
    (((when (endp tokens))
      (reserrf
        (cons (string-append
                   "ran out of tokens when trying to parse symbol: "
                   symbol)
              tokens)))
     (putative-symbol-tree (first tokens))
     ((unless
       (and
         (abnf::tree-case putative-symbol-tree :nonleaf)
         (equal (abnf::tree-nonleaf->rulename? putative-symbol-tree)
                (abnf::rulename "symbol"))))
      (reserrf (cons "token is not a symbol" tokens)))
     (branches (abnf::tree-nonleaf->branches putative-symbol-tree))
     ((unless (and (listp branches)
                   (equal (len branches) 1)
                   (listp (car branches))
                   (equal (len (car branches)) 1)
                   (abnf::treep (caar branches))
                   (abnf::tree-case (caar branches)
                                    :leafterm)))
      (prog2$
       (er
        hard? 'top-level
        (string-append
         "symbol token seems to have the wrong structure for symbol:"
         symbol))
       (reserrf (cons "cst structure error" tokens))))
     (leafterm-nats (abnf::tree-leafterm->get (caar branches)))
     ((unless (acl2::unsigned-byte-listp 8 leafterm-nats))
      (prog2$
       (er
        hard? 'top-level
        (string-append
            "unexpected type of leafterm nats when parsing symbol: "
            symbol))
       (reserrf (cons "cst structure error 2" tokens))))
     (terminal-symbol (acl2::nats=>string leafterm-nats))
     ((unless (equal symbol terminal-symbol))
      (reserrf (cons (concatenate 'string
                                  "looking for symbol: '"
                                  symbol "', but received symbol: '"
                                  terminal-symbol "'")
                     tokens))))
    (abnf::tree-list-fix (rest tokens))))))

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

(defthm tree-list-resultp-of-parse-symbol
  (b* ((tokens-after-symbol-or-reserr (parse-symbol symbol tokens)))
    (abnf::tree-list-resultp tokens-after-symbol-or-reserr))
  :rule-classes :rewrite)

Theorem: len-of-parse-symbol-<

(defthm len-of-parse-symbol-<
 (b* ((?tokens-after-symbol-or-reserr (parse-symbol symbol tokens)))
   (implies (not (reserrp tokens-after-symbol-or-reserr))
            (< (len tokens-after-symbol-or-reserr)
               (len tokens))))
 :rule-classes :linear)