		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) → tree
Arguments: rule-name — Guard (stringp rule-name).; source-code — Guard (stringp source-code).
Returns: tree — Type (abnf::tree-resultp tree).

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.

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* (((mv cst ?lexemes)
          (parse-fragment-to-cst+ rule-name source-code)))
      cst)))

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

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