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

Basic model migration functionality #111

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

All modified lines are covered by tests :white_check_mark:

Comparison is base (4a32bc1) 96.85% compared to head (ee193e0) 97.03%.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## fix_argcontext #111 +/- ## ================================================== + Coverage 96.85% 97.03% +0.17% ================================================== Files 27 28 +1 Lines 1591 1684 +93 ================================================== + Hits 1541 1634 +93 Misses 50 50 ``` | [Files](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?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/111?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL21vZGVscy9Nb2RlbEludGVyZmFjZS5qbA==) | `98.30% <100.00%> (+0.67%)` | :arrow_up: | | [src/stdlib/derivedmodels/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?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/111?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/111?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/111?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/GATs.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9HQVRzLmps) | `97.71% <100.00%> (+0.05%)` | :arrow_up: | | [src/syntax/Scopes.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9TY29wZXMuamw=) | `98.30% <100.00%> (+<0.01%)` | :arrow_up: | | [src/syntax/TheoryInterface.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?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.07%)` | :arrow_up: | | [src/syntax/TheoryMaps.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/111?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9UaGVvcnlNYXBzLmps) | `93.12% <100.00%> (+0.32%)` | :arrow_up: |

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