如何在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

好吧，这里有一种方法，尽管它非常复杂，因为它遵循了您概述的方法:它涉及到数组的线性证明(也称为数据视图)、内存分配和通过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))

如果您不想使用高阶函数，可以尝试以下基于模板的解决方案：

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