• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
              • Print-exprs/decls/stmts
              • Print-expr
              • Pristate
              • Print-fileset
              • Print-dec/oct/hex-const
              • Priopt
                • Priopt-fix
                • Priopt-equiv
                • Make-priopt
                • Priopt->paren-nested-conds
                • Priopt->indent-size
                • Change-priopt
                • Prioptp
              • Print-fundef
              • Print-s-char
              • Print-c-char
              • Print-typequal/attribspec-list-list
              • Print-ident
              • Print-ident-list
              • Print-hex-core-fconst
              • Print-dec-core-fconst
              • Print-oct-digit-achar
              • Print-hex-frac-const
              • Print-hex-digit-achar
              • Print-dec-frac-const
              • Print-dec-digit-achar
              • Print-strunispec
              • Print-file
              • Print-astring
              • Print-asm-name-spec
              • Print-asm-clobber-list
              • Print-stringlit-list
              • Print-inc/dec-op-list
              • Print-cprefix-option
              • Print-binop
              • Print-univ-char-name
              • Print-type-qual
              • Print-transunit
              • Print-simple-escape
              • Print-s-char-list
              • Print-isuffix-option
              • Print-indent
              • Print-fsuffix-option
              • Print-extdecl-list
              • Print-eprefix-option
              • Print-dec-expo-option
              • Print-char
              • Print-c-char-list
              • Print-attrib-name
              • Print-asm-qual-list
              • Print-stor-spec
              • Print-oct-escape
              • Print-escape
              • Print-dec-expo-prefix
              • Print-cconst
              • Print-bin-expo-prefix
              • Dec-pristate-indent
              • Print-stringlit
              • Print-sign-option
              • Print-isuffix
              • Print-fun-spec
              • Print-fconst
              • Print-extdecl
              • Print-dec-expo
              • Print-block
              • Print-bin-expo
              • Print-asm-qual
              • Print-asm-clobber
              • Print-new-line
              • Print-lsuffix
              • Print-inc/dec-op
              • Print-hex-quad
              • Print-fsuffix
              • Print-eprefix
              • Print-cprefix
              • Print-usuffix
              • Print-unop
              • Print-iconst
              • Print-hprefix
              • Print-const
              • Print-chars
              • Print-sign
              • Print-oct-digit-achars
              • Print-hex-digit-achars
              • Print-dec-digit-achars
              • Print-stmt
              • Print-expr-list
              • Init-pristate
              • Print-structdecl-list
              • Inc-pristate-indent
              • Print-param-declor
              • Print-dirdeclor
              • Default-priopt
              • Print-structdeclor
              • Print-initer
              • Print-decl-inline
              • Print-structdecl
              • Print-genassoc-list
              • Print-enumspec
              • Print-absdeclor
              • Print-typequal/attribspec-list
              • Print-desiniter-list
              • Print-const-expr
              • Print-attrib
              • Print-tyname
              • Print-structdeclor-list
              • Print-spec/qual-list
              • Print-param-declon-list
              • Print-param-declon
              • Print-initdeclor-list
              • Print-designor-list
              • Print-decl-spec-list
              • Print-decl-list
              • Print-attrib-spec-list
              • Print-asm-output-list
              • Print-asm-input-list
              • Print-typequal/attribspec
              • Print-statassert
              • Print-spec/qual
              • Print-member-designor
              • Print-initdeclor
              • Print-enumer-list
              • Print-dirabsdeclor
              • Print-desiniter
              • Print-decl-spec
              • Print-decl
              • Print-block-item-list
              • Print-attrib-spec
              • Print-attrib-list
              • Print-asm-output
              • Print-align-spec
              • Print-type-spec
              • Print-label
              • Print-genassoc
              • Print-enumer
              • Print-designor
              • Print-declor
              • Print-block-item
              • Print-asm-stmt
              • Print-asm-input
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Printer

Priopt

Fixtype of printer options.

This is a product type introduced by fty::defprod.

Fields
indent-size — posp
paren-nested-conds — booleanp

This fixtype collects options that control various aspects of how the C code is printed.

Currently we support the following options:

  • The indentation size, i.e. how much each indentation level moves the starting column. This is measured in number of spaces, as a positive integer.
  • A flag saying whether conditional expressions nested in other 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 the flag is t, the printer adds the parentheses.

We may add more options in the future.

Subtopics

Priopt-fix
Fixing function for priopt structures.
Priopt-equiv
Basic equivalence relation for priopt structures.
Make-priopt
Basic constructor macro for priopt structures.
Priopt->paren-nested-conds
Get the paren-nested-conds field from a priopt.
Priopt->indent-size
Get the indent-size field from a priopt.
Change-priopt
Modifying constructor for priopt structures.
Prioptp
Recognizer for priopt structures.