diff --git a/ImportGraph.lean b/ImportGraph.lean index 9646dcb..0ba9185 100644 --- a/ImportGraph.lean +++ b/ImportGraph.lean @@ -24,6 +24,7 @@ public import ImportGraph.Shake.EnvExtension public import ImportGraph.Shake.Environment public import ImportGraph.Shake.Workspace public import ImportGraph.Util.FindSorry +public import ImportGraph.Util.TableMessage public import ImportGraph.WorkspaceModel.Base public import ImportGraph.WorkspaceModel.Build public import ImportGraph.WorkspaceModel.Model diff --git a/ImportGraph/Util/TableMessage.lean b/ImportGraph/Util/TableMessage.lean new file mode 100644 index 0000000..2d6de22 --- /dev/null +++ b/ImportGraph/Util/TableMessage.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + + +import Lean.Elab.Command + +/-! +# Formatting tables + +This module provides basic utilities for formatting tables with aligned columns. +For now, we only supports tables of strings. + +## Future work + +- Specifying dividers and borders, padding characters, right/left alignment, column widths + - Ideally this is granular, e.g. per cell/row/column +- Composing and stacking tables +- Widget version using HTML tables to avoid awkward reflowing + allow `MessageData` +-/ + +namespace ImportGraph + +open ImportGraph + +public section + +/-- Pad a string on the right with `c : Char` (by default `' '`), until it reaches length `n`. Does +not trim strings already over length `n` down to length `n`. -/ +@[inline] def String.rightPad (n : Nat) (s : String) (char : Char := ' ') := + s.pushn char (n - s.positions.length) + +/-- Pad a string on the left with `c : Char` (by default `' '`), until it reaches length `n`. Does +not trim strings already over length `n` down to length `n`. -/ +@[inline] def String.leftPad (n : Nat) (s : String) (char : Char := ' ') := + "".pushn char (n - s.positions.length) ++ s + +namespace Table + +/-- A row with a fixed number of elements in a table such as `Array (Table.Row 5)`. (The `String`s +in a `Row` are allowed to have any length.) -/ +protected abbrev Row (n : Nat) := Vector String n + +/-- Given an array of table rows, arranges them in a table. Each cell is left-aligned, and +separated from the next cell in the row by a space. Spaces at the end of each row are trimmed. -/ +protected def formatSimple (rows : Array (Table.Row n)) : String := Id.run do + if h : rows.size > 0 then + let mut colWidths := rows[0].map (·.positions.length) + for h : i in 1...rows.size do + colWidths := colWidths.zipWith (max · ·.positions.length) rows[i] + let mut table := "" + for hRow : rowIdx in 0...rows.size do + for hCol : i in 0...n do + if h : i + 1 < n then + table := table ++ rows[rowIdx][i].rightPad colWidths[i] |>.push ' ' + else + -- The last column needs neither padding nor a `' '` separator + -- However, it may still have spaces (e.g. empty cell) so trim them; do not drop `'\n'`. + table := table ++ rows[rowIdx][i] |>.dropEndWhile (· = ' ') |>.copy + unless rowIdx + 1 == rows.size do + table := table.push '\n' + return table + else return "" + +/-- An empty row in a table. -/ +def emptyRow {n} : Table.Row n := Vector.replicate n "" + +/-- Increase the size of a row by padding it on the right with empty cells. -/ +def Row.rightPad (row : Table.Row n) (h : n ≤ m := by grind) : Table.Row m := + (show max m n = m by grind) ▸ row.rightpad m "" diff --git a/ImportGraphTest.lean b/ImportGraphTest.lean index 05604b5..513b04f 100644 --- a/ImportGraphTest.lean +++ b/ImportGraphTest.lean @@ -22,6 +22,7 @@ import ImportGraphTest.NormImports import ImportGraphTest.NoLakeAxioms import ImportGraphTest.Shake.Algebra import ImportGraphTest.Shake.Workspace +import ImportGraphTest.TableMessage import ImportGraphTest.ToTarget import ImportGraphTest.Unused import ImportGraphTest.Used diff --git a/ImportGraphTest/Shake/Algebra.lean b/ImportGraphTest/Shake/Algebra.lean index 0117a0b..6931e1a 100644 --- a/ImportGraphTest/Shake/Algebra.lean +++ b/ImportGraphTest/Shake/Algebra.lean @@ -7,6 +7,7 @@ module public meta import ImportGraph.Shake.Algebra public meta import Lean.Elab.Command +public meta import ImportGraph.Util.TableMessage /-! # Tests for the import hierarchy algebra @@ -35,26 +36,26 @@ def NeedsKind.allPairs : Array (NeedsKind × NeedsKind) := def pad (n : Nat) (s : String) : String := s ++ "".pushn ' ' (n - s.length) /-- The composition table of `NeedsKind.andThen`, with the first factor on the left. -/ -meta def compositionTable : String := - let row (cells : List String) := (String.join <| cells.map (pad 7)).trimAsciiEnd.toString +meta def compositionTable : String := Id.run do -- push meta to the end instead of `all` for a cleaner table - let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta) |>.toList - "\n".intercalate <| - row ("(↓) ≫ (→) " :: ks.map shortName) :: - ks.map fun k₁ => - row <| pad 10 (shortName k₁) :: ks.map fun k₂ => - if h : k₁.target = k₂.source then shortName (andThen k₁ k₂) else "-" + let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta) + let mut rows : Array (Table.Row (1 + ks.size)) := + #[#v["(↓) ≫ (→)"] ++ ks.toVector.map shortName] + rows := rows ++ ks.map fun k₁ => + #v[shortName k₁] ++ (ks.toVector.map fun k₂ => + if h : k₁.target = k₂.source then shortName (k₁.andThen k₂) else "-") + Table.formatSimple rows /-- info: -(↓) ≫ (→) pub priv all 𝓶pub 𝓶priv 𝓶all -pub pub priv - 𝓶pub 𝓶priv - -priv - - priv - - 𝓶priv -all - - all - - 𝓶all -𝓶pub 𝓶pub 𝓶priv - 𝓶pub 𝓶priv - -𝓶priv - - 𝓶priv - - 𝓶priv -𝓶all - - 𝓶all - - 𝓶all +(↓) ≫ (→) pub priv all 𝓶pub 𝓶priv 𝓶all +pub pub priv - 𝓶pub 𝓶priv - +priv - - priv - - 𝓶priv +all - - all - - 𝓶all +𝓶pub 𝓶pub 𝓶priv - 𝓶pub 𝓶priv - +𝓶priv - - 𝓶priv - - 𝓶priv +𝓶all - - 𝓶all - - 𝓶all -/ #guard_msgs in #eval IO.println s!"\n\n{compositionTable}" @@ -165,7 +166,7 @@ protected def Needs.randM (hierarchySize : Nat) -- TODO: should maybe choose randomly how many are in each "layer"? /-- A topologically sorted array of needs, i.e. one in which each `Needs` only refers to prior -ones. If the config is `none`, it's randomized each time. This allows for more module-tomodule +ones. If the config is `none`, it's randomized each time. This allows for more module-to-module variation in quality, perhaps more like a real repo. -/ def Needs.randArrayM (hierarchySize : Nat) (cfg? : Option RandNeedsConfig := none) : diff --git a/ImportGraphTest/TableMessage.lean b/ImportGraphTest/TableMessage.lean new file mode 100644 index 0000000..16dc1e1 --- /dev/null +++ b/ImportGraphTest/TableMessage.lean @@ -0,0 +1,33 @@ +module + +public meta import ImportGraph.Util.TableMessage + +import Lean.Elab.Command + +open ImportGraph + +/-- +info: Table: + + header1 h2 header3! h₄ +row₁: item1 foo bar baz +row₂: item₂ foo₂ bar₂ baz₂ + +row₃: 1 2 (long item 3) 4 +shortrow: a₁ a₂ +finalrow: 0 1 1 0 +-/ +#guard_msgs in +run_cmd do + let mut rows : Array (Table.Row 5) := #[] + rows := rows.push #v["", "header1", "h2", "header3!", "h₄"] + let shortRow : Table.Row 3 := #v["shortrow:", "a₁", "a₂"] + rows := rows ++ #[ + #v["row₁:", "item1", "foo", "bar", "baz"], + #v["row₂:", "item₂", "foo₂", "bar₂", "baz₂"], + Table.emptyRow, + #v["row₃:", "1", "2", "(long item 3)", "4"], + shortRow.rightPad, + #v["finalrow:", "0", "1", "1", "0"] + ] + Lean.logInfo m!"Table:\n\n{Table.formatSimple rows}"