-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
20 changed files
with
797 additions
and
81 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,190 @@ | ||
| {date="2024/02/03" hide="true"} | ||
| # Compression kit | ||
|
|
||
| - Varint encode example | ||
|
|
||
| ``` ckit | ||
| zeros = repeat(bit, 0) | ||
| // we will generate two methods: varint_u32.encode and varint_u32.decode | ||
| fn varint_u32.encode(x: [32]bit) ~ varint_u32.decode(bytes: [?: 1..=5]u8) { | ||
| scan x ~ bytes { | ||
| result.push(byte) // ~ byte = result.pop() | ||
| // we can reconstruct computation because suffix is constant | ||
| if x[7..].prefix_of(zeros) ~ byte & 0x80 == 0 { | ||
| byte = x.pop(7) // ~ x.push(byte[0..7]) | ||
| x.pop(0..) // ~ x.push(zeroes[0..]), instead of break explicitly skip rest of the x | ||
| } else { | ||
| byte = x.pop(7) | 0x80 | ||
| } | ||
| } | ||
| } | ||
| ``` | ||
|
|
||
| - Shrink encode example | ||
|
|
||
| ``` ckit | ||
| zeros = repeat(bit, 0) | ||
| fn shrink_u32.encode(x: [32]bit) ~ shrink_u32.decode(bytes: [n: 1..=5]u8) { | ||
| scan x ~ bytes { | ||
| result.push(byte) // ~ byte = result.pop() | ||
| byte = x.pop(8) // ~ x.push(byte) | ||
| if x[0..].prefix_of(zeros) ~ result.empty() { | ||
| x.pop(0..) // ~ x.push(zeroes[0..]) | ||
| } | ||
| } | ||
| } | ||
| ``` | ||
|
|
||
| - Length prefixing | ||
|
|
||
| ``` ckit | ||
| fn length_prefix.encode(b: [n: 0..1<<32]u8) ~ length_prefix.decode(bytes: [?: n+1..=n+5]u8) { | ||
| bytes.write(varint_length) // ~ 1. varint_length: [?]u8 = result.read() | ||
| varint_length = varint_u32(n) // ~ 2. n = varint_u32.decode(varint_length) | ||
| bytes.write_fixed(n, b) // ~ 3. b = result.read_fixed(n) | ||
| } | ||
| ``` | ||
|
|
||
| - Length prefixing with reverse | ||
|
|
||
| ``` ckit | ||
| // idempotent function: reverse(reverse(b)) == b | ||
| extern fn reverse(b: [n]u8) ~ reverse(b: [n]u8); | ||
|
|
||
| fn length_prefix.encode(b: [n: 0..1<<32]u8) ~ length_prefix.decode(bytes: [?: n+1..=n+5]u8) { | ||
| bytes.write(varint_length) // ~ 1. varint_length: [?]u8 = result.read() | ||
| varint_length = varint_u32.encode(n) // ~ 2. n = varint_u32.decode(varint_length) | ||
| bytes.write_fixed(n, reversed) // ~ 3. reversed = result.read_fixed(n) | ||
| reversed = reverse(b) // ~ 4. b = reverse(reversed) | ||
| } | ||
|
|
||
| fn length_prefix.encode(b: [n: 0..1<<32]u8) ~ length_prefix.decode(bytes: [?: n+1..=n+5]u8) { | ||
| varint_length = varint_u32.encode(n) // ~ 2. n = varint_u32.decode(varint_length) | ||
| bytes.write(varint_length) // ~ 1. varint_length: [?]u8 = result.read() | ||
| reversed = reverse(b) // ~ 4. b = reverse(reversed) | ||
| bytes.write_fixed<n>(reversed) // ~ 3. reversed = result.read_fixed< n >() | ||
| } | ||
| ``` | ||
|
|
||
| - Syntax for state definition | ||
|
|
||
| ``` ckit | ||
| forward state [?]T { | ||
| mut push(x: T) ~ pop() // dual method - we must call pop for every push in forward order | ||
| mut write(x: [?]T) ~ read() | ||
| mut<n: 0..1<<32> write_fixed(x: [n]T) ~ read_fixed() | ||
| } | ||
|
|
||
| forward state BlocksLru { | ||
| mut encode(offset: u32) ~ decode(encoded: u32) | ||
| mut touch(offset: u32): void // no dual method - we must call touch with same argument in dual method | ||
| } | ||
|
|
||
| forward state FwdBitStream { | ||
| mut init(): void | ||
| mut flush(): void | ||
| mut close(): void | ||
| mut<n: 0..=64> push(b: [n]bits) ~ pop() | ||
| } | ||
|
|
||
| // for backward state we must generate dual operations in reverse order | ||
| backward state BwdBitStream { | ||
| mut init_write() ~ close_read() | ||
| mut flush() ~ reload() | ||
| mut close_write() ~ init_read() | ||
| mut<n: 0..=64> push(b: [n]bits) ~ pop() | ||
| } | ||
|
|
||
| // must not compile because we .decode can't be implemented | ||
| fn invalid.encode(x: u32) ~ invalid.decode(bytes: [?]u32) { | ||
| var ( blocks: BlocksLru ) | ||
| y = blocks.encode(x) // 2. ~ x = blocks_lru.decode(y) !!! y is unknown here but we can't violate state operations order | ||
| z = blocks.encode(y) // 3. ~ y = blocks_lru.decode(z) | ||
| bytes.push(z) // 1. ~ z = result.pop() | ||
| } | ||
| ``` | ||
|
|
||
| - [QOI](https://qoiformat.org/) | ||
|
|
||
| ``` ckit | ||
|
|
||
| const RGBA = struct { | ||
| r: 0..256, | ||
| g: 0..256, | ||
| b: 0..256, | ||
| a: 0..256, | ||
| } | ||
|
|
||
| const Header { | ||
| magic: "qoif" | ||
| width: 0..1<<32 | ||
| height: 0..1<<32 | ||
| channels: {3, 4} | ||
| colorspace: {0, 1} | ||
| } | ||
|
|
||
| const Operation = union { | ||
| QOI_OP_RGB = struct { r: 0..256, g: 0..256, b: 0..256 }, | ||
| QOI_OP_RGBA = struct { r: 0..256, g: 0..256, b: 0..256, a: 0..256 }, | ||
| QOI_OP_INDEX = struct { index: 0..64 }, | ||
| QOI_OP_DIFF = struct { dr: -2..2, dg: -2..2, db: -2..2 }, | ||
| QOI_OP_LUMA = struct { dr: -32..32, dr_dg: -8..8, db_dg: -8..8 }, | ||
| QOI_OP_RUN = struct { run: 0..64 }, | ||
| } | ||
|
|
||
| fn qoi.encode({ header: Header, operations: [n]Operation }) ~ qoi.decode(bytes: [?]u8) { | ||
| bytes.write_fixed<4>("qoif") // 1. ~ assert!(bytes.read_fixed<4>() == "qoif") | ||
| bytes.write_fixed<4>(header.width) // 2. ~ header.width = bytes.read_fixed<4>() | ||
| bytes.write_fixed<4>(header.height) // 3. ~ header.height = bytes.read_fixed<4>() | ||
| bytes.write_fixed<4>(header.channels) // 4. ~ header.channels = bytes.read_fixed<4>() | ||
| bytes.write_fixed<4>(header.colorspace) // 5. ~ header.colorspace = bytes.read_fixed<4>() | ||
|
|
||
| ~ size = header.width * header.height // initialize counter only for .decode method | ||
| scan operations ~ bytes { | ||
| current = operations.pop() | ||
| match current { | ||
| .QOI_OP_RGB ~ bytes[0] == 0b11111110 { | ||
| bytes.write_fixed<4>([0b11111110, current.r, current.g, current.b]) | ||
| ~ size -= 1 | ||
| } | ||
| .QOI_OP_RGBA ~ bytes[0] == 0b11111111 { | ||
| bytes.write_fixed<5>([0b11111111, current.r, current.g, current.b, current.a]) | ||
| ~ size -= 1 | ||
| } | ||
| .QOI_OP_INDEX ~ bytes[0][0..2] == 0b00 { | ||
| bytes.write_fixed<1>([0b00 || current.index]) | ||
| ~ size -= 1 | ||
| } | ||
| .QOI_OP_DIFF ~ bytes[0][0..2] == 0b01 { | ||
| bytes.write_fixed<1>([0b01 || current.dr + 2 || current.dg + 2 || current.db + 2]) | ||
| ~ size -= 1 | ||
| } | ||
| .QOI_OP_LUMA ~ bytes[0][0..2] == 0b10 { | ||
| bytes.write_fixed<2>([0b10 || current.dg + 32, current.dr_dg + 8 || current.db_dg + 8]) | ||
| ~ size -= 1 | ||
| } | ||
| .QOI_OP_RUN ~ bytes[0][0..2] == 0b11 { | ||
| bytes.write_fixed<1>([0b11 || current.run]) | ||
| ~ size -= current.run | ||
| } | ||
| } | ||
| if ~ size == 0 { | ||
| break | ||
| } | ||
| } | ||
| bytes.write_fixed<8>([0, 0, 0, 0, 0, 0, 0, 1]) | ||
| } | ||
|
|
||
| forward state qoi.Recent { | ||
|
|
||
| } | ||
|
|
||
| fn qoi.compress(image: [height: 0..1<<32, width: 0..1<<32]RGBA) ~ qoi.decompress({ header: Header, operations: [n]Operation }) { | ||
| header = Header { width: width, height: height, channels: 4, colorspace: 0 } | ||
| // how to iterate over 2d array? | ||
| scan image ~ operations { | ||
|
|
||
| } | ||
| } | ||
|
|
||
| ``` |
Oops, something went wrong.