Catlab.jl
Catlab.jl copied to clipboard
Emit imports in @signature, @instance, @syntax macros
These macros create modules that require that you imported the functions like import Catlab.Doctrines: otimes, ⊗, id, braid, dom, codom, compose, mmerge, create, delete, mcopy in order to create new doctrines. This is inconvenient, can the macro emit the imports for us?
We just got bit by this on Decapodes. Its really a problem when we have theory inheritance.
For example making a syntax for the Exterior Calculus requires importing a lot of unicodes.
@theory MetricFreeExtCalc1D₊{Ob,Hom,Space} <: ManifoldCalculus{Ob,Hom,Space} begin
Chain0(X::Space)::Ob
Chain1(X::Space)::Ob
∂₁(X::Space)::Hom(Chain1(X), Chain0(X))
Form0(X::Space)::Ob
Form1(X::Space)::Ob
Form0(X⊔Y) == Form0(X)⊕Form0(Y) ⊣ (X::Space, Y::Space)
Form1(X⊔Y) == Form1(X)⊕Form1(Y) ⊣ (X::Space, Y::Space)
d₀(X::Space)::Hom(Form0(X), Form1(X))
∧₀₀(X::Space)::Hom(Form0(X)⊗Form0(X), Form0(X))
∧₁₀(X::Space)::Hom(Form1(X)⊗Form0(X), Form1(X))
∧₀₁(X::Space)::Hom(Form0(X)⊗Form1(X), Form1(X))
σ(Form0(X),Form0(X)) ⋅ ∧₀₀(X) == ∧₀₀(X) ⊣ (X::Space)
σ(Form0(X),Form1(X)) ⋅ ∧₁₀(X) == ∧₀₁(X) ⊣ (X::Space)
σ(Form1(X),Form0(X)) ⋅ ∧₀₁(X) == ∧₁₀(X) ⊣ (X::Space)
ι₁(X::Space)::Hom(Form1(X)⊗Form1(X), Form0(X))
ℒ₀(X::Space)::Hom(Form1(X)⊗Form0(X), Form0(X))
ℒ₀(X) == (id(Form1(X))⊗d₀(X)) ⋅ ι₁(X) ⊣ (X::Space)
ℒ₁(X::Space)::Hom(Form1(X)⊗Form1(X), Form1(X))
end