		Search-engine friendly clone of the ACL2 documentation.

System-utilities

Untranslate

Show a user-level representation of a term

ACL2 uses a strict notion of ``term'' for its internal computations; see pseudo-termp. Such expressions are sometimes called ``translated terms''. However, ACL2 provides user-level output — for example, in output from the theorem prover — in the form of so-called ``untranslated terms''. For example, the untranslated term (<= 3 x) corresponds to the translated term (not (< x '3)), as is illustrated by applying :trans to the untranslated term:

ACL2 !>:trans (<= 3 x)

(NOT (< X '3))

=> *

ACL2 !>

Notice for example that the macro <= has been eliminated in favors of the functions not and <, and that the constant 3 has been quoted.

The call (untranslate term iff-flg wrld) returns an untranslated term corresponding to the given translated term, term, with respect to the given logical world, wrld. If iff-flg is not nil, then that untranslated term is merely propositionally equivalent to the input term, as the following example illustrates.

ACL2 !>:trans (and x t)

(IF X 'T 'NIL)

=> *

ACL2 !>(untranslate '(IF X 'T 'NIL) nil (w state))
(AND X T)
ACL2 !>(untranslate '(IF X 'T 'NIL) t (w state))
X
ACL2 !>

The latter result, x, is what one might want to see if the term is being used as the first argument of a call of the function, if. Indeed, untranslate is defined so that the iff flag is automatically set in the test position of an if call.

ACL2 !>:trans (if (and x t) y z)

(IF (IF X 'T 'NIL) Y Z)

=> *

ACL2 !>(untranslate '(IF (IF X 'T 'NIL) Y Z) nil (w state))
(IF X Y Z)
ACL2 !>

Also see user-defined-functions-table and add-macro-fn.