Catlab.jl icon indicating copy to clipboard operation
Catlab.jl copied to clipboard

Emit imports in @signature, @instance, @syntax macros

Open jpfairbanks opened this issue 6 years ago • 1 comments

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?

jpfairbanks avatar Jan 30 '20 20:01 jpfairbanks

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

jpfairbanks avatar Jun 23 '22 18:06 jpfairbanks