Wrap an ACL2 term with a type conversion function.
(atj-type-wrap-term term src-types dst-types?) → wrapped-term
The conversion is from the source types to the destination types. If the destination types are the empty list, they are treated as if they were equal to the source types, i.e. the conversion is a no-op.
If the destination type list is not empty, we ensure that the conversion is allowed. If it is not, we stop with an error: this is a ``deep'' input validation error, because the problem is in the ACL2 code provided by the user.
Function:
(defun atj-type-wrap-term (term src-types dst-types?) (declare (xargs :guard (and (pseudo-termp term) (atj-type-listp src-types) (atj-type-listp dst-types?)))) (declare (xargs :guard (consp src-types))) (let ((__function__ 'atj-type-wrap-term)) (declare (ignorable __function__)) (b* (((unless (mbt (pseudo-termp term))) nil) ((when (and (consp dst-types?) (not (atj-types-conv-allowed-p src-types dst-types?)))) (raise "Type annotation failure: ~ cannot convert from ~x0 to ~x1." src-types dst-types?)) (conv (if dst-types? (atj-type-conv src-types dst-types?) (atj-type-conv src-types src-types)))) (fcons-term* conv term))))
Theorem:
(defthm pseudo-termp-of-atj-type-wrap-term (b* ((wrapped-term (atj-type-wrap-term term src-types dst-types?))) (pseudo-termp wrapped-term)) :rule-classes :rewrite)