Atj-type-to-jitype
Java input type denoted by an ATJ type.
- Signature
(atj-type-to-jitype type) → jtype
- Arguments
- type — Guard (atj-typep type).
- Returns
- jtype — Type (atj-jitypep jtype).
The :acl2 types except
:aboolean, :acharacter, and :astring
denote the corresponding AIJ class types.
The :aboolean type denotes
the Java primitive type boolean.
The :acharacter type denotes
the Java primitive type char.
The :astring type denotes
the Java reference type java.lang.String.
The :jprim types denote
the corresponding Java primitive types.
The :jprimarr types denote
the corresponding Java primitive array types.
The mapping of :aboolean, :acharacter, and :astring
to the Java boolean, char, and String types
means that we represent
ACL2 booleans as Java booleans,
ACL2 characters as Java characters, and
ACL2 strings as Java strings.
This only happens in the shallow embedding approach;
the deep embedding approach does not use ATJ types.
Also, :aboolean, :acharacter, and :astring
are used only if :guards is t;
otherwise, only the type :avalue is used.
In other words, we represent
ACL2 booleans/characters/strings as Java booleans/characters/strings
only when :deep is nil and :guards is t.
Even though Java char values (which consist of 16 bits)
are not isomorphic to ACL2 characters (which consist of 8 bits),
when :guards is t the satisfaction of all guards is assumed;
thus, if external code calls the generated Java code
with values that satisfy the guards,
and in particular with char values below 256,
the generated code should manipulate only char values below 256,
which are isomorphic to ACL2 characters.
The same consideration applies to ACL2 strings vs. Java strings;
only Java strings with characters below 256
should be passed to ATJ-generated code,
which will only manipulate strings satisfying that property.
Definitions and Theorems
Function: atj-type-to-jitype
(defun atj-type-to-jitype (type)
(declare (xargs :guard (atj-typep type)))
(let ((__function__ 'atj-type-to-jitype))
(declare (ignorable __function__))
(atj-type-case
type
:acl2 (atj-atype-case type.get
:integer *aij-type-int*
:rational *aij-type-rational*
:number *aij-type-number*
:character (jtype-char)
:string (jtype-class "String")
:symbol *aij-type-symbol*
:boolean (jtype-boolean)
:cons *aij-type-cons*
:value *aij-type-value*)
:jprim (primitive-type-case type.get
:boolean (jtype-boolean)
:char (jtype-char)
:byte (jtype-byte)
:short (jtype-short)
:int (jtype-int)
:long (jtype-long)
:float (jtype-float)
:double (jtype-double))
:jprimarr
(primitive-type-case type.comp
:boolean (jtype-array (jtype-boolean))
:char (jtype-array (jtype-char))
:byte (jtype-array (jtype-byte))
:short (jtype-array (jtype-short))
:int (jtype-array (jtype-int))
:long (jtype-array (jtype-long))
:float (jtype-array (jtype-float))
:double (jtype-array (jtype-double))))))
Theorem: atj-jitypep-of-atj-type-to-jitype
(defthm atj-jitypep-of-atj-type-to-jitype
(b* ((jtype (atj-type-to-jitype type)))
(atj-jitypep jtype))
:rule-classes :rewrite)
Theorem: atj-type-to-jitype-of-atj-type-fix-type
(defthm atj-type-to-jitype-of-atj-type-fix-type
(equal (atj-type-to-jitype (atj-type-fix type))
(atj-type-to-jitype type)))
Theorem: atj-type-to-jitype-atj-type-equiv-congruence-on-type
(defthm atj-type-to-jitype-atj-type-equiv-congruence-on-type
(implies (atj-type-equiv type type-equiv)
(equal (atj-type-to-jitype type)
(atj-type-to-jitype type-equiv)))
:rule-classes :congruence)
