• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
              • Expr
              • Exprs/decls/stmts
              • Type-spec
              • Binop
              • Stmt
              • Amb-expr/tyname
              • Dirdeclor
              • Unop
              • Asm-stmt
              • Dec/oct/hex-const
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
              • Dirabsdeclor
              • Decl-spec
              • Structdecl
              • Fundef
              • Transunit-ensemble
              • Asm-name-spec
              • Amb-declor/absdeclor
                • Amb-declor/absdeclor-equiv
                • Amb-declor/absdeclor-p
                • Make-amb-declor/absdeclor
                • Amb-declor/absdeclor->absdeclor
                • Amb-declor/absdeclor->declor
                • Change-amb-declor/absdeclor
                • Amb-declor/absdeclor-fix
                • Amb-declor/absdeclor-count
              • Param-declor
              • Declor
              • Type-qual
              • Tyname
              • Absdeclor
              • Struni-spec
              • Stor-spec
              • Keyword-uscores
              • Align-spec
              • Label
              • Expr-option
              • Spec/qual
              • Lsuffix
              • Hex-frac-const
              • Desiniter
              • Iconst
              • Dirabsdeclor-option
              • Dec-frac-const
              • Dec-core-fconst
              • Extdecl
              • Amb?-declor/absdeclor
              • Isuffix
              • Initdeclor
              • Hex-core-fconst
              • Const-expr-option
              • Attrib-spec
              • Structdeclor
              • Escape
              • Decl
              • Amb?-expr/tyname
              • Ident-option
              • Bin-expo
              • Absdeclor-option
              • Statassert
              • Param-declon
              • Member-designor
              • Initer-option
              • Initer
              • Fsuffix
              • Enumspec
              • Declor-option
              • Const
              • Hex-quad
              • Eprefix
              • Const-expr
              • Block-item
              • Oct-escape
              • Inc/dec-op
              • Fun-spec
              • Dec-expo
              • Cprefix-option
              • Asm-name-spec-option
              • Amb?-decl/stmt
              • S-char
              • Isuffix-option
              • Genassoc
              • Fundef-option
              • Fsuffix-option
              • Fconst
              • Eprefix-option
              • Dec-expo-option
              • Cprefix
              • C-char
              • Type-spec-option
              • Sign-option
              • Iconst-option
              • Asm-output
              • Asm-input
              • Const-option
              • Usuffix
              • Univ-char-name
              • Transunit
              • Hprefix
              • Enumer
              • Designor
              • Attrib-name
              • Sign
              • Asm-qual
              • Typequal/attribspec
              • Dec-expo-prefix
              • Bin-expo-prefix
              • Stringlit
              • Cconst
              • Expr/tyname
              • Decl/stmt
              • Declor/absdeclor
              • Asm-clobber
              • Typequal/attribspec-list
              • Decl-spec-list
              • Stringlit-list
              • Spec/qual-list
              • Inc/dec-op-list
              • Desiniter-list
              • S-char-list
              • Param-declon-list
              • Decl-list
              • C-char-list
              • Block-item-list
              • Typequal/attribspec-list-list
              • Structdeclor-list
              • Structdecl-list
              • Initdeclor-list
              • Genassoc-list
              • Filepath-transunit-map
              • Extdecl-list
              • Enumer-list
              • Attrib-spec-list
              • Type-spec-list
              • Ident-list
              • Expr-list
              • Asm-qual-list
              • Asm-output-list
              • Asm-input-list
              • Asm-clobber-list
              • Stor-spec-list
              • Ident-set
              • Ident-option-set
              • Eprefix-option-list
              • Designor-list
              • Attrib-list
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
            • Ascii-identifiers
            • Unambiguity
            • Preprocessing
            • Abstraction-mapping
            • Standard
            • Purity
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Riscv
        • 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
  • Abstract-syntax
  • Exprs/decls/stmts

Amb-declor/absdeclor

Fixtype of ambiguous declarators or abstract declarators.

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

Fields
declor — declor
absdeclor — absdeclor

A parameter declaration may include, after the declaration specifiers, either a declarator or an abstract declarator (or also nothing). Syntactically, there is a complex overlap between declarators and abstract declarators. For instance, if I is an identifier, (I) could be either a direct declarator for the parenthesized identifier or a function abstract declarator where I is a type specifier for the (one) parameter. But this is just a simple example: there are infinite overlapping constructs, e.g. obtained by adding array and function declarator parts to (I), but not only those.

So here, analogously to amb-expr/tyname, we introduce a fixtype to capture constructs that, syntactically, are both declarators and abstract declarators. The two components of this fixtype should be the same in concrete syntax, but we do not enforce that in the fixtype.

Subtopics

Amb-declor/absdeclor-equiv
Basic equivalence relation for amb-declor/absdeclor structures.
Amb-declor/absdeclor-p
Recognizer for amb-declor/absdeclor structures.
Make-amb-declor/absdeclor
Basic constructor macro for amb-declor/absdeclor structures.
Amb-declor/absdeclor->absdeclor
Get the absdeclor field from a amb-declor/absdeclor.
Amb-declor/absdeclor->declor
Get the declor field from a amb-declor/absdeclor.
Change-amb-declor/absdeclor
Modifying constructor for amb-declor/absdeclor structures.
Amb-declor/absdeclor-fix
Fixing function for amb-declor/absdeclor structures.
Amb-declor/absdeclor-count
Measure for recurring over amb-declor/absdeclor structures.