		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-disjunctions

Atj-restore-or-calls-in-term

Restore or calls in a translated term.

Signature
(atj-restore-or-calls-in-term term) → new-term
Arguments: term — Guard (pseudo-termp term).
Returns: new-term — Type (pseudo-termp new-term).

Recall that, at this point, terms have already been type-annotated. Thus, we must take the type annotations into account here, as we recognize and transform the terms.

In general, the test of an if may be type-annotated differently from its branches, even when the unannotated test is the same as a branch. The reason is that the type annotation step ensures that the branches have the same type (by inserting suitable type conversions). Thus, even though an untranslated (or a b) is translated to an unannotated (if a a b), then its annotated version may be (C1 (if (C2 a) (C3 a) (C4 b))) where C2 and C3 are different conversions. Thus, we need to unwrap the annotated test and `then' branch before comparing them for equality.

When the unwrapped test is equal to the unwrapped `then' branch, we generate the annotated (C1 (or (C3 a) (C4 b))). It is important that we take the annotated `then' branch, not the annotated test, because it is the type of the annotated `then' branch that matters with regard to the result of the disjunction.

Theorem: return-type-of-atj-restore-or-calls-in-term.new-term

(defthm return-type-of-atj-restore-or-calls-in-term.new-term
  (b* ((?new-term (atj-restore-or-calls-in-term term)))
    (pseudo-termp new-term))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-restore-or-calls-in-terms.new-terms

(defthm return-type-of-atj-restore-or-calls-in-terms.new-terms
  (b* ((?new-terms (atj-restore-or-calls-in-terms terms)))
    (pseudo-term-listp new-terms))
  :rule-classes :rewrite)

Theorem: len-of-atj-restore-or-calls-in-terms

(defthm len-of-atj-restore-or-calls-in-terms
  (b* ((?new-terms (atj-restore-or-calls-in-terms terms)))
    (equal (len new-terms) (len terms))))

Subtopics

Atj-restore-or-calls-in-terms