		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) → tree
Arguments: leo-string — Guard (stringp leo-string).
Returns: tree — Type (abnf::tree-resultp tree).

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.

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* (((mv file-cst ?lexemes)
          (parse-from-string+ leo-string)))
      file-cst)))

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

(defthm tree-resultp-of-parse-from-string
  (b* ((tree (parse-from-string leo-string)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)