• 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
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
        • Process-syntheto-toplevel-fn
        • Translation
        • Language
          • Static-semantics
          • Abstract-syntax
          • Outcome
          • Abstract-syntax-operations
            • Subst-expression-fns
            • Field-list-to-typed-variable-list
            • Negate-expression
            • Get-function-definition-in-function-definitions
            • Get-function-definition
            • Get-type-definition-in-type-definitions
            • Get-type-definition
            • Get-function-specification
            • Get-type-subset
            • Get-alternative-product
            • Direct-supertype
            • Get-function-header-in-list
            • Equate-expression-lists
            • Get-field-type
            • Get-theorem
            • Get-defined-type-names-in-type-definitions
            • Disjoin-expressions
            • Conjoin-expressions
            • Get-type-product
            • Binary-op-nonstrictp
            • Get-type-sum
            • Get-defined-type-names
            • Equate-expressions
            • Field-to-typed-variable
            • Subst-expression
            • Binary-op-strictp
            • Initializer-list-from-flds-vals
            • Typed-variable-list->-expression-variable-list
            • Typed-variable-list->-expression
            • Variable-substitution
            • Local-variables
            • Identifier-list-names
            • Functions-called
            • Subst-expression-list
            • Subst-branch-list
            • Subst-branch
          • Outcome-list
          • Outcomes
        • Process-syntheto-toplevel
        • Shallow-embedding
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Abstract-syntax-operations

Get-type-definition

Find the definition of a type with a given name in a list of top-level constructs.

Signature

(get-type-definition name tops) → typedef?

Arguments

name — Guard (identifierp name).

tops — Guard (toplevel-listp tops).

Returns

typedef? — Type (maybe-type-definitionp typedef?).

We look both at the type definitions at the top level and at the type definitions inside the type recursions.

We return nil if the type definition is not found.

We look up the top-level constructs in order. In well-formed lists of top-level constructs, the defined type names are unique, so any order would yield the same result.

Definitions and Theorems

Function: get-type-definition

(defun get-type-definition (name tops)
 (declare (xargs :guard (and (identifierp name)
                             (toplevel-listp tops))))
 (let ((__function__ 'get-type-definition))
  (declare (ignorable __function__))
  (b* (((when (endp tops)) nil)
       (top (car tops)))
   (toplevel-case
     top :type
     (if (identifier-equiv name (type-definition->name top.get))
         top.get
       (get-type-definition name (cdr tops)))
     :types
     (b* ((definition? (get-type-definition-in-type-definitions
                            name
                            (type-recursion->definitions top.get))))
       (or definition?
           (get-type-definition name (cdr tops))))
     :function (get-type-definition name (cdr tops))
     :functions (get-type-definition name (cdr tops))
     :specification (get-type-definition name (cdr tops))
     :theorem (get-type-definition name (cdr tops))
     :transform (get-type-definition name (cdr tops))))))

Theorem: maybe-type-definitionp-of-get-type-definition

(defthm maybe-type-definitionp-of-get-type-definition
  (b* ((typedef? (get-type-definition name tops)))
    (maybe-type-definitionp typedef?))
  :rule-classes :rewrite)

Theorem: get-type-definition-of-identifier-fix-name

(defthm get-type-definition-of-identifier-fix-name
  (equal (get-type-definition (identifier-fix name)
                              tops)
         (get-type-definition name tops)))

Theorem: get-type-definition-identifier-equiv-congruence-on-name

(defthm get-type-definition-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-type-definition name tops)
                  (get-type-definition name-equiv tops)))
  :rule-classes :congruence)

Theorem: get-type-definition-of-toplevel-list-fix-tops

(defthm get-type-definition-of-toplevel-list-fix-tops
  (equal (get-type-definition name (toplevel-list-fix tops))
         (get-type-definition name tops)))

Theorem: get-type-definition-toplevel-list-equiv-congruence-on-tops

(defthm get-type-definition-toplevel-list-equiv-congruence-on-tops
  (implies (toplevel-list-equiv tops tops-equiv)
           (equal (get-type-definition name tops)
                  (get-type-definition name tops-equiv)))
  :rule-classes :congruence)