		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-type-annotation

Atj-types-of-conv

Source and destination ATJ types of a conversion function.

Signature
(atj-types-of-conv conv) → (mv src-types dst-types)
Arguments: conv — Guard (symbolp conv).
Returns: src-types — Type (atj-type-listp src-types).; dst-types — Type (atj-type-listp dst-types).

This is the inverse of atj-type-conv.

Definitions and Theorems

Function: atj-types-of-conv

(defun atj-types-of-conv (conv)
  (declare (xargs :guard (symbolp conv)))
  (let ((__function__ 'atj-types-of-conv))
    (declare (ignorable __function__))
    (b* ((string (symbol-name conv))
         ((unless (and (> (length string) 0)
                       (eql (char string 0) #\[)
                       (eql (char string (1- (length string)))
                            #\])))
          (raise "Internal error: ~x0 is not a conversion function."
                 conv)
          (mv (list (atj-type-irrelevant))
              (list (atj-type-irrelevant))))
         (pos (position #\> string))
         ((unless (natp pos))
          (raise "Internal error: ~x0 is not a conversion function."
                 conv)
          (mv (list (atj-type-irrelevant))
              (list (atj-type-irrelevant))))
         (src-id (subseq string 1 pos))
         (dst-id (subseq string (1+ pos)
                         (1- (length string))))
         (src-types (atj-types-of-id src-id))
         (dst-types (atj-types-of-id dst-id)))
      (mv src-types dst-types))))

Theorem: atj-type-listp-of-atj-types-of-conv.src-types

(defthm atj-type-listp-of-atj-types-of-conv.src-types
  (b* (((mv ?src-types ?dst-types)
        (atj-types-of-conv conv)))
    (atj-type-listp src-types))
  :rule-classes :rewrite)

Theorem: atj-type-listp-of-atj-types-of-conv.dst-types

(defthm atj-type-listp-of-atj-types-of-conv.dst-types
  (b* (((mv ?src-types ?dst-types)
        (atj-types-of-conv conv)))
    (atj-type-listp dst-types))
  :rule-classes :rewrite)

Theorem: consp-of-atj-types-of-conv.src-types

(defthm consp-of-atj-types-of-conv.src-types
  (b* (((mv ?src-types ?dst-types)
        (atj-types-of-conv conv)))
    (consp src-types))
  :rule-classes :type-prescription)

Theorem: consp-of-atj-types-of-conv.dst-types

(defthm consp-of-atj-types-of-conv.dst-types
  (b* (((mv ?src-types ?dst-types)
        (atj-types-of-conv conv)))
    (consp dst-types))
  :rule-classes :type-prescription)