Move examples out of the main text

This commit is contained in:
Tony Garnock-Jones 2022-06-19 14:36:05 +02:00
parent 90e06f8182
commit 6a5d82d567
1 changed files with 32 additions and 26 deletions

View File

@ -58,14 +58,6 @@ defined recursively as follows:
We write `len(|r|)` for the varint-encoding of the length of `Repr` `r`.
The following table illustrates varint-encoding.
| Number, `m` | `m` in binary, grouped into 7-bit chunks | `len(m)` bytes |
|-------------|-------------------------------------------|-----------------|
| 15 | `0001111` | 143 |
| 300 | `0000010 0101100` | 2 172 |
| 1000000000 | `0000011 1011100 1101011 0010100 0000000` | 3 92 107 20 128 |
There is no requirement that a varint-encoded `m` in a `Repr` be the
unique shortest encoding for that `m`.[^overlong-varint] However,
implementations *SHOULD* use the shortest encoding whereever possible
@ -133,22 +125,6 @@ the first byte in `intbytes(x)` (for `x`≠0) is the sign
bit.[^zero-intbytes] Every `SignedInteger` *MUST* be represented with
its shortest possible encoding.
For example,
«87112285931760246646623899502532662132736»
= A3 01 00 00 00 00 00 00 00
00 00 00 00 00 00 00 00
00 00
«-257» = A3 FE FF «-3» = A3 FD «128» = A3 00 80
«-256» = A3 FF 00 «-2» = A3 FE «255» = A3 00 FF
«-255» = A3 FF 01 «-1» = A3 FF «256» = A3 01 00
«-254» = A3 FF 02 «0» = A3 «32767» = A3 7F FF
«-129» = A3 FF 7F «1» = A3 01 «32768» = A3 00 80 00
«-128» = A3 80 «12» = A3 0C «65535» = A3 00 FF FF
«-127» = A3 81 «13» = A3 0D «65536» = A3 01 00 00
«-4» = A3 FC «127» = A3 7F «131072» = A3 02 00 00
[^zero-intbytes]: The value 0 needs zero bytes to identify the
value, so `intbytes(0)` is the empty byte string. Non-zero values
need at least one byte.
@ -203,8 +179,38 @@ The `Repr` `r` *MUST NOT* already have annotations; that is, it must not
begin with `0xBF`. The sequence `[v_1, ..., v_m]` *MUST* contain at
least one `Value`.
For example, the `Repr` corresponding to textual syntax `@a@b[]`, i.e.
an empty sequence annotated with two symbols, `a` and `b`, is
## Examples
### Varints (length representations).
The following table illustrates varint-encoding.
| Number, `m` | `m` in binary, grouped into 7-bit chunks | `len(m)` bytes |
|-------------|-------------------------------------------|-----------------|
| 15 | `0001111` | 143 |
| 300 | `0000010 0101100` | 2 172 |
| 1000000000 | `0000011 1011100 1101011 0010100 0000000` | 3 92 107 20 128 |
### SignedIntegers.
«87112285931760246646623899502532662132736»
= A3 01 00 00 00 00 00 00 00
00 00 00 00 00 00 00 00
00 00
«-257» = A3 FE FF «-3» = A3 FD «128» = A3 00 80
«-256» = A3 FF 00 «-2» = A3 FE «255» = A3 00 FF
«-255» = A3 FF 01 «-1» = A3 FF «256» = A3 01 00
«-254» = A3 FF 02 «0» = A3 «32767» = A3 7F FF
«-129» = A3 FF 7F «1» = A3 01 «32768» = A3 00 80 00
«-128» = A3 80 «12» = A3 0C «65535» = A3 00 FF FF
«-127» = A3 81 «13» = A3 0D «65536» = A3 01 00 00
«-4» = A3 FC «127» = A3 7F «131072» = A3 02 00 00
### Annotations.
The `Repr` corresponding to textual syntax `@a@b[]`, i.e. an empty sequence annotated with two
symbols, `a` and `b`, is
«@a @b []»
= [0xBF] ++ len(|«[]»|) ++ «[]» ++ len(|«a»|) ++ «a» ++ len(|«b»|) ++ «b»