		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 state)
Arguments: path — Guard (stringp path).
Returns: tree — Type (abnf::tree-resultp tree).

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). If parsing is unsuccessful, we return an error value as first result.

For more details see parse-from-file-at-path+. The only difference between that function and this one is that this one doesn't bother to return the lexemes.

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 file-cst ?lexemes state)
          (parse-from-file-at-path+ path state)))
      (mv file-cst state))))

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

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