Как построить массив в ATS?

Question

Например, как я могу построить массив в ATS, содержащий все буквы в верхнем регистре от A до Z? В C, это может быть сделано следующим образом:

char *Letters() 
{ 
    int i; 
    char *cs = (char *)malloc(26); 
    assert(cs != 0); 
    for (i = 0; i < 26; i += 1) cs[i] = 'A' + i; 
    return cs; 
} 

Answer 1

Ну, вот один из способов, хотя это очень сложно, так как он следует за изложенный подход к письму: она включает в себя линейные доказательства для массивов (ака DataViews) , распределение памяти и инициализацию массива через цикл while.

extern 
fun 
Letters(): arrayptr (char, 26) 
implement 
Letters() = let 
    val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<char> ((i2sz)26) 
    var i: int = 0 
    prval [larr:addr] EQADDR() = eqaddr_make_ptr (p_arr) 
    var p = p_arr 
    prvar pf0 = array_v_nil {char}() 
    prvar pf1 = pf_arr 
    // 
    val() = 
    while* {i:nat | i <= 26} .<26-i>. (
    i: int (i) 
    , p: ptr (larr + i*sizeof(char)) 
    , pf0: array_v (char, larr, i) 
    , pf1: array_v (char?, larr+i*sizeof(char), 26-i) 
) : (
    pf0: array_v (char, larr, 26) 
    , pf1: array_v (char?, larr+i*sizeof(char), 0) 
) => (
    i < 26 
) { 
    // 
    prval (pf_at, pf1_res) = array_v_uncons {char?} (pf1) 
    prval() = pf1 := pf1_res 
    // 
    val c = 'A' + (g0ofg1)i 
    val() = ptr_set<char> (pf_at | p, c) 
    val() = p := ptr1_succ<char> (p) 
    // 
    prval() = pf0 := array_v_extend {char} (pf0, pf_at) 
    val() = i := i + 1 
    // 
    } // end of [val] 
    // 
    prval() = pf_arr := pf0 
    prval() = array_v_unnil {char?} (pf1) 
    // 
    val res = arrayptr_encode (pf_arr, pf_gc | p_arr) 
in 
    res 
end // end of [Letters] 

Вы можете запустить код на Glot.io

Answer 2

Вы можете использовать функцию Tabulate для создания линейных массивов. Например,

extern 
fun 
Letters(): arrayptr(char, 26) 
implement 
Letters() = 
arrayptr_tabulate_cloref<char> 
    (i2sz(26), lam(i) => 'A' + sz2i(i)) 

Если вы не хотите использовать функцию высшего порядка, вы можете попробовать следующий шаблон на основе solutioin:

implement 
Letters() = 
arrayptr_tabulate<char>(i2sz(26)) where 
{ 
    implement array_tabulate$fopr<char> (i) = 'A' + sz2i(i) 
}