AlgebraicJulia / GATlab.jl

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

Theory Morphisms #100

Closed kris-brown closed 11 months ago

kris-brown commented 11 months ago

Some initial work for theory morphism support.

The key features now are @theorymap macro, the pushing forward of terms along theory morphisms and the model GATC (for ThCategory) of GATs and GAT morphisms. Additionally the stdlib now has a file for standard theory morphisms, such as swap: ThMonoid -> ThMonoid, interpreting preorders as categories and interpreting the naturals + addition as a monoid.

Pushing forward terms required a new struct TermInCtx for AlgTerms in a TypeScope as well as an implementation of type inference (TermInCtx -> AlgType).

codecov[bot] commented 11 months ago

Codecov Report

Patch coverage: 95.06% and project coverage change: +0.90% :tada:

Comparison is base (7a20340) 95.64% compared to head (65a34fa) 96.55%. Report is 2 commits behind head on main.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #100 +/- ## ========================================== + Coverage 95.64% 96.55% +0.90% ========================================== Files 22 25 +3 Lines 1148 1334 +186 ========================================== + Hits 1098 1288 +190 + Misses 50 46 -4 ``` | [Files Changed](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia) | Coverage Δ | | |---|---|---| | [src/stdlib/models/module.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9tb2RlbHMvbW9kdWxlLmps) | `100.00% <ø> (ø)` | | | [src/stdlib/module.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9tb2R1bGUuamw=) | `100.00% <ø> (ø)` | | | [src/syntax/module.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9tb2R1bGUuamw=) | `100.00% <ø> (ø)` | | | [src/syntax/GATs.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9HQVRzLmps) | `96.32% <91.75%> (-0.55%)` | :arrow_down: | | [src/syntax/TheoryMaps.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9UaGVvcnlNYXBzLmps) | `97.16% <97.16%> (ø)` | | | [src/stdlib/models/GATs.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9tb2RlbHMvR0FUcy5qbA==) | `100.00% <100.00%> (ø)` | | | [src/stdlib/theorymaps/module.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi90aGVvcnltYXBzL21vZHVsZS5qbA==) | `100.00% <100.00%> (ø)` | | | [src/syntax/ExprInterop.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9FeHBySW50ZXJvcC5qbA==) | `98.61% <100.00%> (+0.01%)` | :arrow_up: | | [src/syntax/Scopes.jl](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9TY29wZXMuamw=) | `97.71% <100.00%> (+3.73%)` | :arrow_up: | ... and [1 file with indirect coverage changes](https://app.codecov.io/gh/AlgebraicJulia/Gatlab.jl/pull/100/indirect-changes?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia)

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