		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Lexemes-to-cst+

Tokenize and parse list of lexemes for a supported grammar rule name.

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

Supported grammar rule names are file, statement, expression, and token.

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

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

Definitions and Theorems

Function: lexemes-to-cst+

(defun lexemes-to-cst+ (rule-name lexemes)
  (declare (xargs :guard (and (stringp rule-name)
                              (abnf::tree-list-resultp lexemes))))
  (let ((__function__ 'lexemes-to-cst+))
    (declare (ignorable __function__))
    (b* (((when (reserrp lexemes))
          (mv (reserrf (cons :lexing-failed lexemes))
              nil))
         (lexemes (abnf::tree-list-fix lexemes))
         (tokens (filter-and-lower-tokens lexemes))
         ((when (reserrp tokens))
          (mv (reserrf (cons :tokenizing-failed tokens))
              lexemes))
         (cst (tokens-to-cst rule-name tokens)))
      (mv cst lexemes))))

Theorem: tree-resultp-of-lexemes-to-cst+.tree

(defthm tree-resultp-of-lexemes-to-cst+.tree
  (b* (((mv ?tree ?lexemes)
        (lexemes-to-cst+ rule-name lexemes)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-listp-of-lexemes-to-cst+.lexemes

(defthm tree-listp-of-lexemes-to-cst+.lexemes
  (b* (((mv ?tree ?lexemes)
        (lexemes-to-cst+ rule-name lexemes)))
    (abnf::tree-listp lexemes))
  :rule-classes :rewrite)