Parse files from a file set constant to a translation unit ensemble constant.
This macro takes as input the name of a named constant whose value is a file set (see fileset), uses the parser to parse the file set into a translation unit ensemble (see transunit-ensemble), which is the abstract syntax representation of the file set, and generates an ACL2 defconst with the translation unit ensemble.
This macro can be used after read-files, which creates a named constant containing a file set from files at specified paths.
This macro currently does not perform very thorough input validation, but we plan to improve that.
(parse-files :const-transunits ... ; no default :const-fileset ... ; no default :gcc ... ; default nil )
Name of the generated constant that contains the translation unit ensemble.
This must be a symbol that is a valid name for a new named constant.
In the rest of this documentation page, let
*const-transunits* be this symbol.
Name of the existing constant that contains the file set.
This must be a symbol that names an existing named constant, whose value must be a file set.
In the rest of this documentation page, let
*const-fileset* be this symbol.
Boolean saying whether certain GCC extensions should be accepted or not.
The named constant containing the translation unit ensemble obtained by parsing the file set in
*const-fileset* .