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

Model Migration #112

Closed kris-brown closed 9 months ago

kris-brown commented 9 months ago

Given a Theory Morphism T->U and a type Mᵤ (whose values are models of U), obtain a type Mₜ which has one parameter (of type Mᵤ) whose values are models of T.

E.g. given NatIsMonoid: ThMonoid->ThNatPlus and IntPlus <: Model{Tuple{Int}} and IntPlus implements ThNatPlus:

@migrate IntPlusMonoid = NatIsMonoid(IntPlus)

Yields:

struct IntPlusMonoid <: Model{Tuple{Int}}
  model::IntPlus
end

@instance ThMonoid [model::IntPlusMonoid] begin ... end

Future work: There is some subtlety in how accessor functions should be handled. TODO: The new instance methods do not yet handle the context keyword argument. No models with where type parameters have been tested yet.

StdLib.DerivedModels has some examples.

codecov[bot] commented 9 months ago

Codecov Report

Attention: 26 lines in your changes are missing coverage. Please review.

Comparison is base (06be9f0) 97.25% compared to head (cd55f7f) 96.18%. Report is 10 commits behind head on scope-level-alias.

:exclamation: Current head cd55f7f differs from pull request most recent head 0075a98. Consider uploading reports for the commit 0075a98 to get more accurate results

Additional details and impacted files ```diff @@ Coverage Diff @@ ## scope-level-alias #112 +/- ## ===================================================== - Coverage 97.25% 96.18% -1.07% ===================================================== Files 27 28 +1 Lines 1494 1706 +212 ===================================================== + Hits 1453 1641 +188 - Misses 41 65 +24 ``` | [Files](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia) | Coverage Δ | | |---|---|---| | [src/models/ModelInterface.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL21vZGVscy9Nb2RlbEludGVyZmFjZS5qbA==) | `98.31% <100.00%> (+0.67%)` | :arrow_up: | | [src/models/SymbolicModels.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL21vZGVscy9TeW1ib2xpY01vZGVscy5qbA==) | `97.36% <100.00%> (ø)` | | | [src/stdlib/derivedmodels/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9kZXJpdmVkbW9kZWxzL21vZHVsZS5qbA==) | `100.00% <100.00%> (ø)` | | | [src/stdlib/models/Arithmetic.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9tb2RlbHMvQXJpdGhtZXRpYy5qbA==) | `100.00% <100.00%> (ø)` | | | [src/stdlib/models/Op.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N0ZGxpYi9tb2RlbHMvT3Auamw=) | `100.00% <ø> (ø)` | | | [src/stdlib/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?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/Presentations.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9QcmVzZW50YXRpb25zLmps) | `97.61% <ø> (ø)` | | | [src/syntax/TheoryInterface.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9UaGVvcnlJbnRlcmZhY2Uuamw=) | `96.07% <100.00%> (-0.36%)` | :arrow_down: | | [src/syntax/TheoryMaps.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9UaGVvcnlNYXBzLmps) | `97.10% <98.85%> (-0.13%)` | :arrow_down: | | [src/syntax/Scopes.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9TY29wZXMuamw=) | `95.50% <92.56%> (-3.05%)` | :arrow_down: | | ... and [1 more](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/112?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.