• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
            • Tyspecseq
              • Tyspecseqp
              • Tyspecseq-fix
              • Tyspecseq-case
              • Tyspecseq-equiv
              • Tyspecseq-sint
              • Tyspecseq-kind
              • Tyspecseq-sshort
              • Tyspecseq-slong
              • Tyspecseq-sllong
              • Tyspecseq-ushort
              • Tyspecseq-union
              • Tyspecseq-ulong
              • Tyspecseq-ullong
              • Tyspecseq-uint
              • Tyspecseq-typedef
              • Tyspecseq-struct
              • Tyspecseq-ldouble
              • Tyspecseq-float
              • Tyspecseq-enum
              • Tyspecseq-double
              • Tyspecseq-void
              • Tyspecseq-uchar
              • Tyspecseq-schar
              • Tyspecseq-char
              • Tyspecseq-bool
            • Expr
            • Binop
            • Fileset
            • Obj-declor
            • Ident
            • Iconst
            • Obj-adeclor
            • Const
            • Fundef
            • Unop
            • File
            • Tag-declon
            • Fun-declor
            • Obj-declon
            • Iconst-length
            • Abstract-syntax-operations
            • Label
            • Struct-declon
            • Initer
            • Ext-declon
            • Fun-adeclor
            • Expr-option
            • Iconst-base
            • Initer-option
            • Iconst-option
            • Tyspecseq-option
            • Stmt-option
            • Scspecseq
            • Param-declon
            • Obj-declon-option
            • File-option
            • Tyname
            • Transunit
            • Fun-declon
            • Transunit-result
            • Param-declon-list
            • Struct-declon-list
            • Expr-list
            • Tyspecseq-list
            • Ident-set
            • Ident-list
            • Ext-declon-list
            • Unop-list
            • Tyname-list
            • Fundef-list
            • Fun-declon-list
            • Binop-list
            • Stmt-fixtypes
            • Expr-fixtypes
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-syntax

Tyspecseq

Fixtype of type specifier sequences [C17:6.7.2].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:void → tyspecseq-void
:char → tyspecseq-char
:schar → tyspecseq-schar
:uchar → tyspecseq-uchar
:sshort → tyspecseq-sshort
:ushort → tyspecseq-ushort
:sint → tyspecseq-sint
:uint → tyspecseq-uint
:slong → tyspecseq-slong
:ulong → tyspecseq-ulong
:sllong → tyspecseq-sllong
:ullong → tyspecseq-ullong
:bool → tyspecseq-bool
:float → tyspecseq-float
:double → tyspecseq-double
:ldouble → tyspecseq-ldouble
:struct → tyspecseq-struct
:union → tyspecseq-union
:enum → tyspecseq-enum
:typedef → tyspecseq-typedef

A sequence of one or more type specifiers in a declaration specifies a type. The allowed sequences are described in [C17:6.7.2]. This fixtype captures some of these sequences.

We capture type specifier sequences for the void type, the plain char type, the standard signed and unsigned integer types (which include _Bool), the (real and complex) floating types, limited forms of structure, union, and enumeration types, and type definition names. Complex floating types are not supported by all implementations; we include them in the abstract syntax, because it must suffice to represent all implementations, but they can be used only if supported.

The form of structure, union, and enumeration types is limited to the case of a single identifier (i.e. tag) [C17:6.7.2.1] [C17:6.7.2.2], without members or enumerators. Syntactically, declarations that define (members of) structure and union types and (enumerators) of enumeration types are also type specifiers. But we capture them elsewhere in our abstract syntax. We use tyspecseq only for parts of the code that reference existing types, not ones that introduce them. In that context, there is a distinction between defining a structure type and merely referencing it.

We do not capture atomic type specifiers for now. These involve additional syntactic complexities, as they contain type names, which are defined below to depend on type specifier sequences; so adding atomic type specifiers would introduce a mutual recursion in the definition of these fixtypes, which is doable but can perhaps be avoided for a while, until we actually need atomic type specifiers.

This tyspecseq fixtype has one constructor for each item in the list in [C17:6.7.2/2], where different items are different types (only syntactically speaking; more generally, type definition names may be also equal to other types). Each item in that list lists one of more sequences, meant to represent multisets, i.e. where order does not matter. We capture all the possible multisets for each item, via boolean fields that say whether elements of a sequence are present or absent: for example, (make-tyspecseq-sshort :signed t :int nil) represents signed short; see the pretty-printer for details. However, we do not capture different sequentializations of the same multiset, e.g. we capture signed short but not short signed. We capture the sequences listed in [C17:6.7.2/2] that represent the multiset. Arguably, those are the sequences that should always be used, despite other equivalent sequences being allowed.

The type specifiers in a declaration may be intermixed with other declaration specifiers [C17:6.7/1] [C17:6.7.2/2] (e.g. one could write unsigned auto int x = 1;), so long as their sequence (ignoring any intermixed non-type specifiers) is valid according to [C17:6.7.2/2]. This intermixing is probably best avoided, so our abstract syntax does not allow it: our type specifier sequences are meant to be contiguous.

Subtopics

Tyspecseqp
Recognizer for tyspecseq structures.
Tyspecseq-fix
Fixing function for tyspecseq structures.
Tyspecseq-case
Case macro for the different kinds of tyspecseq structures.
Tyspecseq-equiv
Basic equivalence relation for tyspecseq structures.
Tyspecseq-sint
Tyspecseq-kind
Get the kind (tag) of a tyspecseq structure.
Tyspecseq-sshort
Tyspecseq-slong
Tyspecseq-sllong
Tyspecseq-ushort
Tyspecseq-union
Tyspecseq-ulong
Tyspecseq-ullong
Tyspecseq-uint
Tyspecseq-typedef
Tyspecseq-struct
Tyspecseq-ldouble
Tyspecseq-float
Tyspecseq-enum
Tyspecseq-double
Tyspecseq-void
Tyspecseq-uchar
Tyspecseq-schar
Tyspecseq-char
Tyspecseq-bool