		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Output-files

Write C files to the file system from an ACL2 representation.

Introduction

In the name of this macro, output is best read as a verb: the macro outputs files from ACL2.

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 output-files macros can provide the final step in that process.

This macro currently does not perform very thorough input validation, but we plan to improve that.

General Form

(output-files :const           ...  ; no default
              :process         ...  ; default :print
              :const-files     ...  ; default nil
              :printer-options ...  ; default nil
  )

Inputs

:const

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) is :write, or an unambiguous translation unit ensemble (i.e. a value of type transunit-ensemble) if the :process input is :print.
In the rest of this documentation page, let *const* be the name of this constant.

:process — default :print

Specifies the processing to perform on the ACL2 representation of the C code in *const*.
This must be one of the following:
:write, for no processing (i.e. just writing the files). In this case, *const* must contain a file set, which is written to the file system as is.
:print (the default), to print the abstract syntax in *const* to a file set that is then written to the file system. In this case, *const* must contain a translation unit ensemble.

:const-files — default nil

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 is :write, 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 not nil.

:printer-options — default nil

Specifies options for various aspects of how the C code is printed.
This must be a keyword-value list (opt-name1 opt-value1 opt-name2 opt-value2 ...) where each opt-namek is a keyword among the ones described below, and each opt-valuek is one of the allowed values for the corresponding keyword as described below.
The following options are supported:
:indentation-size <posint>, where <posint> is a positive integer. This specifies the size of each indentation level, measured in number of spaces. If this option is not supplied, it defaults to 2.
:parenthesize-nested-conditionals <t/nil>, where <t/nil> is a boolean. This specifies whether conditional expressions that are `then' or `else' sub-expressions of outer conditional expressions should be parenthesized or not. For instance, whether the expression
a ? b ? c : d : e ? f g
should be printed as
a ? (b ? c : e) : (e ? f : g)
The two expressions are equivalent due to the precedence rules of C, but the second one is more readable. If this option is t, the printer adds the parentheses; if thie option is nil, no extra parentheses are added. If this option is not supplied, it defaults to nil.
This is currently the only supported printer option. More options may be added in the future.
Unless :process is :print (possibly by default), this :printer-options input must be nil.

Generated Events

This macro generates one file in the file system for each element of the translation unit ensemble or file set in *const*, at the paths that are the keys of the maps. Non-absolute paths are relative to the connected book directory (see cbd).

*const-files*

Optionally, the named constant containing the file set obtained by printing the abstract syntax in *const*.

Subtopics

Output-files-implementation: Implementation of output-files.