Find the definition of a type with a given name in a list of top-level constructs.
(get-type-definition name tops) → typedef?
We look both at the type definitions at the top level and at the type definitions inside the type recursions.
We return
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.
Function:
(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:
(defthm maybe-type-definitionp-of-get-type-definition (b* ((typedef? (get-type-definition name tops))) (maybe-type-definitionp typedef?)) :rule-classes :rewrite)
Theorem:
(defthm get-type-definition-of-identifier-fix-name (equal (get-type-definition (identifier-fix name) tops) (get-type-definition name tops)))
Theorem:
(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:
(defthm get-type-definition-of-toplevel-list-fix-tops (equal (get-type-definition name (toplevel-list-fix tops)) (get-type-definition name tops)))
Theorem:
(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)