		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Printer

Printing for our C syntax for tools.

We provide an executable (pretty-)printer from the abstract syntax to the concrete syntax.

Currently the printer is neither verified nor proof-generating, but we plan to work towards these goals.

Subtopics

Print-exprs/decls/stmts: Print expressions, declarations, statements, and related entities.
Print-expr: Print an expression.
Pristate: Fixtype of printer states.
Print-dec/oct/hex-const: Print a decimal, octal, or hexadecimal constant.
Priopt: Fixtype of printer options.
Print-fundef: Print a function definition.
Print-filepath-transunit-map: Print the files in a file set.
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-q-char: Print a character usable in header names in double quotes.
Print-h-char: Print a character usable in header names in angle brackets.
Print-fileset: Print a file set.
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-file: Print (the data bytes of) a file.
Print-hex-core-fconst: Print a hexadecimal core floating constant.
Print-dec-core-fconst: Print a decimal core floating constant.
Print-ident-list: Print a list of one or more identifiers, separated by commas.
Print-fsuffix: Print a floating suffix.
Print-oct-digit-achar: Print an ACL2 octal digit character.
Print-label-declaration-list: Print zero or more label declarations.
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-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-astring: Print the characters from an ACL2 string.
Print-asm-name-spec: Print an assembler name specifier.
Print-univ-char-name: Print a universal character name.
Print-struni-spec: Print a structure or union specifier.
Print-simple-escape: Print a simple escape.
Print-label-declaration: Print a label declaration consisting of one or more labels.
Print-isuffix-option: Print an optional integer suffix.
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-cprefix-option: Print an optional character constant prefix.
Print-binop: Print a binary operator.
Print-attrib-name: Print an attribute name.
Print-type-qual: Print a type qualifier.
Print-s-char-list: Print a list of zero or more characters or escape sequences usable in string literals.
Print-q-char-list: Print a list of zero or more characters usable in header names in double quotes.
Print-indent: Print an indentation.
Print-ident: Print an identifier.
Print-h-char-list: Print a list of zero or more characters usable in header names in angle brackets.
Print-dec-expo-prefix: Print a decimal exponent prefix.
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-bin-expo-prefix: Print a binary exponent prefix.
Print-asm-qual-list: Print a list of one or more assembler specifiers.
Print-stringlit: Print a string literal.
Print-stor-spec: Print a storage class specifier.
Print-sign-option: Print an optional sign.
Print-oct-escape: Print an octal escape.
Print-header-name: Printe a header name.
Print-extdecl: Print an external declaration.
Print-escape: Print an escape sequence.
Print-cconst: Print a character constant.
Print-asm-qual: Print an assembler qualifier.
Print-asm-clobber: Print an assembler clobber.
Init-pristate: Initial printer state.
Dec-pristate-indent: Decrease the printer state's indentation level by one.
Print-isuffix: Print an integer suffix.
Print-fun-spec: Print a function specifier.
Print-fconst: Print a floating constant.
Print-dec-expo: Print a decimal exponent.
Print-bin-expo: Print a binary exponent.
Print-unop: Print a unary operator.
Print-transunit: Print a translation unit.
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-eprefix: Print an encoding prefix.
Print-cprefix: Print a character constant prefix.
Print-usuffix: Print an unsigned suffix.
Print-iconst: Print an integer constant.
Print-hprefix: Print a hexadecimal prefix.
Print-const: Print a constant.
Print-comp-stmt: Print a compound statement.
Print-hex-digit-achars: Print zero or more ACL2 hexadecimal digit characters.
Print-sign: Print a sign.
Print-oct-digit-achars: Print zero or more ACL2 octal digit characters.
Print-dec-digit-achars: Print zero or more ACL2 decimal digit characters.
Print-chars: Print zero or more characters.
Inc-pristate-indent: Increase the printer state's indentation level by one.
Print-expr-list: Print a list of one or more expressions, separated by commas.
Print-struct-declon-list: Print a list of one or more structure declarations, separated by spaces.
Print-stmt: Print a statement, in one or more lines, with proper indentation.
Print-param-declor: Print a parameter declarator.
Print-dirdeclor: Print a direct declarator.
Default-priopt: Default printer options.
Print-struct-declor: Print a structure declarator.
Print-initer: Print an initializer.
Print-decl-inline: Print a declaration, inline.
Print-struct-declon: Print a structure declaration.
Print-genassoc-list: Print a list of one or more generic associations, separated by commas.
Print-enum-spec: 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-struct-declor-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.