Commit 52a3a98a authored by Camil Staps's avatar Camil Staps 🚀

Merge branch 'genBinary' into 'master'

add Data.Encoding.GenBinary

See merge request !278
parents b05c8af5 52564d3f
Pipeline #29974 passed with stage
in 3 minutes and 7 seconds
......@@ -8,7 +8,7 @@ from Control.Monad import class Monad
mapArrSt :: !(.a -> .(*st -> *(.a, *st))) !*(arr .a) !*st -> *(!*(arr .a), !*st) | Array arr a
foldrArr :: !(a .b -> .b) !.b !.(arr a) -> .b | Array arr a
foldrArr :: !(a -> .(.b -> .b)) !.b !.(arr a) -> .b | Array arr a
foldrArrWithKey :: !(Int a -> .(.b -> .b)) !.b !.(arr a) -> .b | Array arr a
......@@ -18,7 +18,7 @@ foldrUArr :: !(a -> .(.b -> .(*(arr a) -> *(.b, *(arr a))))) .b !*(arr a)
foldrUArrWithKey :: !(Int a -> .(.b -> .(*(arr a) -> *(.b, *(arr a))))) .b !*(arr a)
-> *(.b, *(arr a)) | Array arr a
foldlArr :: !(.b a -> .b) !.b !.(arr a) -> .b | Array arr a
foldlArr :: !(.b -> .(a -> .b)) !.b !.(arr a) -> .b | Array arr a
foldlArrWithKey :: !(Int .b -> .(a -> .b)) !.b !.(arr a) -> .b | Array arr a
......
......@@ -17,7 +17,7 @@ mapArrSt f arr st
#! arr = {arr & [idx] = e}
= mapArrSt` sz (idx + 1) f arr st
foldrArr :: !(a .b -> .b) !.b !.(arr a) -> .b | Array arr a
foldrArr :: !(a -> .(.b -> .b)) !.b !.(arr a) -> .b | Array arr a
foldrArr f b arr = foldrArrWithKey (\_ -> f) b arr
foldrArrWithKey :: !(Int a -> .(.b -> .b)) !.b !.(arr a) -> .b | Array arr a
......@@ -49,7 +49,7 @@ foldrUArrWithKey f b arr
#! (res, arr) = foldUArr` sz (idx + 1) b arr
= f idx elem res arr
foldlArr :: !(.b a -> .b) !.b !.(arr a) -> .b | Array arr a
foldlArr :: !(.b -> .(a -> .b)) !.b !.(arr a) -> .b | Array arr a
foldlArr f b arr = foldlArrWithKey (\_ -> f) b arr
foldlArrWithKey :: !(Int .b -> .(a -> .b)) !.b !.(arr a) -> .b | Array arr a
......
definition module Data.Encoding.GenBinary
/**
* This module provides a compact binary encoding for arbitrary values.
* The encoding is provided as character array.
* Choices of ADTs are represented by a single bit.
* Values of basic types (except `Bool`), arrays and lists are stored byte-aligned, which wastes only little space,
* but significantly improves encoding and decoding time.
*
* @property-bootstrap
* import StdEnv, Data.Maybe.Gast, Data.Maybe.GenPrint, Data.Maybe.GenBinary
*
* :: ADT = A String | B ADT | C ADT ADT | D ADT ADT ADT
*
* derive gEq ADT
* derive class GenBinary ADT
* derive class Gast ADT
*
* instance == ADT where
* == x y = x === y
*
* :: Record = {a :: ADT, b :: ADT , c :: ADT}
*
* derive gEq Record
* derive class GenBinary Record
* derive class Gast Record
*
* instance == Record where
* == x y = x === y
*
* @property-test-with a = Maybe Bool
* @property-test-with a = Int
* @property-test-with a = String
* @property-test-with a = Char
* @property-test-with a = Real
* @property-test-with a = (Int, Int)
* @property-test-with a = (String, String)
* @property-test-with a = (String, Int)
* @property-test-with a = (Int, String)
* @property-test-with a = [Bool]
* @property-test-with a = [Int]
* @property-test-with a = [String]
* @property-test-with a = [Char]
* @property-test-with a = [Real]
* @property-test-with a = ADT
* @property-test-with a = Record
*/
from StdGeneric import :: UNIT (..), :: PAIR (..), :: EITHER (..), :: CONS (..), :: OBJECT (..), :: RECORD (..),
:: FIELD (..)
from StdInt import class + (+), instance + Int
from Data.Maybe import :: Maybe (..), instance Functor Maybe
from Data.Func import $
from Data.Functor import class Functor (fmap)
from Data.Tuple import appFst
/**
* Encodes a values as character array.
*
* @param The value.
* @result The encoded value.
*/
encode :: !a -> {#Char} | gBinaryEncodingSize{|*|}, gBinaryEncode{|*|} a
/**
* Decodes a value.
*
* @param The value encoded as character array.
* @result The corresponding value, if the provided array is a valid representation of a value.
*
* @property correctness: A.a :: a:
* // The `a == a` check is required as NaN Real values do not equal themselves.
* a == a ==> decode (encode a) =.= Just a
*/
decode :: !{#Char} -> Maybe a | gBinaryDecode{|*|} a
class GenBinary a | gBinaryEncode{|*|}, gBinaryEncodingSize{|*|}, gBinaryDecode{|*|} a
:: *EncodingSt
generic gBinaryEncode a :: !a !*EncodingSt -> *EncodingSt
gBinaryEncode{|UNIT|} _ st = st
gBinaryEncode{|PAIR|} cx cy (PAIR x y) st = cy y $ cx x st
gBinaryEncode{|EITHER|} cl cr (LEFT x) st = cl x $ encodeBool False st
gBinaryEncode{|EITHER|} cl cr (RIGHT x) st = cr x $ encodeBool True st
gBinaryEncode{|CONS|} c (CONS x) st = c x st
gBinaryEncode{|FIELD|} c (FIELD x) st = c x st
gBinaryEncode{|OBJECT|} c (OBJECT x) st = c x st
gBinaryEncode{|RECORD|} c (RECORD x) st = c x st
derive gBinaryEncode Int, Real, Bool, Char, String, [], {}, {!}, (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,),
(,,,,,,,)
generic gBinaryEncodingSize a :: !a !Int -> Int
gBinaryEncodingSize{|UNIT|} _ s = s
gBinaryEncodingSize{|PAIR|} cx cy (PAIR x y) s = cy y $ cx x s
gBinaryEncodingSize{|EITHER|} cl _ (LEFT x) s = cl x $ s + 1
gBinaryEncodingSize{|EITHER|} _ cr (RIGHT x) s = cr x $ s + 1
gBinaryEncodingSize{|CONS|} c (CONS x) s = c x s
gBinaryEncodingSize{|FIELD|} c (FIELD x) s = c x s
gBinaryEncodingSize{|OBJECT|} c (OBJECT x) s = c x s
gBinaryEncodingSize{|RECORD|} c (RECORD x) s = c x s
derive gBinaryEncodingSize Int, Real, Bool, Char, String, [], {}, {!}, (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,),
(,,,,,,,)
generic gBinaryDecode a :: !*EncodingSt -> (!Maybe a, !*EncodingSt)
gBinaryDecode{|UNIT|} st = (Just UNIT, st)
gBinaryDecode{|PAIR|} fx fy st
# (mbX, st) = fx st
# (mbY, st) = fy st
= case (mbX, mbY) of
(Just x, Just y) = (Just $ PAIR x y, st)
_ = (Nothing, st)
gBinaryDecode{|EITHER|} fl fr st
# (mbIsRight, st) = decodeBool st
= case mbIsRight of
Just isRight | isRight = appFst (fmap RIGHT) $ fr st
| otherwise = appFst (fmap LEFT) $ fl st
_ = (Nothing, st)
gBinaryDecode{|CONS|} f st = appFst (fmap CONS) $ f st
gBinaryDecode{|FIELD|} f st = appFst (fmap \x -> FIELD x) $ f st
gBinaryDecode{|OBJECT|} f st = appFst (fmap \x -> OBJECT x) $ f st
gBinaryDecode{|RECORD|} f st = appFst (fmap RECORD) $ f st
derive gBinaryDecode Int, Real, Bool, Char, String, [], {}, {!}, (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,),
(,,,,,,,)
// This is only exported because it is used in exposed generic definitions.
decodeBool :: !*EncodingSt -> (!Maybe Bool, !*EncodingSt)
encodeBool :: !Bool !*EncodingSt -> *EncodingSt
implementation module Data.Encoding.GenBinary
import StdGeneric, StdEnv
import Data._Array, Data.Func, Data.Maybe, Data.Functor, Data.Tuple, Data.Array
import System._Unsafe
decode :: !{#Char} -> Maybe a | gBinaryDecode{|*|} a
decode binary = fst $ gBinaryDecode{|*|} $ mkEncodingSt {x \\ x <-: binary}
encode :: !a -> {#Char} | gBinaryEncodingSize{|*|}, gBinaryEncode{|*|} a
encode x
#! encoded_size = gBinaryEncodingSize{|*|} x 0
#! arr_size = (encoded_size+7) >> 3
#! bits = createArray arr_size '\0'
= (gBinaryEncode{|*|} x (mkEncodingSt bits)).cs_bits
mkEncodingSt :: !*{#Char} -> *EncodingSt
mkEncodingSt arr = { cs_pos = 0, cs_bits = arr}
generic gBinaryEncode a :: !a !*EncodingSt -> *EncodingSt
gBinaryEncode{|Int|} x st = encodeInt x st
gBinaryEncode{|Real|} x st = encodeReal x st
gBinaryEncode{|Char|} x st = encodeChar x st
gBinaryEncode{|Bool|} x st = encodeBool x st
gBinaryEncode{|String|} xs st = encodeArray encodeChar xs st
gBinaryEncode{|UNIT|} _ st = st
gBinaryEncode{|PAIR|} cx cy (PAIR x y) st = cy y $ cx x st
gBinaryEncode{|EITHER|} cl cr (LEFT x) st = cl x $ encodeBool False st
gBinaryEncode{|EITHER|} cl cr (RIGHT x) st = cr x $ encodeBool True st
gBinaryEncode{|CONS|} c (CONS x) st = c x st
gBinaryEncode{|FIELD|} c (FIELD x) st = c x st
gBinaryEncode{|OBJECT|} c (OBJECT x) st = c x st
gBinaryEncode{|RECORD|} c (RECORD x) st = c x st
gBinaryEncode{|{}|} c xs st = encodeArray c xs st
gBinaryEncode{|{!}|} c xs st = encodeArray c xs st
gBinaryEncode{|[]|} c xs st = encodeList c xs st
encodeInt :: !Int !*EncodingSt -> *EncodingSt
encodeInt int st = encodeIntUsingNBytes (IF_INT_64_OR_32 8 4) int st
encodeChar :: !Char !*EncodingSt -> *EncodingSt
encodeChar c st = encodeIntUsingNBytes 1 (toInt c) st
encodeBool :: !Bool !*EncodingSt -> *EncodingSt
encodeBool False st = {st & cs_pos = st.cs_pos + 1}
encodeBool True {cs_pos = pos, cs_bits = bits}
#! byte_pos = pos >> 3
#! bit_pos = pos bitand 7
#! int = toInt bits.[byte_pos]
#! bit_mask = 1 << bit_pos
= {cs_pos = inc pos, cs_bits = {bits & [byte_pos] = toChar $ int bitor bit_mask}}
encodeReal :: !Real !*EncodingSt -> *EncodingSt
encodeReal real st = IF_INT_64_OR_32
(encodeInt (unsafeCoerce real) st)
(let (i1, i2) = unsafeCoerce real in encodeInt i2 $ encodeInt i1 st)
encodeArray :: !(a *EncodingSt -> *EncodingSt) !(b a) !*EncodingSt -> *EncodingSt | Array b a
encodeArray f xs st
#! st = encodeInt (size xs) st
= foldlArr (flip f) st xs
encodeList :: !(a *EncodingSt -> *EncodingSt) ![a] !*EncodingSt -> *EncodingSt
encodeList f xs st
#! st = encodeInt (length xs) st
= foldl (flip f) st xs
encodeIntUsingNBytes :: !Int !Int !*EncodingSt -> *EncodingSt
encodeIntUsingNBytes numBytes int st = encode numBytes $ withByteAlignedPosition st
where
encode :: !Int !*EncodingSt -> *EncodingSt
encode 0 st = st
encode remainingBytes st
#! byte_pos = st.cs_pos >> 3
#! st =
{ st
& cs_bits = {st.cs_bits & [byte_pos] = toChar $ int >> ((numBytes - remainingBytes) * 8)}
, cs_pos = st.cs_pos + 8
}
= encode (dec remainingBytes) st
generic gBinaryEncodingSize a :: !a !Int -> Int
gBinaryEncodingSize{|Int|} _ s = (IF_INT_64_OR_32 64 32) + byteAlignedPosition s
gBinaryEncodingSize{|Real|} _ s = 64 + byteAlignedPosition s
gBinaryEncodingSize{|Char|} _ s = 8 + byteAlignedPosition s
gBinaryEncodingSize{|Bool|} _ s = 1 + s
gBinaryEncodingSize{|String|} xs s = IF_INT_64_OR_32 64 32 + size xs * 8 + byteAlignedPosition s
gBinaryEncodingSize{|UNIT|} _ s = s
gBinaryEncodingSize{|PAIR|} cx cy (PAIR x y) s = cy y $ cx x s
gBinaryEncodingSize{|EITHER|} cl _ (LEFT x) s = cl x $ s + 1
gBinaryEncodingSize{|EITHER|} _ cr (RIGHT x) s = cr x $ s + 1
gBinaryEncodingSize{|CONS|} c (CONS x) s = c x s
gBinaryEncodingSize{|FIELD|} c (FIELD x) s = c x s
gBinaryEncodingSize{|OBJECT|} c (OBJECT x) s = c x s
gBinaryEncodingSize{|RECORD|} c (RECORD x) s = c x s
gBinaryEncodingSize{|[]|} c xs s = foldl (flip c) (IF_INT_64_OR_32 64 32 + byteAlignedPosition s) xs
gBinaryEncodingSize{|{}|} c xs s = foldlArr (flip c) (IF_INT_64_OR_32 64 32 + byteAlignedPosition s) xs
gBinaryEncodingSize{|{!}|} c xs s = foldlArr (flip c) (IF_INT_64_OR_32 64 32 + byteAlignedPosition s) xs
generic gBinaryDecode a :: !*EncodingSt -> (!Maybe a, !*EncodingSt)
gBinaryDecode{|Int|} st = decodeInt st
gBinaryDecode{|Real|} st = decodeReal st
gBinaryDecode{|Char|} st = decodeChar st
gBinaryDecode{|Bool|} st = decodeBool st
gBinaryDecode{|String|} st = decodeArray decodeChar st
gBinaryDecode{|UNIT|} st = (Just UNIT, st)
gBinaryDecode{|PAIR|} fx fy st
# (mbX, st) = fx st
# (mbY, st) = fy st
= case (mbX, mbY) of
(Just x, Just y) = (Just $ PAIR x y, st)
_ = (Nothing, st)
gBinaryDecode{|EITHER|} fl fr st
# (mbIsRight, st) = decodeBool st
= case mbIsRight of
Just isRight
| isRight = appFst (fmap RIGHT) $ fr st
| otherwise = appFst (fmap LEFT) $ fl st
_ = (Nothing, st)
gBinaryDecode{|CONS|} f st = appFst (fmap CONS) $ f st
gBinaryDecode{|FIELD|} f st = appFst (fmap \x -> FIELD x) $ f st
gBinaryDecode{|OBJECT|} f st = appFst (fmap \x -> OBJECT x) $ f st
gBinaryDecode{|RECORD|} f st = appFst (fmap RECORD) $ f st
gBinaryDecode{|[]|} f st = decodeList f st
gBinaryDecode{|{}|} f st = decodeArray f st
gBinaryDecode{|{!}|} f st = decodeArray f st
decodeInt :: !*EncodingSt -> (!Maybe Int, !*EncodingSt)
decodeInt st = decodeIntWithNBytes (IF_INT_64_OR_32 8 4) st
decodeChar :: !*EncodingSt -> (!Maybe Char, !*EncodingSt)
decodeChar st
# (mbInt, st) = decodeIntWithNBytes 1 st
= (toChar <$> mbInt, st)
decodeBool :: !*EncodingSt -> (!Maybe Bool, !*EncodingSt)
decodeBool cs=:{cs_pos = pos, cs_bits = bits}
#! s = size bits
#! byte_pos = pos >> 3
#! bit_pos = pos bitand 7
| s == byte_pos = (Nothing, cs)
#! int = toInt bits.[byte_pos]
#! bit_mask = 1 << bit_pos
#! bit = (bit_mask bitand int) <> 0
= (Just bit, {cs & cs_pos = inc pos})
decodeReal :: !*EncodingSt -> (!Maybe Real, !*EncodingSt)
decodeReal st = IF_INT_64_OR_32 decodeReal64 decodeReal32 $ st
where
decodeReal64 st
# (mbInt, st) = decodeInt st
= (unsafeCoerce <$> mbInt, st)
decodeReal32 st
# (mbInt1, st) = decodeInt st
# (mbInt2, st) = decodeInt st
= case (mbInt1, mbInt2) of
(Just int1, Just int2) = (Just $ unsafeCoerce (int1, int2), st)
_ = (Nothing, st)
decodeArray :: !(*EncodingSt -> (Maybe a, *EncodingSt)) !*EncodingSt -> (!Maybe (b a), !*EncodingSt) | Array b a
decodeArray f st
# (mbLength, st) = decodeInt st
= case mbLength of
Just l = decodeArray 0 l (unsafeCreateArray l) st
_ = (Nothing, st)
where
decodeArray i s arr st
| i == s = (Just arr, st)
| otherwise
# (mbX, st) = f st
= case mbX of
Just x = decodeArray (inc i) s {arr & [i] = x} st
_ = (Nothing, st)
decodeList :: !(*EncodingSt -> (Maybe a, *EncodingSt)) !*EncodingSt -> (!Maybe [a], !*EncodingSt)
decodeList xs st
# (mbArr, st) = decodeArray xs st
= (arrToList <$> mbArr, st)
where
arrToList :: !{b} -> [b]
arrToList xs = [x \\ x <-: xs]
decodeIntWithNBytes :: !Int !*EncodingSt -> (!Maybe Int, !*EncodingSt)
decodeIntWithNBytes numBytes st=:{cs_pos} = decode numBytes 0 $ withByteAlignedPosition st
where
// we can decode an entire byte at once, as the start position is byte-aligned
decode :: !Int !Int !*EncodingSt -> (!Maybe Int, !*EncodingSt)
decode 0 int st = (Just int, st)
decode remainingBytes int st=:{cs_bits}
#! byte_pos = st.cs_pos >> 3
| byte_pos == size cs_bits = (Nothing, st)
#! byte = toInt cs_bits.[byte_pos]
= decode (dec remainingBytes) (byte << ((numBytes - remainingBytes) * 8) + int) {st & cs_pos = st.cs_pos + 8}
withByteAlignedPosition :: !*EncodingSt -> *EncodingSt
withByteAlignedPosition st=:{cs_pos} = {st & cs_pos = byteAlignedPosition cs_pos}
byteAlignedPosition :: !Int -> Int
byteAlignedPosition pos = (pos + 7) bitand -8
:: *EncodingSt = {cs_pos :: !Int, cs_bits :: !*{#Char}}
derive gBinaryEncode (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
derive gBinaryEncodingSize (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
derive gBinaryDecode (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
definition module Data.GenCompress
import StdGeneric
from Data.Maybe import :: Maybe
:: BitVector :== {#Int}
:: CompressSt
generic gCompress a :: !a -> *CompressSt -> *CompressSt
derive gCompress Int, Real, Bool, Char, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], {}, {!}
generic gCompressedSize a :: a -> Int
derive gCompressedSize Int, Real, Bool, Char, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], {}, {!}
generic gUncompress a :: (u:CompressSt -> ((Maybe a),u:CompressSt))
derive gUncompress Int, Real, Bool, Char, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], {}, {!}
compress :: !a -> BitVector | gCompressedSize{|*|} a & gCompress{|*|} a
uncompress :: (BitVector -> Maybe a) | gUncompress{|*|} a
implementation module Data.GenCompress
import StdGeneric, StdEnv
from Data.Maybe import :: Maybe(..)
import Data._Array, Data.Func
//--------------------------------------------------
// uncompressor monad
ret :: !.a !u:CompressSt -> (!Maybe .a,!u:CompressSt)
ret a st = (Just a, st)
(>>=) infixl 5
(>>=) pa pb = bind pa pb
where
bind pa pb st
#! (ma, st) = pa st
= case ma of
Nothing -> (Nothing, st)
Just x -> pb x st
//--------------------------------------------------
:: BitVector :== {#Int}
:: BitPos :== Int
:: CompressSt = { cs_pos :: !Int, cs_bits :: !.{#Int} }
mkCompressSt arr = { cs_pos = 0, cs_bits = arr}
:: Compress a :== a -> *CompressSt -> *CompressSt
:: Uncompress a :== .CompressSt -> .(.(Maybe a), .CompressSt)
compressBool :: !Bool !*CompressSt -> *CompressSt
compressBool bit {cs_pos = pos, cs_bits = bits}
#! s = size bits
#! int_pos = pos >> (IF_INT_64_OR_32 6 5)
#! bit_pos = pos bitand (IF_INT_64_OR_32 63 31)
| s == int_pos
= abort "reallocate"
#! int = bits.[int_pos]
#! bit_mask = 1 << bit_pos
#! new_int = if bit (int bitor bit_mask) (int bitand (bitnot bit_mask))
= {cs_pos = inc pos, cs_bits = {bits & [int_pos] = new_int}}
uncompressBool :: !u:CompressSt -> (.(Maybe Bool),v:CompressSt), [u <= v]
uncompressBool cs=:{cs_pos = pos, cs_bits = bits}
#! s = size bits
#! int_pos = pos >> (IF_INT_64_OR_32 6 5)
#! bit_pos = pos bitand (IF_INT_64_OR_32 63 31)
| s == int_pos
= (Nothing, cs)
#! int = bits.[int_pos]
#! bit_mask = 1 << bit_pos
#! bit = (bit_mask bitand int) <> 0
= (Just bit, {cs & cs_pos = inc pos})
compressIntB :: !.Int !.Int -> .(*CompressSt -> .CompressSt)
compressIntB num_bits int
= compress 0 num_bits int
where
compress i n int
| i == n
= id
| otherwise
= compress (inc i) n (int >> 1)
o compressBool ((int bitand 1) == 1)
compressInt = compressIntB (IF_INT_64_OR_32 64 32)
compressChar c = compressIntB 8 (toInt c)
uncompressIntB :: !.Int -> u:CompressSt -> (.(Maybe Int),v:CompressSt), [u <= v]
uncompressIntB num_bits
= uncompress 0 num_bits 0
where
uncompress i n int
| i == n
= ret int
| otherwise
= uncompressBool
>>= \bit -> uncompress (inc i) n int
>>= \x -> ret ((if bit 1 0) + (x << 1))
uncompressInt :: (u:CompressSt -> (.(Maybe Int),v:CompressSt)), [u <= v]
uncompressInt = uncompressIntB (IF_INT_64_OR_32 64 32)
uncompressChar :: (u:CompressSt -> (.(Maybe Char),v:CompressSt)), [u <= v]
uncompressChar = uncompressIntB 8 >>= ret o toChar
realToBinary32 :: !Real -> (!Int,!Int);
realToBinary32 _ = code {
pop_b 0
};
realToBinary64 :: !Real -> Int;
realToBinary64 _ = code {
pop_b 0
};
binaryToReal32 :: !(!Int,!Int) -> Real;
binaryToReal32 _ = code {
pop_b 0
};
binaryToReal64 :: !Int -> Real;
binaryToReal64 _ = code {
pop_b 0
};
compressReal real
= IF_INT_64_OR_32
(compressInt (realToBinary64 real))
(let (i1, i2) = realToBinary32 real in compressInt i2 o compressInt i1)
uncompressReal :: (u:CompressSt -> (.(Maybe Real),v:CompressSt)), [u <= v]
uncompressReal
= IF_INT_64_OR_32
(uncompressInt
>>= \i -> ret (binaryToReal64 i))
(uncompressInt
>>= \i1 -> uncompressInt
>>= \i2 -> ret (binaryToReal32 (i1,i2)))
compressArray :: (a -> u:(v:CompressSt -> w:CompressSt)) !.(b a) -> x:(*CompressSt -> y:CompressSt) | Array b a, [x <= u,w <= v,w <= y]
compressArray f xs
= foldSt f [x \\ x <-: xs] o compressInt (size xs)
foldSt f [] = id
foldSt f [x:xs] = foldSt f xs o f x
uncompressArray :: (u:CompressSt -> ((Maybe v:a),w:CompressSt)) -> .(x:CompressSt -> ((Maybe y:(b v:a)),z:CompressSt)) | Array b a, [x w <= u,y <= v,x w <= z]
uncompressArray f
= uncompressInt >>= \s -> uncompress_array 0 s (unsafeCreateArray s)
where
uncompress_array i s arr
| i == s
= ret arr
= f >>= \x -> uncompress_array (inc i) s {arr & [i] = x}
compressList :: (a *CompressSt -> *CompressSt) ![a] -> *CompressSt -> *CompressSt
compressList c xs = compressArray c (list_to_arr xs)
where
list_to_arr :: [b] -> {b} | Array {} b
list_to_arr xs = {x \\ x <- xs}
uncompressList xs = uncompressArray xs >>= ret o arr_to_list
where
arr_to_list :: {b} -> [b] | Array {} b
arr_to_list xs = [x \\ x <-: xs]
//--------------------------------------------------------------------------------------