Re-wrap an ACL2 term with a type conversion function.
(atj-type-rewrap-term term dst-types) → rewrapped-term
This is used when a term is preliminarily wrapped with a type conversion function, but its wrapping is then finalized with a different conversion function. So here we replace the wrapper.
We only change the destination types of the conversion function. The source types are unchanged.
We also check that the new conversion is allowed. We stop with an error if that is not the case; as in atj-type-wrap-term, this is a ``deep'' input validation error.
If the term is a call of if, we recursively re-wrap its branches, which therefore will return the same types. Then we wrap the if call with the identity conversion. The reason for descending into the if branches is that (the least upper bound of) the types of the if branches are used, in the translation to Java, to determine the types of the Java local variables that store the result of (one or the other) branch. In order to allow the mapping of ATJ subtypes to Java non-subtypes, we need to push the conversions into the if branches.
Function:
(defun atj-type-rewrap-term (term dst-types) (declare (xargs :guard (and (pseudo-termp term) (atj-type-listp dst-types)))) (declare (xargs :guard (consp dst-types))) (let ((__function__ 'atj-type-rewrap-term)) (declare (ignorable __function__)) (b* (((mv term src-types &) (atj-type-unwrap-term term)) ((when (null term)) (raise "Internal error: unwrapped null term ~x0." term)) ((when (not (atj-types-conv-allowed-p src-types dst-types))) (raise "Type annotation failure: ~ cannot convert from ~x0 to ~x1." src-types dst-types)) ((mv ifp test then else) (check-if-call term))) (if ifp (atj-type-wrap-term (fcons-term* 'if test (atj-type-rewrap-term then dst-types) (atj-type-rewrap-term else dst-types)) dst-types dst-types) (atj-type-wrap-term term src-types dst-types)))))
Theorem:
(defthm pseudo-termp-of-atj-type-rewrap-term (b* ((rewrapped-term (atj-type-rewrap-term term dst-types))) (pseudo-termp rewrapped-term)) :rule-classes :rewrite)