Add ATJ type annotations to the formal parameters and body of an ACL2 function definition.
(atj-type-annotate-formals+body formals body in-types out-types mv-typess guards$ wrld) → (mv annotated-formals annotated-body new-mv-typess)
The input and output types of the function are supplied as arguments.
We annotate the body, using the output types as the required types.
We initialize the variable-type alist
to assign the input types to the formal parameters.
We also annotate the formal parameters,
but note that
We collect all the mv types in the body for which we will need to generate mv classes.
Function:
(defun atj-type-annotate-formals+body (formals body in-types out-types mv-typess guards$ wrld) (declare (xargs :guard (and (symbol-listp formals) (pseudo-termp body) (atj-type-listp in-types) (atj-type-listp out-types) (atj-type-list-listp mv-typess) (booleanp guards$) (plist-worldp wrld)))) (declare (xargs :guard (and (int= (len formals) (len in-types)) (consp out-types) (cons-listp mv-typess)))) (let ((__function__ 'atj-type-annotate-formals+body)) (declare (ignorable __function__)) (b* ((var-types (pairlis$ formals in-types)) (formals (atj-type-annotate-vars formals in-types)) ((mv body & mv-typess) (atj-type-annotate-term body out-types var-types mv-typess guards$ wrld))) (mv formals body mv-typess))))
Theorem:
(defthm symbol-listp-of-atj-type-annotate-formals+body.annotated-formals (b* (((mv ?annotated-formals ?annotated-body ?new-mv-typess) (atj-type-annotate-formals+body formals body in-types out-types mv-typess guards$ wrld))) (symbol-listp annotated-formals)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atj-type-annotate-formals+body.annotated-body (b* (((mv ?annotated-formals ?annotated-body ?new-mv-typess) (atj-type-annotate-formals+body formals body in-types out-types mv-typess guards$ wrld))) (pseudo-termp annotated-body)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-type-annotate-formals+body.new-mv-typess (b* (((mv ?annotated-formals ?annotated-body ?new-mv-typess) (atj-type-annotate-formals+body formals body in-types out-types mv-typess guards$ wrld))) (and (atj-type-list-listp new-mv-typess) (cons-listp new-mv-typess))) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-annotate-formals+body.new-formals (b* (((mv ?annotated-formals ?annotated-body ?new-mv-typess) (atj-type-annotate-formals+body formals body in-types out-types mv-typess guards$ wrld))) (equal (len annotated-formals) (len formals))))