2023-10-16 22:31:10 +00:00
|
|
|
For a value <span class="postcard-grammar binarysyntax">*V*</span>, we write <span
|
|
|
|
class="postcard-grammar binarysyntax">«*V*»</span> for the binary encoding of <span
|
|
|
|
class="postcard-grammar binarysyntax">*V*</span>.
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
«`#f`» | = | `80`
|
|
|
|
«`#t`» | = | `81`
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
«`@`*W* *V*» | = | `85` «*W*» «*V*»
|
|
|
|
«`#!`*V*» | = | `86` «*V*»
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
«*V*» | = | `87``04` **binary32**(*V*) | if *V* ∈ Float
|
|
|
|
«*V*» | = | `87``08` **binary64**(*V*) | if *V* ∈ Double
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
«*V*» | = | `B0` **varint**(|**intbytes**(*V*)|) **intbytes**(*V*) | if *V* ∈ SignedInteger
|
|
|
|
«*V*» | = | `B1` **varint**(|**utf8**(*V*)|) **utf8**(*V*) | if *V* ∈ String
|
|
|
|
«*V*» | = | `B2` **varint**(|*V*|) *V* | if *V* ∈ ByteString
|
|
|
|
«*V*» | = | `B3` **varint**(|**utf8**(*V*)|) **utf8**(*V*) | if *V* ∈ Symbol
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
«`<`*L* *F*<sub>1</sub> ... *F*<sub>m</sub>`>`» | = | `B4` «*L*» «*F*<sub>1</sub>» ... «*F*<sub>m</sub>» `84`
|
|
|
|
«`[`*X*<sub>1</sub> ... *X*<sub>m</sub>`]`» | = | `B5` «*X*<sub>1</sub>» ... «*X*<sub>m</sub>» `84`
|
|
|
|
«`#{`*E*<sub>1</sub> ... *E*<sub>m</sub>`}`» | = | `B6` «*E*<sub>1</sub>» ... «*E*<sub>m</sub>» `84`
|
|
|
|
«`{`*K*<sub>1</sub>`:`*V*<sub>1</sub> ... *K*<sub>m</sub>`:`*V*<sub>m</sub>`}`» | = | `B7` «*K*<sub>1</sub>» «*V*<sub>1</sub>» ... «*K*<sub>m</sub>» «*V*<sub>m</sub>» `84`
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
|
|
|
**varint**(*n*) | = | <span class="outputish">*n*</span> | if *n* < 128
|
|
|
|
| | <span class="outputish">(*n* & 127) | 128</span> **varint**(*n* >> 7) | if *n* ≥ 128
|
|
|
|
|
|
|
|
{:.postcard-grammar.binarysyntax}
|
2023-10-16 23:00:54 +00:00
|
|
|
**intbytes**(*n*) | = | <span class="roman">(the empty sequence)</span> | if *n* = 0
|
2023-10-16 22:31:10 +00:00
|
|
|
| | **signedBigEndian**(*n*) | otherwise
|
|
|
|
**signedBigEndian**(*n*) | = | <span class="outputish">*n* & 255</span> | if -128 ≤ *n* ≤ 127
|
|
|
|
| | **signedBigEndian**(*n* >> 8) <span class="outputish">*n* & 255</span> | otherwise
|
|
|
|
|
|
|
|
The functions <span class="postcard-grammar binarysyntax">**binary32**(*F*)</span> and <span
|
|
|
|
class="postcard-grammar binarysyntax">**binary64**(*D*)</span> yield big-endian 4- and 8-byte
|
|
|
|
IEEE 754 binary representations of <span class="postcard-grammar binarysyntax">*F*</span> and
|
|
|
|
<span class="postcard-grammar binarysyntax">*D*</span>, respectively.
|
|
|
|
|
|
|
|
<!--
|
|
|
|
Together, <span class="postcard-grammar binarysyntax">**div**</span> and <span
|
|
|
|
class="postcard-grammar binarysyntax">**mod**</span> give [Euclidean
|
|
|
|
division](https://en.wikipedia.org/wiki/Euclidean_division); that is, if
|
|
|
|
<span class="postcard-grammar binarysyntax">*n* **div** *d* = *q*</span> and
|
|
|
|
<span class="postcard-grammar binarysyntax">*n* **mod** *d* = *r*</span>, then
|
|
|
|
<span class="postcard-grammar binarysyntax">*n* = *dq* + *r*</span> and
|
|
|
|
<span class="postcard-grammar binarysyntax">0 ≤ *r* < |d|</span>.
|
|
|
|
-->
|
|
|
|
|
|
|
|
<!--
|
2023-03-15 16:15:26 +00:00
|
|
|
For a value `V`, we write `«V»` for the binary encoding of `V`.
|
2023-03-15 15:24:02 +00:00
|
|
|
|
|
|
|
«#f» = [0x80]
|
|
|
|
«#t» = [0x81]
|
|
|
|
|
2023-10-14 22:33:41 +00:00
|
|
|
«@W V» = [0x85] ++ «W» ++ «V»
|
2023-03-15 15:24:02 +00:00
|
|
|
«#!V» = [0x86] ++ «V»
|
|
|
|
|
2023-10-13 12:21:40 +00:00
|
|
|
«V» if V ∈ Float = [0x87, 0x04] ++ binary32(V)
|
|
|
|
«V» if V ∈ Double = [0x87, 0x08] ++ binary64(V)
|
2023-03-15 15:24:02 +00:00
|
|
|
|
2023-03-15 16:15:26 +00:00
|
|
|
«V» if V ∈ SignedInteger = [0xB0] ++ varint(|intbytes(V)|) ++ intbytes(V)
|
2023-03-15 15:24:02 +00:00
|
|
|
«V» if V ∈ String = [0xB1] ++ varint(|utf8(V)|) ++ utf8(V)
|
|
|
|
«V» if V ∈ ByteString = [0xB2] ++ varint(|V|) ++ V
|
|
|
|
«V» if V ∈ Symbol = [0xB3] ++ varint(|utf8(V)|) ++ utf8(V)
|
|
|
|
|
|
|
|
«<L F_1...F_m>» = [0xB4] ++ «L» ++ «F_1» ++...++ «F_m» ++ [0x84]
|
|
|
|
«[X_1...X_m]» = [0xB5] ++ «X_1» ++...++ «X_m» ++ [0x84]
|
|
|
|
«#{E_1...E_m}» = [0xB6] ++ «E_1» ++...++ «E_m» ++ [0x84]
|
|
|
|
«{K_1:V_1...K_m:V_m}» = [0xB7] ++ «K_1» ++ «V_1» ++...++ «K_m» ++ «V_m» ++ [0x84]
|
|
|
|
|
2023-10-14 23:04:01 +00:00
|
|
|
varint(v) = [v] if v < 128
|
|
|
|
[(v & 0x7F) + 128] ++ varint(v >> 7) if v ≥ 128
|
2023-03-15 15:24:02 +00:00
|
|
|
|
2023-03-15 16:15:26 +00:00
|
|
|
The functions `binary32(F)` and `binary64(D)` yield big-endian 4- and
|
|
|
|
8-byte IEEE 754 binary representations of `F` and `D`, respectively.
|
2023-03-15 15:24:02 +00:00
|
|
|
|
2023-03-15 16:15:26 +00:00
|
|
|
The function `intbytes(x)` is a big-endian two's-complement signed binary representation of
|
|
|
|
`x`, taking exactly as many whole bytes as needed to unambiguously identify the value and its
|
2023-10-13 12:21:40 +00:00
|
|
|
sign. In particular, `intbytes(0)` is the empty byte sequence.
|
2023-10-16 22:31:10 +00:00
|
|
|
-->
|