Check the new input types passed to atj-other-function-type against the existing function types.
(atj-check-other-function-type new-in-types old-fn-types all-in-typess) → yes/no
The primary and secondary input types attached to a function
are used to generate overloaded methods for the function.
It must be possible, at compile time, to always resolve the method,
based on the most specific argument types.
This should be guaranteed if the set of all the function's input types
(more precisely, the set of all the input type tuples of the function)
is closed under greatest lower bounds that do not include
For example, consider a binary function
Generalizing from this example,
we want the set of all function input types
to be closed under greatest lower bounds.
This way, if some tuple of actual arguments
fits two different overloaded methods,
it will also fit the method corresponding to the greatest lower bound;
therefore, there will be always a ``minimum'' method
that will be selected at compile time and called at run time.
However, recall that atj-type-meet may produce
We calculate these greatest lower bounds on ATJ types, not on the corresponding Java types, even though it is the Java types that are used to resolve the overloaded methods in the Java code. This way, we have more flexibility in mapping ATJ types that are related in the ATJ type partial order to Java types that are not related in the Java type partial order.
The closure property is also needed for ATJ's type annotations. When type-annotating a function call, the arguments are type-annotated first. Based on the initially inferred types of the arguments, a (primary or secondary) function type is searched that matches those inferred types. This may or may not be found (and in the latter case automatic conversions are inserted to the primary input types of the function), but if one exists, it must be unque to avoid an ambiguity. The closure property ensures this.
Besides the closure property just explained, we also ensure that the proposed new input types differ from all the existing input types. We maintain the uniqueness, for each function, of the (primary and secondary) input types in the table, so that there is exactly one overloaded method for each input type tuple. Redundant calls of atj-other-function-type are handled before calling this function.
The
Function:
(defun atj-check-other-function-type (new-in-types old-fn-types all-in-typess) (declare (xargs :guard (and (atj-type-listp new-in-types) (atj-function-type-listp old-fn-types) (atj-type-list-listp all-in-typess)))) (let ((__function__ 'atj-check-other-function-type)) (declare (ignorable __function__)) (b* (((when (endp old-fn-types)) t) (old-fn-type (car old-fn-types)) (old-in-types (atj-function-type->inputs old-fn-type)) ((when (equal new-in-types old-in-types)) (raise "The proposed input types ~x0 must differ from ~ the existing secondary input types ~ for the function, ~ but they are equal to some of these existing types." new-in-types)) ((unless (= (len old-in-types) (len new-in-types))) (raise "Internal error: ~ the number of proposed input types ~x0 differs from ~ the number of existing input types ~x1." new-in-types old-in-types)) (glb (atj-type-list-meet old-in-types new-in-types)) ((unless (or (member-eq nil glb) (member-equal glb all-in-typess))) (raise "The proposed input types ~x0 ~ and some existing input types ~x1, ~ have a greatest lower bound ~x2 ~ that is not in the table ~ and differs from the proposed input types. ~ This may cause type ambiguities. ~ Consider adding types ~x2 first, ~ and then the proposed input types ~x0." new-in-types old-in-types glb))) (atj-check-other-function-type new-in-types (cdr old-fn-types) all-in-typess))))
Theorem:
(defthm booleanp-of-atj-check-other-function-type (b* ((yes/no (atj-check-other-function-type new-in-types old-fn-types all-in-typess))) (booleanp yes/no)) :rule-classes :rewrite)