		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse

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

Signature
(parse pfcs-string) → sys
Arguments: pfcs-string — Guard (stringp pfcs-string).
Returns: sys — Type (system-resultp sys).

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 AST (abstract 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

(defun parse (pfcs-string)
  (declare (xargs :guard (stringp pfcs-string)))
  (let ((__function__ 'parse))
    (declare (ignorable __function__))
    (b* ((cst (parse-from-string-to-cst pfcs-string))
         ((when (reserrp cst)) cst)
         (ast (abs-system cst))
         ((when (reserrp ast))
          (reserrf (cons :problem-abstracting cst))))
      ast)))

Theorem: system-resultp-of-parse

(defthm system-resultp-of-parse
  (b* ((sys (parse pfcs-string)))
    (system-resultp sys))
  :rule-classes :rewrite)