APT domain restriction transformation: restrict the effective domain of a function.

Even though functions are total in ACL2 (i.e. their domain is always the whole ACL2 universe of values), the guard of a function can be regarded as its effective domain (i.e. where it is well-defined). This transformation adds restrictions to the guard, and wraps the body with a test for the restrictions, which may enable further optimizations by taking advantage of the added restrictions. As a special case, this transformation can leave the guard unchanged but wrap the body with a test for the guard, thus treating the guard as the restriction: this may enable further optimizations by effectively removing from consideration, in the body of the function, conditions under which the guard does not hold.

The

(restrict old restriction :undefined ; default :undefined :new-name ; default :auto :new-enable ; default :auto :old-to-new-name ; default from table :old-to-new-enable ; default from table :new-to-old-name ; default from table :new-to-old-enable ; default from table :verify-guards ; default :auto :hints ; default nil :print ; default :result :show-only ; default nil )

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, have at least one formal argument, return a non-multiple value, and have no input or output stobjs.Ifold is recursive, it must be singly (not mutually) recursive and not have a:? measure (see:measure inxargs). If the:verify-guards input ist ,old must be guard-verified.In the rest of this documentation page:

- Let
x1 , ...,xn be the formal arguments ofold , wheren > 0.- Let
old-guard<x1,...,xn> be the guard term ofold .- If
old is not recursive, letold-body<x1,...,xn>be the body ofold .- If
old is recursive, letold-body<x1,...,xn, (old update1-x1<x1,...,xn,old> ... update1-xn<x1,...,xn,old>) ... (old updatem-x1<x1,...,xn,old> ... updatem-xn<x1,...,xn,old>)>be the body ofold , wherem > 0 is the number of recursive calls in the body ofold and eachupdatej-xi<x1,...,xn,old> is thei -th actual argument passed to thej -th recursive call. Furthermore, letcontextj<x1,...,xn,old> be the context (i.e. controlling tests) in which thej -th recursive call occurs. The dependency ofupdatej-xi<...,old> andcontextj<...,old> onold only applies to so-called `reflexive functions', i.e. functions that occur in their own termination theorem.In the

restrict design notes,old is denoted byf . Whenold is not recursive,old-body<x1,...,xn> is denoted bye(\overline{x}) . Whenold is recursive, the design notes use a single non-recursive branchb(\overline{x}) controlled bya(\overline{x}) and a single recursive branchc(\overline{x},f(\overline{d}(\overline{x}))) controlled by the negation ofa(\overline{x}) : this is a representative recursive structure, but the transformation handles multiple non-recursive and recursive branches, and also recursive functions that occur in their termination theorem; in this representative recursive structure,update-xi<x1,...,xn> is denoted byd_i(\overline{x}) andcontext<x1,...,xn> is denoted by the negation ofa(\overline{x}) .

Denotes the restricting predicate for the domain of

old , i.e. the predicate that will be added to the guard (unless this input is:guard , see below), and as the test that wraps the body.It must be one of the following:

- A term that only references logic-mode functions and that includes no free variables other than
x1 , ...,xn . This term must have no output stobjs. This term must return a single (i.e. non-mv value. If the generated function is guard-verified (which is determined by the:verify-guards input; see below), then this term must only call guard-verified functions, except possibly in the:logic subterms ofmbe s or viaec-call . This term must not referenceold .This term must not be the keyword:guard , i.e. if therestriction input is:guard , it is treated as denoting the guard (see below), and not as denoting the term:guard , which may be denoted by using the quoted':guard as therestriction input instead (even though there is no use case for doing so).- They keyword
:guard .The

restriction input denotes the predicate(lambda (x1 ... xn) old-guard<x1,...,xn>) ifrestriction is:guard , otherwise it denotes the predicate(lambda (x1 ... xn) restriction) . In the rest of this documentation page, we refer to this predicate as(lambda (x1 ... xn) pred<x1,...,xn>) .Using

:guard as therestriction input is essentially equivalent to using the guard term ofold as therestriction input. However, using:guard is simpler and more robust (in the face of changes to the guard), and leads to a simpler guard in the new function (see `Generated Events' below).In the

restrict design notes,(lambda (x1 ... xn) pred<x1,...,xn>) is denoted byR .

Denotes the value that the generated new function must return outside of the domain restriction.

A term that only references logic-mode functions and that includes no free variables other thanx1 , ...,xn . This term must have no output stobjs. This term must return a single (i.e. non-mv value. This term must not referenceold .Even if the generated function is guard-verified (which is determined by the

:verify-guards input; see below), the term needs not be guard-verified. Since the term is governed by the negation of the guard (see the generated new function, below), the verification of its guards always succeeds trivially.In the rest of this documentation page, let

undefined be this term.

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.

Determines whether

new is enabled.It must be one of the following:

t , to enable it.nil , to disable it.:auto , to enable it iffold is enabled.

Determines the name of the theorem that rewrites the old function in terms of the new function.

It must be one of the following:

- A keyword, to use as separator between the names of
old andnew . A keyword:kwd specifies the theorem nameoldkwdnew , in the same package asnew .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-new-name.In the rest of this documentation page, let

old-to-new be the name of this theorem.

Determines whether the

old-to-new theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-old-to-new-enable.If this input is

t , the:new-to-old-enable input must benil . At most one of these two inputs may bet at any time.

Determines the name of the theorem that rewrites the new function in terms of the old function.

It must be one of the following:

- A keyword, to use as separator between the names of
new andold . A keyword:kwd specifies the theorem namenewkwdold , in the same package asnew .- Any other symbol, to use as the name of the theorem.
- Absent, to use the value from the APT defaults table, which is set via
set-default-input-new-to-old-name.In the rest of this documentation page, let

new-to-old be the name of this theorem.

Determines whether the

new-to-old theorem is enabled.It must be one of the following:

t , to enable the theorem.nil , to disable the theorem.- Absent, to use the value from the APT defaults table, which is set via
set-default-input-new-to-old-enable.If this input is

t , the:old-to-new-enable input must benil . At most one of these two inputs may bet at any time.

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 functionold are verified.

Hints to prove the applicability conditions.

It must be one of the following:

- A keyword-value list
(appcond1 hints1 appcond2 hints2 ...) , where eachappcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and eachhintsk is a list of hints of the kind that may appear just after:hints in adefthm. The hintshintsk are used to prove applicability conditionappcondk . Theappcond1 ,appcond2 , ... keywords must be all distinct. Anappcondk keyword is allowed only if the corresponding applicability condition is present, as specified in the `Applicability Conditions' section.- A list of hints of the kind that may appear just after
:hints in adefthm. In this case, these same hints are used to prove every applicability condition,.

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 ofrestrict . This is the default value of the:info , to print, besides any error output and the results, also some additional information about the internal operations ofrestrict .: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

restrict is redundant, an indication to that effect is printed on the screen, unlessnil .

Determines whether the event expansion of

restrict 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 ifnil (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:result or:info or:all ; no ACL2 output is printed for the event expansion even if:all (because the event expansion is not submitted). If the call ofrestrict is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

In order for

(lambda (x1 ... xn) pred<x1,...,xn>) is preserved across the recursive calls ofold :(implies pred<x1,...,xn> (and (implies context1<x1,...,xn,?f> pred<update1-x1<x1,...,xn,?f>, ..., update1-xn<x1,...,xn,?f>>) ... (implies contextm<x1,...,xn,?f> pred<updatem-x1<x1,...,xn,?f>, ..., updatem-xn<x1,...,xn,?f>>)))where

?f is ann -ary stub that replacesold (this only applies to reflexive functions; see above).This corresponds to

\mathit{Rd} in therestrict design notes.This applicability condition is present if and only if

old is recursive.

The restricting predicate is well-defined (according to its guard) on every value in the guard of

old :(implies old-guard<x1,...,xn> pred-guard<x1,...,xn>)where

pred-guard<x1,...,xn> is the guard obligation ofpred<x1,...,xn> .This corresponds to

\mathit{GR} in therestrict design notes.This applicability condition is present if and only if the generated function is guard-verified (which is determined by the

:verify-guards input; see above).

Domain-restricted version of

old :;; when old is not recursive: (defun new (x1 ... xn) (if (mbt$ pred<x1,...,xn>) old-body<x1,...,xn> undefined)) ;; when old is recursive: (defun new (x1 ... xn) (if (mbt$ pred<x1,...,xn>) old-body<x1,...,xn, (new update1-x1<x1,...,xn,new> ... update1-xn<x1,...,xn,new>) ... (new updatem-x1<x1,...,xn,new> ... updatem-xn<x1,...,xn,new>)> undefined))If

old is recursive, the measure term and well-founded relation ofnew are the same asold .The guard is

(and old-guard<x1,...,xn> pred<x1,...,xn>) if therestriction input is not:guard . Otherwise, the guard is justold-guard<x1,...,xn> .Since the restriction test follows from the guard, the test is wrapped by

mbt$. The use ofmbt$, as opposed tombt, avoids requiringpred<x1,...,xn> to be boolean-valued.In the

restrict design notes,new is denoted byf' .

Theorem that relates

old tonew :(defthm old-to-new (implies pred<x1,...,xn> (equal (old x1 ... xn) (new x1 ... xn))))In the

restrict design notes,old-to-new is denoted by\mathit{ff}' .

Theorem that relates

new toold :(defthm new-to-old (implies pred<x1,...,xn> (equal (new x1 ... xn) (old x1 ... xn))))In the

restrict design notes,new-to-old is denoted byf'f .

A theory invariant is also generated to prevent
both

A call of

A call of

- Restrict-implementation
- Implementation of
`restrict`.