		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.

The (non-event) macro output-files-prog provides a programmatic interface to the functionality of output-files.

General Form

(output-files :const           ...  ; no default
              :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 an unambiguous translation unit ensemble (i.e. a value of type transunit-ensemble that additionally satisfies transunit-ensemble-unambp). The translation unit is printed to a file set, whose files are written to the file system.
In the rest of this documentation page, let *const* be the name of this constant.

: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.

Generated Events

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

Subtopics

Output-files-prog: Programmatic interface to output-files.
Output-files-implementation: Implementation of output-files.