		Search-engine friendly clone of the ACL2 documentation.

Ec-call

Execute a call in the ACL2 logic instead of raw Lisp

The name ``ec-call'' represents ``executable-counterpart call.'' This utility is intended for users who are familiar with guards. See guard for a general discussion of guards.

Logically, ec-call behaves like the identity macro; during proofs, (ec-call TERM) is typically replaced quickly by TERM during a proof attempt. However, ec-call causes function calls to be evaluated in the ACL2 logic rather than raw Lisp, as explained below.

General Forms:
(ec-call (fn term1 ... termk))
(ec-call (fn term1 ... termk) :dfs-in 'dfs-in :dfs-out dfs-out)

where fn is a known function symbol other than those in the list that is the value of the constant *ec-call-bad-ops*. (But see the Note on Inlining below for an exception pertaining to inlining.) In particular, fn is not a macro. The second form is only relevant for those who use dfs and is discussed at the end of this topic.

Semantically, (ec-call (fn term1 ... termk)) equals (fn term1 ... termk). However, this use of ec-call has two effects.

(1) Guard verification generates no proof obligations from the guard of fn for this call. Indeed, guards need not have been verified for fn.

(2) During evaluation, after the arguments of fn are evaluated as usual, the executable-counterpart of fn is called, rather than its submitted version (see evaluation). That is, the call of fn is made on its evaluated arguments as though this call is being made in the ACL2 top-level loop, rather than in raw Lisp. In particular, the guard of fn is checked, at least by default (see set-guard-checking).

The use of ec-call does not turn off guard-checking, but that can be accomplished by using with-guard-checking as well. Consider the following example.

(defun f1 (x)
  (declare (xargs :guard t))
  (ec-call (nth t x)))

This definition is admitted, but evaluation of (f1 '(a b c)) nevertheless causes a guard violation (at least, by default). However, if instead we submit the following definition, then there is no guard violation for that call of f1.

(defun f1 (x)
  (declare (xargs :guard t))
  (with-guard-checking nil (ec-call (nth t x))))

Note that in the term (ec-call (fn term1 ... termk)), only the indicated call of fn is made in the logic; each termi is evaluated in the normal manner. If you want an entire term evaluated in the logic, wrap ec-call around each function call in the term (other than calls of if and ec-call).

Technical Remark (probably best ignored). During evaluation of a call of defconst or defpkg in raw Lisp, a form (ec-call (fn term1 ... termk)) is treated as (fn term1 ... termk), that is, without calling the executable-counterpart of fn. This situation occurs when loading a compiled file (or expansion file) on behalf of an include-book event. The reason is technical: executable-counterparts are defined below a book's events in the book's compiled file. End of Technical Remark.

Here is another small example. We define foo recursively but with guard verification inhibited on the recursive call, which is to be evaluated in the ACL2 logic.

ACL2 !>(defun foo (x y)
        (declare (xargs :guard (consp y)))
        (if (consp x)
            (cons (car x) (ec-call (foo (cdr x) (cdr y))))
          (car y)))

The admission of FOO is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We could deduce no constraints on the type of FOO.

Computing the guard conjecture for FOO....

The guard conjecture for FOO is trivial to prove.  FOO is compliant
with Common Lisp.

Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FOO
ACL2 !>(foo '(2 3 4 5) '(6 7))

ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X Y),
which is (CONSP Y), is violated by the arguments in the call
(FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.  See :DOC set-guard-checking for information about suppressing
this check with (set-guard-checking :none), as recommended for new
users.

ACL2 !>

The error above arises because eventually, foo recurs down to a value of parameter y that violates the guard. This is clear from tracing (see trace$ and see trace). Each call of the executable-counterpart of foo checks the guard and then invokes the submitted version of foo (see evaluation). The submitted version calls the executable-counterpart on the recursive call. When the guard check fails we get a violation.

ACL2 !>(trace$ foo)
 ((FOO))
ACL2 !>(foo '(2 3 4 5) '(6 7))
1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
  2> (FOO (2 3 4 5) (6 7))
    3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
      4> (FOO (3 4 5) (7))
        5> (ACL2_*1*_ACL2::FOO (4 5) NIL)

ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X Y),
which is (CONSP Y), is violated by the arguments in the call
(FOO '(4 5) NIL).  To debug see :DOC print-gv, see :DOC trace, and
see :DOC wet.  See :DOC set-guard-checking for information about suppressing
this check with (set-guard-checking :none), as recommended for new
users.

ACL2 !>

If we turn off guard errors then we can see the trace as above, but where we avoid calling the raw Lisp function when the guard fails to hold.

ACL2 !>:set-guard-checking nil

Masking guard violations but still checking guards except for self-
recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
:NONE.  See :DOC set-guard-checking.

ACL2 >(foo '(2 3 4 5) '(6 7))
1> (ACL2_*1*_ACL2::FOO (2 3 4 5) (6 7))
  2> (FOO (2 3 4 5) (6 7))
    3> (ACL2_*1*_ACL2::FOO (3 4 5) (7))
      4> (FOO (3 4 5) (7))
        5> (ACL2_*1*_ACL2::FOO (4 5) NIL)
          6> (ACL2_*1*_ACL2::FOO (5) NIL)
            7> (ACL2_*1*_ACL2::FOO NIL NIL)
            <7 (ACL2_*1*_ACL2::FOO NIL)
          <6 (ACL2_*1*_ACL2::FOO (5))
        <5 (ACL2_*1*_ACL2::FOO (4 5))
      <4 (FOO (3 4 5))
    <3 (ACL2_*1*_ACL2::FOO (3 4 5))
  <2 (FOO (2 3 4 5))
<1 (ACL2_*1*_ACL2::FOO (2 3 4 5))
(2 3 4 5)
ACL2 >

Note on Inlining. Although in general, the form (ec-call (fn term1 ... termk)) is only legal if fn is a function symbol, such a form is also legal if fn is introduced with defun-inline, or with define using keyword argument :inline t. In those cases, fn is a macro whose calls expand to corresponding calls of fn$INLINE, the symbol in the same package as fn but with the string "$INLINE" added as a suffix to the symbol-name of fn. We do not however extend this exception to macros in general, even when add-macro-fn has been invoked. Consider the following example.

(encapsulate
 ()
 (defun foo () nil)
 (defun bar () t)
 (defmacro mac () nil)
 (add-macro-alias mac foo)
 (local (add-macro-alias mac bar))
 (defun h () (ec-call (mac)))
 (defthm bad (h)))

Consider what would happen if this were legal, where (ec-call (mac)) used the macro-alias, foo, for mac. Then in the first pass of the encapsulate form above, the final defthm event would prove, since (ec-call (mac)) is treated as (ec-call (bar)). But on the second pass, ACL2 would store bad as a theorem even though (h) would evaluate to nil, since the macro-alias of mac is foo on the second pass.

We conclude with a discussion of the second General Form:

(ec-call (fn term1 ... termk) :dfs-in 'dfs-in :dfs-out 'dfs-out)

Note that either or both keyword arguments may be omitted, and if both are included then they can be given in either order.

See df for background on dfs. Here is an example.

ACL2 !>(ec-call (binary-df+ (df1) (df1)) :dfs-in '(t t) :dfs-out '(t))
#d2.0
ACL2 !>

The keyword arguments indicate, respectively, binary-df+ takes two df arguments and returns a single df value. Without those arguments ACL2 would report an error.

The next example illustrates the use of :dfs-out for multiple value returns. First define g as follows.

(defun g (x)
  (mv (df+ (df1) (to-df x)) (- x 1)))

The use of :dfs-out below tells ACL2 that the given expression (g 3) returns two values: a df and an ordinary value. In the language of :DOC df: (g 3) is a df{0} expression and is not a df{1} expression. Note that the argument of g is an ordinary expression, not a df, so no :dfs-in argument is necessary.

ACL2 !>(ec-call (g 3) :dfs-out '(t nil))
(#d4.0 2)
ACL2 !>

Returning to the second General Form, notice that dfs-in and dfs-out are lists of Booleans, which must be quoted, that indicate for fn which inputs or values (respectively) are dfs. For example, if fn returns a single value, then dfs-out is (t) if the call of fn is a df, else dfs-out is optional but may be supplied as (nil). If fn returns n values where n is greater than 1, then dfs-out should be a list of length n where for each zero-based index i less than n, the ith element of dfs is t if the ith return value is a df (or more precisely, in the language of :DOC df, calls of fn are df{i} expressions), else nil. The rules for the :dfs-in argument are analogous for inputs of the call of fn.

When there are no df inputs (respectively, outputs) of the call, then :dfs-in (respectively, :dfs-out may be omitted or supplied as nil or 'nil.