Maximal supertype of a type.
(max-supertype type tops) → super?
We follow the chain of direct subtypes, returning the last one in the chain, which may be the starting type when it is not a subtype.
The discussion in subtypep
about well-formedness and circularities
applies here.
We use the same approach to ensure termination.
We return
Function:
(defun max-supertype-aux (type defined-names tops) (declare (xargs :guard (and (typep type) (identifier-listp defined-names) (toplevel-listp tops)))) (let ((__function__ 'max-supertype-aux)) (declare (ignorable __function__)) (b* ((defined-names (identifier-list-fix defined-names)) (direct (direct-supertype type tops))) (if direct (b* ((name (type-defined->name type))) (and (member-equal name defined-names) (max-supertype-aux direct (remove1-equal name defined-names) tops))) (type-fix type)))))
Theorem:
(defthm maybe-typep-of-max-supertype-aux (b* ((super? (max-supertype-aux type defined-names tops))) (maybe-typep super?)) :rule-classes :rewrite)
Theorem:
(defthm max-supertype-aux-of-type-fix-type (equal (max-supertype-aux (type-fix type) defined-names tops) (max-supertype-aux type defined-names tops)))
Theorem:
(defthm max-supertype-aux-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (max-supertype-aux type defined-names tops) (max-supertype-aux type-equiv defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm max-supertype-aux-of-identifier-list-fix-defined-names (equal (max-supertype-aux type (identifier-list-fix defined-names) tops) (max-supertype-aux type defined-names tops)))
Theorem:
(defthm max-supertype-aux-identifier-list-equiv-congruence-on-defined-names (implies (identifier-list-equiv defined-names defined-names-equiv) (equal (max-supertype-aux type defined-names tops) (max-supertype-aux type defined-names-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm max-supertype-aux-of-toplevel-list-fix-tops (equal (max-supertype-aux type defined-names (toplevel-list-fix tops)) (max-supertype-aux type defined-names tops)))
Theorem:
(defthm max-supertype-aux-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (max-supertype-aux type defined-names tops) (max-supertype-aux type defined-names tops-equiv))) :rule-classes :congruence)
Function:
(defun max-supertype (type tops) (declare (xargs :guard (and (typep type) (toplevel-listp tops)))) (let ((__function__ 'max-supertype)) (declare (ignorable __function__)) (max-supertype-aux type (get-defined-type-names tops) tops)))
Theorem:
(defthm maybe-typep-of-max-supertype (b* ((super? (max-supertype type tops))) (maybe-typep super?)) :rule-classes :rewrite)
Theorem:
(defthm max-supertype-of-type-fix-type (equal (max-supertype (type-fix type) tops) (max-supertype type tops)))
Theorem:
(defthm max-supertype-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (max-supertype type tops) (max-supertype type-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm max-supertype-of-toplevel-list-fix-tops (equal (max-supertype type (toplevel-list-fix tops)) (max-supertype type tops)))
Theorem:
(defthm max-supertype-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (max-supertype type tops) (max-supertype type tops-equiv))) :rule-classes :congruence)