		Search-engine friendly clone of the ACL2 documentation.

Input-files

Input-files-prog

Programmatic interface to input-files.

This (non-event) macro provides a programmatic interface to the functionality of input-files. It has the form:

(input-files-prog :files             ...  ; required
                  :path              ...  ; default "."
                  :preprocess        ...  ; default nil
                  :preprocess-args   ...  ; default nil
                  :process           ...  ; default :validate
                  :keep-going        ...  ; default nil
                  :std               ...  ; default 17
                  :gcc               ...  ; default nil
                  :short-bytes       ...  ; default 2
                  :int-bytes         ...  ; default 4
                  :long-bytes        ...  ; default 8
                  :long-long-bytes   ...  ; default 8
                  :plain-char-signed ...  ; default nil
  )

This is the same as input-files, except that there is no :const input, because this macro does not generate any events. Instead, it returns an error-value tuple consisting of the value that input-files would assign to the generated named constant. These are the results of the error-value tuple, in order:

code: the code unit ensemble (a value of type code-ensemble) resulting from processing, according to the :process input, the files read from the paths specified by :files (if :preprocess is nil) or the files resulting from their preprocessing (if :preprocess is not nil.
state: the ACL2 state.

Note that the macro implicitly takes state, so it must be used in a context where state is available.

Subtopics

Input-files-prog-fn: Implementation of input-files-prog.
Input-files-prog-definition: Definition of the input-files-prog macro.