source
structure ProofWidgets.Penrose.DiagramProps :
Type

- embeds : Array (String × Html)
- dsl : String
- sty : String
- sub : String
- maxOptSteps : Nat

  Maximum number of optimization steps to take before showing the diagram. Optimization may converge earlier, before taking this many steps.

Instances For

source
def ProofWidgets.Penrose.instInhabitedDiagramProps.default :
DiagramProps
Equations

- ProofWidgets.Penrose.instInhabitedDiagramProps.default = { embeds := default, dsl := default, sty := default, sub := default, maxOptSteps := default }

Instances For

source
instance ProofWidgets.Penrose.instInhabitedDiagramProps :
Inhabited DiagramProps
Equations

- ProofWidgets.Penrose.instInhabitedDiagramProps = { default := ProofWidgets.Penrose.instInhabitedDiagramProps.default }

source
instance ProofWidgets.Penrose.instRpcEncodableDiagramProps :
Lean.Server.RpcEncodable DiagramProps
Equations

- ProofWidgets.Penrose.instRpcEncodableDiagramProps = { rpcEncode := ProofWidgets.Penrose.instRpcEncodableDiagramProps.enc✝, rpcDecode := ProofWidgets.Penrose.instRpcEncodableDiagramProps.dec✝ }

source
def ProofWidgets.Penrose.Diagram :
Component DiagramProps

Displays the given diagram using Penrose. The website contains explanations of how to write domain (`dsl`), style (`sty`), and substance (`sub`) programs.

The diagram may also contain embedded HTML trees which are specified in `embeds`. Each embed is HTML together with the name of an object `x` in the substance program. The object `x` can be of any type but must be assigned an `x.textBox : Rectangle` field in the style program. This rectangle will be replaced with the HTML tree. Its dimensions will be overridden in the style program to match those of the HTML node.

The following additional constants are prepended to the style program:

    theme {
      color foreground
      color tooltipBackground
      color tooltipForeground
      color tooltipBorder
    }

and can be accessed as, for example, `theme.foreground` in the provided `sty` in order to match the editor theme.

Equations

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

Instances For

# `DiagramBuilderM` #

source
structure ProofWidgets.Penrose.DiagramState :
Type

- sub : String

  The Penrose substance program. Note that `embeds` are added lazily at the end.

- embeds : Std.HashMap String (String × Html)

  Components to display as labels in the diagram, stored in the map as name ↦ (type, html).

Instances For

source
@[reducible, inline]
abbrev ProofWidgets.Penrose.DiagramBuilderM (α : Type) :
Type

A monad to easily build Penrose diagrams in.

Equations

- ProofWidgets.Penrose.DiagramBuilderM = StateT ProofWidgets.Penrose.DiagramState Lean.MetaM

Instances For

source
def ProofWidgets.Penrose.DiagramBuilderM.buildDiagram (dsl sty : String) (maxOptSteps : Nat := 500) :
DiagramBuilderM (Option Html)

Assemble the diagram using the provided domain and style programs.

`none` is returned iff nothing was added to the diagram.

Equations

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

Instances For

source
def ProofWidgets.Penrose.DiagramBuilderM.addEmbed (nm tp : String) (h : Html) :
DiagramBuilderM Unit

Add an object `nm` of Penrose type `tp`, labelled by `h`, to the substance program.

Equations

- ProofWidgets.Penrose.DiagramBuilderM.addEmbed nm tp h = modify fun (st : ProofWidgets.Penrose.DiagramState) => { sub := st.sub, embeds := st.embeds.insert nm (tp, h) }

Instances For

source
def ProofWidgets.Penrose.DiagramBuilderM.addExpr (tp : String) (e : Lean.Expr) :
DiagramBuilderM String

Add an object of Penrose type `tp`, corresponding to (and labelled by) the expression `e`, to the substance program. Return its Penrose name.

Equations

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

Instances For

source
def ProofWidgets.Penrose.DiagramBuilderM.addInstruction (i : String) :
DiagramBuilderM Unit

Add an instruction `i` to the substance program.

Equations

- ProofWidgets.Penrose.DiagramBuilderM.addInstruction i = modify fun (st : ProofWidgets.Penrose.DiagramState) => { sub := st.sub ++ (toString i ++ toString "\n"), embeds := st.embeds }

Instances For

source
def ProofWidgets.Penrose.DiagramBuilderM.run {α : Type} (x : DiagramBuilderM α) :
Lean.MetaM α
Equations

- x.run = StateT.run' x { }

Instances For

source
@[reducible, inline]
abbrev ProofWidgets.PenroseDiagramProps :
Type

Abbreviation for backwards-compatibility.

Equations

- ProofWidgets.PenroseDiagramProps = ProofWidgets.Penrose.DiagramProps

Instances For

source
@[reducible, inline]
abbrev ProofWidgets.PenroseDiagram :
Component Penrose.DiagramProps

Abbreviation for backwards-compatibility.

Equations

- ProofWidgets.PenroseDiagram = ProofWidgets.Penrose.Diagram

Instances For