Basic definitions

Layout

ink

structure Layout : Type

• fst : String
• rst : List String

Layout definition. We encode it as a pair of String and List String so that the layout always has at least one line (Section 3.1)

ink

def Layout.max_with_offset : ℕ → Layout → ℕ

Equations

• Layout.max_with_offset x x = match x, x with | col_pos, { fst := fst, rst := rst } => max (col_pos + String.length fst) (List.foldl max 0 (List.map String.length rst))

Document

ink

inductive Doc : Type

• text: String → Doc
• nl: Doc
• concat: Doc → Doc → Doc
• nest: ℕ → Doc → Doc
• align: Doc → Doc
• choice: Doc → Doc → Doc

Document definition (syntax of $\Sigma_e$, Figure 4)

ink

def Doc.size : Doc → ℕ

Equations

• Doc.size (Doc.text s) = 1
• Doc.size Doc.nl = 1
• Doc.size (Doc.concat d₁ d₂) = Doc.size d₁ + Doc.size d₂ + 1
• Doc.size (Doc.nest n d) = Doc.size d + 1
• Doc.size (Doc.align d) = Doc.size d + 1
• Doc.size (Doc.choice d₁ d₂) = Doc.size d₁ + Doc.size d₂ + 1

ink

inductive Choiceless : Doc → Prop

• text: ∀ (s : String), Choiceless (Doc.text s)
• nl: Choiceless Doc.nl
• concat: ∀ (d₁ d₂ : Doc), Choiceless d₁ → Choiceless d₂ → Choiceless (Doc.concat d₁ d₂)
• nest: ∀ (n : ℕ) (d : Doc), Choiceless d → Choiceless (Doc.nest n d)
• align: ∀ (d : Doc), Choiceless d → Choiceless (Doc.align d)

Choiceless document definition (Section 3.2) We make it a predicate of Doc, since it's a subset of Doc.

Rendering and widening

ink

inductive Render : Doc → ℕ → ℕ → Layout → Prop

• text: ∀ {s : String} {c i : ℕ}, Render (Doc.text s) c i { fst := s, rst := [] }
• nl: ∀ {c i : ℕ}, Render Doc.nl c i { fst := "", rst := [List.asString (List.replicate i (Char.ofNat 32))] }
• concat_one: ∀ {d₁ : Doc} {c i : ℕ} {s : String} {d₂ : Doc} {t : String} {ts : List String}, Render d₁ c i { fst := s, rst := [] } → Render d₂ (c + String.length s) i { fst := t, rst := ts } → Render (Doc.concat d₁ d₂) c i { fst := s ++ t, rst := ts }
• concat_multi: ∀ {ss : List String} {slast : String} {d₁ : Doc} {c i : ℕ} {s : String} {d₂ : Doc} {t : String} {ts : List String} (h_non_empty : ss ≠ []), slast = List.getLast ss h_non_empty → Render d₁ c i { fst := s, rst := ss } → Render d₂ (String.length slast) i { fst := t, rst := ts } → Render (Doc.concat d₁ d₂) c i { fst := s, rst := List.dropLast ss ++ [slast ++ t] ++ ts }
• nest: ∀ {d : Doc} {c i n : ℕ} {L : Layout}, Render d c (i + n) L → Render (Doc.nest n d) c i L
• align: ∀ {d : Doc} {c : ℕ} {L : Layout} {i : ℕ}, Render d c c L → Render (Doc.align d) c i L

Rendering relation definition ($⇓_\mathcal{R}$, Figure 6)

ink

inductive Widen : Doc → List Doc → Prop

• text: ∀ (s : String), Widen (Doc.text s) [Doc.text s]
• nl: Widen Doc.nl [Doc.nl]
• concat: ∀ {d₁ : Doc} {L₁ : List Doc} {d₂ : Doc} {L₂ : List Doc}, Widen d₁ L₁ → Widen d₂ L₂ → Widen (Doc.concat d₁ d₂) (List.join (List.map (fun d₁ => List.map (fun d₂ => Doc.concat d₁ d₂) L₂) L₁))
• nest: ∀ {d : Doc} {L : List Doc} {n : ℕ}, Widen d L → Widen (Doc.nest n d) (List.map (fun d => Doc.nest n d) L)
• align: ∀ {d : Doc} {L : List Doc}, Widen d L → Widen (Doc.align d) (List.map (fun d => Doc.align d) L)
• choice: ∀ {d₁ : Doc} {L₁ : List Doc} {d₂ : Doc} {L₂ : List Doc}, Widen d₁ L₁ → Widen d₂ L₂ → Widen (Doc.choice d₁ d₂) (L₁ ++ L₂)

Widening relation definition ($⇓_\mathcal{W}$, Figure 6)

Measure

ink

structure Meas {α : Type} : Type

• last : ℕ
• cost : α
• doc : Doc
• x : ℕ
• y : ℕ

Measure definition (Figure 10)

Various measure operations (Figure 10)

ink

def Meas.adjust_align {α : Type} (i : ℕ) : Meas → Meas

• adjustAlign;

Equations

• Meas.adjust_align i x = match x with | { last := last, cost := cost, doc := doc, x := x, y := y } => { last := last, cost := cost, doc := Doc.align doc, x := x, y := max i y }

ink

def Meas.adjust_nest {α : Type} (n : ℕ) : Meas → Meas

• adjustNest;

Equations

• Meas.adjust_nest n x = match x with | { last := last, cost := cost, doc := doc, x := x, y := y } => { last := last, cost := cost, doc := Doc.nest n doc, x := x, y := y }

ink

def Meas.concat {α : Type} (F : Factory α) : Meas → Meas → Meas

• concatenation (∘); and

Equations

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

ink

def dominates {α : Type} (F : Factory α) (m₁ : Meas) (m₂ : Meas) : Bool

• domination (≼)

Equations

• dominates F m₁ m₂ = decide (m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true)

Measure computation/rendering

ink

inductive MeasRender {α : Type} (F : Factory α) : Doc → ℕ → ℕ → Meas → Prop

• text: ∀ {α : Type} {F : Factory α} {c i : ℕ} (s : String), MeasRender F (Doc.text s) c i { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s, x := c + String.length s, y := i }
• nl: ∀ {α : Type} {F : Factory α} {c i : ℕ}, MeasRender F Doc.nl c i { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }
• concat: ∀ {α : Type} {F : Factory α} {d₁ : Doc} {c i : ℕ} {m₁ : Meas} {d₂ : Doc} {m₂ m : Meas}, MeasRender F d₁ c i m₁ → MeasRender F d₂ m₁.last i m₂ → m = Meas.concat F m₁ m₂ → MeasRender F (Doc.concat d₁ d₂) c i m
• nest: ∀ {α : Type} {F : Factory α} {d : Doc} {c i n last : ℕ} {cost : α} {x y : ℕ}, MeasRender F d c (i + n) { last := last, cost := cost, doc := d, x := x, y := y } → MeasRender F (Doc.nest n d) c i { last := last, cost := cost, doc := Doc.nest n d, x := x, y := y }
• align: ∀ {α : Type} {F : Factory α} {d : Doc} {c last : ℕ} {cost : α} {x y i : ℕ}, MeasRender F d c c { last := last, cost := cost, doc := d, x := x, y := y } → MeasRender F (Doc.align d) c i { last := last, cost := cost, doc := Doc.align d, x := x, y := max i y }

Measure computation/rendering definition (Figure 11)

Pareto frontier

ink

def cost_increasing {α : Type} (F : Factory α) (ms : List Meas) : Prop

A list of measures is strictly increasing in cost

Equations

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

ink

def cost_increasing_non_strict {α : Type} (F : Factory α) (ms : List Meas) : Prop

A list of measures is (non-strictly) increasing in cost

Equations

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

ink

def last_decreasing {α : Type} (ms : List Meas) : Prop

A list of measures is strictly decreasing in length of last line

Equations

• last_decreasing ms = ∀ (i : ℕ) (hi : i < List.length ms) (hj : i + 1 < List.length ms), (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

ink

def pareto {α : Type} (F : Factory α) (ms : List Meas) : Prop

A predicate that a list of measures form a Pareto frontier (Section 5.4) This definition is not the same as the definition described in the paper, which is based on non-domination. However, they are equivalent, proven at pareto_nondom_iff_pareto in Pretty.Claims.Pareto.

Equations

• pareto F ms = (last_decreasing ms ∧ cost_increasing F ms)

Various list of measures operations (Figure 12)

ink

def dedup {α : Type} (F : Factory α) : List Meas → List Meas

• dedup;

Equations

• dedup F [] = []
• dedup F [m] = [m]
• dedup F (m₁ :: m₂ :: ms) = if Factory.le F m₂.cost m₁.cost = true then dedup F (m₂ :: ms) else m₁ :: dedup F (m₂ :: ms)

ink

def merge {α : Type} (F : Factory α) : List Meas × List Meas → List Meas

• merge (⊎);

Equations

• One or more equations did not get rendered due to their size.
• merge F ([], ms) = ms
• merge F (ms, []) = ms

Measure set

ink

inductive MeasureSet {α : Type} : Type

• tainted: {α : Type} → Meas → MeasureSet
• set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet

Measure set definition (Figure 12). Unlike the definition in the paper, we carry the proof that ms is non-empty instead of relying on the implicit non-empty assumption everywhere.