		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Subtypep

Check if a type is a subtype of another type.

Signature
(subtypep sub sup tops) → yes/no
Arguments: sub — Guard (typep sub).; sup — Guard (typep sup).; tops — Guard (toplevel-listp tops).
Returns: yes/no — Type (booleanp 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 sub is a subtype of sup, we first check if they are the same type. Otherwise, the subtype relation cannot hold unless sub has a direct supertype. If the latter is the same as sup, the subtype relation holds. Otherwise, we recursively check whether the direct supertype is a subtype of sup.

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 nil (i.e. no subtype relation) if we detect a circularity. The length of the list is the measure for termination.

Definitions and Theorems

Function: subtypep-aux

(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: booleanp-of-subtypep-aux

(defthm booleanp-of-subtypep-aux
  (b* ((yes/no (subtypep-aux sub sup defined-names tops)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: subtypep-aux-of-type-fix-sub

(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: subtypep-aux-type-equiv-congruence-on-sub

(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: subtypep-aux-of-type-fix-sup

(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: subtypep-aux-type-equiv-congruence-on-sup

(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: subtypep-aux-of-identifier-list-fix-defined-names

(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: subtypep-aux-identifier-list-equiv-congruence-on-defined-names

(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: subtypep-aux-of-toplevel-list-fix-tops

(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: subtypep-aux-toplevel-list-equiv-congruence-on-tops

(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: subtypep

(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: booleanp-of-subtypep

(defthm booleanp-of-subtypep
  (b* ((yes/no (subtypep sub sup tops)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: subtypep-of-type-fix-sub

(defthm subtypep-of-type-fix-sub
  (equal (subtypep (type-fix sub) sup tops)
         (subtypep sub sup tops)))

Theorem: subtypep-type-equiv-congruence-on-sub

(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: subtypep-of-type-fix-sup

(defthm subtypep-of-type-fix-sup
  (equal (subtypep sub (type-fix sup) tops)
         (subtypep sub sup tops)))

Theorem: subtypep-type-equiv-congruence-on-sup

(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: subtypep-of-toplevel-list-fix-tops

(defthm subtypep-of-toplevel-list-fix-tops
  (equal (subtypep sub sup (toplevel-list-fix tops))
         (subtypep sub sup tops)))

Theorem: subtypep-toplevel-list-equiv-congruence-on-tops

(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)