		Search-engine friendly clone of the ACL2 documentation.

Parser-abstractor-interface

Ast-from-string

Parse UTF-8 ACL2 string and abstract to a Leo file AST.

Signature
(ast-from-string leo-string) → tree
Arguments: leo-string — Guard (stringp leo-string).
Returns: tree — Type (file-resultp tree).

Lexes, tokenizes, parses, and abstracts a Leo source file expressed as a string of acl2 characters whose char-codes are UTF-8 bytes. Returns a file abstract syntax tree (AST).

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: ast-from-string

(defun ast-from-string (leo-string)
  (declare (xargs :guard (stringp leo-string)))
  (let ((__function__ 'ast-from-string))
    (declare (ignorable __function__))
    (b* ((file-cst (parse-from-string leo-string))
         ((when (reserrp file-cst)) file-cst))
      (abs-file file-cst))))

Theorem: file-resultp-of-ast-from-string

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