		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Read-input-file-to-preproc

Read a file to preprocess, explicitly specified as user input.

Signature
(read-input-file-to-preproc path file state) → (mv erp bytes state)
Arguments: path — Guard (stringp path).; file — Guard (stringp file).
Returns: bytes — Type (byte-listp bytes).

This is used for the files whose paths are explicitly passed to pproc-files. We concatenate the path prefix to the file path suffix, with a slash in between (this is for Unix-like systems). We read the bytes from the file system, and return them.

Definitions and Theorems

Function: read-input-file-to-preproc

(defun read-input-file-to-preproc (path file state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp path) (stringp file))))
  (b* (((reterr) nil state)
       (path-to-read (str::cat path "/" file))
       ((mv erp bytes state)
        (acl2::read-file-into-byte-list path-to-read state))
       ((when erp)
        (reterr (msg "Reading ~x0 failed." path-to-read))))
    (retok bytes state)))

Theorem: byte-listp-of-read-input-file-to-preproc.bytes

(defthm byte-listp-of-read-input-file-to-preproc.bytes
  (b* (((mv acl2::?erp ?bytes acl2::?state)
        (read-input-file-to-preproc path file state)))
    (byte-listp bytes))
  :rule-classes :rewrite)