Macro to prove and record the primary input and output types of an ACL2 function.
This has to be used on the functions of interest
(i.e. functions for which we want to generate Java code)
prior to calling ATJ,
so that ATJ can take advantage of the type information
recorded for the functions.
This is only relevant
when
For instance, the file
If ATJ encounters a function that is not in the table, it assumes the widest possible type (i.e. the one for all ACL2 values) for all the inputs and outputs of the function. See the code generation functions for details.
Macro:
(defmacro atj-main-function-type (fn in-type-specs out-type-spec/specs &key hints) (cons 'make-event (cons (cons 'atj-main-function-type-fn (cons (cons 'quote (cons fn 'nil)) (cons (cons 'quote (cons in-type-specs 'nil)) (cons (cons 'quote (cons out-type-spec/specs 'nil)) (cons (cons 'quote (cons hints 'nil)) '((w state))))))) 'nil)))