data_io.anubis
2.43 KB
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
*Project* Anubis
*Title* Data Input/Output functions.
*Copyright* Copyright (c) David René 2007.
*Author* David René
*Created* February 2007
*Status* Beta
public type Data_IO:...
public type Data_IO_Result:
failure,
time_out,
success(ByteArray),
truncated(ByteArray).
public define Data_IO_Result read_bytes (Data_IO data, Int how_many).
public define Data_IO make_data_io(RStream file).
public define Data_IO make_data_io(ByteArray byte_array).
public type Data_IO:
data_io(Int -> Data_IO_Result read_bytes,// read a bytes
One -> Int offset, // offset
One -> Bool rewind).
/* File interface */
define Int -> Data_IO_Result
make_read_bytes // making the 'rb' function
(
RStream file,
Var(Int) offset,
) =
(Int how_many) |->
if read(file, how_many, 10) is //by default the time_out is 10 seconds
{
error then failure,
timeout then time_out,
ok(bytes) then
with len = length(bytes),
offset <- *offset + len; //update the offset
if len = how_many then
success(bytes)
else
truncated(bytes)
}.
public define Data_IO
make_data_io
(
RStream file
) =
with o = var((Int)0), // offset
data_io(
make_read_bytes(file, o),
(One u) |-> *o,
(One u) |-> seek(file, 0)).
/* ByteArray interface */
define Int -> Data_IO_Result
make_read_bytes // making the 'rb' function
(
ByteArray byte_array,
Var(Int) offset,
) =
(Int how_many) |->
with result_ba = extract(byte_array, *offset, *offset + how_many),
len = length(result_ba),
offset <- *offset + len; //update the offset
//if the returned length size is 0, it means we are at end of buffer
if len = 0 then
failure
else if len = how_many then
success(result_ba)
else
truncated(result_ba).
public define Data_IO
make_data_io
(
ByteArray byte_array
) =
with o = var((Int)0), // offset
data_io(
make_read_bytes(byte_array, o),
(One u) |-> *o,
(One u) |-> o<-0;true).
public define Data_IO_Result
read_bytes
(
Data_IO io,
Int how_many
) =
read_bytes(io)(how_many).