Check if a type is a subtype of another type.
(subtypep sub sup tops) → yes/no
The subtype definitions in a list of Syntheto top-level constructs induce a subtype relation over types. In Syntheto, subtype means true inclusion of values, not an embedding as in other languages; thus, certain values belong to multiple types, e.g. the integer 4 belongs to the type of integers, but also to a possible subtype of natural numbers, and to a possible subtype of even numbers.
A primitive, collection, or options type is only (reflexively) a subtype of itself. Currently Syntheto's subtypes do not lift from element types to collection types. A defined type is only a subtype of itself if it is a sum or product type; otherwise, it is a subtype not only of itself, but also of its direct supertype (i.e. the one referenced in its subtype definition), and of all the direct supertype's supertypes.
Thus, to check whether
In well-formed Syntheto there are no subtype circularities
and so the recursion terminates.
However, this ACL2 function has
no assumption of well-formedness.
The latter notion needs the notion of maximal supertype to be expressed:
it may be possible to set up a large mutual recursion
to define all these concepts,
but that may increase the complexity of the static semantics.
Thus, we prefer to totalize this function here
to work on non-well-formed lists of Syntheto top-level constructs.
We extract the list of all defined type names
from the list of top-level constructs,
and use that list to look up the type definitions,
removing each used up definition from the list.
This way, circularities are detected when attempting to look up
the same definition twice, which will not be in the list the second time;
we return
Function:
(defun subtypep-aux (sub sup defined-names tops) (declare (xargs :guard (and (typep sub) (typep sup) (identifier-listp defined-names) (toplevel-listp tops)))) (let ((__function__ 'subtypep-aux)) (declare (ignorable __function__)) (b* ((defined-names (identifier-list-fix defined-names))) (or (type-equiv sub sup) (b* ((direct (direct-supertype sub tops))) (and direct (b* ((name (type-defined->name sub))) (and (member-equal name defined-names) (subtypep-aux direct sup (remove1-equal name defined-names) tops)))))))))
Theorem:
(defthm booleanp-of-subtypep-aux (b* ((yes/no (subtypep-aux sub sup defined-names tops))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm subtypep-aux-of-type-fix-sub (equal (subtypep-aux (type-fix sub) sup defined-names tops) (subtypep-aux sub sup defined-names tops)))
Theorem:
(defthm subtypep-aux-type-equiv-congruence-on-sub (implies (type-equiv sub sub-equiv) (equal (subtypep-aux sub sup defined-names tops) (subtypep-aux sub-equiv sup defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm subtypep-aux-of-type-fix-sup (equal (subtypep-aux sub (type-fix sup) defined-names tops) (subtypep-aux sub sup defined-names tops)))
Theorem:
(defthm subtypep-aux-type-equiv-congruence-on-sup (implies (type-equiv sup sup-equiv) (equal (subtypep-aux sub sup defined-names tops) (subtypep-aux sub sup-equiv defined-names tops))) :rule-classes :congruence)
Theorem:
(defthm subtypep-aux-of-identifier-list-fix-defined-names (equal (subtypep-aux sub sup (identifier-list-fix defined-names) tops) (subtypep-aux sub sup defined-names tops)))
Theorem:
(defthm subtypep-aux-identifier-list-equiv-congruence-on-defined-names (implies (identifier-list-equiv defined-names defined-names-equiv) (equal (subtypep-aux sub sup defined-names tops) (subtypep-aux sub sup defined-names-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm subtypep-aux-of-toplevel-list-fix-tops (equal (subtypep-aux sub sup defined-names (toplevel-list-fix tops)) (subtypep-aux sub sup defined-names tops)))
Theorem:
(defthm subtypep-aux-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (subtypep-aux sub sup defined-names tops) (subtypep-aux sub sup defined-names tops-equiv))) :rule-classes :congruence)
Function:
(defun subtypep (sub sup tops) (declare (xargs :guard (and (typep sub) (typep sup) (toplevel-listp tops)))) (let ((__function__ 'subtypep)) (declare (ignorable __function__)) (subtypep-aux sub sup (get-defined-type-names tops) tops)))
Theorem:
(defthm booleanp-of-subtypep (b* ((yes/no (subtypep sub sup tops))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm subtypep-of-type-fix-sub (equal (subtypep (type-fix sub) sup tops) (subtypep sub sup tops)))
Theorem:
(defthm subtypep-type-equiv-congruence-on-sub (implies (type-equiv sub sub-equiv) (equal (subtypep sub sup tops) (subtypep sub-equiv sup tops))) :rule-classes :congruence)
Theorem:
(defthm subtypep-of-type-fix-sup (equal (subtypep sub (type-fix sup) tops) (subtypep sub sup tops)))
Theorem:
(defthm subtypep-type-equiv-congruence-on-sup (implies (type-equiv sup sup-equiv) (equal (subtypep sub sup tops) (subtypep sub sup-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm subtypep-of-toplevel-list-fix-tops (equal (subtypep sub sup (toplevel-list-fix tops)) (subtypep sub sup tops)))
Theorem:
(defthm subtypep-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (subtypep sub sup tops) (subtypep sub sup tops-equiv))) :rule-classes :congruence)