For-loop$
Iteration with loop$ over an interval of integers or a list
This topic assumes that you have read the introduction to
loop$ expressions in ACL2; see loop$. Here we give more complete
documentation on FOR loop$ expressions, beginning with informal
discussion and then continuing with detailed syntax (General Form) and
semantics. For a discussion of proofs about loop$s, see stating-and-proving-lemmas-about-loop$s.
Examples of loop$ expressions, including FOR loop$s, may
be found in community-book projects/apply/loop-tests.lisp.
The only allowed iteration clauses are IN, where the variable ranges
over the elements of the given true list; ON, where the variable ranges
over the tails of the given true-list; and FROM/TO/BY, where the
variable ranges over the integers between two bounds, stepping by a positive
integer increment (or by 1 if no BY clause is provided).
You may have as many iteration clauses as you wish, connected with
AS. Each must introduce a unique iteration variable and that variable
may be optionally followed by an OF-TYPE type-spec specification.
OF-TYPE is a Common Lisp feature that allows the compiler to optimize
operations on the variable in question. Here is an example.
(loop$ for v of-type (and integer (not (satisfies zerop)))
from 1 to 100
sum (/ 1 v))
Here is that same example with a more concise type specification.
(loop$ for v of-type (integer 1 *)
from 1 to 100
sum (/ 1 v))
After all of the iteration clauses, you may have a termination test,
signaled by UNTIL, and/or a conditional test, signaled by WHEN. If
both are provided, the UNTIL test must come first. Iteration stops when
the UNTIL test is satisfied. The conditional test determines whether
the loop body is executed for the current value of the iteration
variables.
Between the UNTIL symbol and the expression to be tested, and between
the WHEN symbol and its expression, you may include a :GUARD
clause. This is useful if guard verification requires an invariant
relating multiple iteration variables. An example of a guarded UNTIL
clause is
(loop$ for u in lst1 as v in lst2
until :guard (invariantp u v) (test u v)
collect (body u v))
ACL2 supports only five operators in FOR loop$s: SUM,
COLLECT, ALWAYS, THEREIS and APPEND. We anticipate
adding other Common Lisp operators eventually.
The special symbols noted above, sometimes called ``FOR loop$
keywords'' or just ``loop$ keywords'' may be in any package. These are
FOR, IN, ON, FROM, TO, BY, OF-TYPE,
WHEN, UNTIL, SUM, COLLECT, ALWAYS, THEREIS, and
APPEND.
Between the operator, e.g., SUM or COLLECT, and the
loop$ body you may include a :GUARD clause as in
(loop$ for u in lst1 as v in lst2
collect :guard (invariantp u v) (body u v))
This is sometimes necessary in the verification of the guards for
the loop$ body because Common Lisp's OF-TYPE clauses do not permit
you to relate one variable to another.
See lp-section-6 of the Loop$ Primer for some exercises in
writing FOR Loop$s (with answers in a Community Book). But
remember to come back here when you get to the end of that section.
General Form
The syntax of Common Lisp loop expressions is extremely complicated.
Rather than try to write the abstract syntax of ACL2's loop$ expressions
in the same formal style, we take a different approach, which is workable
because loop$ allows fewer options.
First we introduce the syntax of a ``target clause,'' a ``type-spec,'' and
the ``operators.'' Then we describe the most elaborate form of a loop$
expression in terms of these elements and ordinary ACL2 terms. Every legal
loop$ expression can be produced by omitting certain optional elements
from the most elaborate loop$ form. So we conclude the syntactic
description of loop$ by listing the elements that can be omitted.
A target clause has one of four forms
- IN list-expr
- ON expr
- FROM lo-expr TO hi-expr
- FROM lo-expr TO hi-expr BY
step-expr
where list-expr is a term (which is expected to evaluate to a true
list), expr is a term, lo-expr and hi-expr are
terms (which are expected to evaluate to integers), and step-expr is a
term (which is expected to evaluate to a positive integer).
The legal type-specs are listed in type-spec.
The legal operators are SUM, COLLECT, ALWAYS,
THEREIS, and APPEND.
The most elaborate loop$ expression is of the form
(LOOP$ FOR v1 OF-TYPE spec1
target1
AS v2 OF-TYPE spec2
target2
...
AS vn
OF-TYPE specn targetn
UNTIL :GUARD guard1
until-expr
WHEN :GUARD guard2
when-expr
; Note the ALWAYS/THEREIS Exceptions
below!
op :GUARD guard3
body-expr)
where each vi is a legal variable symbol and they are all
distinct, each type-speci is a type-spec, each
targeti is a target clause, each guardi,
until-expr, and when-expr is a term, op is
an operator, and body-expr is a term. Furthermore,
until-expr, when-expr, and body-expr must be
tame!
The ALWAYS/THEREIS Exception: Common Lisp prohibits loops
with both a WHEN clause and either an ALWAYS or a THEREIS
operator. For example, if you are tempted to use WHEN p with
ALWAYS q you can instead write ALWAYS (implies p
q) or, if you want to evaluate q only when p is true, you
can write ALWAYS (if p q t).
The following elements may be omitted.
- any line beginning with AS, UNTIL or WHEN,
- any OF-TYPE speci, and
- any :GUARD guardi.
As noted above, the FOR loop$ keywords (as used above) may be in
any package. These are FOR, IN, ON, FROM, TO,
BY, OF-TYPE, WHEN, UNTIL, SUM, COLLECT,
ALWAYS, THEREIS, and APPEND.
We give names to certain classes of the syntactic entities above. The
v1, ..., vn are called the iteration variables. The
spec1, ..., specn are called type specs, each
corresponds to a certain iteration variable, and each gives rise to a type
term about its variable in the sense that ``X OF-TYPE (SATISFIES
NATP)'' gives rise to the type term (NATP X) and ``I OF-TYPE
INTEGER'' gives rise to the type term (INTEGERP I). The terms
involved in the target expressions, e.g., the list-expr and
expr in ``IN list-expr'' and ``ON expr'' and
the lo-expr, hi-expr and optional step-expr in the
``FROM lo-expr TO hi-expr BY step-expr''
targets are called target terms. Finally, the until-expr,
when-expr, and body-expr are called iterative forms.
We distinguish the target terms from the iterative forms because they are
handled very differently at evaluation time. When a loop$ is evaluated,
the target terms are evaluated just once. But the iterative forms are
evaluated multiple times as the iteration variables range over the values of
the targets.
A FOR loop$ expression with just one iteration variable and in
which the iterative forms mention no free variable other than the iteration
variable is called a simple loop$ (or, sometimes, a simple
loop). An example of a simple loop is
(loop$ for x in lst when (evenp x) collect (+ 1 (sq x)))
A FOR loop$ expression is called a fancy loop$ if it
is not simple. Both of the following loop$s are fancy.
(loop$ for x in xlst as y on ylst collect (expr x y))
(loop$ for x in xlst collect (expr x z))
The first is fancy because it has two iteration variables. The second is
fancy because the body freely uses the variable z which is not the
iteration variable. The free variables cannot be stobjs or dfs, since the translation of the loop$ will put them into a list; see
discussion of the semantics, below. In such cases you may wish to use
DO loop$ expressions (see do-loop$) instead.
Semantics
FOR loop$ expressions are translated into calls of scions, with the UNTIL and WHEN clauses translated into
preprocessors of the targets. But which scions are used depend on whether
the loop is simple or fancy. Recall that a fancy loop is one that has either
or both of the following characteristics: (a) there is one or more as
clauses, and/or (b) one of the iterative forms (the UNTIL, WHEN or
loop body expression) refers to variables other than an iteration variable.
If the loop$ expression is simple, the simple scions are used; otherwise
the fancy scions are used.
loop$ simple fancy
keyword scion scion
______________________________________________
SUM sum$ sum$+
COLLECT collect$ collect$+
ALWAYS always$ always$+
THEREIS thereis$ thereis$+
APPEND append$ append$+
UNTIL until$ until$+
WHEN when$ when$+
We deal with simple loop$s first.
Semantics of Simple Loop$s
For example, the simple loop$
(loop$ for x in lst collect (+ 1 (sq x)))
translates to (a term equivalent to)
(collect$ (lambda$ (x)
(declare (ignorable x))
(+ 1 (sq x)))
lst).
Note: The actual translation is tagged with various markers that
play a role in evaluation but which are logically irrelevant and which are
removed during proof. In this discussion we will not display the marked-up
translations but logically equivalent terms instead. You can see the actual
translations for yourself with trans.
In the translation the target term, lst, appears as an ordinary
subterm of the translation. But the iterative form, (+ 1 (sq x)),
becomes the body of a lambda$ expression, which means its translation
becomes a component of a quoted LAMBDA object. When the collect$
is evaluated, the target term is evaluated once but the iterative form is
evaluated once for each element of the value of the target.
UNTIL and WHEN clauses are handled by preprocessing the target.
E.g.,
(loop$ for x in lst
until (> x 100)
when (evenp x)
collect (+ 1 (sq x)))
becomes
(collect$ (lambda$ (x)
(declare (ignorable x))
(+ 1 (sq x)))
(when$ (lambda$ (x)
(declare (ignorable x))
(evenp x))
(until$ (lambda$ (x)
(declare (ignorable x))
(> x 100))
lst)))
So from a logical perspective, the presence of an UNTIL and/or
WHEN clause in a collect iteration over lst ``copies'' the
target value. The until$ copies lst until encountering the first
element on which its functional argument is true. The when$ then copies
that (shortened?) target, keeping only the elements that satisfy its
functional argument. Finally, the collect$ then applies its functional
argument and collects all the values.
ON and FROM/TO/BY targets are handled by listing all the
elements in the given target. For example,
(loop$ for x on lst collect (expr x))
which maps x over successive non-empty tails of lst and collects
the value of expr has the logical meaning
(collect$ (lambda$ (x) (expr x))
(tails lst))
where, for example, (tails '(1 2 3)) is ((1 2 3) (2 3) (3)).
Spiritually similarly,
(loop$ for i from 1 to max by step collect (expr x))
logically becomes
(collect$ (lambda$ (x) (expr x))
(from-to-by 1 max step))
where, for example, (from-to-by 1 10 2) is (1 3 5 7 9).
Similar translations are done for the other operators, e.g., SUM and
ALWAYS. The advantage of this translation style is that it allows
compositional reasoning. We discuss this further below.
The following example illustrates basic guard proof obligations, in
particular showing that WHEN clauses do not help with verifying guards
for the loop$ bodies. (Similarly, UNTIL clauses do not help
either.) The basic problem is that ACL2 requires that lambda objects
be guard verifiable in isolation, not confined to the context in which a
particular lambda object appears. Consider the following.
(include-book "projects/apply/top" :dir :system)
(defun$ sq (n)
(declare (xargs :guard (natp n)))
(* n n))
(defun foo (lst)
(declare (xargs :guard (nat-listp lst)))
(loop$ for x of-type (satisfies nat-listp) on lst
when (consp x)
sum (sq (car x))))
Guard verification fails for foo. The summary says that a goal of
NIL was generated. Using :pso we can see that the NIL
goal came from:
Subgoal 1.2
(IMPLIES (NAT-LISTP LOOP$-IVAR)
(INTEGERP (CAR LOOP$-IVAR))).
Let's see what is going on by looking at the following simplified
translation of the loop$ expression.
(sum$ '(lambda (loop$-ivar)
(declare (type (satisfies nat-listp) loop$-ivar))
(sq (car loop$-ivar)))
(when$ '(lambda ...) (tails lst)))
Notice that the lambda object supplied to sum$ cannot be guard
verified in isolation: nil satisfies the :guard and (car nil)
violates the guard of sq. The following modification, which adds a
:guard directive after the SUM op keyword, solves the problem.
(defun foo (lst)
(declare (xargs :guard (nat-listp lst)))
(loop$ for x of-type (satisfies nat-listp) on lst
when (consp x)
sum :guard (consp x) ; note new :guard
(sq (car x))))
This new :guard may feel redundant, coming as it does after the
when (consp x) clause. But it is necessary given the compositional
semantics.
A simplified translation of the defun above shows that the
application (sq (car x)) is protected by a suitable guard in the
lambda object.
(sum$ '(lambda (loop$-ivar)
(declare (type (satisfies nat-listp) loop$-ivar)
(xargs :guard (consp loop$-ivar)))
(sq (car loop$-ivar)))
(when$ '(lambda ...) (tails lst)))
Naively we might have expected that the guard proof obligation for the
loop$ body (sq (car x)) could assume the WHEN clause, but that
expectation would be wrong because of the compositional semantics we use and
the fact that lambda objects must be guard-verifiable on their own.
The reason for the latter requirement is that our implementation caches
guard-verified lambda objects for evaluation in raw Lisp, which may take
place in other contexts different from that in which the lambda first
appeared. See print-cl-cache.
Semantics of Fancy Loop$s
An example of a fancy loop$ is
(loop$ for x in xlst as y in ylst collect (expr x y z))
This loop exhibits both characteristics (a) and (b): it has an AS
clause and the variable z appears in the loop body. Either
characteristic is sufficient to classify the loop as fancy. So fancy scions
are used. Here is its semantic counterpart, i.e., its simplified
translation.
(collect$+
(lambda$ (loop$-gvars loop$-ivars)
(declare (xargs :guard (and (true-listp loop$-gvars)
(equal (len loop$-gvars) 1)
(true-listp loop$-ivars)
(equal (len loop$-ivars) 2))))
(let ((z (car loop$-gvars))
(x (car loop$-ivars))
(y (car (cdr loop$-ivars))))
(declare (ignorable x y))
(expr x y z)))
(list z)
(loop$-as (list xlst ylst)))
Before we show the definition of collect$+, note that the arguments
above to collect$+ are (i) a lambda$ expression that handles the
evaluation of the iterative form, in this case (expr x y z), where
x and y are iteration variables and z is a ``global'' variable
not among the iteration variables; (ii) the list of values of the ``global''
variables, in this case the list containing z; and (iii) a target list
constructed by loop$-as from the various targets provided in the
loop$, in this case xlst and ylst, supplying values for
iteration variables x and y respectively. For example,
(loop$-as (list '(a b c d e) '(1 2 3))) is ((a 1) (b 2) (c 3)).
These tuples contain successive corresponding values of x and
y.
The definition of collect$+ is essentially
(defun collect$+ (fn loop$-gvars lst)
(if (endp lst)
nil
(cons (apply$ fn (list loop$-gvars (car lst)))
(collect$+ fn loop$-gvars (cdr lst)))))
We have omitted the guard and an mbe form that make it run more
efficiently. All the fancy loop$ scions are defined analogously.
Inspection of the lambda$ expression above reveals that it takes a
list of global variable values and a list of iteration variable values,
unpacks them with a let that binds the global variables, here just
z, to their values and binds the iteration variables, here x and
y, to the corresponding pair of values from the target, and then
evaluates the loop$ body, (expr x y z).
The names of the formals for the lambda$ expressions generated by
fancy loop$ expressions are always loop$-gvars and
loop$-ivars, for ``loop$ global variables'' and ``loop$
iteration variables.''
UNTIL and WHEN clauses in a fancy loop$ are handled exactly
as they are in simple loop$s, except that the fancy scions are used
since the target list is a list of tuples of iteration variable values and
the UNTIL and WHEN forms may refer to global variables.
See lp-section-10 of the Loop$ Primer for a step-by-step
discussion of the evaluation of the formal semantics of an example of a fancy
Loop$. But remember to come back here when you get to the end of that
section.
Special Guard Conjectures for FOR loop$s
Since every loop$ expands to a call of a loop$ scion on a lambda
object and a target, one would expect that guard verification would
generate the guard conjectures for that scion and target. Indeed, it does.
In particular, the lambda object must have the correct number of
formals (which is guaranteed by translation) and the target must satisfy
true-listp.
But in addition to the expected guard conjectures, we generate some
special ones for the terms produced by translating FOR loop$
expressions. We discuss the reasons in the next section, but here we just
state what the special conjectures are. We limit ourselves to a simple
loop$. Fancy loop$s generalize in the obvious way. The two
classes of ``special guard conjectures'' for FOR loop$ expressions
are as follows.
- First, every element (or tail, in the case of ON loop$s))
satisfies the type-spec, if any, and the loop$ body's :GUARD, if
any.
- Second, the loop$ body produces a value acceptable to the loop$
operator, e.g., the body of a SUM loop$ produces a number and
the body of an APPEND loop$ produces a true list.
See lp-section-8 of the Loop$ Primer for some exercises in
converting recursive functions to guard verified functions using FOR
loop$s rather than recursion (with answers in a Community Book). But
remember to come back here when you get to the end of that section.
Discussion of Why LOOP$s Have Special Guards
All of the simple loop$ scions have the same guard, namely
(AND (APPLY$-GUARD FN '(NIL))
(TRUE-LISTP LST)),
and all the fancy loop$ scions have the same guard, namely
(AND (APPLY$-GUARD FN '(NIL NIL))
(TRUE-LISTP LOOP$-GVARS)
(TRUE-LIST-LISTP LST)).
In addition to the normal guard conjectures that would be generated by
calls of these scions, ACL2 generates some special guard conjectures because
the normal guard conjectures are insufficient to guarantee the error-free
execution of the corresponding Common Lisp loop expressions.
For example, the simplified translation of the body of
(defun foo (lst)
(declare (xargs :guard (foo-guardp lst)))
(loop$ for x of-type (satisfies spec) on lst sum (expr x)))
is as follows. (One might expect the second argument of the sum$
call to be (tails lst), and of course that is what it equals, logically;
the change is to support guards, as discussed in the Technical Note
below.)
(sum$ (lambda$ (loop$-ivar)
(declare (type (satisfies spec) loop$-ivar))
(expr loop$-ivar))
(tails (prog2$ (let ((loop$-last-cdr (last-cdr lst)))
(declare (type (satisfies spec) loop$-last-cdr))
loop$-last-cdr)
lst)))
Prior to the provision for special guards, the normal guard conjectures
generated for foo would be
(and (implies (foo-guardp lst) ; [1]
(apply$-guard
(lambda$ (loop$-ivar)
(expr loop$-ivar))
'(nil)))
(implies (foo-guardp lst) ; [2]
(true-listp (tails lst)))
(implies (spec loop$-ivar) (expr-guardp loop$-ivar))) ; [3]
(implies (foo-guardp lst) ; [4]
(let ((loop$-last-cdr (last-cdr lst)))
(spec loop$-last-cdr)))
Conjectures [1] and [2] stem from the guard for sum$ and establish
that the guard for foo implies that sum$ is passed a function
object of one argument and a true-list. Conjecture [3] establishes that the
guard on the lambda$ implies the guard of its body. Conjecture [4] says
that the final tail of lst (which is nil if lst is a true
list; see last-cdr) satisfies spec. At first [4] may be
surprising, but inspection of Common Lisp reveals that even though (expr
x) is never called on the final tail of lst, implementations running
with high safety settings check that the final tail satisfies spec. If
you see a runtime guard violation involving variable loop$-last-cdr, you
can reasonably assume that you are seeing case [4] above. A guard proof
failure involving a call of last-cdr may also be from [4].
(Technical Note. The production of [4] is accomplished as follows for an
expression (loop for var of-type type-spec on lst ...): for the
translation to a scion call, the target term, lst, is replaced by the
following expression (simplifying slightly).
(prog2$ (let ((loop$-last-cdr (last-cdr lst)))
(declare (type type-spec loop$-last-cdr))
loop$-last-cdr)
lst)
The declare form causes formula [4] above to be generated as a
guard proof obligation. End of Technical Note.)
The guard proof obligation shown as [4] above, for an expression (loop$
for ... on ...), has a variant for an expression (loop$ for n from i to
j by k ...), where “by k” may be implicit if k is
1. Instead of the requirement in [4] above that the bound variable
loop$-last-cdr satisfy the type-spec, variables loop$-lo,
loop$-hi, and loop$-by, which are bound respectively to i,
j, and k, are required to satisfy the type-spec. A fourth
requirement is that the last value tested must also satisfy the
type-spec. That last value tested is (+ loop$-lo loop$-by (*
loop$-by (floor (- loop$-hi loop$-lo) loop$-by))). If you see a runtime
guard violation involving variable loop$-lo, loop$-hi,
loop$-by, or loop$-final, you can reasonably assume that you are
seeing this variant of [4].
But consider the raw Lisp loop generated by the loop$ in the raw
Lisp definition of foo,
(loop for x of-type (satisfies spec) on lst sum (expr x)).
For this loop to execute without error we need to know that [5] every
non-empty tail of lst satisfies spec, and [6] every non-empty tail
x of lst is such that (expr x) returns a number.
So when ACL2's guard verification process encounters a sum$ like that
in the logical defun of foo, it generates two additional guard
conjectures as described above. These are as mentioned above: [5] every
element (or tail) satisfies the type-spec, and [6] the value of the
loop$ body is acceptable to the loop$ operator.
(implies (and (warrant ...) ; see below ; [5]
(foo-guardp lst)
(member-equal newv (tails lst)))
(spec newv))
(implies (and (warrant ...) ; see below ; [6]
(foo-guardp lst)
(member-equal newv (tails lst)))
(acl2-numberp
(apply$ (lambda$ (loop$-ivar) (expr loop$-ivar))
(list newv))))
Notice the addition of hypotheses above of the form (warrant ...).
ACL2 adds such warrant hypotheses for function symbols that
might be apply$'d during evaluation of a scion call (in this case,
sum$).
In general, you may notice that ACL2 generates such ``special'' guard
conjectures for all calls of FOR loop$ scions, whether or not they
stemmed from uses of loop$. FROM/TO/BY targets require that the
bounds and step all satisfy the OF-TYPE specification, and the
APPEND operator requires that the loop body generate a true-listp (instead of an ACL2-numberp as required by the SUM
operator).
The Compromise Between Reasoning and Efficiency
The translation of loop$ expressions into formal terms reflects a
compromise between facilitating compositional reasoning and efficient
execution.
One sign of that compromise is our use of scions to handle UNTIL and
WHEN clauses. As noted above, by translating
(loop$ for x in lst until ... when ... collect ...)
into
(collect$ ... (when$ ... (until$ ... lst)))
we're forcing the evaluation of the formal semantics to copy the target
twice before collecting. But it gives us the ability to reason
compositionally about collect$, when$, and until$. We could
have defined a version of collect$ that took three lambda$
expressions, one to terminate the collection, one to filter for the elements
we're interested in, and one to transform those elements into the values we
wish to collect. This would avoid copying upon evaluation but make it more
difficult to reason.
Another example of compositionality is to consider a simple loop$
over the IN target (append a b). There are 8 different ways you
can do a simple COLLECT over an (append a b) target,
(loop$ for x in (append a b) collect (expr x))
(loop$ for x on (append a b) collect (expr x))
(loop$ for x in (append a b) until (stop x) collect (expr x))
(loop$ for x on (append a b) until (stop x) collect (expr x))
(loop$ for x in (append a b) when (test x) collect (expr x))
(loop$ for x on (append a b) when (test x) collect (expr x))
(loop$ for x in (append a b) until (stop x) when (test x)
collect (expr x))
(loop$ for x on (append a b) until (stop x) when (test x)
collect (expr x))
Similarly, there are 8 ways to SUM over an (append a b) target,
8 ways to APPEND over an (append a b), and 4 ways each to
ALWAYS or THEREIS over an (append a b) target. Thus, there
are 32 different simple loop$s over (append a b). And you can
arrange to distribute the simple loop$ over the (append a b) with
just seven rewrite rules.
(equal (collect$ fn (append a b))
(append (collect$ fn a)
(collect$ fn b)))
(equal (sum$ fn (append a b))
(+ (sum$ fn a)
(sum$ fn b)))
(equal (always$ fn (append a b))
(and (always$ fn a)
(always$ fn b)))
(equal (thereis$ fn (append a b))
(or (thereis$ fn a)
(thereis$ fn b)))
(equal (append$ fn (append a b))
(append (append$ fn a)
(append$ fn b)))
(equal (until$ fn (append a b))
(if (exists$ fn a)
(until$ fn a)
(append a (until$ fn b))))
(equal (when$ fn (append a b))
(append (when$ fn a)
(when$ fn b)))
Thus, you can reason about WHEN and UNTIL clauses without having
to consider how they are used in the superior loop$ expression.
To deal with fancy loop$ you need seven more rewrite rules, one for
each fancy loop$ scion. But since every simple loop$ can be
expressed by an appropriate use of fancy scions, we could have translated
every FOR loop$ to fancy scions. We chose to break
compositionality here because we think simple loop$s are most common and
wanted to keep their semantics simple. I.e., we compromised.
By the way, if you want the prover to convert every simple scion to its
fancy counterpart you could prove rewrite rules like that below.
(defthm convert-collect$-to-collect$+
(implies (ok-fnp fn)
(equal (collect$ fn lst)
(collect$+ `(lambda (loop$-gvars loop$-ivars)
(,fn (car loop$-ivars)))
nil
(loop$-as (list lst)))))
:hints (("[1]Goal"
:expand ((tamep (cons fn '(x)))
(tamep (cons fn '((car loop$-ivars))))))))
