		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Tokens-to-cst

Parse list of tokens for a supported grammar rule name.

Signature
(tokens-to-cst rule-name tokens) → tree
Arguments: rule-name — Guard (stringp rule-name).; tokens — Guard (abnf::tree-listp tokens).
Returns: tree — Type (abnf::tree-resultp tree).

Supported grammar rule names are file, statement, expression, and token (expressed as strings).

Given a list of tokens resulting from lexing and tokenizing, this function attempts to parse the tokens into a CST for the the given grammar rule name.

In the case of rule-name being "token", the rule names at the top of the trees in the tokens argument are actually the rule names on the right hand side of the rule for token, although that is not checked here.

If the given rule cannot be parsed or if there are tokens left over, then a reserr is returned.

Definitions and Theorems

Function: tokens-to-cst

(defun tokens-to-cst (rule-name tokens)
 (declare (xargs :guard (and (stringp rule-name)
                             (abnf::tree-listp tokens))))
 (let ((__function__ 'tokens-to-cst))
  (declare (ignorable __function__))
  (b*
   (((unless
          (member-equal rule-name
                        '("file" "statement" "expression" "token")))
     (reserrf
          (cons :not-yet-supported-top-level-rule-name rule-name)))
    ((when (and (null tokens)
                (not (equal rule-name "file"))))
     (reserrf (cons :not-enough-tokens rule-name)))
    ((mv cst next-token rest-input)
     (cond
      ((equal rule-name "file")
       (parse-file tokens))
      ((equal rule-name "statement")
       (parse-statement (first tokens)
                        (rest tokens)))
      ((equal rule-name "expression")
       (parse-expression (first tokens)
                         (rest tokens)))
      ((equal rule-name "token")
       (b* (((mv tree? rest-tokens)
             (parse-token tokens))
            ((unless (abnf::treep tree?))
             (mv (reserrf (cons :no-more-tokens tokens))
                 nil nil))
            ((when (null rest-tokens))
             (mv tree? nil nil)))
         (mv tree? (car rest-tokens)
             (cdr rest-tokens))))
      (t
       (mv
        (reserrf
            (cons :not-yet-supported-top-level-rule-name rule-name))
        nil nil))))
    ((when (reserrp cst)) cst)
    ((when (or next-token rest-input))
     (reserrf (list :not-all-tokens-parsed
                    cst next-token rest-input))))
   cst)))

Theorem: tree-resultp-of-tokens-to-cst

(defthm tree-resultp-of-tokens-to-cst
  (b* ((tree (tokens-to-cst rule-name tokens)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)