Lines of text

Lean module Esm.Document.Source.Lines, formal/Esm/Document/Source/Lines.lean at 184aa13d35e5
Imports Mathlib.Data.List.Basic

Containers are line-oriented: a fenced block ends at the first line that starts with its closing fence. heads lists the characters that start a line, so “no line of s starts with a backtick” is '’ ∉ heads true s`.

def heads source

def heads : Bool → List Char → List Char

The characters that start a line of s: the first character when s starts at the beginning of a line (bol), and every character right after a newline.

def endBol source

def endBol (bol : Bool) (s : List Char) : Bool

Whether the text after s starts at the beginning of a line.

Decoding the input

A source file may start with a UTF-8 byte-order mark and may use CRLF line endings, as editors on some systems write them. decodeText normalizes both before a reader lexes the text: a leading U+FEFF is dropped, and when the first line ends in CRLF every CRLF becomes LF. A text whose first line ends in a bare LF (everything the printers write) is read as it is (decodeText_line ), so a carriage return inside, say, a description still reads back.

def dropBOM source

def dropBOM : List Char → List Char

The text with a leading byte-order mark removed.

def firstCRLF source

def firstCRLF : List Char → Bool

Whether the first line ends in CRLF.

def unCRLF source

def unCRLF : List Char → List Char

Every CRLF as LF.

def decodeText source

def decodeText (s : List Char) : List Char

The input decoding: no byte-order mark, and LF line endings when the first line ends in CRLF.

theorem decodeText_line proved source

theorem decodeText_line (l t : List Char) (hn : '\n' ∉ l) (hr : '\r' ∉ l)
    (hb : l.head? ≠ some '\uFEFF') : decodeText (l ++ '\n' :: t) = l ++ '\n' :: t

A text whose first line has no carriage return and does not start with a byte-order mark is read as written.

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