Text scanning shared by the containers

Lean module Esm.Document.Source.Text, formal/Esm/Document/Source/Text.lean at 184aa13d35e5
Imports Esm.Document.Source.Facts, Esm.Document.Source.Lines, Esm.Document.Yaml, Esm.Document.TypstDict, Esm.Document.Math.RoundTripLatex, Esm.Document.Math.RoundTripTypst

Prefixes, lines, fenced bodies ended by a closing line, and the facts the containers' round trips use about them.

Prefixes

def pre source

def pre : List Char → List Char → Bool

p is a prefix of s.

def hasSub source

def hasSub (p s : List Char) : Bool

p occurs in s.

theorem pre_app_long proved source

theorem pre_app_long : ∀ (p x t : List Char), p.length ≤ x.length → pre p (x ++ t) = pre p x

A prefix no longer than x is decided within x.

theorem pre_app_false proved source

theorem pre_app_false : ∀ (p x t : List Char), pre p x = false → pre x p = false →
    pre p (x ++ t) = false

Two texts neither of which starts the other differ before either ends.

theorem pre_line proved source

theorem pre_line {stop x : List Char} (hn : '\n' ∉ stop) (hx : '\n' ∈ x) (y : List Char) :
    pre stop (x ++ y) = pre stop x

A prefix without a newline is decided within the first line.

Lines

def splitLine source

def splitLine : List Char → List Char × List Char

The rest of the current line, and what follows its newline.

def noStop source

def noStop (stop : List Char) (s : List Char) : Bool

No line of s starts with stop.

def untilStop source

def untilStop (stop : List Char) : Nat → List Char → Option (List Char × List Char × List Char)

Lines up to the first one that starts with stop: the lines before it (each with its newline), the rest of the closing line, and the text after the closing line.

def Lines source

def Lines (body : List Char) : Prop

Complete lines: empty, or ending with a newline.

theorem untilStop_body proved source

theorem untilStop_body (stop : List Char) (hs : stop ≠ []) (hn : '\n' ∉ stop) :
    ∀ (body sl t : List Char), Lines body → noStop stop body = true → '\n' ∉ sl →
      ∀ f, body.length + stop.length < f →
        untilStop stop f (body ++ stop ++ sl ++ '\n' :: t) = some (body, sl, t)

A fenced body is read back up to its closing line.

theorem noStop_of_heads proved source

theorem noStop_of_heads {c : Char} (p : List Char) (s : List Char) (h : c ∉ heads true s) :
    noStop (c :: p) s = true

A line never starts with stop when no line starts with its first character.

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