Tensor trees to dot files

Dot files are used by graphviz to create visualizations of graphs. Here we define a function that converts a tensor tree into a dot file.

def TensorTree.dotString {S : TensorSpecies} (m nt : ℕ) {n : ℕ} {c : Fin n → S.C} : TensorTree S c → String

Turns a nodes of tensor trees into nodes and edges of a dot file.

Equations

• One or more equations did not get rendered due to their size.
• TensorTree.dotString m nt (TensorTree.tensorNode T) = " node" ++ toString m ++ " [label=\"T" ++ toString nt ++ "\"];\n"

def TensorTree.dot {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) : String

Used to form a dot graph from a tensor tree. use e.g. #tensor_dot {T4 | i j l d ⊗ T5 | i j k a b}ᵀ.dot. Dot files can be viewed by copying and pasting into: https://dreampuf.github.io/GraphvizOnline.

Equations

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

def TensorTree.tensorDot : Lean.ParserDescr

Syntax for showing the dot file associated with a tensor tree. Use as #tensor_dot {T4 | i j l d ⊗ T5 | i j k a b}ᵀ.dot.

Equations

• TensorTree.tensorDot = Lean.ParserDescr.node `TensorTree.tensorDot 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#tensor_dot ") (Lean.ParserDescr.cat `term 0))

unsafe def TensorTree.dotElab (term : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Adapted from Lean.Elab.Command.elabReduce in file copyright Microsoft Corporation.

Equations

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

unsafe def TensorTree.elabTensorDot : Lean.Elab.Command.CommandElab

Elaborator for the syntax tensorDot.

Equations

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