Flet
Local binding of function symbols
See macrolet for an analogous utility for defining macros
locally.
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)))
General Forms:
(flet (def1 ... defk) body)
(flet (def1 ... defk) declare-form1 .. declare-formk body)
where body is a term, and each defi is a definition as in defun but with the leading defun symbol omitted. See defun, but
see declare for the declarations permitted directly under the
defi. On the other hand, regarding the declare-formi (if any are
supplied): each must be of the form (declare decl1 ... decln), where each
decli is of the form (inline g1 ... gm) or (notinline g1
... gm), and each gi is defined by some defi.
The innermost flet or macrolet binding of a symbol, f,
above a call of f, is the one that provides the definition of f for
that call. Note that neither flet nor macrolet provide recursion:
that is, the definition of f in an flet or macrolet binding of
f is ignored in the body of that binding. Consider the following
example.
; Give a global definition of f:
(defun f (x) (+ x 3))
; Evaluate an expression using a local binding of f:
(flet ((f (x) (cons x (f (1+ x)))))
(f 4))
In the above term (cons x (f (1+ x))), f refers to the global
definition of f above the flet expression. However, (f 4)
refers to the flet-binding of f, (f (x) (cons x (f x))). The
result of the flet expression is thus obtained by evaluating (f 4)
where (f 4) is (cons 4 (f (1+ 4))), where the latter call of f
refers to the global definition; thus we have (cons 4 (f 5)), which
evaluates to (4 . 8).
Although flet behaves in ACL2 essentially as it does in Common Lisp,
ACL2 imposes the following restrictions and qualifications.
- Every declare form for a local definition (def1 through
defk, above) must be an ignore, ignorable, or type
expression. Such type declarations affect evaluation and guard-checking in a way that is completely analogous to such declarations
that occur between the formal parameters and the body in a defun
form.
- Each defi must bind a different function symbol.
- Each defi must 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.
- Every variable occurring in the body of a defi must be a formal
parameter of that defi. (This restriction is not enforced in Common
Lisp.)
- If the flet-binding defi is in the body of a function f,
then the stobj inputs for defi are implicitly those of its inputs
that are declared stobj inputs of f.
- When an expression (flet (... defi ...) ...) occurs in the body of a
DO loop$ expression, nevertheless constructs such as PROGN
and SETQ that ACL2 permits in DO loop$ bodies are not permitted
in defi (unless they occur within the scope of a DO loop$
expression in that body). (This restriction is only for ACL2; for example, it
may be reasonable to call RETURN in such situations but ACL2 does not
allow that.)
Flet bindings are evaluated in parallel. Consider the following
example.
(defun f (x) x)
(flet ((f (x) (cons x x))
(g (x) (f x)))
(g 3))
The binding of g refers to the global value of f, not the
flet-binding of f. Thus, the flet expression evaluates to 3.
Compare the flet expression 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 lambda
expressions (see term), throwing away the inline and
notinline declarations (if any). The following example illustrates this
point.
ACL2 !>:trans (flet ((f (x) (cons x x))
(g (x y) (+ x y)))
(declare (inline f))
(f (g 3 4)))
((LAMBDA (X) (CONS X X))
((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))
=> *
ACL2 !>
Flet is part of Common Lisp. See any Common Lisp documentation for
more information. We conclude by pointing out an important aspect of
flet shared by ACL2 and Common Lisp: The binding is lexical, not dynamic.
That is, the flet binding of a function symbol only applies to calls of
that function symbol in the body of the flet, not other calls made in the
course of evaluation. Consider the following example. Suppose we define:
(defun f (x) x)
(defun g (x) (f x))
(defun h (x)
(flet ((f (x) (cons x x)))
(g x)))
Then evaluation of (h 3) results in 3, not in the cons pair
(3 . 3), because the flet binding of f only applies to calls of
f that appear in the body of that flet. In this case, only g
is called in the body of that flet.
