git.iko.soy/Idris-dev
on master help sign in
Get and set Double in Data.Buffer
commit578134cda6f20614dec57ce0aa30f32317a6f184 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 22 Jan 2018, 12:49 (9 years ago) parent6dca7b8
5 files changed+57−2
compare with master
unifiedsplit
libs/base/Data/Buffer.idr+18 rts/idris_buffer.c+27 rts/idris_buffer.h+3−1 test/buffer002/buffer002.idr+7 test/buffer002/expected+2−1
libs/base/Data/Buffer.idr+18
@@ -60,6 +60,15 @@ setInt b loc val
6060 = foreign FFI_C "idris_setBufferInt" (ManagedPtr -> Int -> Int -> IO ())
6161 (rawdata b) loc val
6262
63+||| Set the double at position 'loc' to 'val'.
64+||| Uses 8 bytes (assumes 64 bit double).
65+||| Does nothing if the location is outside the bounds of the buffer
66+export
67+setDouble : Buffer -> (loc : Int) -> (val : Double) -> IO ()
68+setDouble b loc val
69+ = foreign FFI_C "idris_setBufferDouble" (ManagedPtr -> Int -> Double -> IO ())
70+ (rawdata b) loc val
71+
6372||| Set the byte at position 'loc' to 'val'.
6473||| Does nothing if the location is out of bounds of the buffer, or the string
6574||| is too long for the location
@@ -96,6 +105,15 @@ getInt b loc
96105 = foreign FFI_C "idris_getBufferInt" (ManagedPtr -> Int -> IO Int)
97106 (rawdata b) loc
98107
108+||| Return the value at the given location in the buffer, assuming 8
109+||| bytes to store the Double.
110+||| Returns 0 if out of bounds.
111+export
112+getDouble : Buffer -> (loc : Int) -> IO Double
113+getDouble b loc
114+ = foreign FFI_C "idris_getBufferDouble" (ManagedPtr -> Int -> IO Double)
115+ (rawdata b) loc
116+
99117||| Return the string at the given location in the buffer, with the given
100118||| length. Returns "" if out of bounds.
101119export
rts/idris_buffer.c+27
@@ -49,6 +49,17 @@ void idris_setBufferInt(void* buffer, int loc, int val) {
4949 }
5050}
5151
52+void idris_setBufferDouble(void* buffer, int loc, double val) {
53+ Buffer* b = buffer;
54+ // I am not proud of this
55+ if (loc >= 0 && loc + sizeof(double) < b->size) {
56+ unsigned char* c = (unsigned char*)(& val);
57+ for (int i = 0; i < sizeof(double); ++i) {
58+ b->data[loc+i] = c[i];
59+ }
60+ }
61+}
62+
5263void idris_setBufferString(void* buffer, int loc, char* str) {
5364 Buffer* b = buffer;
5465 int len = strlen(str);
@@ -79,6 +90,22 @@ int idris_getBufferInt(void* buffer, int loc) {
7990 }
8091}
8192
93+double idris_getBufferDouble(void* buffer, int loc) {
94+ Buffer* b = buffer;
95+ double d;
96+ // I am even less proud of this
97+ unsigned char *c = (unsigned char*)(& d);
98+ if (loc >= 0 && loc + sizeof(double) < b->size) {
99+ for (int i = 0; i < sizeof(double); ++i) {
100+ c[i] = b->data[loc+i];
101+ }
102+ return d;
103+ }
104+ else {
105+ return 0;
106+ }
107+}
108+
82109VAL idris_getBufferString(void* buffer, int loc, int len) {
83110 Buffer* b = buffer;
84111
rts/idris_buffer.h+3−1
@@ -11,7 +11,8 @@ void* idris_newBuffer(int bytes);
1111int idris_getBufferSize(void* buffer);
1212
1313void idris_setBufferByte(void* buffer, int loc, uint8_t byte);
14−void idris_setBufferInt(void* buffer, int loc, int byte);
14+void idris_setBufferInt(void* buffer, int loc, int val);
15+void idris_setBufferDouble(void* buffer, int loc, double val);
1516void idris_setBufferString(void* buffer, int loc, char* str);
1617
1718void idris_copyBuffer(void* from, int start, int len,
@@ -22,6 +23,7 @@ void idris_writeBuffer(FILE* h, void* buffer, int loc, int len);
2223
2324uint8_t idris_getBufferByte(void* buffer, int loc);
2425int idris_getBufferInt(void* buffer, int loc);
26+double idris_getBufferDouble(void* buffer, int loc);
2527VAL idris_getBufferString(void* buffer, int loc, int len);
2628
2729#endif
test/buffer002/buffer002.idr+7
@@ -6,12 +6,19 @@ main = do Just buf <- newBuffer 40
66 setInt buf 5 1234567890
77 setInt buf 36 1234567890
88 setString buf 20 "Hello world!"
9+
10+ setDouble buf 10 123.456
11+
912 printLn !(bufferData buf)
1013
1114 val <- getInt buf 5
1215 printLn val
1316 val <- getInt buf 6
1417 printLn val
18+
19+ val <- getDouble buf 10
20+ printLn val
21+
1522 val <- getInt buf 36
1623 printLn val
1724 val <- getInt buf 37 -- out of bounds, expect 0
test/buffer002/expected+2−1
@@ -1,7 +1,8 @@
1140
2−[00, 00, 00, 00, 00, D2, 02, 96, 49, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, D2, 02, 96, 49]
2+[00, 00, 00, 00, 00, D2, 02, 96, 49, 00, 77, BE, 9F, 1A, 2F, DD, 5E, 40, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, D2, 02, 96, 49]
331234567890
444822530
5+123.456
561234567890
670
78Hello worl