APT isomorphic data transformation: change function arguments and results into isomorphic representations.

This transformation changes the representation of one or more of a function's arguments and results into an isomorphic representation. This transformation is useful to carry out certain data type refinements (when synthesizing programs), or to raise the level of abstraction of certain types (when analyzing programs).

When at least one argument's representation is being changed, then by regarding the arguments whose representation is not changed as being changed via an indentity isomorphism, we can say that this transformation changes the representation of (the tuple of) all the function's arguments into a new representation that consists of (the tuple of) all the new function's arguments. In this case, there are two variants of this transformation:

- When the function operates only on argument tuples in the old representation (i.e. when the function's guard is a subset of the old representation), the function is transformed to operate in the same way on exactly the argument tuples in the new representation that are isomorphic to the old guard.
- When the function operates on at least all the tuples in the old representation (and possibly more) (i.e. the function's guard is a superset of the old representation), and is used as a predicate to recognize a subset of argument tuples all of which are in the old representation, the function is transformed to recognize exactly the argument tuples in the new representation that are isomorphic to the ones recognized by the old function.

These two variants involve slightly different applicability conditions
and produce slightly different results.
These two variants are selected
via the

If only the representation of some results (and of no arguments) is changed, then there is a single variant of this transformation, namely one that operates on the same tuples as the old function but returns isomorphic results in the new representation.

These

The

(isodata old isomaps :predicate ; default nil :undefined ; default :auto :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 :newp-of-new-name ; default :auto :newp-of-new-enable ; default t :verify-guards ; default :auto :untranslate ; default :nice :hints ; default nil :print ; default :result :show-only ; default nil :compatibility ; 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, and have no input or output stobjs. If the:predicate input (see below) ist , thenold must return a non-multiple value. Ifold is recursive, it must be singly (not mutually) recursive, not have a:? measure, and not occur in its own termination theorem (i.e. not occur in the tests and arguments of its own recursive calls). If the:verify-guards input ist ,old must be guard-verified.In the rest of this documentation page:

- Let
x1 , ...,xn be the arguments ofold , wheren > 0.- Let
m > 0 be the number of results ofold .- 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> ... update1-xn<x1,...,xn>) ... (old updater-x1<x1,...,xn> ... updater-xn<x1,...,xn>)>be the body ofold , wherer > 0 is the number of recursive calls in the body ofold and eachupdatek-xi<x1,...,xn> is thei -th actual argument passed to thek -th recursive call. Furthermore, letcontextk<x1,...,xn> be the context (i.e. controlling tests) in which thek -th recursive call occurs, and letmeasure<x1,...,xn> be the measure term ofold .In the

isodata design notes,old is denoted byf when:predicate isnil , andp when:predicate ist .

Specifies the arguments and results of

old that are transformed and the way in which they are transformed.It must be a non-empty list of doublets

((arg/res-list1 iso1) ... (arg/res-listq isoq)) , where:

Each

arg/res-listk denotes the subset of the arguments and results ofold whose representation is transformed according toisok .It must be one of the following:

- A list without duplicates of elements among
x1 , ...xn ,:result1 , ...,:resultm , in any order. The list is allowed to be empty (to facilitate iterative development), in which case the doublet does not induce any transformation.- A single element among
x1 , ...xn ,:result1 , ...,:resultm , abbreviating the singleton list with that element.- The single element
:result , abbreviating the singleton list:result1 . This is allowed only ifm is 1.Each

isok denotes the isomorphic mapping to apply to the arguments and results inarg/res-listk . Eachisok specifies old and new representations and the conversions between them.It must be one of the following:

- A symbol that references a previous successful call of
defiso, i.e. the symbol must be thename input of that call. The domains and conversions recorded under that name specify: the recognizer of the old representation (doma ), which we calloldp here; the recognizer of the new representation (domb ), which we callnewp here; the conversion from the old to the new representation (alpha ), which we callforth here; and the conversion from the new to the old representation (beta ), which we callback here. Botholdp andnewp must be unary. If the generated function is guard-verified (which is determined by the:verify-guards input; see below), the call ofdefisomust have:guard-thms equal tot , i.e. it must have proved and recorded the guard-related theorems.- A list
(oldp newp forth back :hints hints) such that the call(defiso name oldp newp forth back :guard-thms guard-thms :thm-names thm-names :hints hints) is successful, wherename andthm-names consist of suitably fresh names, and whereguard-thms ist if the generated function is guard-verified (which is determined by the:verify-guards input; see below) andnil otherwise. A list(oldp newp forth back) abbreviates(oldp newp forth back :hints nil) . Theisodata transformation generates this call ofdefiso, and uses it in the same way as it uses a call referenced byiso wheniso is a symbol; however, this generateddefisocall is local to theencapsulategenerated byisodata , and cannot be therefore referenced after the call ofisodata .The lists

arg/res-list1 , ...,arg/res-listq are pairwise disjoint, i.e. eachxi and:result appears in at most one of those lists.In the rest of this documentation page, for each

i from 1 ton , letoldpi ,newpi ,forthi , andbacki be:

- The
oldp ,newp ,forth , andback of the (pre-existing or locally generated)defisospecified byisok , ifxi is inarg/res-listk .- The functions
(lambda (x) t) ,(lambda (x) t) ,(lambda (x) x) , and(lambda (x) x) that form the identity isomorphic mapping over all values, ifxi is not in anyarg/res-listk .Furthermore, for each

j from 1 tom , letoldp_rj ,newp_rj ,forth_rj , andback_rj be:

- The
oldp ,newp ,forth , andback of the (pre-existing or locally generated)defisospecified byisok , if:resultj is inarg/res-listk .- The functions
(lambda (x) t) ,(lambda (x) t) ,(lambda (x) x) , and(lambda (x) x) that form the identity isomorphic mapping over all values, if:resultj is not in anyarg/res-listk .In the

isodata design notes, the section `Compositional Establishment of Isomorphic Mappings on Tuples' describes the compositional establishment of an isomorphic mapping between the inputs of old and new function. Theisomaps input currently supported by this transformation amounts to the following partitioning and sub-mappings:

- The new function's arguments are the same (i.e. have the same names) as the old function's arguments, i.e.
x1 , ...,xn .- The new function has the same number of results as the old function.
- The arguments are partitioned into
n singleton partitions.- The results are partitioned into
m singleton partitions.- The isomorphic mapping consisting of
oldpi ,newpi ,forthi , andbacki is used for the partition consisting of argumentxi .- The isomorphic mapping consisting of
oldp_rj ,newp_rj ,forth_rj , andback_rj is used for the partition consisting of resultj .- The identity isomorphic mapping is used for the partitions of all the results, if
:result is not in anyarg/res-listk .In the design notes, the resulting isomorphic mapping over all function arguments is denoted as consisting of the domains

A andA' and the conversions\alpha and\alpha' , and the resulting isomorphic mapping over all function results is denoted as consisting of the domainsB andB' and the conversions\beta and\beta' .

Selects between the two variants of this transformation:

t , to select the variant in whichold is treated like a predicate that recognizes argument tuples that are all in the old representation.nil , to select the variant in whichold is treated as a function that operates only on argument tuples that are all in the old representation.This input may be

t only ifisomaps does not include:result .In the

isodata design notes, the sections with `Function' in their title refer to the case in which:predicate isnil , while the sections with `Predicate' in their title refer to the case in which:predicate ist .

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

It must be one of the following:

:auto , to usenil or(mv nil ... nil) for single-value and multi-value functions respectively.:base-case-then , to search for a base-case within the domain of the new function. A base-case of a term may be be the whole term when the term does not include any recursive calls, or it may be a base-case of the `then' or `else' branch when the translated term is an `if'. This search for a base-case is biased toward `then' branches.:base-case-else , to search for a base-case with a bias toward `else' branches.- Any other term. It must be a term that only references logic-mode functions and that includes no free variables other than
x1 , ...,xn . This term must have no output ACL2::stobjs. This term must return the same number of results asold . This term must not referenceold .If one wishes to use the term

:auto as the undefined result, this may be accomplished by providing the quoted constant':auto . The same applies for:base-case-then and:base-case-else .Even if the generated function is guard-verified (which is determined by the

:verify-guards input; see below), the undefined term need 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 specified by:undefined .

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 the name of the theorem asserting that

new maps arguments in the new representation to results in the new representation.It must be one of the following:

:auto , to use the concatenation of the name ofnew followed by-new-representation , in the same package asnew .- Any other symbol, to use as the name of the theorem.
This input may be present only if

isomaps includes some:resultj .In the rest of this documentation page, let

newp-of-new be the name of this theorem.

Determines whether

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

t , to enable the theorem.nil , to disable the theorem.This input may be present only if

isomaps includes some:resultj .

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.

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.

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 ofisodata . 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 ofisodata .: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

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

Determines whether the event expansion of

isodata 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 ofisodata is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

This is a temporary option that is not documented because it should not be used, except in very specific transitional situations.

In order for

The following conditions must be proved in order for the transformation to apply.

old maps arguments in the old representation to results in the old representation:;; when m = 1: (implies (and (oldp1 x1) ... (oldpn xn)) (oldp_r1 (old x1 ... xn))) ;; when m > 1: (implies (and (oldp1 x1) ... (oldpn xn)) (mv-let (y1 ... ym) (old x1 ... xn) (and (oldp_r1 y1) ... (oldp_rm ym))))This corresponds to

fAB in theisodata design notes.This applicability condition is present if and only if

isomaps includes some:resultj .

old holds only on argument tuples such thatx1 , ...,xn are all in the old representation:(implies (old x1 ... xn) (and (oldp1 x1) ... (oldpn xn)))This corresponds to

pA in theisodata design notes.This applicability condition is present if and only if

:predicate ist .

The old representation is preserved on the arguments of the recursive calls of

old :(implies (and (oldp1 x1) ... (oldpn xn)) (and (implies context1<x1,...,xn> (and (oldp1 update1-x1<x1,...,xn>) ... (oldpn update1-xn<x1,...,xn>))) ... (implies contextr<x1,...,xn> (and (oldp1 updater-x1<x1,...,xn>) ... (oldpn updater-xp<x1,...,xn>)))))This corresponds to

Ad in theisodata design notes.This applicability condition is present if and only if

old is recursive.

old is well-defined (according to its guard) only on tuples in the old representation:(implies old-guard<x1,...,xn> (and (oldp1 x1) ... (oldpn xn)))This corresponds to

Gf in theisodata 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) and:predicate isnil .

old is well-defined (according to its guard) on all tuples in the old representation:(implies (and (oldp1 x1) ... (oldpn xn)) old-guard<x1,...,xn>)This corresponds to

Gp in theisodata 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) and:predicate ist .

Unless `defiso`s,
there are additional applicability conditions
that pertain to the locally generated `defiso`s.
These additional applicability conditions are described
in the documentation of `defiso`.

Isomorphic version of

old :;; when old is not recursive ;; and :predicate is t: (defun new (x1 ... xn) (and (mbt$ (and (newp1 x1) ... (newpn xn))) old-body<(back1 x1),...,(backn xn)>)) ;; when old is not recursive, ;; :predicate is nil: ;; and isomaps includes no :resultj: (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) old-body<(back1 x1),...,(backn xn)> undefined)) ;; when old is not recursive, ;; :predicate is nil, ;; m = 1, ;; and isomaps includes :result1 (or :result): (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) (forth_r1 old-body<(back1 x1),...,(backn xn)>) undefined)) ;; where forth_r1 is actually pushed into ;; the 'if' branches of old-body if it starts with 'if', ;; and recursively into their 'if' branches (if any) ;; when old is not recursive, ;; :predicate is nil, ;; m > 1, ;; and isomaps includes some :resultj: (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) (mv-let (y1 ... ym) old-body<(back1 x1),...,(backn xn)> (mv (forth_r1 y1) ... (forth_rm ym))) undefined)) ;; when old is recursive ;; and :predicate is t: (defun new (x1 ... xn) (and (mbt$ (and (newp1 x1) ... (newpn xn))) old-body<(back1 x1),...,(backn xn), (new (forth1 update1-x1<(back1 x1), ..., (backn xn)>) ... (forthn update1-xn<(back1 x1), ..., (backn xn)>)), ... (new (forth1 updater-x1<(back1 x1), ..., (backn xn)>) ... (forthn updater-xn<(back1 x1), ..., (backn xn)>))>)) ;; when old is recursive, ;; :predicate is nil, ;; and isomaps includes no :resultj: (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) old-body<(back1 x1),...,(backn xn), (new (forth1 update1-x1<(back1 x1), ..., (backn xn)>) ... (forthn update1-xn<(back1 x1), ..., (backn xn)>)), ... (new (forth1 updater-x1<(back1 x1), ..., (backn xn)>) ... (forthn updater-xn<(back1 x1), ..., (backn xn)>))> undefined)) ;; when old is recursive, ;; :predicate is nil, ;; m = 1, ;; and isomaps include :result1 (or :result): (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) (forth_r1 old-body<(back1 x1),...,(backn xn), (back_r1 (new (forth1 update1-x1<(back1 x1), ..., (backn xn)>) ... (forthn update1-xn<(back1 x1), ..., (backn xn)>))), ... (back_r1 (new (forth1 updater-x1<(back1 x1), ..., (backn xn)>) ... (forthn updater-xn<(back1 x1), ..., (backn xn)>)))>) undefined)) ;; where forth_r1 is actually pushed into ;; the 'if' branches of old-body if it starts with 'if', ;; and recursively into their 'if' branches (if any) ;; when old is recursive, ;; :predicate is nil, ;; m > 1, ;; and isomaps includes some :resultj: (defun new (x1 ... xn) (if (mbt$ (and (newp1 x1) ... (newpn xn))) (mv-let (y1 ... ym) old-body<(back1 x1),...,(backn xn), (mv-let (y1 ... ym) (new (forth1 update1-x1<(back1 x1), ..., (backn xn)>) ... (forthn update1-xn<(back1 x1), ..., (backn xn)>)) (mv (back_r1 y1) ... (back_rm ym))), ... (mv-let (y1 ... ym) (new (forth1 updater-x1<(back1 x1), ..., (backn xn)>) ... (forthn updater-xn<(back1 x1), ..., (backn xn)>)) (mv (back_r1 y1) ... (back_rm ym)))> (mv (forth_r1 y1) ... (forth_rm ym))) undefined))If

old is recursive, the measure term ofnew ismeasure<(back1 x1),...,(backn xn)> and the well-founded relation ofnew is the same asold .The guard of

new is:;; when :predicate is nil: (and (newp1 x1) ... (newpn xn) old-guard<(back1 x1),...,(backn xn)>) ;; when :predicate is t: (and (newp1 x1) ... (newpn xn))That is, when

:predicate ist the guard consists of the new representation; when:predicate isnil , the guard consists of the argument tuples that are isomorphic to the ones in the guard ofold .In the

isodata design notes,new is denoted byf' when:predicate isnil , andp' when:predicate ist .Note that:

- When
:predicate ist ,new is defined to hold exactly on the argument tuples in the new representation that are isomorphic the argument tuples in the old representation on whichold holds.- When
:predicate isnil ,new is defined to map each argument tuple in the new representation to the same or isomorphic value thatold maps the isomorphic argument tuple in the old representation.

Theorem that relates

new toold :;; when :predicate is t: (defthm new-to-old (implies (and (newp1 x1) ... (newpn xn)) (equal (new x1 ... xn) (old (back1 x1) ... (backn xn))))) ;; when :predicate is nil ;; and isomaps includes no :resultj: (implies (and (newp1 x1) ... (newpn xn)) (equal (new x1 ... xn) (old (back1 x1) ... (backn xn)))) ;; when :predicate is nil, ;; m = 1, ;; and isomaps includes :result1 (or :result): (implies (and (newp1 x1) ... (newpn xn)) (equal (new x1 ... xn) (forth_r1 (old (back1 x1) ... (backn xn))))) ;; when :predicate is nil, ;; m > 1, ;; and isomaps includes some :resultj: (implies (and (newp1 x1) ... (newpn xn)) (equal (new x1 ... xn) (mv-let (y1 ... ym) (old (back1 x1) ... (backn xn)) (mv (forth_r1 y1) ... (forth_rm ym)))))In the

isodata design notes,new-to-old is denoted byf'f when:predicate isnil , and'pp when:predicate ist .

Theorem that relates

old tonew :;; when :predicate is t: (defthm old-to-new (implies (and (oldp1 x1) ... (oldpn xn)) (equal (old x1 ... xn) (new (forth1 x1) ... (forthn xn))))) ;; when :predicate is nil ;; and isomaps includes no :resultj: (defthm old-to-new (implies (and (oldp1 x1) ... (oldpn xn)) (equal (old x1 ... xn) (new (forth1 x1) ... (forthn xn))))) ;; when :predicate is nil, ;; m = 1, ;; and isomaps includes :result1 (or :result): (defthm old-to-new (implies (and (oldp1 x1) ... (oldpn xn)) (equal (old x1 ... xn) (back_r1 (new (forth1 x1) ... (forthn xn)))))) ;; when :predicate is nil, ;; m > 1, ;; and isomaps includes some :resultj: (defthm old-to-new (implies (and (oldp1 x1) ... (oldpn xn)) (equal (old x1 ... xn) (mv-let (y1 ... ym) (new (forth1 x1) ... (forthn xn)) (mv (back_r1 y1) ... (back_rm ym)))))In the

isodata design notes,old-to-new is denoted byff' when:predicate isnil , andpp' when:predicate ist .

Theorem asserting that

new maps arguments in the new representation to results in the new representation:;; when m = 1: (defthm newp-of-new (implies (and (newp1 x1) ... (newpn xn)) (newp_r1 (new x1 ... xn)))) ;; when m > 1: (defthm newp-of-new (implies (and (newp1 x1) ... (newpn xn)) (mv-let (y1 ... ym) (new x1 ... xn) (and (newp_r1 y1) ... (newp_rm ym)))))In the

isodata design notes,newp-of-new is denoted byf'A'B' .This is generated if and only if

isomaps includes some:resultj .

A theory invariant is also generated to prevent
both

A call of

A call of

- Isodata-implementation
- Implementation of
`isodata`.