The strict YAML subset codec
The YAML spelling of a Json
value, used for esm:<path> blocks and front matter in
Markdown documents. The printed text is block-style YAML 1.2:
- A non-empty object is one
key: valueline per entry at the current indentation. - A non-empty array is one
- itemline per element at the current indentation. - A scalar,
[]or{}value follows itskey:or-on the same line. - A non-empty object or array under a key starts on the next line, indented two
spaces deeper (
key:then the block). - A non-empty object as an array element starts on the
-line (- key: v), its other entries indented to align with the first key (two spaces past the-). - A non-empty array as an array element starts on the next line, indented two
spaces deeper (
-alone, then the block). - A top-level scalar,
[]or{}is one line.
Scalars: null, true, false, numbers in the canonical spelling (Number.print
),
and strings ALWAYS double-quoted with JSON-style escapes (\uXXXX for the characters
of Strings.needsHex
), which avoids YAML’s implicit typing. A key is bare when it
matches [A-Za-z_][A-Za-z0-9_]* and is not, in any letter case, one of YAML’s
special plain scalars (true false null yes no on off y n); otherwise it is quoted
like a string. A key whose spelling is longer than 1024 characters (YAML’s limit on
an implicit key) is written in the explicit form instead: ? "key" on its own line,
then : and the value on the next line at the same indentation.
Every line ends with a newline. The reader only accepts this layout (it is the
canonical form; other YAML is out of scope), a bare key only when it would print bare,
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 specialWords : List String
Plain scalars YAML 1.1 or 1.2 reads as something other than a string; a key equal to one of them (in any letter case) is quoted.
def reserved (k : String) : Bool
A key equal (in any letter case) to a special plain scalar: never bare.
def longKey (k : String) : Bool
A key whose spelling is longer than YAML’s 1024-character limit on implicit keys.
def keyPart (m : Nat) (k : String) : List Char
The key of an entry at indentation m, up to its :. A long key uses the explicit
form: ? "key" on its own line, then the : on the next line at the same
indentation.
def inline : Json → List Char
The one-line spelling of a scalar or an empty container. (A non-empty container
is never printed inline; it gets []/{} here only to keep the function total.)
def encItems (m : Nat) : List Json → List Char
The lines of a non-empty array at indentation m.
def itemBody (m : Nat) : Json → List Char
What follows the - of an array element at indentation m.
def encEntries (m : Nat) : List (String × Json) → List Char
The lines of a non-empty object at indentation m.
def valBody (m : Nat) : Json → List Char
What follows the : of an entry whose key is at indentation m.
Reader
def parseKeyAt (m : Nat) : List Char → Option (String × List Char)
The key of an entry at indentation m: an explicit ? "key" line followed by
the indentation of the : line, or a plain key.
def pInline : List Char → Option (Json × List Char)
A scalar or an empty container.
def pScalarLine (input : List Char) : Option (Json × List Char)
A scalar and the end of its line.
def isItemLine (m : Nat) (input : List Char) : Bool
A line at indentation m that starts an array element.
def isEntryLine (m : Nat) (input : List Char) : Bool
A line at indentation m that starts an object entry.
def pItems : Nat → Nat → List Char → Option (List Json × List Char)
Array elements at indentation m, as long as lines start with - there.
def pItemBody : Nat → Nat → List Char → Option (Json × List Char)
After the - of an element at indentation m.
def pEntries : Nat → Nat → List Char → Option (List (String × Json) × List Char)
Object entries at indentation m, as long as lines start with a key there.
def pEntry : Nat → Nat → List Char → Option ((String × Json) × List Char)
One entry, at its key, whose key is at indentation m.
def pValBody : Nat → Nat → List Char → Option (Json × List Char)
After the : of an entry whose key is at indentation m.
def pTop (f : Nat) (input : List Char) : Option (Json × List Char)
A whole document: an array, an object, or one scalar line.
def decode (s : List Char) : Option Json
Read a document; all of the input must be consumed, and the value must be well
formed (no repeated key; numbers are already canonical, Number.parse
).
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 keyHead_facts {c : Char} (h : c = '"' ∨ c = '?' ∨ isIdentStart c = true) :
c ≠ ' ' ∧ c ≠ '-' ∧ (c == '"' || c == '?' || isIdentStart c) = true
A key never starts with a space or -.
theorem parseKeyAt_keyPart (m : Nat) (k : String) (rest : List Char)
(hr : ∀ c ∈ rest.head?, isIdentChar c = false) :
parseKeyAt m (keyPart m k ++ rest) = some (k, rest)
A printed key, plain or explicit, reads back, when what follows is not an identifier character.
Indentation
def Ends (m : Nat) (rest : List Char) : Prop
What may follow a block at indentation m: nothing, or a line indented less.
Scalars
Line structure
theorem pEntry_enc (f m : Nat) (k : String) (v : Json) (rest : List Char)
(h : pValBody f m (valBody m v ++ rest) = some (v, rest)) :
pEntry (f + 1) m (keyPart m k ++ ':' :: (valBody m v ++ rest)) = some ((k, v), rest)
An entry reads back once its value does.
Whole documents
theorem decode_encode (v : Json) (hv : v.WF) : decode (encode v) = some v
The YAML round trip. Reading the canonical YAML spelling of a well-formed value gives the value back.