Process an output type specification in atj-main-function-type or atj-other-function-type.
(atj-process-output-type-spec out-type-spec formals in-types) → (mv type array)
An output type specification must be
either a keyword that denotes an ATJ type,
or a doublet consisting of a non-
Function:
(defun atj-process-output-type-spec (out-type-spec formals in-types) (declare (xargs :guard (and (symbol-listp formals) (atj-type-listp in-types)))) (declare (xargs :guard (= (len formals) (len in-types)))) (let ((__function__ 'atj-process-output-type-spec)) (declare (ignorable __function__)) (if (tuplep 2 out-type-spec) (b* (((list sym kwd) out-type-spec) ((unless (symbolp sym)) (raise "Invalid array name ~x0." sym) (mv (atj-type-irrelevant) nil)) (array sym) ((unless (keywordp kwd)) (raise "Invalid type keyword ~x0." kwd) (mv (atj-type-irrelevant) nil)) (type (atj-type-from-keyword kwd)) ((when (and sym (not (atj-type-case type :jprimarr)))) (raise "Invalid array name ~x0 for non-array type ~x1." array kwd) (mv (atj-type-irrelevant) nil)) (pos (index-of array formals)) ((when (not pos)) (raise "Array name ~x0 not among formals ~x1." array formals) (mv (atj-type-irrelevant) nil)) (in-type (nth pos in-types)) ((unless (equal type in-type)) (raise "The type ~x0 of the ~x1 input does not match ~ the type ~x2 of the ~x1 output." (atj-type-to-keyword in-type) array kwd) (mv (atj-type-irrelevant) nil))) (mv type array)) (if (keywordp out-type-spec) (mv (atj-type-from-keyword out-type-spec) nil) (prog2$ (raise "Invalid output type specification ~x0." out-type-spec) (mv (atj-type-irrelevant) nil))))))
Theorem:
(defthm atj-typep-of-atj-process-output-type-spec.type (b* (((mv common-lisp::?type common-lisp::?array) (atj-process-output-type-spec out-type-spec formals in-types))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atj-process-output-type-spec.array (b* (((mv common-lisp::?type common-lisp::?array) (atj-process-output-type-spec out-type-spec formals in-types))) (symbolp array)) :rule-classes :rewrite)