search

AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
21 stars 2 forks source link

Simple theory maps and simple pushouts #146

Open kris-brown opened 4 months ago

kris-brown commented 4 months ago

This adds a new instance of AbsTheoryMap which maps generators to generators, rather than to complex terms. For this kind of map we can easily compute pushouts, which is a matter of renaming.

The universal property of these colimits is not yet implemented.

Also, this is all at the GAT data structure level, rather than the module level.

codecov[bot] commented 4 months ago

Codecov Report

Attention: Patch coverage is 96.96970% with 3 lines in your changes are missing coverage. Please review.

Project coverage is 94.80%. Comparing base (53c6086) to head (a65ffdf).

Files Patch % Lines
src/syntax/TheoryMaps.jl 94.33% 3 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #146 +/- ## ========================================== + Coverage 94.52% 94.80% +0.27% ========================================== Files 38 38 Lines 2082 2174 +92 ========================================== + Hits 1968 2061 +93 + Misses 114 113 -1 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

olynch commented 2 weeks ago

My thought is that we are going to use the multiple-inheritance branch instead of this, so this should not be merged, is that right @kris-brown?

kris-brown commented 2 weeks ago

I imagined them as two different means of doing the same thing - I'd be happy to re-implement this down the line (in case we discover a need for programmatically merging theories), using the underlying implementation in multiple-inheritance, so I think it's fine to put this branch on pause / close the PR for now.