Integrate homomorphism search with @migration #160
Description
The @acset_colim macro is a beloved method of constructing individual ACSets. But, when people try to create rewrite rules, they need to specify a whole diagram of ACSets. After constructing the objects, they have lost the nice names they wrote down in the @acset_colim macro. The solution seems to be to use the @migration macro to directly specify the diagram. Something like:1
@migration(SchGraph, begin
L => @join begin
(e1,e2)::E
src(e2)==tgt(e1)
end
I => @join begin
(e1,e2)::E
(v1,v2)::V
src(e1)==v2
end
R => @join begin
e::E
src(e)==tgt(e)
end
left::(I=>L) => begin
e1 => e1
e2 => e1
v1 => v2
end
right::(I=>R) => begin end
end)Here, the maps left and right are uniquely determined by these particular generators. A homomorphisms search with those values initialized would return exactly one morphism (for starters, anything else could throw an error).
Footnotes
-
Maybe this syntax isn't exactly compatible with
@migrationbecause it's defining the shape category at the same time. You could ignore the::(I=>L)stuff and pretend we have a macro specific for the span diagram. It would be helpful, though for a syntax which lets you do the shape on the fly since we may have negative/positive application conditions as well as other sorts of morphisms showing up relevant to rewriting. ↩