Atj-tutorial-deep-guards
ATJ tutorial: Guards in the Deep Embedding Approach.
This tutorial page describes the effect of ATJ's :guards option
when :deep is t, i.e. in the deep embedding approach. The effect of :guards in the shallow embedding approach
is described in later tutorial pages.
Even though, as noted in atj-tutorial-deep-shallow,
the shallow embedding approach is generally preferred over the deep one,
some of the concepts common to the two approaches are discussed here.
So, if this tutorial page is skipped at first reading,
it may be necessary to come back to it
while reading the pages on the shallow embedding approach.
Ignoring Guards
As briefly noted in the factorial example in atj-tutorial-deep,
the option :guards nil specifies
not to assume the satisfaction of guards.
More precisely, this option tells ATJ that the generated Java code
must mimic ACL2's execution in the logic, i.e. ignoring guards completely.
(Indeed, AIJ's representation of the ACL2 function definitions currently does not even include the functions' guards.)
ACL2's execution in the logic is described in the manual page on ACL2 evaluation. It means that ACL2 functions, which are total in the logic,
may be called on any argument values (inside or outside the guards),
and functions will return the corresponding results.
For instance, one can call car on a number and obtain nil,
or call binary-+ on a symbol and a string and obtain 0.
Accordingly, the call(Acl2Symbol, Acl2Value[]) method
generated by ATJ (see atj-tutorial-deep)
accepts any array of Acl2Values,
independently from the guard of the function named by the Acl2Symbol,
and returns the resulting Acl2Value.
When ACL2 executes in the logic,
calls of the form (mbe :logic a :exec b)
are executed as just a, ignoring b.
Untranslated ACL2 terms of the form (mbe :logic a :exec b)
are translated to the form (return-last 'acl2::mbe1-raw b a).
Therefore, with the option :guards nil,
ATJ treats terms (return-last 'acl2::mbe1-raw b a)
as if they were just a,
for the purpose of generating Java code:
that is, ATJ generates Java code for a, ignoring b.
This is also discussed in atj-tutorial-translated.
Assuming Guards
The :guards t option tells ATJ to assume that all guards are satisfied.
This assumption is not checked by ATJ.
Ideally, it should be only used when
the ACL2 functions that ATJ translates to Java are all guard-verified,
or at least when the user is confident that
guards should be always satisfied.
Furthermore, external Java code that calls ATJ-generated code
must do so with values that satisfy the guards of the called functions.
If any of these assumption of guard satisfaction is violated
(whether due to internal calls if guards are not verified,
or to external calls even if guards are verified),
the Java code generated by ATJ may behave in unpredictable ways.
It should be possible to extend the code generated by ATJ
to check guards under suitable conditions,
in particular at the top level (i.e. for calls from external Java code),
as ACL2 does by default even for guard-verified code.
In fact, it should be possible to mimic ACL2's various guard checking modes in ATJ-generated Java code.
This is future work.
Currently, in the deep embedding approach,
the only effect of assuming guard satisfaction is that
for terms (return-last 'acl2::mbe1-raw b a),
which result from translating (mbe :logic a :exec b),
ATJ generates Java code for b, ignoring a.
Compare this with the description above for :guards nil.
When ACL2 executes in raw Lisp (i.e. not in the logic),
calls of the form (mbe :logic a :exec b)
are executed as just b, ignoring a.
Compare this with the description above for execution in the logic.
Even with :guards t, the call(Acl2Symbol, Acl2Value[]) method
generated by ATJ (see atj-tutorial-deep)
accepts any array of Acl2Values,
whether they satisfy the guard of the function named by the Acl2Symbol
or not.
If they do not, unpredictable behavior may occur.
Given that, in the deep embedding approach,
the ACL2 functions are executed via AIJ's Java interpreter, it is natural for all the ACL2 values manipulated by the interpreter
to have the same Java type (i.e. Acl2Value),
rather than using narrower types derived from the guards.
Executing the :exec portion of mbes
may be much faster than executing the :logic portion.
For example, some fixing functions use mbe
to logically fix values without any run-time penalty:
the :exec part does nothing,
while the :logic part may perform expensive computations,
e.g. fix every element of a long list.
As another examples, mbts are really mbes
that do nothing in the :exec part
but may perform expensive tests in the :logic part.
Thus, if the assumption of guard satisfaction can be supported,
it may be advantageous to use :guards t
in the deep embedding approach,
even if the difference with :guards nil
is just the treatment of (translated) mbes.
The difference between :guards nil and :guards t
is much more significant in the shallow embedding approach.
This is described in detail in later tutorial pages.
Previous: ACL2 Functions Translated To Java
Next: Generation of Tests
