Top-level event generated by atj-main-function-type.
(atj-main-function-type-fn fn in-type-specs out-type-spec/specs hints wrld) → event
This includes the theorems for the function inputs and outputs (if the function is in logic mode), as well as an event to record the function type in the table.
If the table already includes an entry for the function, the proposed function type is compared with the existing one. If they are the same, the call is considered redundant and no further action is taken. If they differ, it is an error.
Function:
(defun atj-main-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-main-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)) ((when fn-info?) (b* ((main (atj-function-type-info->main fn-info?))) (if (and (equal (atj-function-type->inputs main) in-types) (equal (atj-function-type->outputs main) out-types)) '(value-triple :redundant) (raise "The proposed ATJ main function type [~x0 -> ~x1] for ~x2 ~ differs from the already recorded [~x3 -> ~x4]." in-type-specs out-type-spec/specs fn (atj-type-list-to-keyword-list (atj-function-type->inputs main)) (atj-type-list-to-keyword-list (atj-function-type->outputs main)))))) (guard (guard fn nil wrld)) (input-thms (and (logicp fn wrld) (atj-main-function-type-input-theorems fn guard formals in-types hints wrld))) (output-thms (and (logicp fn wrld) (if (= nresults 1) (list (atj-main-function-type-output-theorem fn guard formals nil (car out-types) hints wrld)) (atj-main-function-type-output-theorems fn guard formals nresults (rev out-types) hints wrld)))) (fn-ty (make-atj-function-type :inputs in-types :outputs out-types :arrays arrays)) (fn-info (make-atj-function-type-info :main fn-ty :others nil))) (cons 'encapsulate (cons 'nil (cons '(set-ignore-ok t) (append input-thms (append output-thms (cons (cons 'table (cons *atj-function-type-info-table-name* (cons (cons 'quote (cons fn 'nil)) (cons (cons 'quote (cons fn-info 'nil)) 'nil)))) 'nil)))))))))