6.72. kink/javahost/JAVA

Javaオブジェクト、値、クラス、メソッドを操作する方法を提供する。

JAVAモジュールは、ホストシステムとの、境界のはっきりした統合を提供する意図で設計されている。Kinkの世界とJavaの世界の間には、明確な境界がある。たとえば、JavaのメソッドをKinkの関数として直接呼び出すことはできない。その代わりに、 .call_method を通して呼び出さなければならない。

この設計にはいくつかの理由がある。

1) オブジェクトシステムと、実行の意味論の両方で、KinkとJavaは根本的に異なる。したがって、シームレスな統合を実現することは難しい。

2) 一般的に、規模の大きなアプリケーションは、異なるシステム間に境界がある方が簡潔に設計できる。

3) 明確な境界があることで、KinkはJavaと独立に改善できる。

型付け可能

ここでは、Javaのオブジェクト参照とJavaのクラスオブジェクトの間の二項関係、「型付け可能」を定義する。

オブジェクト参照RがクラスオブジェクトTで型付け可能であるとき、次の条件のうちひとつが成り立つ。

• Tが参照型を表すクラスオブジェクトで、かつRがその参照型のインスタンスである。

• Tが参照型を表すクラスオブジェクトで、かつRがnullである。

• RがBoolean, Character, Byte, Short, Integer, Long, Float, Doubleのいずれかのインスタンスであり、かつTが対応するプリミティブ型を表すクラスオブジェクトである。

以降では、クラスオブジェクトと、そのクラスオブジェクトが表す型を、区別せずに言及する。

6.72.1. java型

java値は、(objectReference, type)の対である。ここで、objectReferenceはJavaのオブジェクトの参照であり、typeはクラスオブジェクトである。

typeは、Javaのインスタンスメソッド、インスタンスフィールドを検索するために使われる。

不変条件

objectReferenceはtypeで型付け可能でなければならない。

6.72.1.1. J.type

typeメソッドは、Jのtype属性を戻す。

typeメソッドの結果は、java値(t, java.lang.Class)になる。ここでtは、Jのtype属性である。

例

6.72.1.2. J.as(New_type)

asは、typeをNew_typeに変える。

asの結果は、(ref, nt)のjava値になる。ここで、refはJのobjectReferenceであり、ntはNew_typeのobjectReferenceである。

事前条件

New_typeはjava値(nt, *)でなければならない。ここで、ntはクラスオブジェクトであり、JのobjectReferenceはntで型付け可能でなければならない。

例

6.72.1.3. J.instance_of?(Klass)

instance_of?は、JのobjectReferenceがKlassのインスタンスであるかどうかを戻す。このチェックは、Javaのinstanceof演算子と同値である。

事前条件

Klassはjava値(klass, *)でなければならない。ここでklassは、java.lang.Classのインスタンスでなければならない。

例

6.72.1.4. J.eq_eq?(Another)

eq_eq?は、JとAnotherのobjectReference属性が、Javaの == 演算子の意味で同一かどうかを戻す。

事前条件

Anotherはjava値でなければならない。

例

6.72.1.5. J.null?

null?は、JのobjectReference属性がnullであるかどうかを戻す。

6.72.1.6. J.to_kink_str

to_kink_strは、Java文字列からstr値を作って戻す。

事前条件

JのobjectReferenceはjava.lang.Stringのインスタンスでなければならない。

例

6.72.1.7. J.to_kink_bool

to_kink_boolは、Javaのbooleanからbool値を作って戻す。

事前条件

JのobjectReferenceはjava.lang.Booleanのインスタンスでなければならない。

例

6.72.1.8. J.to_kink_num

to_kink_numは、Javaの数値からnum値を作って戻す。

Character, Byte, Short, Integer, Long, BigIntegerからの変換

JのobjectReferenceがCharacter, Byte, Short, Integer, Long, BigIntegerのいずれかの場合、結果のnumのScaleは0になる。また、結果のnumのMantissaは元の整数になる。

Float, Doubleからの変換

JのobjectReferenceがFloatかDoubleの場合、結果のnumのScaleは、数値が正確に表現できる最小の非負の整数になる。また、Mantissaは `J * (10 ^ Scale)` になる。

0の符号は結果に保持されない。

BigDecimalからの変換

JのobjectReferenceがBigDecimalの場合、結果のnumのScaleはBigDecimal.scale()の結果と等しくなり、MantissaはBigDecimal.unscaledValue()の結果と等しくなる。

事前条件

JのobjectReferenceは、Character, Byte, Short, Integer, Long, Float, Double, BigInteger, BigDecimalのいずれかのインスタンスでなければならない。

参照がFloatかDoubleのとき、それはNaNや正負の無限大であってはならない。

参照がBigIntegerのとき: NUM.min_mantissa ≦ bigInteger ≦ NUM.max_mantissa

参照がBigDecimalのとき: 0 ≦ bigDecimal.scale() ≦ NUM.max_scale && NUM.min_mantissa ≦ bigDecimal.unscaledValue() ≦ NUM.max_mantissa

例

6.72.1.9. J.to_kink_bin(...[From To])

to_kink_binは、Javaのバイト配列からbin値を作って戻す。

Fromのデフォルト値は0である。Toのデフォルト値はバイト配列の長さである。

結果のbinの長さは `To - From` になる。binは、Jの[From, To)の範囲のスライスのバイトを含む。

事前条件

Jはjava値(bytes, *)でなければならない。ここでbytesはbyte[]のインスタンスでなければならない。

FromとToは整数のnum値でなければならない。

0 <= From <= To <= bytes.length

例

6.72.1.10. J.to_kink_exception

to_kink_exceptionは、JavaのThrowableからexception値を作って戻す。

to_kink_exceptionはThrowable.toStringをMessageに、Throwable.getStackTraceをTracesに、Throwable.getCauseとgetSuppressedをNextに、それぞれexception値の属性としてエンコードする。

他のthrowableの属性、たとえばSQLException.getErrorCodeなどは保持されない。

事前条件

JのobjectReferenceはjava.lang.Throwableのインスタンスでなければならない。

例

6.72.1.11. J.unwrap

unwrapは、JAVA.wrapでラップされたKinkの値を抜き出す。

Jがjava値(Wrapped, ? super org.kink_lang.kink.Val)のとき、unwrapはWrappedを戻す。

事前条件

Jはjava値(Wrapped, *)でなければならない。ここで、Wrappedはorg.kink_lang.kink.Valのインスタンスで、かつWrappedのランタイムは現在のランタイムと同じでなければならない。

例

6.72.1.12. J.array_class

array_classは、与えられた要素型の配列クラスのクラスオブジェクトを戻す。

JのobjectReferenceがクラスオブジェクトCのとき、array_classはjava値(C[], java.lang.Class)を戻す。

事前条件

Jはjava値(C, *)でなければならない。ここでCはクラスオブジェクトでなければならない。

Cはvoidクラスであってはならない。

Cが配列クラスのとき、その次元は254を超えてはならない。

例

6.72.1.13. J.array_new(Size)

array_newは、与えられた要素型とサイズの配列を戻す。

JのobjectReferenceがクラスオブジェクトCのとき、array_newはjava値(Array, C[])を戻す。ここで、Arrayは長さがSizeの配列である。

Arrayの要素はCのゼロ値で初期化される。

事前条件

Jはjava値(C, *)でなければならない。ここでCはクラスオブジェクトでなければならない。

Cはvoidクラスであってはならない。

Cが配列クラスのとき、その次元は254を超えてはならない。

Sizeは非負の整数のnum値でなければならない。

例

6.72.1.14. J.array_of(...[E0 E1 ,,,])

array_ofは、与えられた要素を含む配列を戻す。

JのobjectReferenceがクラスオブジェクトCのとき、array_ofはjava値(Array, C[])を戻す。ここで、ArrayはE0, E1, ,,, を要素として持つ配列である。

事前条件

Jはjava値(C, *)でなければならない。ここでCはクラスオブジェクトでなければならない。

Cはvoidクラスであってはならない。

Cが配列クラスのとき、その次元は254を超えてはならない。

E0, E1, ,,, はjava値であり、そのobjectReference属性は、JのobjectReferenceで型付け可能でなければならない。

例

6.72.1.15. J.array_length

array_lengthは、配列の長さを整数のnum値として戻す。

事前条件

Jはjava値(array, *)でなければならない。ここでarrayは配列でなければならない。

6.72.1.16. J.array_get(Ind)

array_getは、配列Jの添字Indにおける要素を戻す。

配列の要素型が参照型rtのとき、array_getは、java値(element, rt)を戻す。ここでelementは配列の要素である。

配列の要素型がプリミティブ型ptのとき、array_getはjava値(box, pt)を戻す。ここでboxは、対応するラッパ型のインスタンスであり、その中身として配列の要素を持つ。

事前条件

Jはjava値(array, *)でなければならない。ここでarrayは配列でなければならない。

Indは、[0, length)の範囲の整数のnumでなければならない。ここでlengthは配列の長さである。

6.72.1.17. J.array_set(Ind Elem)

array_setは、値Elemを配列Jの添字Indの場所に書き込む。

事前条件

Jはjava値(array, *)でなければならない。ここでarrayは配列でなければならない。

Indは、[0, length)の範囲の整数のnumでなければならない。ここでlengthは配列の長さである。

Elemはjava値(elem, *)でなければならない。ここでelemは配列の要素型で型付け可能でなければならない。

6.72.1.18. J.get_field(Field_name)

get_fieldは、publicなインスタンスフィールドの内容を戻す。

フィールドは、Jのtypeから、Class.getField(String)を使って検索される。

フィールドの宣言型が参照型rtのとき、結果はjava値(contentObj, rt)になる。ここでcontentObjはフィールドの内容である。

フィールドの宣言型がプリミティブ型ptのとき、結果はjava値(box, pt)になる。ここでboxは、対応するラッパ型のインスタンスであり、その中身としてフィールドの内容を持つ。

事前条件

Jはjava値でなければならない。

JのobjectReferenceがnullであってはならない。

Field_nameはstrでなければならない。

Jのtypeは、Field_nameの名前の、publicなインスタンスフィールドを持っていなければならない。

例

6.72.1.19. J.set_field(Field_name Content)

set_fieldは、Contentをpublicなインスタンスフィールドに書き込む。

フィールドは、Jのtypeから、Class.getField(String)を使って検索される。

事前条件

Jはjava値でなければならない。

JのobjectReferenceがnullであってはならない。

Field_nameはstrでなければならない。

Jのtypeは、Field_nameの名前の、publicなインスタンスフィールドを持っていなければならない。

フィールドはfinalであってはならない。

Contentはjava値(contentObj, *)でなければならない。ここでcontentObjは、フィールドの宣言型で型付け可能でなければならない。

6.72.1.20. J.get_static(Field_name)

get_staticは、クラスJのpublic staticフィールドの内容を戻す。

JのobjectReferenceがクラスオブジェクトownerClassのとき、フィールドはownerClassから、Class.getField(String)を使って検索される。

フィールドの宣言型が参照型rtのとき、結果はjava値(contentObj, rt)になる。ここでcontentObjはフィールドの内容である。

フィールドの宣言型がプリミティブ型ptのとき、結果はjava値(box, pt)になる。ここでboxは、対応するラッパ型のインスタンスであり、その中身としてフィールドの内容を持つ。

事前条件

Jはjava値(ownerClass, *)でなければならない。ここで、ownerClassはjava.lang.Classのインスタンスでなければならない。

Field_nameはstrでなければならない。

ownerClassは、Field_nameの名前を持つpublic staticフィールドを持っていなければならない。

例

6.72.1.21. J.set_static(Field_name Content)

set_staticは、クラスJのpublic staticフィールドにContentを書き込む。

JのobjectReferenceがクラスオブジェクトownerClassのとき、フィールドはownerClassから、Class.getField(String)を使って検索される。

事前条件

Jはjava値(ownerClass, *)でなければならない。ここで、ownerClassはjava.lang.Classのインスタンスでなければならない。

Field_nameはstrでなければならない。

ownerClassは、Field_nameの名前を持つpublic staticフィールドを持っていなければならない。

フィールドはfinalであってはならない。

Contentはjava値(contentObj, *)でなければならない。ここでcontentObjは、フィールドの宣言型で型付け可能でなければならない。

6.72.1.22. J.call_method(Method_name ...[A0 A1 ,,,] ...[$config={}])

call_methodは、オブジェクトJのpublicなインスタンスメソッドを呼び出す。

検索

インスタンスメソッドは `J.type.getMethod(Method_name, A0.type, A1.type, ,,,)` で検索される。

結果

1) メソッドの宣言された戻り型が参照型rtで、メソッドが例外を投げずに終わったとき、call_methodは、java値(resultObj, rt)を引数として成功時継続を末尾呼び出しする。ここでresultObjはメソッドの戻り値である。

2) メソッドの宣言された戻り型ptがchar, boolean, byte, short, int, long, float, doubleのいずれかで、メソッドが例外を投げずに終わったとき、call_methodは、java値(resultObj, pt)を引数として成功時継続を末尾呼び出しする。ここでresultObjは戻り値のラッパインスタンスである。

3) メソッドの宣言された戻り型がvoidで、メソッドが例外を投げずに終わったとき、call_methodは、引数なしで成功時継続を末尾呼び出しする。

4) メソッドがJavaの例外exceptionObjを投げて終わり、その例外がC.catchの呼び出しで指定されたひとつ以上の例外型のインスタンスであるとき、call_methodは、最も狭い型etに対応するエラー時継続を、java値(exceptionObj, et)を引数として末尾呼び出しする。

5) メソッドがJavaの例外を投げて終わり、C.catchに渡された例外型のどれもが投げられた例外に合致しなかったとき、call_methodはKinkの例外を投げる。

コンフィグ値のC.on_successが呼ばれず、メソッドの宣言された戻り型がvoidのときは、{ nada }がデフォルトの成功時継続として使われる。

コンフィグ値のC.on_successが呼ばれず、メソッドの宣言された戻り型がvoidでないときは、VAL.identityがデフォルトの成功時継続として使われる。

事前条件

Method_nameはstrでなければならない。

A0, A1 ,,, はjava値でなければならない。

Jのtypeは、指定されたpublicインスタンスメソッドを持っていなければならない。

$configは、java_call_config値を取る関数でなければならない。

例

デフォルトでは、Javaの例外はKinkの例外として投げられる。

成功、エラーの継続は、コンフィグ関数で設定できる。

Javaメソッドの戻り型がvoidのとき、成功時継続は引数なしで末尾呼び出しされる。

6.72.1.23. J.call_static(Method_name ...[A0 A1 ,,,] ...[$config={}])

call_staticは、クラスJのpublicなstaticメソッドを呼び出す。

検索

JのobjectReferenceがownerClassのとき、staticメソッドは `ownerClass.getMethod(Method_name, A0.type, A1.type, ,,,)` で検索される。

結果

J.call_methodと同じ。

事前条件

Jはjava値(ownerClass, *)でなければならない。ここでownerClassはクラスオブジェクトでなければならない。

Method_nameはstrでなければならない。

A0, A1 ,,, はjava値でなければならない。

ownerClassは指定されたpublicなstaticメソッドを持っていなければならない。

$configは、java_call_config値を取る関数でなければならない。

例

6.72.1.24. J.new(...[A0 A1 ,,,] ...[$config={}])

newは、Jのpublicなコンストラクタを呼んで、新しいインスタンスを戻す。

検索

JのobjectReferenceがクラスオブジェクトownerClassのとき、publicコンストラクタは、 `ownerClass.getConstructor(A0.type, A1.type, ,,,)` で検索される。

結果

1) 新しいインスタンスresultObjが作られたとき、newは、java値(resultObj, ownerClass)を引数として成功時継続を末尾呼び出しする。

2) コンストラクタがJavaの例外exceptionObjを投げて終わり、その例外がC.catchの呼び出しで指定されたひとつ以上の例外型のインスタンスであるとき、newは、最も狭い型etに対応するエラー時継続を、java値(exceptionObj, et)を引数として末尾呼び出しする。

3) コンストラクタがJavaの例外を投げて終わり、C.catchに渡された例外型のどれもが投げられた例外に合致しなかったとき、newはKinkの例外を投げる。

コンフィグ値のC.on_successが呼ばれないときは、VAL.identityがデフォルトの成功時継続として使われる。

事前条件

Jはjava値(ownerClass, *)でなければならない。ここでownerClassはクラスオブジェクトでなければならない。

A0, A1 ,,, はjava値でなければならない。

ownerClassは指定されたpublicなコンストラクタを持っていなければならない。

$configは、java_call_config値を取る関数でなければならない。

例

6.72.2. java_call_config型

java_call_configは、J.call_method, J.call_static, J.newのコンフィグ値である。

6.72.2.1. C.on_success($success)

on_successは、$successを成功時継続として指定する。

6.72.2.2. C.catch(Exception_class $error)

catchは、例外型Exception_classに対応するエラー時継続として$errorを指定する。

catchは、異なる例外型に対応するエラー時継続を指定するために、複数回呼び出せる。

事前条件

Exception_classはjava値(et, *)でなければならない。ここでetは、java.lang.Throwableのサブクラスでなければならない。

Exception_classは、先行するcatchの呼び出しで指定された例外型の部分型であってはならない。

$errorはjava値を取る関数でなければならない。

6.72.3. JAVA.is?(Val)

is?は、Valがjava値であるかどうかを戻す。

6.72.4. JAVA.string(Str)

stringは、Strと同じ文字列を持つJava文字列を戻す。

結果はjava値(string, java.lang.String)になる。ここでstringはStringのインスタンスであり、Strと同じ文字列を持つ。

事前条件

Strはstr値でなければならない。

6.72.5. JAVA.bytes(Bin ...[From=0 To=Bin.size])

bytesは、Binの範囲[From, To)のスライスからJavaのバイト配列を作って戻す。

結果はjava値(byteArray, byte[])になる。ここでbyteArrayはbyte配列であり、その要素はBinの範囲[From, To)のスライスからコピーされる。

事前条件

Binはbin値でなければならない。

FromとToは整数のnum値でなければならない。

0 <= From <= To <= Bin.size

6.72.6. JAVA.byte_buffer(Bin)

byte_bufferは、Binのバイト列を持つ読み込み専用のByteBufferを戻す。

結果はjava値(byteBuffer, java.nio.ByteBuffer)になる。ここでbyteBufferは次の属性を持つ。

• capacityと、limitの初期値はBin.sizeになる。

• positionの初期値は0になる。

事前条件

Binはbin値でなければならない。

6.72.7. JAVA.runtime_exception(Exc)

runtime_exceptionは、Kinkの例外から変換された、JavaのRuntimeExceptionを戻す。

結果は、java値(rte, java.lang.RuntimeException)になる。ここでrteは、RuntimeExceptionのインスタンスである。

事前条件

Excはexception値でなければならない。

6.72.8. JAVA.boolean(Bool)

booleanは、Boolに対応するJavaのboolean値を戻す。

Boolがtrueのとき、booleanはjava値(Boolean.TRUE, boolean)を戻す。

Boolがfalseのとき、booleanはjava値(Boolean.FALSE, boolean)を戻す。

事前条件

Boolはbool値でなければならない。

6.72.9. JAVA.char(Num)

charはNumに対応するJavaのchar値を戻す。

結果は(objectReference=ch, type=char)というjava値になる。chはjava.lang.Characterのインスタンスである。

事前条件

Numは[0, 0xffff]の範囲内の整数のnum値でなければならない。

6.72.10. JAVA.byte(Num)

byteはNumに対応するJavaのbyte値を戻す。

結果は(objectReference=bt, type=byte)というjava値になる。btはjava.lang.Byteのインスタンスである。

事前条件

Numは[-128, 127]の範囲内の整数のnum値でなければならない。

6.72.11. JAVA.short(Num)

shortはNumに対応するJavaのshort値を戻す。

結果は(objectReference=sh, type=short)というjava値になる。shはjava.lang.Shortのインスタンスである。

事前条件

Numは[- 2**15, 2**15 - 1]の範囲内の整数のnum値でなければならない。

6.72.12. JAVA.int(Num)

intはNumに対応するJavaのint値を戻す。

結果は(objectReference=n, type=int)というjava値になる。nはjava.lang.Integerのインスタンスである。

事前条件

Numは[- 2**31, 2**31 - 1]の範囲内の整数のnum値でなければならない。

6.72.13. JAVA.long(Num)

longはNumに対応するJavaのlong値を戻す。

結果は(objectReference=ln, type=long)というjava値になる。lnはjava.lang.Longのインスタンスである。

事前条件

Numは[- 2**63, 2**63 - 1]の範囲内の整数のnum値でなければならない。

6.72.14. JAVA.float(Num)

floatは、数値的にNumに近いJavaのfloat値を戻す。

結果はjava値(fl, float)になる。ここでflは、java.lang.Floatのインスタンスであり、その値はBigDecimal.floatValue()でNumから変換されたものである。

事前条件

Numはnum値でなければならない。

6.72.15. JAVA.double(Num)

doubleは、数値的にNumに近いJavaのdouble値を戻す。

結果はjava値(dbl, double)になる。ここでdblは、java.lang.Doubleのインスタンスであり、その値はBigDecimal.doubleValue()でNumから変換されたものである。

事前条件

Numはnum値でなければならない。

6.72.16. JAVA.big_integer(Num)

big_integerはNumに対応するJavaのBigInteger値を戻す。

結果はjava値(objectReference=bi, type=java.math.BigInteger)になる。biはjava.math.BigIntegerのインスタンスであり、その値はNumに等しい。

事前条件

Numは整数のnum値でなければならない。

6.72.17. JAVA.big_decimal(Num)

big_decimalは、Numに対応するJavaのBigDecimalを戻す。

結果はjava値(bd, java.math.BigDecimal)になる。ここでbdは、java.math.BigDecimalのインスタンスであり、そのscaleはNumのScaleに等しく、unscaledValueはNumのMantissaに等しい。

事前条件

Numはnum値でなければならない。

6.72.18. JAVA.wrap(Wrapped)

wrapは、Kinkの値をラップするjava値を戻す。

Wrappedはどんな型の値でも良い。wrapは、(Wrapped, org.kink_lang.kink.Val)のjava値を戻す。

Wrappedは、結果のjava値から、unwrapメソッドで抜き出せる。

例

6.72.19. JAVA.true

trueは、java値(Boolean.TRUE, boolean)を戻す。

6.72.20. JAVA.false

falseは、java値(Boolean.FALSE, boolean)を戻す。

6.72.21. JAVA.null

nullは、java値(null, java.lang.Object)を戻す。

6.72.22. JAVA.runtime

runtimeは現在のランタイムを戻す。

結果はjava値(vm, org.kink_lang.kink.Vm)である。ここでvmは現在のランタイムである。

6.72.23. JAVA.boolean_class

boolean_classは、java値(boolean.class, java.lang.Class)を戻す。

6.72.24. JAVA.char_class

char_classは、java値(char.class, java.lang.Class)を戻す。

6.72.25. JAVA.byte_class

byte_classは、java値(byte.class, java.lang.Class)を戻す。

6.72.26. JAVA.short_class

short_classは、java値(short.class, java.lang.Class)を戻す。

6.72.27. JAVA.int_class

int_classは、java値(int.class, java.lang.Class)を戻す。

6.72.28. JAVA.long_class

long_classは、java値(long.class, java.lang.Class)を戻す。

6.72.29. JAVA.float_class

float_classは、java値(float.class, java.lang.Class)を戻す。

6.72.30. JAVA.double_class

double_classは、java値(double.class, java.lang.Class)を戻す。

6.72.31. JAVA.void_class

void_classは、java値(void.class, java.lang.Class)を戻す。

6.72.32. JAVA.class(Class_name)

classは、バイナリ名Class_nameでクラスを検索する。

classは、指定されたクラスをロードするのに、現在のランタイムのorg.kink_lang.kink.Vmクラスがロードされたクラスローダの、無名モジュールのリフレクションアクセスを使う。クラスklassが見つかったとき、classは、java値(klass, java.lang.Class)を戻す。

事前条件

Class_nameはstr値でなければならない。

ランタイムをロードしたクラスローダから、Class_nameで指定されたクラスが到達可能でなければならない。クラスはpublicでなければならない。