Return the direct supertype of a type, if any.
(direct-supertype type tops) → super?
Only a type defined as a subtype has a direct supertype, namely the one referenced in the subtype definition. All the other types do not.
Function:
(defun direct-supertype (type tops) (declare (xargs :guard (and (typep type) (toplevel-listp tops)))) (let ((__function__ 'direct-supertype)) (declare (ignorable __function__)) (type-case type :boolean nil :character nil :string nil :integer nil :set nil :sequence nil :map nil :option nil :defined (b* ((typedef (get-type-definition type.name tops)) ((when (not typedef)) nil) (definer (type-definition->body typedef)) ((when (not definer)) nil)) (type-definer-case definer :product nil :sum nil :subset (type-subset->supertype definer.get))))))
Theorem:
(defthm maybe-typep-of-direct-supertype (b* ((super? (direct-supertype type tops))) (maybe-typep super?)) :rule-classes :rewrite)
Theorem:
(defthm defined-type-when-direct-supertype (implies (direct-supertype type tops) (type-case type :defined)) :rule-classes :forward-chaining)
Theorem:
(defthm direct-supertype-of-type-fix-type (equal (direct-supertype (type-fix type) tops) (direct-supertype type tops)))
Theorem:
(defthm direct-supertype-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (direct-supertype type tops) (direct-supertype type-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm direct-supertype-of-toplevel-list-fix-tops (equal (direct-supertype type (toplevel-list-fix tops)) (direct-supertype type tops)))
Theorem:
(defthm direct-supertype-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (direct-supertype type tops) (direct-supertype type tops-equiv))) :rule-classes :congruence)