		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-from-codepoints

Parse Unicode code points into a CST.

Signature
(parse-from-codepoints codepoints) → tree
Arguments: codepoints — Guard (nat-listp codepoints).
Returns: tree — Type (abnf::tree-resultp tree).

Lexes, tokenizes, and parses a Leo source file expressed as a list of Unicode code points. Returns a file CST.

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

Definitions and Theorems

Function: parse-from-codepoints

(defun parse-from-codepoints (codepoints)
  (declare (xargs :guard (nat-listp codepoints)))
  (let ((__function__ 'parse-from-codepoints))
    (declare (ignorable __function__))
    (b* (((mv file-cst ?lexemes)
          (parse-from-codepoints+ codepoints)))
      file-cst)))

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

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