Lean4
/-- Given a 2-morphism, return a string diagram. Otherwise `none`. -/
def stringM? (e : Expr) : MetaM (Option Html) := do
let e ← instantiateMVars e
let k ← mkKind e
let x : Option (List (List Node) × List (List Strand)) ←
(match k with
| .monoidal => do
let some ctx ← BicategoryLike.mkContext? (ρ := Monoidal.Context) e |
return none
CoherenceM.run (ctx := ctx)
(do
let e' := (← BicategoryLike.eval k.name (← MkMor₂.ofExpr e)).expr
return some (← e'.nodes, ← e'.strands))
| .bicategory => do
let some ctx ← BicategoryLike.mkContext? (ρ := Bicategory.Context) e |
return none
CoherenceM.run (ctx := ctx)
(do
let e' := (← BicategoryLike.eval k.name (← MkMor₂.ofExpr e)).expr
return some (← e'.nodes, ← e'.strands))
| .none => return none)
match x with
| none =>
return none
| some (nodes, strands) =>
do
DiagramBuilderM.run
(do
mkStringDiagram nodes strands
trace[string_diagram]"Penrose substance: \n{(← get).sub}"
match ← DiagramBuilderM.buildDiagram dsl sty with
| some html =>
return html
| none =>
return <span>No non-structural morphisms found.</span>)
