		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-type-annotation

Atj-type-unwrap-term

Unwrap an ACL2 term wrapped by atj-type-wrap-term.

Signature
(atj-type-unwrap-term term) → (mv unwrapped-term src-types dst-types)
Arguments: term — Guard (pseudo-termp term).
Returns: unwrapped-term — Type (pseudo-termp unwrapped-term).; src-types — Type (atj-type-listp src-types).; dst-types — Type (atj-type-listp dst-types).

This is essentially the inverse function, except that it always returns a list of destination types, never nil.

Definitions and Theorems

Function: atj-type-unwrap-term

(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: pseudo-termp-of-atj-type-unwrap-term.unwrapped-term

(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: atj-type-listp-of-atj-type-unwrap-term.src-types

(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: atj-type-listp-of-atj-type-unwrap-term.dst-types

(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: consp-of-atj-type-unwrap-term.src-types

(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: consp-of-atj-type-unwrap-term.dst-types

(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: acl2-count-of-atj-type-unwrap-term-linear

(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: pseudo-term-count-of-atj-type-unwrap-term

(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)