		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-keyword

Attempts to eat the named keyword.

Signature
(parse-keyword keyword tokens) → (mv ast-node tokens-after-keyword-or-reserr)
Arguments: keyword — Guard (stringp keyword).; tokens — Guard (abnf::tree-listp tokens).
Returns: ast-node — Type (statement-optionp ast-node).; tokens-after-keyword-or-reserr — Type (abnf::tree-list-resultp tokens-after-keyword-or-reserr).

Returns two values: an optional statement AST node and either the list of remaining tokens or a reserr.

If a keyword is found, and if it is leave, break, or continue, then the appropriate statement is built and returned as the first value. If a different keyword is found, the first value returned is NIL, since no other Yul AST node has surface syntax consisting solely of a single keyword. In either case, the second value returns is the list of remaining tokens after eating the keyword token.

If no keyword is found, the first value returned is NIL and the second is a reserr.

In this context, keyword is a nonterminal in the ABNF grammar for Yul, and its alternatives are terminals (aka terminal symbols) that are the actual keywords. See grammar.abnf.

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

Definitions and Theorems

Function: parse-keyword

(defun parse-keyword (keyword tokens)
 (declare (xargs :guard (and (stringp keyword)
                             (abnf::tree-listp tokens))))
 (let ((__function__ 'parse-keyword))
  (declare (ignorable __function__))
  (if
   (not (member-equal keyword *yul-keywords*))
   (prog2$
    (er
     hard? 'top-level
     (string-append
         "parse-keyword called on something not in *yul-keywords*: "
         keyword))
    (mv nil
        (reserrf (cons "program logic error" tokens))))
   (b*
    (((when (endp tokens))
      (mv
       nil
       (reserrf
        (cons
             (string-append
                  "ran out of tokens when trying to parse keyword: "
                  keyword)
             tokens))))
     (putative-keyword-tree (first tokens))
     ((unless
       (and
        (abnf::tree-case putative-keyword-tree :nonleaf)
        (equal (abnf::tree-nonleaf->rulename? putative-keyword-tree)
               (abnf::rulename "keyword"))))
      (mv nil
          (reserrf (cons "token is not a keyword" tokens))))
     (branches (abnf::tree-nonleaf->branches putative-keyword-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
         "keyword token seems to have the wrong structure for keyword:"
         keyword))
       (mv nil
           (reserrf (cons "cst structure error" tokens)))))
     (leafterm-nats (abnf::tree-leafterm->get (caar branches)))
     ((unless (unsigned-byte-listp 8 leafterm-nats))
      (prog2$
       (er
        hard? 'top-level
        (string-append
           "unexpected type of leafterm nats when parsing keyword: "
           keyword))
       (mv nil
           (reserrf (cons "cst structure error 2" tokens)))))
     (terminal-keyword (nats=>string leafterm-nats))
     ((unless (equal keyword terminal-keyword))
      (mv
        nil
        (reserrf
             (cons (concatenate 'string
                                "looking for keyword: '"
                                keyword "', but received keyword: '"
                                terminal-keyword "'")
                   tokens)))))
    (mv (cond ((equal keyword "leave")
               (make-statement-leave))
              ((equal keyword "break")
               (make-statement-break))
              ((equal keyword "continue")
               (make-statement-continue))
              (t nil))
        (abnf::tree-list-fix (rest tokens)))))))

Theorem: statement-optionp-of-parse-keyword.ast-node

(defthm statement-optionp-of-parse-keyword.ast-node
  (b* (((mv ?ast-node
            ?tokens-after-keyword-or-reserr)
        (parse-keyword keyword tokens)))
    (statement-optionp ast-node))
  :rule-classes :rewrite)

Theorem: tree-list-resultp-of-parse-keyword.tokens-after-keyword-or-reserr

(defthm
  tree-list-resultp-of-parse-keyword.tokens-after-keyword-or-reserr
  (b* (((mv ?ast-node
            ?tokens-after-keyword-or-reserr)
        (parse-keyword keyword tokens)))
    (abnf::tree-list-resultp tokens-after-keyword-or-reserr))
  :rule-classes :rewrite)

Theorem: len-of-parse-keyword-<

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