The Typst value codec
A Json
value prints as a Typst code-mode value:
none,true,false; numbers in the canonical spelling (Number.print), except-2^63, printed(-9223372036854775807 - 1)because Typst reads the literal-9223372036854775808as a float;- strings
"…"with Typst escapes (\\,\",\n,\r,\t,\u{XXXX}); - arrays
(a, b),()empty; dictionaries(key: v, "quoted key": v),(:)empty. A key is bare when it matches[A-Za-z_][A-Za-z0-9_]*and is not a Typst keyword, otherwise quoted.
The canonical layout is one element per line: (, a newline, then each element on
its own line indented two spaces deeper than the opening line, each followed by ,
(so a one-element array is (a,)), then ) at the opening line’s indentation.
The reader skips whitespace between tokens, so it accepts any layout of the same
tokens (including the -2^63 expression), with or without a trailing comma, except
that a one-element array needs its comma: Typst reads (x) as the value x, not an
array, so the reader rejects it. It accepts a bare key only when it would print bare
(Typst rejects a keyword as a key), and only well-formed values (decode_wf
): it
rejects a repeated key, and numbers are read by Number.parse
(canonical form; no
leading zero; integers in Int64). decode_encode
is the round trip.
Printer
def minTail : List Char
After (: the rest of (-9223372036854775807 - 1). Typst reads the literal
9223372036854775808 as a float (it overflows Int64 before the minus applies), so
-2^63 is printed as this integer expression instead.
def minLit : List Char
-9223372036854775807, the first operand of the -2^63 expression.
def printNum (n : JNum) : List Char
A number: the canonical spelling, except -2^63 (see minTail
).
def enc (m : Nat) : Json → List Char
The canonical print of a value whose first line is indented by m spaces (the
indentation itself is not printed).
Reader
def isEntry (input : List Char) : Bool
The input starts with a key and a colon: the first element of a dictionary.
inductive Next where
/-- `,` and another element. -/
| more
/-- `)`, after a `,` (`comma`) or directly. -/
| close (comma : Bool)
What follows one element.
def pNext (r : List Char) : Option (Next × List Char)
After one element: , then either ) or the next element, or ) directly.
def pMin (r : List Char) : Option (List Char)
After ( and any whitespace: the rest of the -2^63 expression
(-9223372036854775807 - 1), with any whitespace between its tokens.
def pVal : Nat → List Char → Option (Json × List Char)
A value, at its first character.
def pParen : Nat → List Char → Option (Json × List Char)
After ( and any whitespace.
def pItems : Nat → Bool → List Char → Option (List Json × List Char)
Array elements, at one of them (first: the first, which needs a , after it even
when it is the last).
def pEntries : Nat → List Char → Option (List (String × Json) × List Char)
Dictionary entries, at the first key.
def decode (s : List Char) : Option Json
Read a value: whitespace, the value, whitespace, end of input. The value must be well formed.
theorem decode_wf {s : List Char} {v : Json} (h : decode s = some v) : v.WF
What decode
reads is well formed.
The round trip
Characters
theorem enc_head (m : Nat) (v : Json) (hv : v.WF) :
∃ c t, enc m v = c :: t ∧ isWs c = false ∧ c ≠ ')' ∧ c ≠ ':'
What a printed value starts with.
Keys
theorem keyHead_facts {c : Char} (h : c = '"' ∨ isIdentStart c = true) :
c ≠ ')' ∧ c ≠ ':' ∧ isWs c = false ∧ c ≠ '-'
A key starts with " or an identifier start: never whitespace, ), : or -.
Reader steps
The -2^63 expression is never mistaken for another value
theorem print_minLit : Number.print (.int (-9223372036854775807)) = minLit
-9223372036854775807 prints as the first operand of the -2^63 expression.
theorem pMin_num (n : JNum) (hn : n.WF) (t : List Char) :
pMin (Number.print n ++ ',' :: t) = none
A printed number followed by , is not the -2^63 expression, even when it is its
first operand -9223372036854775807.
theorem pMin_enc (m : Nat) (v : Json) (hv : v.WF) (t : List Char) :
pMin (enc m v ++ ',' :: t) = none
A printed value followed by , is not the -2^63 expression.
def itemsTail (m : Nat) : List Json → List Char
The elements of a non-empty array after the first one’s indentation.
def entriesTail (m : Nat) : List (String × Json) → List Char
The entries of a non-empty dictionary after the first one’s indentation.
theorem decode_encode (v : Json) (hv : v.WF) : decode (encode v) = some v
The Typst round trip. Reading the canonical Typst spelling of a well-formed value gives the value back.