aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

Refactor Module #1135

Closed HoshinoTented closed 2 weeks ago

HoshinoTented commented 4 weeks ago

This PR redesigned the module system:

ice1000 commented 3 weeks ago

Do you intend to supersede ModuleExport with ModuleExport2? (and also the other similarly named classes)

HoshinoTented commented 3 weeks ago

Do you intend to supersede ModuleExport with ModuleExport2? (and also the other similarly named classes)

Yes, I keep it because I am too lazy to delete it.

HoshinoTented commented 3 weeks ago

The code compiles. However, there are some problems: We have a lot of usage of import xxx::base, and they cause name conflicts since the name base.

HoshinoTented commented 3 weeks ago

Well, a lot of code is reverted cause:

HoshinoTented commented 3 weeks ago

However, I found an unnatural place in CompiledModule::SerExport, and I fixed it in this PR.

codecov[bot] commented 3 weeks ago

Codecov Report

Attention: Patch coverage is 83.16832% with 34 lines in your changes missing coverage. Please review.

Project coverage is 79.77%. Comparing base (8f52aab) to head (5bbf969). Report is 21 commits behind head on main.

Files with missing lines Patch % Lines
...ain/java/org/aya/resolve/context/ModuleExport.java 70.73% 4 Missing and 8 partials :warning:
...in/java/org/aya/resolve/context/ModuleContext.java 78.37% 4 Missing and 4 partials :warning:
...main/java/org/aya/cli/interactive/ReplContext.java 91.22% 0 Missing and 5 partials :warning:
...ain/java/org/aya/resolve/context/ModuleSymbol.java 55.55% 4 Missing :warning:
...c/main/java/org/aya/resolve/context/Candidate.java 88.00% 2 Missing and 1 partial :warning:
...c/main/java/org/aya/resolve/error/NameProblem.java 50.00% 1 Missing :warning:
.../java/org/aya/resolve/visitor/StmtPreResolver.java 75.00% 0 Missing and 1 partial :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #1135 +/- ## ============================================ + Coverage 79.44% 79.77% +0.33% + Complexity 3361 3356 -5 ============================================ Files 306 307 +1 Lines 10172 10158 -14 Branches 1228 1220 -8 ============================================ + Hits 8081 8104 +23 + Misses 1411 1388 -23 + Partials 680 666 -14 ```

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

ice1000 commented 2 weeks ago

bors r+