Return the type subset that defines a type, if any.
(get-type-subset type tops) → tsub
This is like an enriched version of direct-supertype: instead of returning just the supertype, it returns the whole type subset, consisting of the supertype, restriction, etc.
Function:
(defun get-type-subset (type tops) (declare (xargs :guard (and (typep type) (toplevel-listp tops)))) (let ((__function__ 'get-type-subset)) (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 definer.get)))))
Theorem:
(defthm maybe-type-subsetp-of-get-type-subset (b* ((tsub (get-type-subset type tops))) (maybe-type-subsetp tsub)) :rule-classes :rewrite)
Theorem:
(defthm defined-type-when-get-type-subset (implies (get-type-subset type tops) (type-case type :defined)) :rule-classes :forward-chaining)
Theorem:
(defthm get-type-subset-of-type-fix-type (equal (get-type-subset (type-fix type) tops) (get-type-subset type tops)))
Theorem:
(defthm get-type-subset-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (get-type-subset type tops) (get-type-subset type-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm get-type-subset-of-toplevel-list-fix-tops (equal (get-type-subset type (toplevel-list-fix tops)) (get-type-subset type tops)))
Theorem:
(defthm get-type-subset-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (get-type-subset type tops) (get-type-subset type tops-equiv))) :rule-classes :congruence)