Translam
Print the translation of a lambda$ expression
:translam (lambda$ (x) (+ 1 x))
:translam (lambda (x) (+ 1 x))
This function takes a lambda$ term or an unquoted LAMBDA
constant. In the former case, it translates the lambda$ and prints the
result. In the latter case it puts the LAMBDA in a QUOTE and
translates it as though it occurred in a :FN slot. Unless an error is
signaled it prints the same LAMBDA object as the result.
This utility exists because you cannot write, say,
:trans (lambda$ (x) (+ 1 x))
because the trans utility assumes its argument in an ordinary (ilk
NIL) slot. In such slots, lambda$ terms are disallowed and no
restrictions are enforced on quoted LAMBDA objects.
This utility is useful for seeing what the formal translation of a
lambda$ term is. For example,
ACL2 !>:translam (lambda$ (x)
(declare (type (satisfies natp) x))
(* x x))
produces the quoted well-formed LAMBDA expression:
'(LAMBDA (X)
(DECLARE (TYPE (SATISFIES NATP) X)
(XARGS :GUARD (NATP X) :SPLIT-TYPES T)
(IGNORABLE X))
(RETURN-LAST 'PROGN
'(LAMBDA$ (X)
(DECLARE (TYPE (SATISFIES NATP) X))
(* X X))
(BINARY-* X X)))
You might now have an inkling about why we discourage you from trying to
enter quoted well-formed LAMBDA objects by hand! The normal form of a
quoted well-formed LAMBDA object is complicated so that apply$ can
rapidly identify the parts, generate guard conditions, compile the object,
recognize objects coming from lambda$ terms, etc.
