• 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

Type-to-tyname

Turn a type into a type name.

Signature

(type-to-tyname type) → tyname

Arguments

type — Guard (typep type).

Returns

tyname — Type (tynamep tyname).

We pick a particular choice of type specifier sequence, and thus of type name, for each integer type.

Definitions and Theorems

Function: type-to-tyname-aux

(defun type-to-tyname-aux (type)
 (declare (xargs :guard (typep type)))
 (let ((__function__ 'type-to-tyname-aux))
  (declare (ignorable __function__))
  (type-case type :void
             (mv (tyspecseq-void) (obj-adeclor-none))
             :char
             (mv (tyspecseq-char) (obj-adeclor-none))
             :schar
             (mv (tyspecseq-schar)
                 (obj-adeclor-none))
             :uchar
             (mv (tyspecseq-uchar)
                 (obj-adeclor-none))
             :sshort
             (mv (tyspecseq-sshort nil nil)
                 (obj-adeclor-none))
             :ushort
             (mv (tyspecseq-ushort nil)
                 (obj-adeclor-none))
             :sint
             (mv (tyspecseq-sint nil t)
                 (obj-adeclor-none))
             :uint
             (mv (tyspecseq-uint t)
                 (obj-adeclor-none))
             :slong
             (mv (tyspecseq-slong nil nil)
                 (obj-adeclor-none))
             :ulong
             (mv (tyspecseq-ulong nil)
                 (obj-adeclor-none))
             :sllong
             (mv (tyspecseq-sllong nil nil)
                 (obj-adeclor-none))
             :ullong
             (mv (tyspecseq-ullong nil)
                 (obj-adeclor-none))
             :struct
             (mv (tyspecseq-struct type.tag)
                 (obj-adeclor-none))
             :pointer
             (b* (((mv tyspec declor)
                   (type-to-tyname-aux type.to)))
               (mv tyspec
                   (make-obj-adeclor-pointer :decl declor)))
             :array
             (b* (((mv tyspec declor)
                   (type-to-tyname-aux type.of))
                  (size (if type.size (positive-to-iconst type.size)
                          nil)))
               (mv tyspec
                   (make-obj-adeclor-array :decl declor
                                           :size size))))))

Theorem: tyspecseqp-of-type-to-tyname-aux.tyspec

(defthm tyspecseqp-of-type-to-tyname-aux.tyspec
  (b* (((mv ?tyspec ?declor)
        (type-to-tyname-aux type)))
    (tyspecseqp tyspec))
  :rule-classes :rewrite)

Theorem: obj-adeclorp-of-type-to-tyname-aux.declor

(defthm obj-adeclorp-of-type-to-tyname-aux.declor
  (b* (((mv ?tyspec ?declor)
        (type-to-tyname-aux type)))
    (obj-adeclorp declor))
  :rule-classes :rewrite)

Theorem: type-to-tyname-aux-of-type-fix-type

(defthm type-to-tyname-aux-of-type-fix-type
  (equal (type-to-tyname-aux (type-fix type))
         (type-to-tyname-aux type)))

Theorem: type-to-tyname-aux-type-equiv-congruence-on-type

(defthm type-to-tyname-aux-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (type-to-tyname-aux type)
                  (type-to-tyname-aux type-equiv)))
  :rule-classes :congruence)

Function: type-to-tyname

(defun type-to-tyname (type)
  (declare (xargs :guard (typep type)))
  (let ((__function__ 'type-to-tyname))
    (declare (ignorable __function__))
    (b* (((mv tyspec declor)
          (type-to-tyname-aux type)))
      (make-tyname :tyspec tyspec
                   :declor declor))))

Theorem: tynamep-of-type-to-tyname

(defthm tynamep-of-type-to-tyname
  (b* ((tyname (type-to-tyname type)))
    (tynamep tyname))
  :rule-classes :rewrite)

Theorem: type-to-tyname-of-type-fix-type

(defthm type-to-tyname-of-type-fix-type
  (equal (type-to-tyname (type-fix type))
         (type-to-tyname type)))

Theorem: type-to-tyname-type-equiv-congruence-on-type

(defthm type-to-tyname-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (type-to-tyname type)
                  (type-to-tyname type-equiv)))
  :rule-classes :congruence)