Write C files to the file system from an ACL2 representation.
This macro takes as input an ACL2 representation of C code
and writes that C code to the file system.
The ACL2 representation of the C code could be
the result of applying transformations to
code obtained via input-files;
so this
This macro currently does not perform very thorough input validation, but we plan to improve that.
(output-files :const ... ; no default :process ... ; default nil :const-files ... ; default nil
Name of the existing ACL2 constant that contains the representation of the C code to write to the file system.
This constant must contain a fileset (i.e. a value of type fileset) if the
:process input (see below) isnil , or a translation unit ensemble (i.e. a value of type transunit-ensemble) if the:process input isIn the rest of this documentation page, let
*const* be the name of this constant.
Specifies the processing to perform on the ACL2 representation of the C code in
*const* .This must be one of the following:
nil , for no processing. In this case,*const* must contain a file set, which is written to the file system as is.*const* to a file set that is then written to the file system. In this case,*const* must contain a translation unit ensemble.
Name of the generated ACL2 constant whose value is the file set obtained by printing
*const* .If this input is
nil , this constant is not generated.This input must be
nil if:process isnil , because in that case*const* already contains a file set.In the rest of this documentation page, let
*const-files* be the name of this constant, if notnil .
This macro generates one file in the file system
for each element of the translation unit ensemble or file set
in
Optionally, the named constant containing the file set obtained by printing the abstract syntax in
*const* .