translate form and clean it up

Examples: :tc (member e a) :tc (list (cadr x) (loop$ for e in lst collect (+ 1 e))) :tcp (list (cadr x) (loop$ for e in lst collect (+ 1 e))) :tca (list (cadr x) (loop$ for e in lst collect (+ 1 e))) General Form: :tc form :tca form :tcp form (tc 'form) (tca 'form) (tcp 'form)

The `trans` command prints the translation of a form into a
formal term. However, sometimes the translation can be hard to understand
because various tags and declarations are included, usually for execution
efficiency.

For example, consider

ACL2 !>:trans (member e a) ((LAMBDA (X L) (RETURN-LAST 'MBE1-RAW (MEMBER-EQL-EXEC X L) (RETURN-LAST 'PROGN (MEMBER-EQL-EXEC$GUARD-CHECK X L) (MEMBER-EQUAL X L)))) E A) => * ACL2 !>:tcp (member e a) (MEMBER-EQUAL E A)

The `loop$`,
scions or `lambda$` forms are involved in the form to be
translated. But they are also useful when `mbe`, `return-last`,
`progn$` and other special forms are used or show up in the
translation. The `state`, since errors are signaled when ill-formed forms are
submitted.

:tc *form*— translate*form*and remove everything not relevant to the logical value. This is the logical semantics*form*and is returned in the ``internal format'' of ACL2 terms, i.e., macros have been expanded and all constants are quoted. The prover will reduce*form*to this term almost immediately. Typically, this is the term that the rewriter will encounter during a proof involving this*form*. Of course, rewrite rules can further change the form. However, see the note below concerning warrants.:tcp *form*— translate*form*and remove everything not relevant to the logical value as above, and then`untranslate`, restoring the use of such system macros as`lambda$`,`let`,`and`,`list`,`cadr`, and`+`and`*`. This is the semantics of*form*in a ``user friendly'' syntax. The suffix ``p'' in:tcp stands for ``pretty.'':tca *form*— translate*form*and thenuntranslate as noted above. This effectively leaves ``annotations'' in place such as aprog2$ joining eachloop$ in*form*to its semantics,declare forms inlambda objects, and`let`forms associating user variable names to values. This term is mainly meant as a pedagogical device to help you understand howloop$ s are translated. The suffix ``a'' in:tca stands for ``annotated.''

The terms returned by the three flavors of *form* provided the
necessary warrants are assumed.

For example, if

ACL2 !>:tc (loop$ for e in lst collect (sq e)) ; sq is warranted (COLLECT$ '(LAMBDA (LOOP$-IVAR) (SQ LOOP$-IVAR)) LST)

Nevertheless, the equivalence of the input and output of

(thm (equal (loop$ for e in lst collect (sq e)) (COLLECT$ '(LAMBDA (LOOP$-IVAR) (SQ LOOP$-IVAR)) LST)))

will fail with a checkpoint indicating that the warrant for

(thm (implies (warrant sq) (equal (loop$ for e in lst collect (sq e)) (COLLECT$ '(LAMBDA (LOOP$-IVAR) (SQ LOOP$-IVAR)) LST))))

succeeds.

If there is no warrant for

ACL2 !>:tc (loop$ for e in lst collect (sq e)) ; sq is badged not warranted (COLLECT$ '(LAMBDA (LOOP$-IVAR) (RETURN-LAST 'PROGN '(LAMBDA$ (LOOP$-IVAR) (LET ((E LOOP$-IVAR)) (DECLARE (IGNORABLE E)) (SQ E))) ((LAMBDA (E) (SQ E)) LOOP$-IVAR))) LST)

By the way, if you see a quoted

The differences between `loop$` statement.

ACL2 !>:trans (list (cadr x) (loop$ for e in lst collect (+ 1 e))) (CONS (CAR (CDR X)) (CONS (RETURN-LAST 'PROGN '(LOOP$ FOR E IN LST COLLECT (+ 1 E)) (COLLECT$ '(LAMBDA (LOOP$-IVAR) (DECLARE (IGNORABLE LOOP$-IVAR)) (RETURN-LAST 'PROGN '(LAMBDA$ (LOOP$-IVAR) (LET ((E LOOP$-IVAR)) (DECLARE (IGNORABLE E)) (+ 1 E))) ((LAMBDA (E) (BINARY-+ '1 E)) LOOP$-IVAR))) LST)) 'NIL)) => * ACL2 !>:tc (list (cadr x) (loop$ for e in lst collect (+ 1 e))) (CONS (CAR (CDR X)) (CONS (COLLECT$ '(LAMBDA (LOOP$-IVAR) (BINARY-+ '1 LOOP$-IVAR)) LST) 'NIL)) ACL2 !>:tcp (list (cadr x) (loop$ for e in lst collect (+ 1 e))) (LIST (CADR X) (COLLECT$ (LAMBDA$ (LOOP$-IVAR) (+ 1 LOOP$-IVAR)) LST)) ACL2 !>:tca (list (cadr x) (loop$ for e in lst collect (+ 1 e))) (LIST (CADR X) (PROG2$ '(LOOP$ FOR E IN LST COLLECT (+ 1 E)) (COLLECT$ (LAMBDA$ (LOOP$-IVAR) (LET ((E LOOP$-IVAR)) (DECLARE (IGNORABLE E)) (+ 1 E))) LST)))

First, notice that

The other two commands have ``prettied up'' the output into a more
user-friendly format. Third, the

It is often helpful to look at the semantics of fancy

ACL2 !>:tca (loop$ for x in xlst as y in ylst collect (+ (* a x) (* b y))) (PROG2$ '(LOOP$ FOR X IN XLST AS Y IN YLST COLLECT (+ (* A X) (* B Y))) (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS) (EQUAL (LEN LOOP$-GVARS) 2) (TRUE-LISTP LOOP$-IVARS) (EQUAL (LEN LOOP$-IVARS) 2)))) (LET ((A (CAR LOOP$-GVARS)) (B (CAR (CDR LOOP$-GVARS))) (X (CAR LOOP$-IVARS)) (Y (CAR (CDR LOOP$-IVARS)))) (DECLARE (IGNORABLE A B X Y)) (+ (* A X) (* B Y)))) (LIST A B) (LOOP$-AS (LIST XLST YLST))))

Notice what happens to the

ACL2 !>:tca (loop$ for x of-type (satisfies natp) in xlst as y of-type integer in ylst collect (+ (* a x) (* b y))) (PROG2$ '(LOOP$ FOR X OF-TYPE (SATISFIES NATP) IN XLST AS Y OF-TYPE INTEGER IN YLST COLLECT (+ (* A X) (* B Y))) (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS) (EQUAL (LEN LOOP$-GVARS) 2) (TRUE-LISTP LOOP$-IVARS) (EQUAL (LEN LOOP$-IVARS) 2) (NATP (CAR LOOP$-IVARS)) (INTEGERP (CAR (CDR LOOP$-IVARS)))))) (LET ((A (CAR LOOP$-GVARS)) (B (CAR (CDR LOOP$-GVARS))) (X (CAR LOOP$-IVARS)) (Y (CAR (CDR LOOP$-IVARS)))) (DECLARE (TYPE (SATISFIES NATP) X) (TYPE INTEGER Y) (IGNORABLE A B X Y)) (+ (* A X) (* B Y)))) (LIST A B) (LOOP$-AS (LIST XLST YLST))))

And notice how the

ACL2 !>:tca (loop$ for x of-type (satisfies natp) in xlst as y of-type integer in ylst collect :guard (and (rationalp a) (complex-rationalp b)) (+ (* a x) (* b y))) (PROG2$ '(LOOP$ FOR X OF-TYPE (SATISFIES NATP) IN XLST AS Y OF-TYPE INTEGER IN YLST COLLECT :GUARD (AND (RATIONALP A) (COMPLEX-RATIONALP B)) (+ (* A X) (* B Y))) (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS) (EQUAL (LEN LOOP$-GVARS) 2) (TRUE-LISTP LOOP$-IVARS) (EQUAL (LEN LOOP$-IVARS) 2) (NATP (CAR LOOP$-IVARS)) (INTEGERP (CAR (CDR LOOP$-IVARS))) (AND (RATIONALP (CAR LOOP$-GVARS)) (COMPLEX-RATIONALP (CAR (CDR LOOP$-GVARS))))))) (LET ((A (CAR LOOP$-GVARS)) (B (CAR (CDR LOOP$-GVARS))) (X (CAR LOOP$-IVARS)) (Y (CAR (CDR LOOP$-IVARS)))) (DECLARE (TYPE (SATISFIES NATP) X) (TYPE INTEGER Y) (IGNORABLE A B X Y)) (+ (* A X) (* B Y)))) (LIST A B) (LOOP$-AS (LIST XLST YLST))))

Of course, while these declarations play a role in

ACL2 !>:tcp (loop$ for x of-type (satisfies natp) in xlst as y of-type integer in ylst collect :guard (and (rationalp a) (complex-rationalp b)) (+ (* a x) (* b y))) (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS) (+ (* (CAR LOOP$-GVARS) (CAR LOOP$-IVARS)) (* (CADR LOOP$-GVARS) (CADR LOOP$-IVARS)))) (LIST A B) (LOOP$-AS (LIST XLST YLST)))