How to construct an array in ATS?

Question

For instance, how can I construct an array in ATS containing all of the letters in the upper case from A to Z? In C, this can be done as follows:

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

You could use the tabulate function for creating linear arrays. For instance,

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

If you don't want to use a higher-order function, you can try the following template-based solutioin:

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

Answer 2

Well, here's one way, although it's extremely complicated, because it follows your outlined approach to the letter: it involves linear proofs for arrays (aka dataviews), memory allocation, and array initialization via a while loop.

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]

You can run the code at Glot.io