Unwrap an ACL2 term wrapped by atj-type-wrap-term.
(atj-type-unwrap-term term) → (mv unwrapped-term src-types dst-types)
This is essentially the inverse function,
except that it always returns a list of destination types,
never
Function:
(defun atj-type-unwrap-term (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atj-type-unwrap-term)) (declare (ignorable __function__)) (b* ((term (if (mbt (pseudo-termp term)) term nil)) ((when (or (variablep term) (fquotep term) (flambda-applicationp term))) (raise "Internal error: the term ~x0 has the wrong format." term) (mv nil (list (atj-type-irrelevant)) (list (atj-type-irrelevant)))) (fn (ffn-symb term)) ((when (flambdap fn)) (raise "Internal error: the term ~x0 has the wrong format." term) (mv nil (list (atj-type-irrelevant)) (list (atj-type-irrelevant)))) ((mv src-types dst-types) (atj-types-of-conv fn))) (mv (fargn term 1) src-types dst-types))))
Theorem:
(defthm pseudo-termp-of-atj-type-unwrap-term.unwrapped-term (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (pseudo-termp unwrapped-term)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-listp-of-atj-type-unwrap-term.src-types (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (atj-type-listp src-types)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-listp-of-atj-type-unwrap-term.dst-types (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (atj-type-listp dst-types)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-type-unwrap-term.src-types (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (consp src-types)) :rule-classes :type-prescription)
Theorem:
(defthm consp-of-atj-type-unwrap-term.dst-types (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (consp dst-types)) :rule-classes :type-prescription)
Theorem:
(defthm acl2-count-of-atj-type-unwrap-term-linear (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (implies unwrapped-term (< (acl2-count unwrapped-term) (acl2-count term)))) :rule-classes :linear)
Theorem:
(defthm pseudo-term-count-of-atj-type-unwrap-term (b* (((mv ?unwrapped-term ?src-types ?dst-types) (atj-type-unwrap-term term))) (implies (not (pseudo-term-case unwrapped-term :null)) (< (pseudo-term-count unwrapped-term) (pseudo-term-count term)))) :rule-classes :linear)