ATSに2次元配列を作成するには？

Question

たとえば、私が行うATSの例を探しています多かれ少なかれ、次のCコードが何をするか：

int *theMultable[10][10]; 

void 
theMultable_initialize() 
{ 
    int i, j; 
    for (i = 0; i < 10; i++) 
    { 
    for (j = 0; j < 10; j++) theMultable[i][j] := i * j; 
    } 
    return; 
} 

Answer 1

一つの可能​​なアプローチは、しかしC.への直接変換を試みることで、私は今だと思います代わりに組み込みのmatrixを使っていたはずです。このコードは、高度な機能のかなり上に（私も運動のために1未確認補題を左に依存する：。

extern 
fun 
multable_init (
    mat: &(@[@[int][10]][10])? >> _ 
): void // end of [multable_init] 

：それは N*sizeof(T) == sizeof(@[T][N])

2次元アレイを初期化するループ機能内に実装されていることを示しています

この関数は2つの関数（基本的に要素の配列を初期化します）とグローバル変数multableを割り当てて、multable_initを使って初期化します。 。

ここにグローバルvaの初期化のコードがありますriable：

var multable : @[int?][100] 
val p_multable = addr@multable 
prval pf_multable = array_v_group (view@multable) 
val() = multable_init (!p_multable) 
prval pf_multable = array_v_ungroup (pf_multable) 
prval pf_multable = array2matrix_v (pf_multable) 
val theMultable = ref_make_viewptr {matrix (int, 10, 10)} (pf_multable | p_multable) 

可変配列をスタック上に割り当てられ、その後、我々は、そのアドレス（ライン2）、それは、（ライン3にグルーピングを介して）@[int?][100]から@[@[int?][10]][10]とでプルーフ対応ターンを取り、それを初期化します。次に、グループ化された配列ビューを行列ビューに変換し、最後にそれをref-cellに入れます。

完全なコードは、残りの補助定理を証明するようGlot.io