Partial order over all the ATJ types.
The ATJ types form a partial order.
The ordering on the
This definition of partial order is motivated by
the automatic conversions that we want to allow,
in the generated Java code,
between (the Java representations of) the ACL2 values denoted by the types.
While we want to allow conversions between the
More precisely, a type is less than another type if and only if, in the generated Java code, values of the Java type denoted by the smaller ATJ type can be automatically converted (possibly via a no-op, but not necessarily) to values of the Java type denoted by the larger ATJ type. This happens, for instance, when a value of the smaller type is passed to a function whose formal argument has the larger type: if the two types were not related like that, ATJ's type analysis would disallow the function call.
Furthermore, a type may be less than another type only if the ACL2 predicate denoted by the first type is a subset of the ACL2 predicate denoted by the second ATJ type; this is a necessary but not sufficient condition. The reason for this necessary condition is that, in ATJ's type analysis, the types of the branches of an if are merged via the least upper bound operation for the partial order: therefore, it must be the case that ACL2 values of a smaller type are also ACL2 values of a larger type.
For the
On the other hand, we do not want any automatic conversions
among the
To validate this definition of partial order, we prove that the relation is indeed a partial order, i.e. reflexive, anti-symmetric, and transitive. We also prove that atj-type-to-pred is monotonic, i.e. that for each subtype/supertype pair each value satisfying the subtype's predicate also satisfies the supertype's predicate; we generate a theorem for each such pair, because the predicate inclusion relation is at the meta level. The monotonicity theorem validates that the partial order satisfies the necessary condition described above.
While atj-type-to-pred is order-presering (i.e. monotonic),
it is not order-reflecting (and thus not an order embedding):
if
Function:
(defun atj-type-<= (sub sup) (declare (xargs :guard (and (atj-typep sub) (atj-typep sup)))) (let ((__function__ 'atj-type-<=)) (declare (ignorable __function__)) (atj-type-case sub :acl2 (atj-type-case sup :acl2 (atj-atype-<= sub.get sup.get) :jprim nil :jprimarr nil) :jprim (atj-type-case sup :acl2 nil :jprim (primitive-type-equiv sub.get sup.get) :jprimarr nil) :jprimarr (atj-type-case sup :acl2 nil :jprim nil :jprimarr (primitive-type-equiv sub.comp sup.comp)))))
Theorem:
(defthm booleanp-of-atj-type-<= (b* ((yes/no (atj-type-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-<=-reflexive (implies (atj-type-equiv x y) (atj-type-<= x y)))
Theorem:
(defthm atj-type-<=-antisymmetric (implies (and (atj-type-<= x y) (atj-type-<= y x)) (atj-type-equiv x y)))
Theorem:
(defthm atj-type-<=-transitive (implies (and (atj-type-<= x y) (atj-type-<= y z)) (atj-type-<= x z)))
Function:
(defun atj-type-to-pred-gen-mono-thm (sub sup) (declare (xargs :guard (and (atj-typep sub) (atj-typep sup)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thm)) (declare (ignorable __function__)) (if (atj-type-<= sub sup) (cons (cons 'defthm (cons (packn (list 'atj-type-to-pred-thm- (atj-type-to-keyword sub) '- (atj-type-to-keyword sup))) (cons (cons 'implies (cons (cons (atj-type-to-pred sub) '(val)) (cons (cons (atj-type-to-pred sup) '(val)) 'nil))) '(:rule-classes nil)))) 'nil) nil)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-of-atj-type-fix-sub (equal (atj-type-to-pred-gen-mono-thm (atj-type-fix sub) sup) (atj-type-to-pred-gen-mono-thm sub sup)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-atj-type-equiv-congruence-on-sub (implies (atj-type-equiv sub sub-equiv) (equal (atj-type-to-pred-gen-mono-thm sub sup) (atj-type-to-pred-gen-mono-thm sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-of-atj-type-fix-sup (equal (atj-type-to-pred-gen-mono-thm sub (atj-type-fix sup)) (atj-type-to-pred-gen-mono-thm sub sup)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-atj-type-equiv-congruence-on-sup (implies (atj-type-equiv sup sup-equiv) (equal (atj-type-to-pred-gen-mono-thm sub sup) (atj-type-to-pred-gen-mono-thm sub sup-equiv))) :rule-classes :congruence)
Function:
(defun atj-type-to-pred-gen-mono-thms-1 (sub sups) (declare (xargs :guard (and (atj-typep sub) (atj-type-listp sups)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thms-1)) (declare (ignorable __function__)) (cond ((endp sups) nil) (t (append (atj-type-to-pred-gen-mono-thm sub (car sups)) (atj-type-to-pred-gen-mono-thms-1 sub (cdr sups)))))))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-of-atj-type-fix-sub (equal (atj-type-to-pred-gen-mono-thms-1 (atj-type-fix sub) sups) (atj-type-to-pred-gen-mono-thms-1 sub sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-atj-type-equiv-congruence-on-sub (implies (atj-type-equiv sub sub-equiv) (equal (atj-type-to-pred-gen-mono-thms-1 sub sups) (atj-type-to-pred-gen-mono-thms-1 sub-equiv sups))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-of-atj-type-list-fix-sups (equal (atj-type-to-pred-gen-mono-thms-1 sub (atj-type-list-fix sups)) (atj-type-to-pred-gen-mono-thms-1 sub sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-1-atj-type-list-equiv-congruence-on-sups (implies (atj-type-list-equiv sups sups-equiv) (equal (atj-type-to-pred-gen-mono-thms-1 sub sups) (atj-type-to-pred-gen-mono-thms-1 sub sups-equiv))) :rule-classes :congruence)
Function:
(defun atj-type-to-pred-gen-mono-thms-2 (subs sups) (declare (xargs :guard (and (atj-type-listp subs) (atj-type-listp sups)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thms-2)) (declare (ignorable __function__)) (cond ((endp subs) nil) (t (append (atj-type-to-pred-gen-mono-thms-1 (car subs) sups) (atj-type-to-pred-gen-mono-thms-2 (cdr subs) sups))))))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-of-atj-type-list-fix-subs (equal (atj-type-to-pred-gen-mono-thms-2 (atj-type-list-fix subs) sups) (atj-type-to-pred-gen-mono-thms-2 subs sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-atj-type-list-equiv-congruence-on-subs (implies (atj-type-list-equiv subs subs-equiv) (equal (atj-type-to-pred-gen-mono-thms-2 subs sups) (atj-type-to-pred-gen-mono-thms-2 subs-equiv sups))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-of-atj-type-list-fix-sups (equal (atj-type-to-pred-gen-mono-thms-2 subs (atj-type-list-fix sups)) (atj-type-to-pred-gen-mono-thms-2 subs sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-atj-type-list-equiv-congruence-on-sups (implies (atj-type-list-equiv sups sups-equiv) (equal (atj-type-to-pred-gen-mono-thms-2 subs sups) (atj-type-to-pred-gen-mono-thms-2 subs sups-equiv))) :rule-classes :congruence)
Function:
(defun atj-type-to-pred-gen-mono-thms nil (declare (xargs :guard t)) (let ((__function__ 'atj-type-to-pred-gen-mono-thms)) (declare (ignorable __function__)) (b* ((types (list (atj-type-acl2 (atj-atype-integer)) (atj-type-acl2 (atj-atype-rational)) (atj-type-acl2 (atj-atype-number)) (atj-type-acl2 (atj-atype-character)) (atj-type-acl2 (atj-atype-string)) (atj-type-acl2 (atj-atype-symbol)) (atj-type-acl2 (atj-atype-boolean)) (atj-type-acl2 (atj-atype-cons)) (atj-type-acl2 (atj-atype-value)) (atj-type-jprim (primitive-type-boolean)) (atj-type-jprim (primitive-type-char)) (atj-type-jprim (primitive-type-byte)) (atj-type-jprim (primitive-type-short)) (atj-type-jprim (primitive-type-int)) (atj-type-jprim (primitive-type-long)) (atj-type-jprim (primitive-type-float)) (atj-type-jprim (primitive-type-double)) (atj-type-jprimarr (primitive-type-boolean)) (atj-type-jprimarr (primitive-type-char)) (atj-type-jprimarr (primitive-type-byte)) (atj-type-jprimarr (primitive-type-short)) (atj-type-jprimarr (primitive-type-int)) (atj-type-jprimarr (primitive-type-long)) (atj-type-jprimarr (primitive-type-float)) (atj-type-jprimarr (primitive-type-double))))) (cons 'encapsulate (cons 'nil (cons '(set-ignore-ok t) (atj-type-to-pred-gen-mono-thms-2 types types)))))))
Theorem:
(defthm atj-type-to-pred-thm-ainteger-ainteger (implies (integerp val) (integerp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-ainteger-arational (implies (integerp val) (rationalp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-ainteger-anumber (implies (integerp val) (acl2-numberp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-ainteger-avalue (implies (integerp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-arational-arational (implies (rationalp val) (rationalp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-arational-anumber (implies (rationalp val) (acl2-numberp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-arational-avalue (implies (rationalp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-anumber-anumber (implies (acl2-numberp val) (acl2-numberp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-anumber-avalue (implies (acl2-numberp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-acharacter-acharacter (implies (characterp val) (characterp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-acharacter-avalue (implies (characterp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-astring-astring (implies (stringp val) (stringp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-astring-avalue (implies (stringp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-asymbol-asymbol (implies (symbolp val) (symbolp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-asymbol-avalue (implies (symbolp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-aboolean-asymbol (implies (booleanp val) (symbolp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-aboolean-aboolean (implies (booleanp val) (booleanp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-aboolean-avalue (implies (booleanp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-acons-acons (implies (consp val) (consp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-acons-avalue (implies (consp val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-avalue-avalue (implies ((lambda (_) 't) val) ((lambda (_) 't) val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jboolean-jboolean (implies (boolean-valuep val) (boolean-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jchar-jchar (implies (char-valuep val) (char-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jbyte-jbyte (implies (byte-valuep val) (byte-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jshort-jshort (implies (short-valuep val) (short-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jint-jint (implies (int-valuep val) (int-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jlong-jlong (implies (long-valuep val) (long-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jfloat-jfloat (implies (float-valuep val) (float-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jdouble-jdouble (implies (double-valuep val) (double-valuep val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jboolean[]-jboolean[] (implies (boolean-arrayp val) (boolean-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jchar[]-jchar[] (implies (char-arrayp val) (char-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jbyte[]-jbyte[] (implies (byte-arrayp val) (byte-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jshort[]-jshort[] (implies (short-arrayp val) (short-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jint[]-jint[] (implies (int-arrayp val) (int-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jlong[]-jlong[] (implies (long-arrayp val) (long-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jfloat[]-jfloat[] (implies (float-arrayp val) (float-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-to-pred-thm-jdouble[]-jdouble[] (implies (double-arrayp val) (double-arrayp val)) :rule-classes nil)
Theorem:
(defthm atj-type-<=-of-atj-type-fix-sub (equal (atj-type-<= (atj-type-fix sub) sup) (atj-type-<= sub sup)))
Theorem:
(defthm atj-type-<=-atj-type-equiv-congruence-on-sub (implies (atj-type-equiv sub sub-equiv) (equal (atj-type-<= sub sup) (atj-type-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-<=-of-atj-type-fix-sup (equal (atj-type-<= sub (atj-type-fix sup)) (atj-type-<= sub sup)))
Theorem:
(defthm atj-type-<=-atj-type-equiv-congruence-on-sup (implies (atj-type-equiv sup sup-equiv) (equal (atj-type-<= sub sup) (atj-type-<= sub sup-equiv))) :rule-classes :congruence)