		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-from-string-to-cst

Parse UTF-8 ACL2 string into a PFCS system in CST form.

Signature
(parse-from-string-to-cst pfcs-string) → tree
Arguments: pfcs-string — Guard (stringp pfcs-string).
Returns: tree — Type (abnf::tree-resultp tree).

Lexes, tokenizes, and parses a PFCS system expressed as a string of acl2 characters whose char-codes are UTF-8 bytes. Returns a PFCS system CST (concrete syntax tree).

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, pfcs-string, when converted to codes, is required to be valid UTF-8.

Definitions and Theorems

Function: parse-from-string-to-cst

(defun parse-from-string-to-cst (pfcs-string)
  (declare (xargs :guard (stringp pfcs-string)))
  (let ((__function__ 'parse-from-string-to-cst))
    (declare (ignorable __function__))
    (b* ((tokens (tokenize-pfcs pfcs-string))
         ((when (reserrp tokens)) tokens)
         ((mv top-object next-token rest-tokens)
          (parse-system tokens))
         ((when (reserrp top-object)) top-object)
         ((unless (and (null next-token)
                       (null rest-tokens)))
          (reserrf (list next-token rest-tokens))))
      top-object)))

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

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