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 ... ; no default
:process ... ; default :validate
: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:
- tunits:
the translation unit ensemble
(a value of type transunit-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.
