		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-from-string+

Parse UTF-8 ACL2 string into a CST.

Signature
(parse-from-string+ leo-string) → (mv tree lexemes)
Arguments: leo-string — Guard (stringp leo-string).
Returns: tree — Type (abnf::tree-resultp tree).; lexemes — Type (abnf::tree-listp lexemes).

Lexes, tokenizes, and parses a Leo source file expressed as a string of ACL2 characters whose char-codes are UTF-8 bytes. Returns a file CST, and the full list of lexemes, including comments and whitespace.

If any step fails, returns a reserr. The parse consumes the entire string or a reserr is returned.

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

Definitions and Theorems

Function: parse-from-string+

(defun parse-from-string+ (leo-string)
  (declare (xargs :guard (stringp leo-string)))
  (let ((__function__ 'parse-from-string+))
    (declare (ignorable __function__))
    (b* ((lexemes-or-err (lexemize-leo-from-string leo-string)))
      (lexemes-to-cst+ "file" lexemes-or-err))))

Theorem: tree-resultp-of-parse-from-string+.tree

(defthm tree-resultp-of-parse-from-string+.tree
  (b* (((mv ?tree ?lexemes)
        (parse-from-string+ leo-string)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-from-string+.lexemes

(defthm tree-listp-of-parse-from-string+.lexemes
  (b* (((mv ?tree ?lexemes)
        (parse-from-string+ leo-string)))
    (abnf::tree-listp lexemes))
  :rule-classes :rewrite)