EC-CALL

execute a call in the ACL2 logic instead of raw Lisp 
Major Section:  ACL2-BUILT-INS

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 Form:
(ec-call (fn term1 ... termk))
where fn is a known function symbol other than those in the list that is the value of the constant *ec-call-bad-ops*. In particular, fn is not a macro. 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 fn as defined in raw Lisp. 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.

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 a 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 (the so-called ``*1*'' function for foo) checks the guard and then invokes the raw Lisp version of foo. The raw Lisp 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 >