Lexical pieces shared by the YAML and Typst codecs

Lean module Esm.Document.Strings, formal/Esm/Document/Strings.lean at 184aa13d35e5
Imports Esm.Document.Number

Double-quoted strings with JSON-style escapes: \", \\, \n, \t, \r, and a four-digit hex escape for the other characters a reader might not take literally (needsHex ). YAML writes the hex escape \uXXXX, Typst \u{XXXX}; everything else is literal. parseQuoted_quote is the round trip, for both spellings at once.
Bare identifiers [A-Za-z_][A-Za-z0-9_]* (keys) and the reader of a maximal run of identifier characters.
Runs of spaces (indentation).
Object keys, bare or quoted, with the codec’s reserved words (which a reader would not take as a key string) always quoted, and never accepted bare. parseKey_printKey is the round trip.
What a number or a key never starts with, which the codecs’ readers use to tell them apart from other tokens.

Hex escapes

def hexChar source

def hexChar (d : Nat) : Char

A lowercase hex digit.

def hexVal source

def hexVal (c : Char) : Option Nat

The value of a hex digit (either case).

def hex4 source

def hex4 (n : Nat) : List Char

Four hex digits, most significant first.

def hex4Val source

def hex4Val (a b c d : Char) : Option Nat

The value of four hex digits.

def needsHex source

def needsHex (c : Char) : Bool

Characters written as a hex escape: the C0 controls, DEL, the C1 controls, the Unicode line and paragraph separators, the byte-order mark, and the two BMP noncharacters U+FFFE, U+FFFF. (YAML does not allow the controls literally, and YAML 1.1 readers treat U+0085, U+2028, U+2029 as line breaks.)

Quoted strings

def escChar source

def escChar (braces : Bool) (c : Char) : List Char

The escape of one character. braces selects Typst’s \u{XXXX} over YAML’s \uXXXX.

def escape source

def escape (braces : Bool) (cs : List Char) : List Char

The escaped characters of a string, without the quotes.

def quote source

def quote (braces : Bool) (s : String) : List Char

A double-quoted string literal.

def unquoteBody source

def unquoteBody (braces : Bool) : List Char → Option (List Char × List Char)

The body of a quoted string after the opening quote: the characters up to the closing quote, and what follows it.

def parseQuoted source

def parseQuoted (braces : Bool) : List Char → Option (String × List Char)

A quoted string literal.

theorem parseQuoted_quote proved source

theorem parseQuoted_quote (braces : Bool) (s : String) (rest : List Char) :
    parseQuoted braces (quote braces s ++ rest) = some (s, rest)

The string round trip, for both escape spellings: reading a quoted literal gives the string back, whatever follows it.

Identifiers and spaces

def isIdent source

def isIdent (cs : List Char) : Bool

[A-Za-z_][A-Za-z0-9_]*.

def readIdent source

def readIdent : List Char → List Char × List Char

The maximal run of identifier characters at the front.

def spaces source

def spaces (n : Nat) : List Char

n spaces.

Keys

def bareKey source

def bareKey (reserved : String → Bool) (k : String) : Bool

A key prints bare when it is an identifier and not one of the codec’s reserved words.

def printKey source

def printKey (braces : Bool) (reserved : String → Bool) (k : String) : List Char

A key: bare when it can be, otherwise quoted (braces as in quote ).

def parseKey source

def parseKey (braces : Bool) (reserved : String → Bool) : List Char → Option (String × List Char)

A key: quoted, or an identifier that is not a reserved word.

theorem parseKey_printKey proved source

theorem parseKey_printKey (braces : Bool) (reserved : String → Bool) (k : String)
    (rest : List Char) (hr : ∀ c ∈ rest.head?, isIdentChar c = false) :
    parseKey braces reserved (printKey braces reserved k ++ rest) = some (k, rest)

A printed key reads back, when what follows is not an identifier character.

def nonKeyHeads source

def nonKeyHeads : List Char

Characters a printed key never starts with.

theorem keyHead_ne proved source

theorem keyHead_ne {c : Char} (h : c = '"' ∨ isIdentStart c = true) (x : Char)
    (hx : x ∈ nonKeyHeads := by decide) : c ≠ x

A key starts with " or an identifier start, so not with any of nonKeyHeads .

Number heads

def nonNumHeads source

def nonNumHeads : List Char

Characters a printed number never starts with.

This module also proves 12 lemmas without doc comments; they are in the source.