Repository: AlgebraicJulia/Catlab.jl
Pull request #189 (2020-07-08 11:02:47)

Dependent Presentations


Patch:
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 80c02d41d..03eaa6060 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -7,7 +7,7 @@ export AbstractCSet, CSet, CSetType, nparts, subpart, incident,
 using LabelledArrays, StaticArrays
 
 using ...Present
-using ...Theories: Category, FreeCategory, dom, codom
+using ...Theories: Category, dom, codom
 
 # C-sets
 ########
diff --git a/src/categorical_algebra/Graphs.jl b/src/categorical_algebra/Graphs.jl
index 17a25fd77..3410f86a2 100644
--- a/src/categorical_algebra/Graphs.jl
+++ b/src/categorical_algebra/Graphs.jl
@@ -17,7 +17,7 @@ import LightGraphs: nv, ne, src, dst, edges, vertices, has_edge, has_vertex,
   neighbors, inneighbors, outneighbors, all_neighbors
 
 using ...Present
-using ...Theories: Category, FreeCategory, dom, codom, compose, id
+using ...Theories: FreeCategory
 using ..CSets
 
 # Graphs
@@ -72,11 +72,7 @@ all_neighbors(g::AbstractGraph, v::Int) =
 # Symmetric graphs
 ##################
 
-@present TheorySymmetricGraph(FreeCategory) begin
-  V::Ob
-  E::Ob
-  src::Hom(E,V)
-  tgt::Hom(E,V)
+@present TheorySymmetricGraph <: TheoryGraph begin
   inv::Hom(E,E)
 
   compose(inv,inv) == id(E)
@@ -119,13 +115,8 @@ Concrete types are [`PropertyGraph`](@ref) and [`SymmetricPropertyGraph`](@ref).
 """
 abstract type AbstractPropertyGraph{T} end
 
-@present TheoryPropertyGraph(FreeCategory) begin
-  V::Ob
-  E::Ob
+@present TheoryPropertyGraph <: TheoryGraph begin
   Props::Ob
-
-  src::Hom(E,V)
-  tgt::Hom(E,V)
   vprops::Hom(V,Props)
   eprops::Hom(E,Props)
 end
@@ -153,20 +144,11 @@ PropertyGraph{T,G}() where {T,G<:_AbstractPropertyGraph} =
                 Dict{Symbol,T}())
 PropertyGraph{T}() where T = PropertyGraph{T,_PropertyGraph}()
 
-@present TheorySymmetricPropertyGraph(FreeCategory) begin
-  V::Ob
-  E::Ob
+@present TheorySymmetricPropertyGraph <: TheorySymmetricGraph begin
   Props::Ob
-
-  src::Hom(E,V)
-  tgt::Hom(E,V)
-  inv::Hom(E,E)
   vprops::Hom(V,Props)
   eprops::Hom(E,Props)
 
-  compose(inv,inv) == id(E)
-  compose(inv,src) == tgt
-  compose(inv,tgt) == src
   compose(inv,eprops) == eprops # Edge involution preserves edge properties.
 end
 
diff --git a/src/core/Present.jl b/src/core/Present.jl
index 5a50adf03..12f2a78c1 100644
--- a/src/core/Present.jl
+++ b/src/core/Present.jl
@@ -27,18 +27,23 @@ struct Presentation{Theory,Name}
   generators::NamedTuple
   generator_name_index::Dict{Name,Pair{Symbol,Int}}
   equations::Vector{Pair}
-  
-  function Presentation{Name}(syntax::Module) where Name
-    Theory = syntax.theory()
-    theory = GAT.theory(Theory)
-    names = Tuple(type.name for type in theory.types)
-    vectors = ((getfield(syntax, name){:generator})[] for name in names)
-    new{Theory,Name}(syntax, NamedTuple{names}(vectors),
-                     Dict{Name,Pair{Symbol,Int}}(), Pair[])
-  end
+end
+
+function Presentation{Name}(syntax::Module) where Name
+  Theory = syntax.theory()
+  theory = GAT.theory(Theory)
+  names = Tuple(type.name for type in theory.types)
+  vectors = ((getfield(syntax, name){:generator})[] for name in names)
+  Presentation{Theory,Name}(syntax, NamedTuple{names}(vectors),
+                            Dict{Name,Pair{Symbol,Int}}(), Pair[])
 end
 Presentation(syntax::Module) = Presentation{Symbol}(syntax)
 
+function Base.copy(pres::Presentation{T,Name}) where {T,Name}
+  Presentation{T,Name}(pres.syntax, map(copy, pres.generators),
+                       copy(pres.generator_name_index), copy(pres.equations))
+end
+
 # Presentation
 ##############
 
@@ -109,23 +114,24 @@ end
 """ Define a presentation using a convenient syntax.
 """
 macro present(head, body)
-  name, syntax_name = @match head begin
-    Expr(:call, [name::Symbol, arg::Symbol]) => (name, arg)
+  name, pres = @match head begin
+    Expr(:call, [name::Symbol, syntax_name::Symbol]) =>
+      (name, :($(module_ref(:Presentation))($syntax_name)))
+    Expr(:(<:), [name::Symbol, parent::Symbol]) => (name, :(copy($parent)))
     _ => throw(ParseError("Ill-formed presentation header $head"))
   end
-  let_expr = Expr(:let, Expr(:block), translate_presentation(syntax_name, body))
+  let_expr = Expr(:let, Expr(:block), translate_presentation(pres, body))
   esc(Expr(:(=), name, let_expr))
 end
 
 """ Translate a presentation in the DSL to a block of Julia code.
 """
-function translate_presentation(syntax_name::Symbol, body::Expr)::Expr
+function translate_presentation(pres::Expr0, body::Expr)::Expr
   @assert body.head == :block
   code = Expr(:block)
-  append_expr!(code,
-    :(_presentation = $(module_ref(:Presentation))($syntax_name)))
+  append_expr!(code, :(_presentation = $pres))
   for expr in strip_lines(body).args
-    append_expr!(code, translate_expr(syntax_name, expr))
+    append_expr!(code, translate_statement(expr))
   end
   append_expr!(code, :(_presentation))
   code
@@ -133,15 +139,14 @@ end
 
 """ Translate a single statement in the presentation DSL to Julia code.
 """
-function translate_expr(syntax_name::Symbol, expr::Expr)::Expr
+function translate_statement(expr::Expr)::Expr
   @match expr begin
     Expr(:(::), [name::Symbol, type_expr]) =>
-      translate_generator(syntax_name, name, type_expr)
+      translate_generator(name, type_expr)
     Expr(:(::), [type_expr]) =>
-      translate_generator(syntax_name, nothing, type_expr)
+      translate_generator(nothing, type_expr)
     Expr(:(:=), [name::Symbol, def_expr]) =>
       translate_definition(name, def_expr)
-    Expr(:(=), _) => expr
     Expr(:call, [:(==), lhs, rhs]) => translate_equation(lhs, rhs)
     _ => throw(ParseError("Ill-formed presentation statement $expr"))
   end
@@ -149,40 +154,43 @@ end
 
 """ Translate declaration of a generator.
 """
-function translate_generator(syntax_name::Symbol, name::Union{Symbol,Nothing},
-                             type_expr)::Expr
-  function rewrite(expr)
-    @match expr begin
-      Expr(:call, [name::Symbol, args...]) =>
-        Expr(:call, GlobalRef(Syntax, :invoke_term), syntax_name,
-             QuoteNode(name), map(rewrite, args)...)
-      _ => expr
-    end
-  end
+function translate_generator(name::Union{Symbol,Nothing}, type_expr)::Expr
   type_name, args = @match type_expr begin
     name::Symbol => (name, [])
     Expr(:call, [name::Symbol, args...]) => (name, args)
     _ => throw(ParseError("Ill-formed type expression $type_expr"))
   end
-  call_expr = Expr(
-    :call, module_ref(:add_generator!), :_presentation,
-    rewrite(Expr(:call, type_name,
-                 isnothing(name) ? :nothing : QuoteNode(name), args...)))
-  isnothing(name) ? call_expr : :($(name) = $call_expr)
+  gen_expr = Expr(:call, type_name,
+                  isnothing(name) ? :nothing : QuoteNode(name), args...)
+  Expr(:call, module_ref(:add_generator!), :_presentation,
+       translate_expr(gen_expr))
 end
 
 """ Translate definition of generator in terms of other generators.
 """
 function translate_definition(name::Symbol, def_expr)::Expr
-  call_expr = Expr(:call, module_ref(:add_definition!), :_presentation,
-                   QuoteNode(name), def_expr)
-  :($name = $call_expr)
+  Expr(:call, module_ref(:add_definition!), :_presentation,
+       QuoteNode(name), translate_expr(def_expr))
 end
 
 """ Translate declaration of equality between terms.
 """
 function translate_equation(lhs, rhs)::Expr
-  Expr(:call, module_ref(:add_equation!), :_presentation, lhs, rhs)
+  Expr(:call, module_ref(:add_equation!), :_presentation,
+       translate_expr(lhs), translate_expr(rhs))
+end
+
+""" Translate GAT expression appearing in presentation.
+"""
+function translate_expr(expr)
+  @match expr begin
+    Expr(:call, [name::Symbol, args...]) =>
+      Expr(:call, GlobalRef(Syntax, :invoke_term), :(_presentation.syntax),
+           QuoteNode(name), map(translate_expr, args)...)
+    name::Symbol =>
+      Expr(:call, module_ref(:generator), :_presentation, QuoteNode(name))
+    _ => expr
+  end
 end
 
 module_ref(sym::Symbol) = GlobalRef(Present, sym)


Test patch:
diff --git a/test/categorical_algebra/CSets.jl b/test/categorical_algebra/CSets.jl
index 116385852..85a7e2060 100644
--- a/test/categorical_algebra/CSets.jl
+++ b/test/categorical_algebra/CSets.jl
@@ -2,7 +2,7 @@ module TestCSets
 using Test
 
 using Catlab: @present
-using Catlab.Theories: Category, FreeCategory
+using Catlab.Theories: FreeCategory
 using Catlab.CategoricalAlgebra.CSets
 
 # Discrete dynamical systems
diff --git a/test/core/Present.jl b/test/core/Present.jl
index 017c55058..1dfde87a6 100644
--- a/test/core/Present.jl
+++ b/test/core/Present.jl
@@ -50,11 +50,8 @@ add_generators!(pres, (f,g))
   second_level_manager := compose(manager, manager)
   third_level_manager := compose(manager, manager, manager)
   
-  # Abbreviations (no syntactic term for LHS).
-  boss = manager
-  
   # Managers work in the same department as their employees.
-  compose(boss, works_in) == works_in
+  compose(manager, works_in) == works_in
   # The secretary of a department works in that department.
   compose(secretary, works_in) == id(Department)
 end
@@ -100,6 +97,18 @@ I = munit(FreeSymmetricMonoidalCategory.Ob)
 @test generator(C, :f) == Hom(:f, otimes(A,B), otimes(B,A))
 @test generator(C, :scalar) == Hom(:scalar, I, I)
 
+# Inheritance.
+@present TheorySet(FreeCategory) begin
+  X::Ob
+end
+@present TheoryDDS <: TheorySet begin
+  Φ::Hom(X,X)
+end
+X = Ob(FreeCategory, :X)
+Φ = Hom(:Φ, X, X)
+@test generators(TheoryDDS, :Ob) == [X]
+@test generators(TheoryDDS, :Hom) == [Φ]
+
 # Serialization
 ###############