diff --git a/ImportGraph.lean b/ImportGraph.lean index 9646dcb..37cfd08 100644 --- a/ImportGraph.lean +++ b/ImportGraph.lean @@ -23,7 +23,9 @@ public import ImportGraph.Shake.DeclNeeds public import ImportGraph.Shake.EnvExtension public import ImportGraph.Shake.Environment public import ImportGraph.Shake.Workspace +public import ImportGraph.Util.Diff 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/Shake/Basic.lean b/ImportGraph/Shake/Basic.lean index f31f12f..cd74b89 100644 --- a/ImportGraph/Shake/Basic.lean +++ b/ImportGraph/Shake/Basic.lean @@ -301,6 +301,9 @@ Rephrasing of `f (n.get k)` for readability. -/ @[inline] def foldWithKind (n : Needs) (f : α → NeedsKind → Bitset → α) (init : α) : α := NeedsKind.all.foldl (init := init) fun a k => n.applyAt k (f a k) +/-- The union of all bitsets in a `Needs`-/ +def flatten (n : Needs) : Bitset := n.fold (· ∪ ·) (init := ∅) + /-- Applies `f` to all component `Bitset`s of the given `Needs`. -/ @[specialize f] def map (n : Needs) (f : Bitset → Bitset) : Needs where pub := f n.pub @@ -429,6 +432,17 @@ instance : ToString NeedsKind where | .privOfPriv => "all" | .metaPrivOfPriv => "meta all" +/-- The prefix to the import command corresponding to the import. If `clarifyPriv` is `true`, +(default `false`), we include "`private`" in front of private imports. This is useful in display +situations, even though it is not a valid form of `import`. -/ +def toImportString (clarifyPriv := false) : NeedsKind → String + | .pub => "public import" + | .metaPub => "public meta import" + | .priv => s!"{if clarifyPriv then "private " else ""}import" + | .metaPriv => s!"{if clarifyPriv then "private " else ""}meta import" + | .privOfPriv => "import all" + | .metaPrivOfPriv => "meta import all" + /-- The `NeedsKind`s which land (directly) in the private scope. -/ @[inline, expose, grind] def toPrivate : Array NeedsKind := #[.priv, .privOfPriv, .metaPriv, .metaPrivOfPriv] @@ -530,4 +544,16 @@ def connecting? (src tgt : Environment.Visibility) (isMeta : Bool := false) : Op | .private, .private => some { isExported := false, isMeta, isAll := true } | .private, .public => none -end ImportGraph.Shake.NeedsKind +end NeedsKind + +namespace Provides + +/-- Intersects each field of two `Provides`. + +Generally, intersection is not meaningful on a bare `Needs`, but is meaningful on a +transitively closed and linearized `Provides`. + +We avoid making this an instance of `Inter` to avoid `a ∩ b` succeeding on `Needs`. -/ +@[inline] def inter (a b : Provides) := a.map₂ b (· ∩ ·) + +end Provides diff --git a/ImportGraph/Util/Diff.lean b/ImportGraph/Util/Diff.lean new file mode 100644 index 0000000..9dcae5f --- /dev/null +++ b/ImportGraph/Util/Diff.lean @@ -0,0 +1,5 @@ +module + +public import ImportGraph.Util.Diff.Basic +public import ImportGraph.Util.Diff.Message +public import ImportGraph.Util.Diff.Shake diff --git a/ImportGraph/Util/Diff/Basic.lean b/ImportGraph/Util/Diff/Basic.lean new file mode 100644 index 0000000..910ac8a --- /dev/null +++ b/ImportGraph/Util/Diff/Basic.lean @@ -0,0 +1,167 @@ +/- +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 + +public section + +open Lean + +namespace ImportGraph + +namespace Diff + +protected class Measurable α where + measure : α → Nat +export Measurable (measure) + +instance : Diff.Measurable Nat := ⟨id⟩ + +open Diff + +/-- If an integer is (strictly) greater than 0, display it with `+`. -/ +def Int.toStringWithSign (i : Int) := if i > 0 then s!"+{i}" else s!"{i}" + +/-- A simple structure with two states, `initial : α` and `final : α`, which models a transition. -/ +structure Transition (α : Type u) where + /-- The state before `final`. -/ + initial : α + /-- The state after `initial`. -/ + final : α +deriving Inhabited, Hashable, BEq, Repr + +namespace Transition + +/-- Apply `f` to both the initial and final state. -/ +@[inline] def map (t : Transition α) (f : α → β) : Transition β where + initial := f t.initial + final := f t.final + +/-- The difference between the measures of the `final` state and `initial` state. -/ +@[inline] def delta (t : Transition α) [Diff.Measurable α] : Int := + (measure t.final : Int) - measure t.initial + +/-- `abbrev` for `Transition Nat`. The result of measuring a `Transition` with +`Transition.measure`. -/ +protected abbrev Measured := Transition Nat + +@[inline] def measure (t : Transition α) [Diff.Measurable α] : Transition.Measured := + t.map Diff.measure + +end Transition + +/-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and +final state. -/ +structure Venn (α : Type u) where + /-- What the final state has gained that was not present in the initial state. -/ + plus : α + /-- What the initial state has lost that is no longer present in the final state. -/ + minus : α + /-- What the initial and final state have in common. -/ + shared : α +deriving Inhabited, Hashable, BEq, Repr + +/-- Convert a `Transition α` into a `Venn β` according to the provided notions of set difference +and interesection. Note that this is slightly more general than using a `VennLike α` instance, as +it allows changing the type to `β` and does not require `isEmpty`. -/ +@[inline] def Transition.toVennBy (t : Transition α) (sdiff : α → α → β) (inter : α → α → β) : + Venn β where + plus := sdiff t.final t.initial + minus := sdiff t.initial t.final + shared := inter t.initial t.final + +/-- Provides the structure necessary to view `α` as "setlike" enough to support `Venn`, namely a +means of taking the set difference, a means of intersection, and a notion of emptiness. This +typeclass is homogeneous, i.e. we assume that `α` itself is sufficient for representing both states +and the differences/shared aspects between them. -/ +class VennLike α where + /-- A "set difference" such that `VennLike.sdiff a b` tells us what `a` has that `b` does not. -/ + protected sdiff : α → α → α + /-- + An "intersection" such that `VennLike.inter a b` tells us what is common to both `a` and `b`. + -/ + protected inter : α → α → α + /-- A notion of emptiness. `VennLike.isEmpty <| VennLike.sdiff a b = true` should imply that, for + the purposes of the Venn diagram, `a` is a "subset" of `b`. (Both directions should indicate + equality.) Likewise, `VennLike.isEmpty <| VennLike.inter a b` should imply that `a` is disjoint + from `b`. -/ + protected isEmpty : α → Bool + +/-- Convert an `initial` and `final` state into their Venn diagram using the type's `VennLike` +instance. -/ +def Transition.toVenn (t : Transition α) [VennLike α] : Venn α := + t.toVennBy VennLike.sdiff VennLike.inter + +namespace Venn + +/-- Apply `f` to each field of `v`. -/ +@[inline] def map (v : Venn α) (f : α → β) : Venn β where + plus := f v.plus + minus := f v.minus + shared := f v.shared + +/-- A `v : Venn α` represents no change iff both `isEmpty v.plus` and `isEmpty v.minus`. -/ +@[inline] def isUnchangedBy (v : Venn α) (isEmpty : α → Bool) := + isEmpty v.plus && isEmpty v.minus + +/-- A `v : Venn α` represents a change of some kind iff `v.plus` is not `isEmpty` or\ +`v.minus` is not `isEmpty`. -/ +@[inline] def isChangedBy (v : Venn α) (isEmpty : α → Bool) := !(v.isUnchangedBy isEmpty) + +/-- If comparable, the relationship `final ≷ initial`, according to the provided notion of +`isEmpty`. + +- `some .gt`: the `Venn` diagram implicitly represents a strict increase +- `some .lt`: the `Venn` diagram implicitly represents a strict decrease +- `some .eq`: no change in state at all +- `none`: incomparable states (some increase, some decrease) -/ +@[inline] def compareBy? (v : Venn α) (isEmpty : α → Bool) : Option Ordering := + match isEmpty v.plus, isEmpty v.minus with + | true, true => some .eq + | true, false => some .lt + | false, true => some .gt + | false, false => none + +/-- The net difference between the implicit initial and final state, collapsing the independent +measurements of `plus` and `minus` together. -/ +@[inline] def delta (v : Venn α) [Diff.Measurable α] : Int := + (Diff.measure v.plus : Int) - Diff.measure v.minus + +/-- A `v : VennMeasure` represents no change iff both `v.plus` and `v.minus` satisfy +`VennLike.isEmpty`. -/ +@[inline] def isUnchanged (v : Venn α) [VennLike α] := + v.isUnchangedBy VennLike.isEmpty + +/-- A `v : VennMeasure` represents a change of some kind iff either `v.plus` is not empty or +`v.minus` is not empty, according to `VennLike.isEmpty`. -/ +@[inline] def isChanged (v : Venn α) [VennLike α] := + !v.isUnchanged + +/-- If comparable, the relationship `final ≷ initial`. + +- `some .gt`: the `Venn` diagram implicitly represents a strict increase +- `some .lt`: the `Venn` diagram implicitly represents a strict decrease +- `some .eq`: no change in state at all +- `none`: incomparable states (some increase, some decrease) + +The presence of a change is determined by `VennLike.isEmpty`. -/ +@[inline] def compare? (v : Venn α) [VennLike α] : Option Ordering := + v.compareBy? VennLike.isEmpty + +/-- Apply `f` to the `shared` field. -/ +@[inline] def modifyShared (v : Venn α) (f : α → α) : Venn α := { v with shared := f v.shared } + +/-- Removes `ignored` from the `shared` field, according to `VennLike.sdiff`. This is useful when we want to ignore "obvious" common factors. -/ +def ignoreShared (ignored : α) (v : Venn α) [VennLike α] : Venn α := + v.modifyShared (VennLike.sdiff · ignored) + +/-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state +and final state. Abbrev for `Venn Nat`. -/ +protected abbrev Measured := Venn Nat + +@[inline] def measure (t : Venn α) [Diff.Measurable α] : Venn.Measured := + t.map Diff.measure + +end Diff.Venn diff --git a/ImportGraph/Util/Diff/Message.lean b/ImportGraph/Util/Diff/Message.lean new file mode 100644 index 0000000..7229e9a --- /dev/null +++ b/ImportGraph/Util/Diff/Message.lean @@ -0,0 +1,35 @@ +module + +public import ImportGraph.Util.Diff.Basic +public import ImportGraph.Util.TableMessage + +public section + +namespace ImportGraph.Diff + +open ImportGraph.Diff + +namespace Transition + +/-- A header row for a table consisting of rows created by `Transition.toRow`. -/ +def header : Table.Row 4 := #v["", "Δ", "new", "old"] + +def toRow (rowHeader : String) (t : Transition α) [Diff.Measurable α] : Table.Row 4 := + #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"] + +end Transition + +namespace Venn + +/-- A header row for a table consisting of rows created by `Venn.toRow`. -/ +def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"] + +/-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/ +def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[ + rowHeader, + t.delta.toStringWithSign, + s!"+{Diff.measure t.plus}", + s!"-{Diff.measure t.minus}", + s!"{Diff.measure t.shared}"] + +end Venn diff --git a/ImportGraph/Util/Diff/Shake.lean b/ImportGraph/Util/Diff/Shake.lean new file mode 100644 index 0000000..e3a829f --- /dev/null +++ b/ImportGraph/Util/Diff/Shake.lean @@ -0,0 +1,37 @@ +/- +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 + +public import ImportGraph.Util.Diff.Basic +public import ImportGraph.Shake.Algebra + +public section + +namespace ImportGraph.Diff + +open ImportGraph Diff Shake + +instance : Diff.Measurable Bitset where + measure := (·.size) + +instance : VennLike Bitset where + sdiff := (· \ ·) + inter := (· ∩ ·) + isEmpty := (·.isEmpty) + +/-- Measures the Venn diagram of `Bitset`s at the given `NeedsKind`. -/ +def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : Venn.Measured := + needs.map (·.get k |>.size) + +instance : Diff.Measurable Provides where + measure := (·.flatten.size) + +instance : VennLike Provides where + -- avoid linearizing to capture one `Provides` providing public while the other provides public + sdiff := (· \ ·) + -- `a` and `b` should be linearized already and remain linearized under intersection + inter := Provides.inter + isEmpty := (·.isEmpty) 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}"