• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
      • Make-event
      • Defmacro
      • Untranslate-patterns
      • Tc
      • Trans*
      • Macro-aliases-table
      • Macro-args
      • Defabbrev
      • User-defined-functions-table
      • Trans
      • Untranslate-for-execution
      • Add-macro-fn
      • Check-vars-not-free
      • Safe-mode
      • Macro-libraries
      • Trans1
      • Defmacro-untouchable
      • Set-duplicate-keys-action
      • Add-macro-alias
      • Magic-macroexpand
      • Defmacroq
      • Trans!
      • Remove-macro-fn
      • Remove-macro-alias
      • Add-binop
      • Untrans-table
      • Trans*-
      • Remove-binop
      • Tcp
      • Tca
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Macros

Tc

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 :trans versus :tcp of (member e a).

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 :tc command and its variants, :tca and :tcp, translate the given form and then ``clean'' it up, returning the result in an error-triple. These commands are especially useful when 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 tc commands are macros that expand into terms involving 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 then untranslate as noted above. This effectively leaves ``annotations'' in place such as a prog2$ joining each loop$ in form to its semantics, declare forms in lambda objects, and let forms associating user variable names to values. This term is mainly meant as a pedagogical device to help you understand how loop$s are translated. The suffix ``a'' in :tca stands for ``annotated.''

The terms returned by the three flavors of tc are all provably equivalent to each other and to the original form provided the necessary warrants are assumed.

For example, if sq is a user-defined function of arity 1 and (defwarrant sq) has issued a warrant for sq, then

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 :tc above cannot be proved unless the warrants are assumed. That is,

(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 sq must be provided. However,

(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 sq but there is a badge, then :tc cannot clean up the translation because without a warrant the lambda object calling sq is not tame. Thus,

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 lambda objects like that above in output from the prover, it probably means the lambda object contains unwarranted user-defined symbols!

The differences between :trans and the three commands (:tc, :tcp, and :tca) are perhaps best illustrated by considering their respective outputs on a single 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 :trans also reports the output signature of the term but the :tc commands do not. They all return the cleaned up translation in an error triple. Second, :tc returns a term in the internal format: the lambda objects are quoted list constants and their bodies are in internal format, e.g., note the binary-+ and quoted constant 1 in the output of :tc above. If you use the :tc command on the left-hand side of the conclusion of a :rewrite rule the term you see is the term under which the rule is stored, i.e., the rule will be tried to rewrite instances of that term.

The other two commands have ``prettied up'' the output into a more user-friendly format. Third, the :tca command uses a prog2$ to show the untranslated loop$ as a list constant and then show its pretty semantics, with a let form in the body of the lambda$ reminding you that loop$-ivar is what was called e.

It is often helpful to look at the semantics of fancy loop$s.

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 :guard of the lambda$ if we insert type specifications with of-type.

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 :guard keyword after the collect in the loop$ statement is added to the :guard of the generated lambda$.

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 :guard verification and execution in raw Lisp, they are irrelevant to the formal semantics, as made clear by :tcp.

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