Top-level event generated by atj-other-function-type.
(atj-other-function-type-fn fn in-type-specs out-type-spec/specs hints wrld) → event
This includes the theorem(s) stating that the guard and input types imply the output type(s), as well as an event to record the function type in the table.
It is an error if the function does not have a primary type already; that is, atj-main-function-type must be called before calling atj-other-function-type.
The proposed input types must be narrower than the primary input types; otherwise, there would be no advantage in adding these secondary input types, and in generating overloaded method corresponding to these types. The proposed output types must be narrower than or the same as the primary output types: since the primary output types are proved under the guard assumption only, while the secondary output types are proved with additional type hypotheses, it does not make sense that the secondary output types is wider than, or unrelated to, the primary output types; this situation probably signals the misstatement of some types to either atj-main-function-type or atj-other-function-type.
If the proposed function type is already in the table, the call of atj-other-function-type is considered redundant and no further action is taken.
We also ensure that the addition of the proposed types does not cause type ambiguities: see atj-check-other-function-type for details.
We may add additional sanity checks in the future, e.g. that if the new input types are narrower than or equal to some already existing secondary types, then the output types must satisfy that relation too. The reason is analogous to the one discussed above to motivate the check against the primary output types; but here we are talking about the secondary output types.
Function:
(defun atj-other-function-type-fn (fn in-type-specs out-type-spec/specs hints wrld) (declare (xargs :guard (and (true-listp hints) (plist-worldp wrld)))) (let ((__function__ 'atj-other-function-type-fn)) (declare (ignorable __function__)) (b* (((unless (function-namep fn wrld)) (raise "The first input, ~x0, must be the name of a function." fn)) (formals (formals fn wrld)) ((unless (keyword-listp in-type-specs)) (raise "The second input, ~x0, ~ must be a list of ATJ type keywords." in-type-specs)) (in-types (atj-type-list-from-keyword-list in-type-specs)) ((unless (= (len in-types) (len formals))) (raise "The number of input types ~x0 must match ~ the arity ~x1 of the function ~x2." in-type-specs (len formals) fn)) (nresults (atj-number-of-results fn wrld)) ((mv out-types arrays) (if (= nresults 1) (b* (((mv out-type array) (atj-process-output-type-spec out-type-spec/specs formals in-types))) (mv (list out-type) (list array))) (if (tuplep nresults out-type-spec/specs) (atj-process-output-type-specs out-type-spec/specs formals in-types) (prog2$ (raise "The third input, ~x0, ~ must be a list of length ~x1 ~ of output type specifications." out-type-spec/specs nresults) (mv nil nil))))) ((unless (no-duplicatesp-eq (remove-eq nil arrays))) (raise "The list of output array names, ~x0, ~ contains non-NIL duplicates." arrays)) (fn-info? (atj-get-function-type-info-from-table fn wrld)) ((unless fn-info?) (raise "The function ~x0 does not have a primary function type yet. ~ Use ATJ-MAIN-FUNCTION-TYPE to define it, ~ and then try again this ATJ-OTHER-FUNCTION-TYPE." fn)) (main-fn-type (atj-function-type-info->main fn-info?)) (main-in-types (atj-function-type->inputs main-fn-type)) (main-out-types (atj-function-type->outputs main-fn-type)) ((unless (atj-type-list-< in-types main-in-types)) (raise "The proposed inputs types ~x0 must be strictly narrower ~ than the primary input types ~x1." in-type-specs (atj-type-list-to-keyword-list main-in-types))) ((unless (atj-type-list-<= out-types main-out-types)) (raise "The proposed output types ~x0 must be ~ narrower than or equal to, ~ the primary output types ~x1." out-type-spec/specs (atj-type-list-to-keyword-list main-out-types))) (other-fn-types (atj-function-type-info->others fn-info?)) (new-fn-type (make-atj-function-type :inputs in-types :outputs out-types :arrays (repeat nresults nil))) ((when (member-equal new-fn-type other-fn-types)) '(value-triple :redundant)) (other-in-types (atj-function-type-list->inputs other-fn-types)) (all-in-typess (cons in-types other-in-types)) (- (atj-check-other-function-type in-types other-fn-types all-in-typess)) (guard (guard fn nil wrld)) (thms (if (= nresults 1) (list (atj-other-function-type-theorem fn guard formals in-types nil (car out-types) hints wrld)) (atj-other-function-type-theorems fn guard formals in-types nresults out-types hints wrld))) (new-fn-info (change-atj-function-type-info fn-info? :others (cons new-fn-type other-fn-types)))) (cons 'encapsulate (cons 'nil (cons '(set-ignore-ok t) (append thms (cons (cons 'table (cons *atj-function-type-info-table-name* (cons (cons 'quote (cons fn 'nil)) (cons (cons 'quote (cons new-fn-info 'nil)) 'nil)))) 'nil))))))))