		Search-engine friendly clone of the ACL2 documentation.

Parteval

APT partial evaluation transformation: specialize a function by setting one or more parameters to specified constant values.

Introduction

Partial evaluation is a well-known program transformation technique. This APT transformation realizes this technique in ACL2. Partial evaluation is a broad topic; the current version of this APT transformation is relatively simple, but will be extended in the future.

This partial evaluation transformation specializes an ACL2 function by setting some of its parameters to specified constant values, and eliminating such parameters from the function. In partial evaluation terminology, the parameters that are set to constant values are static, while the remaining parameters are dynamic.

This transformation is related to restrict, which also specializes a function, but does not change its parameters.

The parteval design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to them in some places.

General Form

(parteval old
          static
          :new-name       ; default :auto
          :new-enable     ; default :auto
          :thm-name       ; default :auto
          :thm-enable     ; default t
          :verify-guards  ; default :auto
          :untranslate    ; default :nice
          :print          ; default :result
          :show-only      ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be in logic mode, be defined, return a non-multiple value, and have no input or output stobjs. If the :verify-guards input is t, old must be guard-verified.
In the rest of this documentation page:
Let x1, ..., xn, y1, ..., ym be the formal parameters of old, where n \geq 0 and m > 0.
Let old-guard<x1,...,xn,y1,...,ym> be the guard term of old.
Let old-body<x1,...,xn,y1,...,ym> be the body of old.
The current implementation distinguishes the following three cases:
old is not recursive. In this case, let its body be old-body<x1,...,xn,y1,...,ym>.
old is recursive, y1, ..., ym are unchanged in all the recursive calls, and old does not occur in its termination theorem. In this case, let its body be
old-body<x1,...,xn,y1,...,ym,
         (old update1-x1<x1,...,xn,y1,...,ym>
              ...
              update1-xn<x1,...,xn,y1,...,ym>
              y1 ... ym)
         ...
         (old updatep-x1<x1,...,xn,y1,...,ym>
              ...
              updatep-xn<x1,...,xn,y1,...,ym>
              y1 ... ym)>
old is recursive but it does not satisfy some of the conditions in case 2 above.
In the parteval design notes, old is denoted by f.

static

Specifies the static parameters of old, along with the constant values to assign to these parameters.
It must be a non-empty list of doublets ((y1 c1) ... (ym cm)). Each yj must be a parameter of old. The y1, ..., ym must be all distinct. Each cj must be a ground term that only calls logic-mode functions, that returns a non-multiple value, and that has no output stobjs. If the generated function is guard-verified (which is determined by the :verify-guards input; see below), then each cj must only call guard-verified functions, except possibly in the :logic subterms of mbes and via ec-call. Each cj must not include any calls to old.
The transformation specializes old by setting each yj to the value of the term cj.
In this documentation page, for expository convenience, the static parameters y1, ..., ym come after the dynamic parameters x1, ..., xn. However, this is not required: static and dynamic parameters can be intermixed in any way.
In the parteval design notes, cj is denoted by \widetilde{y}_j, for 1 \leq j \leq m.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

thm-name — default :auto

Determines the name of the theorem that relates old to new:
:auto, to use the paired name obtained by pairing the name of old and the name of new, putting the result into the same package as new.
Any other symbol (that is not in the main Lisp package and that is not a keyword), to use as the name of the theorem.
In the rest of this documentation page, let old-to-new be this theorem.

:thm-enable — default t

Determines whether old-to-new is enabled:
t, to enable it.
nil, to disable it.
If old has the form of case 3 above and new is enabled (as determined by the :new-enable input), then :thm-enable cannot be t.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:untranslate — default :nice

Specifies if and how the body of new should be turned from internal translated form to external untranslated form.
It must be an untranslate specifier; see that documentation topic for details.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of parteval. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of parteval.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of parteval is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of parteval is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of parteval is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Generated Events

new

Specialized version of old, where cases 1, 2, and 3 refer to the description of old above:
;; case 1:
(defun new (x1 ... xn)
  old-body<x1,...,xn,c1,...,cm>)

;; case 2:
(defun new (x1 ... xn)
  old-body<x1,...,xn,c1,...,cm,
           (new update1-x1<x1,...,xn,c1,...,cm>
                ...
                update1-xn<x1,...,xn,c1,...,cm>)
           ...
           (new updatep-x1<x1,...,xn,c1,...,cm>
                ...
                updatep-xn<x1,...,xn,c1,...,cm>)>)

;; case 3:
(defun new (x1 ... xn)
  (old x1 ... xn c1 ... cm))
The guard is old-guard<x1,...,xn,c1,...cm>.
In case 2, the measure is the same as old.
In case 3, the new function is not recursive. This is simple, preliminary approach; support for more forms of recursive functions (besides case 2) may be added in the future.
In the parteval design notes, new is denoted by f'.

old-to-new

Theorem that relates old to new:
(defthm old-to-new
  (implies (and (equal y1 c1)
                ...
                (equal ym cm)
           (equal (old x1 ... xn y1 ... ym)
                  (new x1 ... xn)))
In the parteval design notes, old-to-new is denoted by \mathit{ff}'.

Redundancy

A call of parteval is redundant if and only if it is identical to a previous successful call of parteval whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of parteval whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Parteval-implementation: Implementation of parteval.