Rendered Code

Lean's pretty printer produces CodeWithInfos (a TaggedText SubexprInfo), which carries rich metadata such as expression types, universe levels, elaboration state, etc. This is too large to serialize to disk.

RenderedCode is a TaggedText RenderedCode.Tag that keeps only the information needed for HTML rendering: which tokens are declaration references (for linking), which are sorts (for linking to the foundational types page), and which are keywords or strings (for syntax highlighting). The conversion from CodeWithInfos to RenderedCode happens in renderTagged at the bottom of this file.

RenderedCode is serialized to the database as a binary blob via ToBinary/FromBinary instances. If the RenderedCode.Tag or TaggedText types change, the type hash in DocGen4.DB.Schema will detect the mismatch and require a rebuild.

inductive DocGen4.SortFormer : Type

Used in RenderedCode.Tag to track what kind of sort this is.

• type : SortFormer
• prop : SortFormer
• sort : SortFormer

def DocGen4.instToJsonSortFormer.toJson : SortFormer → Lean.Json

Equations

• DocGen4.instToJsonSortFormer.toJson DocGen4.SortFormer.type = Lean.toJson "type"
• DocGen4.instToJsonSortFormer.toJson DocGen4.SortFormer.prop = Lean.toJson "prop"
• DocGen4.instToJsonSortFormer.toJson DocGen4.SortFormer.sort = Lean.toJson "sort"

@[implicit_reducible]

instance DocGen4.instToJsonSortFormer : Lean.ToJson SortFormer

Equations

• DocGen4.instToJsonSortFormer = { toJson := DocGen4.instToJsonSortFormer.toJson }

def DocGen4.instFromJsonSortFormer.fromJson : Lean.Json → Except String SortFormer

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instFromJsonSortFormer : Lean.FromJson SortFormer

Equations

• DocGen4.instFromJsonSortFormer = { fromJson? := DocGen4.instFromJsonSortFormer.fromJson }

@[implicit_reducible]

instance DocGen4.instBEqSortFormer : BEq SortFormer

Equations

• DocGen4.instBEqSortFormer = { beq := DocGen4.instBEqSortFormer.beq }

def DocGen4.instBEqSortFormer.beq : SortFormer → SortFormer → Bool

Equations

• DocGen4.instBEqSortFormer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def DocGen4.instHashableSortFormer.hash : SortFormer → UInt64

Equations

• DocGen4.instHashableSortFormer.hash DocGen4.SortFormer.type = 0
• DocGen4.instHashableSortFormer.hash DocGen4.SortFormer.prop = 1
• DocGen4.instHashableSortFormer.hash DocGen4.SortFormer.sort = 2

@[implicit_reducible]

instance DocGen4.instHashableSortFormer : Hashable SortFormer

Equations

• DocGen4.instHashableSortFormer = { hash := DocGen4.instHashableSortFormer.hash }

def DocGen4.instReprSortFormer.repr : SortFormer → Nat → Std.Format

Equations

• DocGen4.instReprSortFormer.repr DocGen4.SortFormer.type prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DocGen4.SortFormer.type")).group prec✝
• DocGen4.instReprSortFormer.repr DocGen4.SortFormer.prop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DocGen4.SortFormer.prop")).group prec✝
• DocGen4.instReprSortFormer.repr DocGen4.SortFormer.sort prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DocGen4.SortFormer.sort")).group prec✝

@[implicit_reducible]

instance DocGen4.instReprSortFormer : Repr SortFormer

Equations

• DocGen4.instReprSortFormer = { reprPrec := DocGen4.instReprSortFormer.repr }

inductive DocGen4.RenderedCode.Tag : Type

Tags for code elements in rendered code. Used to indicate semantic meaning for HTML rendering (linking, syntax highlighting).

• keyword : Tag
• string : Tag
• const (name : Lean.Name) : Tag
• sort (former : Option SortFormer) : Tag
• otherExpr : Tag

@[implicit_reducible]

instance DocGen4.RenderedCode.instBEqTag : BEq Tag

Equations

• DocGen4.RenderedCode.instBEqTag = { beq := DocGen4.RenderedCode.instBEqTag.beq }

def DocGen4.RenderedCode.instBEqTag.beq : Tag → Tag → Bool

Equations

• DocGen4.RenderedCode.instBEqTag.beq DocGen4.RenderedCode.Tag.keyword DocGen4.RenderedCode.Tag.keyword = true
• DocGen4.RenderedCode.instBEqTag.beq DocGen4.RenderedCode.Tag.string DocGen4.RenderedCode.Tag.string = true
• DocGen4.RenderedCode.instBEqTag.beq (DocGen4.RenderedCode.Tag.const a) (DocGen4.RenderedCode.Tag.const b) = (a == b)
• DocGen4.RenderedCode.instBEqTag.beq (DocGen4.RenderedCode.Tag.sort a) (DocGen4.RenderedCode.Tag.sort b) = (a == b)
• DocGen4.RenderedCode.instBEqTag.beq DocGen4.RenderedCode.Tag.otherExpr DocGen4.RenderedCode.Tag.otherExpr = true
• DocGen4.RenderedCode.instBEqTag.beq x✝¹ x✝ = false

def DocGen4.RenderedCode.instHashableTag.hash : Tag → UInt64

Equations

• DocGen4.RenderedCode.instHashableTag.hash DocGen4.RenderedCode.Tag.keyword = 0
• DocGen4.RenderedCode.instHashableTag.hash DocGen4.RenderedCode.Tag.string = 1
• DocGen4.RenderedCode.instHashableTag.hash (DocGen4.RenderedCode.Tag.const a) = mixHash 2 (hash a)
• DocGen4.RenderedCode.instHashableTag.hash (DocGen4.RenderedCode.Tag.sort a) = mixHash 3 (hash a)
• DocGen4.RenderedCode.instHashableTag.hash DocGen4.RenderedCode.Tag.otherExpr = 4

@[implicit_reducible]

instance DocGen4.RenderedCode.instHashableTag : Hashable Tag

Equations

• DocGen4.RenderedCode.instHashableTag = { hash := DocGen4.RenderedCode.instHashableTag.hash }

@[implicit_reducible]

instance DocGen4.RenderedCode.instReprTag : Repr Tag

Equations

• DocGen4.RenderedCode.instReprTag = { reprPrec := DocGen4.RenderedCode.instReprTag.repr }

def DocGen4.RenderedCode.instReprTag.repr : Tag → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToBinaryTag : SQLite.Blob.ToBinary RenderedCode.Tag

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instFromBinaryTag : SQLite.Blob.FromBinary RenderedCode.Tag

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToBinaryTaggedText_docGen4 {α : Type u_1} [SQLite.Blob.ToBinary α] : SQLite.Blob.ToBinary (Lean.Widget.TaggedText α)

Equations

• DocGen4.instToBinaryTaggedText_docGen4 = { serializer := DocGen4.instToBinaryTaggedText_docGen4.go }

partial def DocGen4.instToBinaryTaggedText_docGen4.go {α : Type u_1} [SQLite.Blob.ToBinary α] : Lean.Widget.TaggedText α → ByteArray → ByteArray

@[implicit_reducible]

instance DocGen4.instFromBinaryTaggedText_docGen4 {α : Type} [SQLite.Blob.FromBinary α] : SQLite.Blob.FromBinary (Lean.Widget.TaggedText α)

Equations

• DocGen4.instFromBinaryTaggedText_docGen4 = { deserializer := DocGen4.instFromBinaryTaggedText_docGen4.go }

partial def DocGen4.instFromBinaryTaggedText_docGen4.go {α : Type} [SQLite.Blob.FromBinary α] : SQLite.Blob.Deserializer (Lean.Widget.TaggedText α)

partial def DocGen4.instHashableTaggedText_docGen4.hash {α✝ : Type u_1} [Hashable α✝] : Lean.Widget.TaggedText α✝ → UInt64

@[implicit_reducible]

instance DocGen4.instHashableTaggedText_docGen4 {α✝ : Type u_1} [Hashable α✝] : Hashable (Lean.Widget.TaggedText α✝)

Equations

• DocGen4.instHashableTaggedText_docGen4 = { hash := DocGen4.instHashableTaggedText_docGen4.hash }

def DocGen4.RenderedCode : Type

A simplified representation of code with semantic tags for rendering. Unlike CodeWithInfos, this only contains the information needed for HTML rendering (links to declarations, syntax highlighting) and can be serialized to/from the database.

Equations

• DocGen4.RenderedCode = Lean.Widget.TaggedText DocGen4.RenderedCode.Tag

@[implicit_reducible]

instance DocGen4.instInhabitedRenderedCode : Inhabited RenderedCode

Equations

• DocGen4.instInhabitedRenderedCode = { default := DocGen4.instInhabitedRenderedCode._aux_1 }

@[implicit_reducible]

instance DocGen4.instBEqRenderedCode : BEq RenderedCode

Equations

• DocGen4.instBEqRenderedCode = { beq := DocGen4.instBEqRenderedCode._aux_1 }

@[implicit_reducible]

instance DocGen4.instReprRenderedCode : Repr RenderedCode

Equations

• DocGen4.instReprRenderedCode = { reprPrec := DocGen4.instReprRenderedCode._aux_1 }

@[implicit_reducible]

instance DocGen4.instToBinaryRenderedCode : SQLite.Blob.ToBinary RenderedCode

Equations

• DocGen4.instToBinaryRenderedCode = { serializer := DocGen4.instToBinaryRenderedCode._aux_1 }

@[implicit_reducible]

instance DocGen4.instFromBinaryRenderedCode : SQLite.Blob.FromBinary RenderedCode

Equations

• DocGen4.instFromBinaryRenderedCode = { deserializer := DocGen4.instFromBinaryRenderedCode._aux_1 }

@[implicit_reducible]

instance DocGen4.instHashableRenderedCode : Hashable RenderedCode

Equations

• DocGen4.instHashableRenderedCode = { hash := DocGen4.instHashableRenderedCode._aux_1 }

def DocGen4.RenderedCode.empty : RenderedCode

Equations

• DocGen4.RenderedCode.empty = Lean.Widget.TaggedText.append #[]

partial def DocGen4.RenderedCode.textLength : RenderedCode → Nat

partial def DocGen4.RenderedCode.pushRight (xs : Array RenderedCode) (x : RenderedCode) : Array RenderedCode

partial def DocGen4.RenderedCode.pushLeft (x : RenderedCode) (xs : Array RenderedCode) : Array RenderedCode

partial def DocGen4.RenderedCode.appendImpl : RenderedCode → RenderedCode → RenderedCode

@[implicit_reducible]

instance DocGen4.instAppendRenderedCode : Append RenderedCode

Equations

• DocGen4.instAppendRenderedCode = { append := DocGen4.RenderedCode.appendImpl }

def DocGen4.splitWhitespaces (s : String) : String × String × String

In Lean syntax declarations the following pattern is quite common:

syntax term " + " term : term

that is, we place spaces around the operator in the middle. When the InfoTree framework provides us with information about what source token corresponds to which identifier it will thus say that " + " corresponds to HAdd.hadd. This is however not the way we want this to be linked, in the HTML only + should be linked, taking care of this is what this function is responsible for.

Equations

• One or more equations did not get rendered due to their size.

partial def DocGen4.renderTagged (doc : Lean.Widget.CodeWithInfos) : RenderedCode

Convert CodeWithInfos (from Lean's pretty printer) to RenderedCode by extracting only the information needed for HTML rendering.