1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(* ****** ****** *)
//
// HX-2017-10-28:
// For supporting
// "unityped" programming
//
(* ****** ****** *)
//
(*
#define
ATS_DYNLOADFLAG 1
*)
#define
ATS_PACKNAME
"ATSLIB.libats.ML.COMPILE"
//
(* ****** ****** *)
//
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)
#staload UN = $UNSAFE
(* ****** ****** *)
//
#staload
"libats/ML/SATS/basis.sats"
//
(* ****** ****** *)
//
#staload
"libats/SATS/dynarray.sats"
#staload _(*DA*) =
"libats/DATS/dynarray.dats"
//
#staload
"libats/ML/SATS/array0.sats"
#staload _(*anon*) =
"libats/ML/DATS/array0.dats"
//
//
// HX: Interface
//
(* ****** ****** *)
//
extern
fun
array0_make_stream
{a:type}(xs: stream(a)): array0(a)
//
extern
fun
array0_make_stream_vt
{a:vtype}(xs: stream_vt(a)): array0(a)
//
(* ****** ****** *)
//
// HX: Implementation
//
(* ****** ****** *)
implement
array0_make_stream
{a}(xs) = let
//
fun
loop
(
DA: dynarray(a), xs: stream(a)
) : dynarray(a) =
(
case+ !xs of
| stream_nil() => DA
| stream_cons(x, xs) =>
loop(DA, xs) where
{
val () =
dynarray_insert_atend_exn<a>(DA, x)
} (* end of [stream_cons] *)
)
//
implement
dynarray$recapacitize<>() = 1
//
val DA = dynarray_make_nil<a>(i2sz(16))
//
var n0 : size_t
val DA = loop(DA, xs)
val A0 = dynarray_getfree_arrayptr<>(DA, n0)
//
in
array0_make_arrayref(arrayptr_refize{a}(A0), n0)
end // end of [array0_make_stream]
(* ****** ****** *)
implement
array0_make_stream_vt
{a}(xs) = let
//
fun
loop
(
DA: dynarray(a), xs: stream_vt(a)
) : dynarray(a) =
(
case+ !xs of
| ~stream_vt_nil() => DA
| ~stream_vt_cons(x, xs) =>
loop(DA, xs) where
{
val () =
dynarray_insert_atend_exn<a>(DA, x)
} (* end of [stream_cons] *)
)
//
implement
dynarray$recapacitize<>() = 1
//
val DA = dynarray_make_nil<a>(i2sz(16))
//
var n0 : size_t
val DA = loop(DA, xs)
val A0 = dynarray_getfree_arrayptr<>(DA, n0)
//
in
array0_make_arrayref(arrayptr_refize{a}(A0), n0)
end // end of [dynarray$recapacitize]
(* ****** ****** *)
(* end of [array0.dats] *)
|
