staload
"share/atspre_staload.hats"
staload _ = "prelude/DATS/integer.dats"
staload _ = "prelude/DATS/array.dats"
staload _ = "prelude/DATS/pointer.dats"
staload _ = "prelude/DATS/arrayptr.dats"
(*
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;
}
*)
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]
implement main0 () = let
val arr = Letters ()
val () = println!("results of [Letters]:")
implement
fprint_ref<char> (out, c) = fprint!(out, c)
val () = fprint_arrayptr<char> (stdout_ref, arr, (i2sz)26)
val () = arrayptr_free (arr)
in
end
