Supremum (i.e. least upper bound) of two Syntheto types.
(supremum-type type1 type2 tops) → supremum?
If one type is a subtype of the other, the latter is the supremum.
Otherwise, we move up one step from either type if possible
(i.e. if the chosen type has a direct one),
and continue like that.
It does not matter which type we choose.
If the two types have a supremum, all paths converge to it.
Here we always choose the first type,
The discussion in subtypep
about well-formedness and circularities
applies here.
We use the same approach to ensure termination.
We return
Function:
(defun supremum-type-aux (type1 type2 defined-names tops) (declare (xargs :guard (and (typep type1) (typep type2) (identifier-listp defined-names) (toplevel-listp tops)))) (let ((__function__ 'supremum-type-aux)) (declare (ignorable __function__)) (b* ((defined-names (identifier-list-fix defined-names)) ((when (subtypep type1 type2 tops)) (type-fix type2)) ((when (subtypep type2 type1 tops)) (type-fix type1)) (direct (direct-supertype type1 tops))) (and direct (b* ((name (type-defined->name type1))) (and (member-equal name defined-names) (supremum-type-aux direct type2 (remove1-equal name defined-names) tops)))))))
Theorem:
(defthm maybe-typep-of-supremum-type-aux (b* ((supremum? (supremum-type-aux type1 type2 defined-names tops))) (maybe-typep supremum?)) :rule-classes :rewrite)
Theorem:
(defthm supremum-type-aux-of-type-fix-type1 (equal (supremum-type-aux (type-fix type1) type2 defined-names tops) (supremum-type-aux type1 type2 defined-names tops)))
Theorem:
(defthm supremum-type-aux-type-equiv-congruence-on-type1 (implies (type-equiv type1 type1-equiv) (equal (supremum-type-aux type1 type2 defined-names tops) (supremum-type-aux type1-equiv type2 defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-aux-of-type-fix-type2 (equal (supremum-type-aux type1 (type-fix type2) defined-names tops) (supremum-type-aux type1 type2 defined-names tops)))
Theorem:
(defthm supremum-type-aux-type-equiv-congruence-on-type2 (implies (type-equiv type2 type2-equiv) (equal (supremum-type-aux type1 type2 defined-names tops) (supremum-type-aux type1 type2-equiv defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-aux-of-identifier-list-fix-defined-names (equal (supremum-type-aux type1 type2 (identifier-list-fix defined-names) tops) (supremum-type-aux type1 type2 defined-names tops)))
Theorem:
(defthm supremum-type-aux-identifier-list-equiv-congruence-on-defined-names (implies (identifier-list-equiv defined-names defined-names-equiv) (equal (supremum-type-aux type1 type2 defined-names tops) (supremum-type-aux type1 type2 defined-names-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-aux-of-toplevel-list-fix-tops (equal (supremum-type-aux type1 type2 defined-names (toplevel-list-fix tops)) (supremum-type-aux type1 type2 defined-names tops)))
Theorem:
(defthm supremum-type-aux-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (supremum-type-aux type1 type2 defined-names tops) (supremum-type-aux type1 type2 defined-names tops-equiv))) :rule-classes :congruence)
Function:
(defun supremum-type (type1 type2 tops) (declare (xargs :guard (and (typep type1) (typep type2) (toplevel-listp tops)))) (let ((__function__ 'supremum-type)) (declare (ignorable __function__)) (supremum-type-aux type1 type2 (get-defined-type-names tops) tops)))
Theorem:
(defthm maybe-typep-of-supremum-type (b* ((supremum? (supremum-type type1 type2 tops))) (maybe-typep supremum?)) :rule-classes :rewrite)
Theorem:
(defthm supremum-type-of-type-fix-type1 (equal (supremum-type (type-fix type1) type2 tops) (supremum-type type1 type2 tops)))
Theorem:
(defthm supremum-type-type-equiv-congruence-on-type1 (implies (type-equiv type1 type1-equiv) (equal (supremum-type type1 type2 tops) (supremum-type type1-equiv type2 tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-of-type-fix-type2 (equal (supremum-type type1 (type-fix type2) tops) (supremum-type type1 type2 tops)))
Theorem:
(defthm supremum-type-type-equiv-congruence-on-type2 (implies (type-equiv type2 type2-equiv) (equal (supremum-type type1 type2 tops) (supremum-type type1 type2-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-of-toplevel-list-fix-tops (equal (supremum-type type1 type2 (toplevel-list-fix tops)) (supremum-type type1 type2 tops)))
Theorem:
(defthm supremum-type-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (supremum-type type1 type2 tops) (supremum-type type1 type2 tops-equiv))) :rule-classes :congruence)