		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-fragment-to-cst+

Parse source string for a supported grammar rule name.

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

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

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

Since ACL2 strings are sequences of characters with codes from 0 to 255, source-code, when converted to codes, is required to be valid UTF-8.

As a second value, returns the full list of lexemes, including comments and whitespace. If the first value is an error, the second value is undefined.

Definitions and Theorems

Function: parse-fragment-to-cst+

(defun parse-fragment-to-cst+ (rule-name source-code)
  (declare (xargs :guard (and (stringp rule-name)
                              (stringp source-code))))
  (let ((__function__ 'parse-fragment-to-cst+))
    (declare (ignorable __function__))
    (b* ((lexemes-or-err (lexemize-leo-from-string source-code)))
      (lexemes-to-cst+ rule-name lexemes-or-err))))

Theorem: tree-resultp-of-parse-fragment-to-cst+.tree

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

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

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