Major Section: PROGRAMMING
Example Form: ; The following evaluates to (mv 7 10): (flet ((f (x) (+ x 3)) (g (x) (declare (type integer x)) (* x 2))) (mv (f 4) (g 5)))where
General Form: (flet (def1 ... defk) body)
bodyis a term, and each
defiis a definition as in
defunbut with the leading
defunsymbol omitted. See defun. The innermost
flet-binding of a function symbol,
f, above a call of
f, is the one that provides the definition of
ffor that call. Note that
fletdoes not provide recursion. Consider the following example.
(defun f (x) (+ x 3)) (flet ((f (x) (cons x (f (1+ x))))) (f 4))In the above term
(cons x (f (1+ x))),
frefers to the global definition of
(f 4)refers to the
(f (x) (cons x (f x))). The result of the
fletexpression is thus obtained by evaluating
(cons 4 (f (1+ 4))), where the latter call of
frefers to the global definition; thus we have
(cons 4 (f 5)), which evaluates to
(4 . 8).
flet behaves in ACL2 essentially as it does in Common Lisp, ACL2
imposes the following restrictions and qualifications.
declareform for a local definition (
defk, above) must be an
defimust bind a different function symbol.
defimust bind a symbol that is a legal name for an ACL2 function symbol. In particular, the symbol may not be in the keyword package or the main Lisp package. Moreover, the symbol may not be a built-in ACL2 function or macro.
o Every variable occurring in the body of a
defimust be a formal parameter of that
defi. (This restriction is not enforced in Common Lisp. If the restriction is inconvenient for you, the ACL2 implementors may be able to remove it, with some effort, if you ask.)
o If the
defiis in the body of a function
f, then the stobj inputs for
defiare implicitly those of its inputs that are declared stobj inputs of
Flet bindings are evaluated in parallel. Consider the following
(defun f (x) x) (flet ((f (x) (cons x x)) (g (x) (f x))) (g 3))The binding of
grefers to the global value of
f, not the
f. Thus, the
fletexpression evaluates to 3. Compare the
fletexpression above to the following one, which instead evaluates to
(3 . 3).
(defun f (x) x) (flet ((f (x) (cons x x))) (flet ((g (x) (f x))) (g 3)))
Under the hood, ACL2 translates
flet bindings to
(see term). The following example illustrates this point.
ACL2 !>:trans (flet ((f (x) (cons x x)) (g (x y) (+ x y))) (f (g 3 4)))
((LAMBDA (X) (CONS X X)) ((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))
Flet is part of Common Lisp. See any Common Lisp documentation
for more information.