		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Parse-from-file-at-path+

Parse a Leo file at a path.

Signature
(parse-from-file-at-path+ path state) → (mv tree lexemes state)
Arguments: path — Guard (stringp path).
Returns: tree — Type (abnf::tree-resultp tree).; lexemes — Type (abnf::tree-listp lexemes).

This function attempts to parse a Leo source file at a given path. If parsing is successful, we return an ABNF file tree (and state), along with the list of lexemes that the file consists of (these cannot be completely derived from the file tree, which only contains tokens, while the lexemes also include whitespace and comments). If parsing is unsuccessful, we return an error value as first result, and nil as list of lexemes.

Since Leo files are encoded in UTF-8, we use the Unicode library function read-utf8 to obtain a list of Unicode code points. If the reading or UTF-8 decoding fails, that function returns an ACL2 string instead of a list of code points: we return that string as part of the error value, as it may be informative.

If reading and decoding are successful, we call parse-from-codepoints+, and we inspect its results. If there is an error, we try to provide an indication of where the error occurs in the file. For now we simply return the position in the file by turning the lexemes returned into a list of Unicode code points (not bytes) and counting such code points. While this may not be quite exactly where the error occurs (as the parser has not been optimized for error reporting yet), it should be at least close enough to significantly narrow the search.

Definitions and Theorems

Function: parse-from-file-at-path+

(defun parse-from-file-at-path+ (path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp path)))
  (let ((__function__ 'parse-from-file-at-path+))
    (declare (ignorable __function__))
    (b* (((mv unicodes state)
          (acl2::read-utf8 (str-fix path) state))
         ((unless (nat-listp unicodes))
          (mv (reserrf unicodes) nil state))
         ((mv tree lexemes)
          (parse-from-codepoints+ unicodes))
         ((when (reserrp tree))
          (b* ((pos (len (abnf::tree-list->string lexemes))))
            (mv (reserrf (list :position pos :error tree))
                nil state))))
      (mv tree lexemes state))))

Theorem: tree-resultp-of-parse-from-file-at-path+.tree

(defthm tree-resultp-of-parse-from-file-at-path+.tree
  (b* (((mv ?tree ?lexemes acl2::?state)
        (parse-from-file-at-path+ path state)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-from-file-at-path+.lexemes

(defthm tree-listp-of-parse-from-file-at-path+.lexemes
  (b* (((mv ?tree ?lexemes acl2::?state)
        (parse-from-file-at-path+ path state)))
    (abnf::tree-listp lexemes))
  :rule-classes :rewrite)

Theorem: parse-from-file-at-path+-of-str-fix-path

(defthm parse-from-file-at-path+-of-str-fix-path
  (equal (parse-from-file-at-path+ (str-fix path)
                                   state)
         (parse-from-file-at-path+ path state)))

Theorem: parse-from-file-at-path+-streqv-congruence-on-path

(defthm parse-from-file-at-path+-streqv-congruence-on-path
  (implies (acl2::streqv path path-equiv)
           (equal (parse-from-file-at-path+ path state)
                  (parse-from-file-at-path+ path-equiv state)))
  :rule-classes :congruence)