		Search-engine friendly clone of the ACL2 documentation.

Pproc-include-directive

Preprocess a #include directive.

Signature
(pproc-include-directive path file preprocessed preprocessing rev-lexemes ppstate state) → (mv erp new-rev-lexemes new-ppstate new-preprocessed state)
Arguments: path — Guard (stringp path).; file — Guard (stringp file).; preprocessed — Guard (string-plexeme-list-alistp preprocessed).; preprocessing — Guard (string-listp preprocessing).; rev-lexemes — Guard (plexeme-listp rev-lexemes).; ppstate — Guard (ppstatep ppstate).
Returns: new-rev-lexemes — Type (plexeme-listp new-rev-lexemes).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).; new-preprocessed — Type (string-plexeme-list-alistp new-preprocessed).

This is called just after the include identifier has been parsed.

If we do not find a token or new line, it is an error, because there is no header name.

If we find a new line, it is an error, because there is no header name.

If we find a header name, we find the file referenced by it and we recursively preprocess it. Note that we pass t as the headerp flag.

If we find any other token, for now we return an error, but we should preprocess that token and any subsequent tokens, and see if they result in a header name.