FLET

local binding of function symbols 
Major Section:  ACL2-BUILT-INS


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. If any declare-formi are supplied, then 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 only effect of the declarations is to provide advice to the host Lisp compiler. The declarations are otherwise ignored by ACL2, so we mainly ignore them in the discussion below.

The innermost flet-binding of a function symbol, f, above a call of f, is the one that provides the definition of f for that call. Note that flet does not provide recursion. 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.

o Every declare form for a local definition (def1 through defk, above) must be an ignore, ignorable, or type expression.

o Each defi must bind a different function symbol.

o 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.

o 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 restriction is inconvenient for you, the ACL2 implementors may be able to remove it, with some effort, if you ask.)

o 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.

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