		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Printer

A printer of C from the abstract syntax.

We provide a (pretty-)printer that turns our abstract syntax into C code, according to our concrete syntax formulation. This printer is relatively simple initially, but we will make it more feature-rich in the future.

Our abstract syntax is broader than the concrete syntax, in the sense that it represents more constructs than allowed by the concrete syntax. For instance, identifiers in the abstract syntax can be anything (for the reasons explained in ident), but they follow certain restrictions in the concrete syntax. We plan to define, and use in the printer as guards, predicates over the abstract syntax that check whether the abstract syntax conforms to the concrete syntax. For now, we use run-time checks, where needed, to ensure that the abstract syntax matches the concrete syntax; in some cases we actually use weaker checks. If these run-time checks fail, we throw hard errors, which is not ideal in general, but we want to keep the printing functions's inputs and outputs simpler, without using error-value tuples or other forms (like error triples) needed for non-hard errors. After all, a printer is not supposed to fail, and once we have the aforementioned guards, it will never fail. For now, we can regard calls to the printer with non-compliant abstract syntax a form of internal error, for which hard errors are generally appropriate. But we use the term `misusage error' in the hard error messages, to reflect the fact that the printer is being misused in some sense, as opposed to an `internal error' which is generally used for situations are due to some proper implementation error.

Subtopics

Print-exprs/decls/stmts: Print expressions, declarations, statements, and related entities.
Print-expr: Print an expression.
Pristate: Fixtype of printer states.
Print-fileset: Print a file set.
Print-dec/oct/hex-const: Print a decimal, octal, or hexadecimal constant.
Priopt: Fixtype of printer options.
Print-fundef: Print a function definition.
Print-s-char: Print a character or escape sequence usable in string literals.
Print-c-char: Print a character or escape sequence usable in character constants.
Print-typequal/attribspec-list-list: Print a list or one or more lists of type qualifiers and attribute specifiers corresponding to a `pointer' in the grammar.
Print-ident: Print an identifier.
Print-ident-list: Print a list of one or more identifiers, separated by commas.
Print-hex-core-fconst: Print a hexadecimal core floating constant.
Print-dec-core-fconst: Print a decimal core floating constant.
Print-oct-digit-achar: Print an ACL2 octal digit character.
Print-hex-frac-const: Print a hexadecimal fractional constant.
Print-hex-digit-achar: Print an ACL2 hexadecimal digit character.
Print-dec-frac-const: Print a decimal fractional constant.
Print-dec-digit-achar: Print an ACL2 decimal digit character.
Print-strunispec: Print a structure or union specifier.
Print-file: Print (the data bytes of) a file.
Print-astring: Print the characters from an ACL2 string.
Print-asm-name-spec: Print an assembler name specifier.
Print-asm-clobber-list: Print a list of one or more assembler clobbers, separated by commas.
Print-stringlit-list: Print a list of one or more string literals, separated by spaces.
Print-inc/dec-op-list: Print a list of zero or more increment or decrement operators.
Print-cprefix-option: Print an optional character constant prefix.
Print-binop: Print a binary operator.
Print-univ-char-name: Print a universal character name.
Print-type-qual: Print a type qualifier.
Print-transunit: Print a translation unit.
Print-simple-escape: Print a simple escape.
Print-s-char-list: Print a list of zero or more characters or escape sequences usable in string-literals.
Print-isuffix-option: Print an optional integer suffix.
Print-indent: Print an indentation.
Print-fsuffix-option: Print an optional floating suffix.
Print-extdecl-list: Print a list of zero or more external declarations.
Print-eprefix-option: Print an optional encoding prefix.
Print-dec-expo-option: Print an optional decimal exponent.
Print-char: Print a character.
Print-c-char-list: Print a list of zero or more characters or escape sequences usable in character constants.
Print-attrib-name: Print an attribute name.
Print-asm-qual-list: Print a list of one or more assembler specifiers.
Print-stor-spec: Print a storage class specifier.
Print-oct-escape: Print an octal escape.
Print-escape: Print an escape sequence.
Print-dec-expo-prefix: Print a decimal exponent prefix.
Print-cconst: Print a character constant.
Print-bin-expo-prefix: Print a binary exponent prefix.
Dec-pristate-indent: Decrease the printer state's indentation level by one.
Print-stringlit: Print a string literal.
Print-sign-option: Print an optional sign.
Print-isuffix: Print an integer suffix.
Print-fun-spec: Print a function specifier.
Print-fconst: Print a floating constant.
Print-extdecl: Print an external declaration.
Print-dec-expo: Print a decimal exponent.
Print-block: Print a block.
Print-bin-expo: Print a binary exponent.
Print-asm-qual: Print an assembler qualifier.
Print-asm-clobber: Print an assembler clobber.
Print-new-line: Print a new-line character.
Print-lsuffix: Print a length suffix.
Print-inc/dec-op: Print an increment or decrement operator.
Print-hex-quad: Print a quadruple of hexadecimal digits.
Print-fsuffix: Print a floating suffix.
Print-eprefix: Print an encoding prefix.
Print-cprefix: Print a character constant prefix.
Print-usuffix: Print an unsigned suffix.
Print-unop: Print a unary operator.
Print-iconst: Print an integer constant.
Print-hprefix: Print a hexadecimal prefix.
Print-const: Print a constant.
Print-chars: Print zero or more characters.
Print-sign: Print a sign.
Print-oct-digit-achars: Print zero or more ACL2 octal digit characters.
Print-hex-digit-achars: Print zero or more ACL2 hexadecimal digit characters.
Print-dec-digit-achars: Print zero or more ACL2 decimal digit characters.
Print-stmt: Print a statement, in one or more lines, with proper indentation.
Print-expr-list: Print a list of one or more expressions, separated by commas.
Init-pristate: Initial printer state.
Print-structdecl-list: Print a list of one or more structure declarations, separated by spaces.
Inc-pristate-indent: Increase the printer state's indentation level by one.
Print-param-declor: Print a parameter declarator.
Print-dirdeclor: Print a direct declarator.
Default-priopt: Default printer options.
Print-structdeclor: Print a structure declarator.
Print-initer: Print an initializer.
Print-decl-inline: Print a declaration, inline.
Print-structdecl: Print a structure declaration.
Print-genassoc-list: Print a list of one or more generic associations, separated by commas.
Print-enumspec: Print an enueration specifier.
Print-absdeclor: Print an abstract declarator.
Print-typequal/attribspec-list: Print a list of one or more type qualifiers and attribute specifiers, separated by spaces.
Print-desiniter-list: Print a list of one or more initializers with optional designations, separated by commas.
Print-const-expr: Print a constant expression.
Print-attrib: Print a GCC attribute.
Print-tyname: Print a type name.
Print-structdeclor-list: Print a list of one or more structure declarators, separated by commas.
Print-spec/qual-list: Print a list of one or more specifiers and qualifiers, separated by spaces.
Print-param-declon-list: Print a list of one or more parameter declarations, separated by commas.
Print-param-declon: Print a parameter declaration.
Print-initdeclor-list: Print a list of one or more initializer declarators, separated by commas.
Print-designor-list: Print a list of one or more designators.
Print-decl-spec-list: Print a list of one or more declaration specifiers, separated by spaces.
Print-decl-list: Print a list of one or more declarations, one per line, all with the same indentation.
Print-attrib-spec-list: Print a list of one or more attribute specifiers, separated by single spaces.
Print-asm-output-list: Print a list of one or more assembler output operands, separated by commas.
Print-asm-input-list: Print a list of one or more assembler input operands, separated by commas.
Print-typequal/attribspec: Print a type qualifier or attribute specifier.
Print-statassert: Print a static assertion declaration.
Print-spec/qual: Print a specifier or qualifier.
Print-member-designor: Print a member designator.
Print-initdeclor: Print an initializer declarator.
Print-enumer-list: Print a list of one or more enumerators, separated by commas.
Print-dirabsdeclor: Print a direct abstract declarator.
Print-desiniter: Print an initializer with optional designations.
Print-decl-spec: Print a declaration specifier.
Print-decl: Print a declaration, in its own indented line.
Print-block-item-list: Print a list of zero or more block items.
Print-attrib-spec: Print an attribute specifier.
Print-attrib-list: Print a list of one or more GCC attributes, comma-separated.
Print-asm-output: Print an assembler output operand.
Print-align-spec: Print an alignment specifier.
Print-type-spec: Print a type specifier.
Print-label: Print a label.
Print-genassoc: Print a generic association.
Print-enumer: Print an enumerator.
Print-designor: Print a designator.
Print-declor: Print a declarator.
Print-block-item: Print a block item.
Print-asm-stmt: Print an assembler statement.
Print-asm-input: Print an assembler input operand.