		Search-engine friendly clone of the ACL2 documentation.

Parser-abstractor-interface

Ast-from-file-at-path

Parse and abstract a Leo file at a path into an AST.

Signature
(ast-from-file-at-path path state) → (mv tree state)
Arguments: path — Guard (stringp path).
Returns: tree — Type (file-resultp tree).

This function attempts to parse and abstract a Leo source file at a given path. If parsing is successful, we return a file AST (and state). If parsing is unsuccessful, we return an error value as first result.

Definitions and Theorems

Function: ast-from-file-at-path

(defun ast-from-file-at-path (path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp path)))
  (let ((__function__ 'ast-from-file-at-path))
    (declare (ignorable __function__))
    (b* (((mv file-cst state)
          (parse-from-file-at-path path state))
         ((when (reserrp file-cst))
          (mv file-cst state)))
      (mv (abs-file file-cst) state))))

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

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