Atj-pre-translation-type-annotation
Pre-translation step performed by ATJ:
addition of type annotations.
This is done only in the shallow embedding.
This step annotates ACL2 terms with ATJ types:
(i) each ACL2 term is wrapped with a function named [src>dst],
where src identifies the ATJ types of the term
and dst identifies ATJ types to which the term must be converted to;
(ii) each ACL2 variable var in a term is renamed to [type]var,
where type identifies the ATJ type of the variable.
Both src and dst above identify non-empty lists of ATJ types.
This is because an ACL2 term may return multiple values (see mv):
each list consists of two or more ATJ types when he ACL2 term does;
otherwise, it consists of one ATJ type only.
The two lists (for src and dst) will always have the same length,
because ACL2 prevents treating
single values as multiple values,
multiple values as single values,
or multiple values of a certain number
as multiple values of a different number.
Non-executable functions relax these restrictions,
but their body includes calls of acl2::throw-nonexec-error,
which has raw Lisp code and is currently not whitelisted by ATJ.
These annotations facilitate the ACL2-to-Java translation,
which uses the type annotations as ``instructions'' for
(i) which types to declare Java local variables with, and
(ii) which Java conversion code to insert around expressions.
The annotated terms are still ACL2 terms, but with a specific structure.
This should let us prove, in the ACL2 logic,
the equality of the annotated terms with the original terms,
under suitable variable rebinding,
and by introducing the [src>dst] functions as identities.
(This has not been done yet.)
Subtopics
- Atj-type-annotate-term
- Add ATJ type annotations to ACL2 terms.
- Atj-check-annotated-mv-let-call
- Recognize and decompose type-annotated mv-lets.
- Atj-type-conv-allowed-p
- Ensure that a conversion between ATJ types is allowed.
- Atj-type-annotate-formals+body
- Add ATJ type annotations to the formal parameters and body
of an ACL2 function definition.
- Atj-type-rewrap-term
- Re-wrap an ACL2 term with a type conversion function.
- Atj-type-conv
- ATJ type conversion function names used to annotate ACL2 terms.
- Atj-type-unwrap-term
- Unwrap an ACL2 term wrapped by atj-type-wrap-term.
- Atj-type-id
- Short string identifying an ATJ type.
- Atj-type-wrap-term
- Wrap an ACL2 term with a type conversion function.
- Atj-types-id
- String identifying a non-empty list of ATJ types.
- Atj-types-of-conv
- Source and destination ATJ types of a conversion function.
- Atj-types-conv-allowed-p
- Lift atj-type-conv-allowed-p to lists of types.
- Atj-type-annotate-var
- Annotate an ACL2 variable with a non-empty list of types.
- Atj-type-unannotate-var
- Decompose an annotated ACL2 variable into
its unannotated counterpart and its types.
- Atj-type-of-id
- ATJ type identified by a short string.
- Atj-types-of-id
- Non-empty list of ATJ types identified by
a concatenation of short strings.
- Atj-type-annotate-mv-nth-terms
- Atj-type-annotate-vars
- Annotate each of a list of ACL2 variable
with a corresponding singleton list of types.
- Atj-select-mv-term-types
- Atj-type-unannotate-vars
- Remove the type annotations from a list of variables.
- Atj-type-rewrap-terms
- Lift atj-type-rewrap-term to lists.
- Atj-type-wrapped-variable-p
- Check whether an annotated term is a variable.