• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
              • Type-to-tyname
              • Ident+type-to-tyspec+declor
              • Positive-to-iconst
              • Type-to-maker
              • Irr-type
            • Atc-macro-definition
          • Atc-tutorial
        • Syntax-for-tools
        • Language
        • Representation
        • Transformation-tools
        • Pack
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atc-types

Ident+type-to-tyspec+declor

Turn an identifier and a type into a type specifier sequence and an object declarator.

Signature

(ident+type-to-tyspec+declor id type) → (mv tyspec declor)

Arguments

id — Guard (identp id).

type — Guard (typep type).

Returns

tyspec — Type (tyspecseqp tyspec).

declor — Type (obj-declorp declor).

This function provides the consituents to construct a declaration of an identifier with a given type. The type specifier sequence and the object declarator can be used to construct various kinds of declarations (see our C abstract syntax).

Note that we pick a specific type specifier sequence for each type, out of possibly multiple ones possible, via the use of type-to-tyname.

Definitions and Theorems

Function: ident+type-to-tyspec+declor

(defun ident+type-to-tyspec+declor (id type)
  (declare (xargs :guard (and (identp id) (typep type))))
  (let ((__function__ 'ident+type-to-tyspec+declor))
    (declare (ignorable __function__))
    (ident+tyname-to-tyspec+declor id (type-to-tyname type))))

Theorem: tyspecseqp-of-ident+type-to-tyspec+declor.tyspec

(defthm tyspecseqp-of-ident+type-to-tyspec+declor.tyspec
  (b* (((mv ?tyspec ?declor)
        (ident+type-to-tyspec+declor id type)))
    (tyspecseqp tyspec))
  :rule-classes :rewrite)

Theorem: obj-declorp-of-ident+type-to-tyspec+declor.declor

(defthm obj-declorp-of-ident+type-to-tyspec+declor.declor
  (b* (((mv ?tyspec ?declor)
        (ident+type-to-tyspec+declor id type)))
    (obj-declorp declor))
  :rule-classes :rewrite)

Theorem: ident+type-to-tyspec+declor-of-ident-fix-id

(defthm ident+type-to-tyspec+declor-of-ident-fix-id
  (equal (ident+type-to-tyspec+declor (ident-fix id)
                                      type)
         (ident+type-to-tyspec+declor id type)))

Theorem: ident+type-to-tyspec+declor-ident-equiv-congruence-on-id

(defthm ident+type-to-tyspec+declor-ident-equiv-congruence-on-id
  (implies (ident-equiv id id-equiv)
           (equal (ident+type-to-tyspec+declor id type)
                  (ident+type-to-tyspec+declor id-equiv type)))
  :rule-classes :congruence)

Theorem: ident+type-to-tyspec+declor-of-type-fix-type

(defthm ident+type-to-tyspec+declor-of-type-fix-type
  (equal (ident+type-to-tyspec+declor id (type-fix type))
         (ident+type-to-tyspec+declor id type)))

Theorem: ident+type-to-tyspec+declor-type-equiv-congruence-on-type

(defthm ident+type-to-tyspec+declor-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (ident+type-to-tyspec+declor id type)
                  (ident+type-to-tyspec+declor id type-equiv)))
  :rule-classes :congruence)