-
Notifications
You must be signed in to change notification settings - Fork 27
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: d3 directed graph component (#82)
* feat: start on d3 digraph component * feat: embedded graph nodes * feat: selection * chore: add deep-equal and bump dependencies * feat: more customization * feat: arrowheads * feat: expression graph demo Co-authored-by: Adam Topaz <github@adamtopaz.com> * feat: demo --------- Co-authored-by: Adam Topaz <github@adamtopaz.com>
- Loading branch information
Showing
12 changed files
with
2,118 additions
and
431 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,117 @@ | ||
import ProofWidgets.Component.Basic | ||
import ProofWidgets.Data.Html | ||
|
||
namespace ProofWidgets.DigraphDisplay | ||
open Lean Server Jsx | ||
|
||
structure Vertex where | ||
/-- Identifier for this vertex. Must be unique. -/ | ||
id : String | ||
/-- The label is drawn at the vertex position. | ||
This must be an SVG element. | ||
Use `<foreignObject>` to draw non-SVG elements. -/ | ||
label : Html := | ||
<circle | ||
r={5} | ||
className="dim" | ||
fill="var(--vscode-editor-background)" | ||
stroke="var(--vscode-editor-foreground)" | ||
strokeWidth={.num 1.5} | ||
/> | ||
/-- Radius of a circle bounding this vertex. | ||
Used to place incident edge endpoints. -/ | ||
radius : Float := 5 | ||
/-- Details are shown below the graph display | ||
after the vertex label has been clicked. -/ | ||
details? : Option Html := none | ||
deriving Inhabited, RpcEncodable | ||
|
||
structure Edge where | ||
/-- Source vertex. Must match the `id` of one of the vertices. -/ | ||
source : String | ||
/-- Target vertex. Must match the `id` of one of the vertices. -/ | ||
target : String | ||
/-- Attributes to set on the SVG `<line>` element representing this edge. -/ | ||
attrs : Json := json% { | ||
className: "dim", | ||
fill: "var(--vscode-editor-foreground)", | ||
stroke: "var(--vscode-editor-foreground)", | ||
strokeWidth: 2 | ||
} | ||
/-- Details are shown below the graph display | ||
after the edge has been clicked. -/ | ||
details? : Option Html := none | ||
deriving Inhabited, RpcEncodable | ||
|
||
structure ForceCenterParams where | ||
x? : Option Float := none | ||
y? : Option Float := none | ||
strength? : Option Float := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceCollideParams where | ||
radius? : Option Float := none | ||
strength? : Option Float := none | ||
iterations? : Option Nat := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceLinkParams where | ||
distance? : Option Float := none | ||
strength? : Option Float := none | ||
iterations? : Option Nat := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceManyBodyParams where | ||
strength? : Option Float := none | ||
theta? : Option Float := none | ||
distanceMin? : Option Float := none | ||
distanceMax? : Option Float := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceXParams where | ||
x? : Option Float := none | ||
strength? : Option Float := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceYParams where | ||
y? : Option Float := none | ||
strength? : Option Float := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure ForceRadialParams where | ||
radius : Float | ||
x? : Option Float := none | ||
y? : Option Float := none | ||
strength? : Option Float := none | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
/-- Settings for the simulation of forces on vertices. | ||
See https://d3js.org/d3-force. -/ | ||
inductive ForceParams where | ||
| center : ForceCenterParams → ForceParams | ||
| collide : ForceCollideParams → ForceParams | ||
| link : ForceLinkParams → ForceParams | ||
| manyBody : ForceManyBodyParams → ForceParams | ||
| x : ForceXParams → ForceParams | ||
| y : ForceYParams → ForceParams | ||
| radial : ForceRadialParams → ForceParams | ||
deriving Inhabited, FromJson, ToJson | ||
|
||
structure Props where | ||
vertices : Array Vertex | ||
edges : Array Edge | ||
/-- Which forces to apply to the vertices. | ||
Most force parameters are optional, using default values if not specified. -/ | ||
forces : Array ForceParams := #[ .link {}, .manyBody {}, .x {}, .y {} ] | ||
/-- Whether to show the details box below the graph. -/ | ||
showDetails : Bool := false | ||
deriving Inhabited, RpcEncodable | ||
|
||
end DigraphDisplay | ||
|
||
/-- Display a directed graph with an interactive force simulation. -/ | ||
@[widget_module] | ||
def DigraphDisplay : Component DigraphDisplay.Props where | ||
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "d3Graph.js" | ||
|
||
end ProofWidgets |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,71 @@ | ||
import ProofWidgets.Component.Digraph | ||
import ProofWidgets.Component.HtmlDisplay | ||
|
||
/-! ## Directed graphs with `DigraphDisplay` -/ | ||
|
||
open ProofWidgets Jsx | ||
|
||
/-! ### Basic usage -/ | ||
|
||
def mkEdge (st : String × String) : DigraphDisplay.Edge := {source := st.1, target := st.2} | ||
|
||
-- Place your cursor here. | ||
#html <DigraphDisplay | ||
vertices={#["a", "b", "c", "d", "e", "f"].map ({id := ·})} | ||
edges={#[("b","c"), ("d","e"), ("e","f"), ("f","d")].map mkEdge} | ||
/> | ||
|
||
/-! ### Custom layout -/ | ||
|
||
def complete (n : Nat) : Array DigraphDisplay.Vertex × Array DigraphDisplay.Edge := Id.run do | ||
let mut verts := #[] | ||
let mut edges := #[] | ||
for i in [:n] do | ||
verts := verts.push {id := toString i} | ||
for j in [:i] do | ||
edges := edges.push {source := toString i, target := toString j} | ||
edges := edges.push {source := toString j, target := toString i} | ||
return (verts, edges) | ||
|
||
def K₁₀ := complete 10 | ||
|
||
#html <DigraphDisplay | ||
vertices={K₁₀.1} | ||
edges={K₁₀.2} | ||
-- Specify forces to control graph layout. | ||
forces={#[ | ||
.link { distance? := some 150 } | ||
]} | ||
/> | ||
|
||
/-! ### Styling -/ | ||
|
||
#html <DigraphDisplay | ||
vertices={#[ | ||
{ id := "a" | ||
-- Arbitrary SVG elements can be used as vertex labels. | ||
label := <circle r={5} fill="#ff0000" /> | ||
}, | ||
{ id := "b" | ||
-- Use `<foreignObject>` to draw non-SVG elements. | ||
label := <foreignObject height={50} width={50}> | ||
-- TODO: the extra `<p>` node messes up positioning | ||
<MarkdownDisplay contents="$xyz$" /> | ||
</foreignObject> | ||
} | ||
]} | ||
edges={#[{ source := "a", target := "b" }]} | ||
/> | ||
|
||
/-! ### Extra details -/ | ||
|
||
#html <DigraphDisplay | ||
vertices={#[ | ||
{ id := "a", details? := Html.text "Vertex a." }, | ||
{ id := "b", details? := <b>Vertex b.</b> } | ||
]} | ||
edges={ #[ { source := "a", target := "b", details? := Html.text "Edge a → b." } ] } | ||
-- Use this to display a details box with extra information | ||
-- about vertices and edges. | ||
showDetails={true} | ||
/> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,81 @@ | ||
import ProofWidgets.Component.Digraph | ||
import ProofWidgets.Component.HtmlDisplay | ||
import Lean.Util.FoldConsts | ||
|
||
open ProofWidgets Jsx | ||
|
||
/-- Display the graph of all constants appearing in a given constant. -/ | ||
syntax (name := exprGraphCmd) "#expr_graph" ident : command | ||
|
||
open Lean Elab Command in | ||
@[command_elab exprGraphCmd] | ||
def elabExprGraphCmd : CommandElab := fun | ||
| stx@`(#expr_graph $i:ident) => runTermElabM fun _ => do | ||
let env ← getEnv | ||
let c ← realizeGlobalConstNoOverloadWithInfo i | ||
let some c := env.find? c | throwError "internal error" | ||
let nodes : NameSet := c.getUsedConstantsAsSet | ||
let mut edges : Std.HashSet (String × String) := {} | ||
for a in nodes do for b in nodes do | ||
let some bb := env.find? b | continue | ||
if bb.getUsedConstantsAsSet.contains a then | ||
edges := edges.insert (toString a, toString b) | ||
let mut nodesWithInfos : Array DigraphDisplay.Vertex := #[] | ||
let mut maxRadius := 10 | ||
for node in nodes.toArray do | ||
let some c := env.find? node | continue | ||
let doc? ← findDocString? env node | ||
let ee ← Lean.Widget.ppExprTagged c.type | ||
let us ← Meta.mkFreshLevelMVarsFor c | ||
let e ← Lean.Widget.ppExprTagged (.const node us) | ||
let node := toString node | ||
let rx := node.length * 3 | ||
maxRadius := Nat.max maxRadius rx | ||
let newNode : DigraphDisplay.Vertex := { | ||
id := node | ||
label := | ||
<g> | ||
<ellipse | ||
fill="var(--vscode-editor-background)" | ||
stroke="var(--vscode-editorHoverWidget-border)" | ||
rx={(rx*2 : Nat)} | ||
ry="10" | ||
/> | ||
<text x={s!"-{rx}"} y="5" className="font-code">{.text node}</text> | ||
</g> | ||
radius := 15 | ||
details? := | ||
match doc? with | ||
| some d => | ||
<div> | ||
<InteractiveCode fmt={e} />{.text " : "}<InteractiveCode fmt={ee} /> | ||
<MarkdownDisplay contents={d} /> | ||
</div> | ||
| none => | ||
<span> | ||
<InteractiveCode fmt={e} />{.text " : "}<InteractiveCode fmt={ee} /> | ||
</span> | ||
} | ||
nodesWithInfos := nodesWithInfos.push newNode | ||
let html : Html := <DigraphDisplay | ||
vertices={nodesWithInfos} | ||
edges={edges.fold (init := #[]) fun acc (a,b) => acc.push {source := a, target := b}} | ||
forces={#[ | ||
.link { distance? := Float.ofNat (maxRadius * 2) }, | ||
.collide { radius? := Float.ofNat maxRadius }, | ||
.x { strength? := some 0.05 }, | ||
.y { strength? := some 0.05 } | ||
]} | ||
/> | ||
Widget.savePanelWidgetInfo | ||
(hash HtmlDisplayPanel.javascript) | ||
(return json% { html : $(← Server.rpcEncode html) }) | ||
stx | ||
| stx => throwError "Unexpected syntax {stx}" | ||
|
||
def a : Nat := 0 | ||
def b : Nat := 1 | ||
def foo (c : Nat) : Nat × Int := (a + b * c, a / b) | ||
|
||
-- Put your cursor here. | ||
#expr_graph foo |
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
Oops, something went wrong.