		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-identifier

Attempts to eat an identifier token and build an identifier AST node.

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

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

If an identifier token is found, the first value returned is an identifier AST node with the full token leaf text.

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

Definitions and Theorems

Function: parse-identifier

(defun parse-identifier (tokens)
 (declare (xargs :guard (abnf::tree-listp tokens)))
 (let ((__function__ 'parse-identifier))
  (declare (ignorable __function__))
  (b*
   (((when (endp tokens))
     (mv
      nil
      (reserrf
           (cons "ran out of tokens when trying to parse identifier"
                 tokens))))
    (putative-identifier-tree (first tokens))
    ((unless
      (and
       (abnf::tree-case putative-identifier-tree :nonleaf)
       (equal
            (abnf::tree-nonleaf->rulename? putative-identifier-tree)
            (abnf::rulename "identifier"))))
     (mv nil
         (reserrf (cons "token is not an identifier" tokens)))))
   (b*
    ((fringe (abnf::tree->string (first tokens)))
     ((unless (unsigned-byte-listp 8 fringe))
      (prog2$
       (er
         hard? 'top-level
         "unexpected type of leafterm nats when parsing identifier")
       (mv nil
           (reserrf (cons "cst structure error" tokens))))))
    (mv (make-identifier :get (nats=>string fringe))
        (abnf::tree-list-fix (rest tokens)))))))

Theorem: identifier-optionp-of-parse-identifier.ast-node

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

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

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

Theorem: len-of-parse-identifier-<

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