Module structure refactorings #80
Conversation
There was a problem hiding this comment.
Thank you very much for these welcome changes! This looks a lot better now. I went through the commits chronologically one by one. So sometimes a comment got invalidated or addressed by a later change.
I don't have many requests, just a few questions and, as always, I would like to see a little bit of documentation here and there. :)
(Also: Nobody will think that I contributed anything to this code base after you acquired every line of git blame. 🤣 )
|
Do we have a version number? If so, we should probably increment? |
ibbem
force-pushed
the
module-structure-refactorings
branch
from
96a9be0 to
2be45ac
Compare
All other languages just append an "L" not a "VL" suffix.
It's way easier to make module parameters implicit for some definitions and not others than to add a module parameter after the fact.
Although `renaming` makes the identifiers shorter (especially the semantics), the suffixes where context dependent (e.g., ₐ, ₙ for ADT, NADT and ₂, ₙ for 2CC, NCC) and used inconsistently. Note that The length issue is only really an issue for `VariantList` which could be named `CaO` as in the paper to make it shorter.
This order is already used in a lot of places and makes the selection language the first argument which is nice when fixing the selection language.
This order is already used in a lot of places and makes the selection language the first argument which is nice when fixing the selection language.
Importing `Vatras.Lang.All` or `Vatras.Lang.All.Fixed` should be the canonical form for importing any language.
I'm not sure when agda-mode started to generate these files, or if this is a bug. Anyways, these can be safely ignored.
ibbem
force-pushed
the
module-structure-refactorings
branch
from
2be45ac to
ec4b3f4
Compare
|
Yes, there is one version number in |
|
Does this adequately fix #76? |
|
Not yet but it is a first necessary step towards fixing #76. To address #76 fully, it would also be good to have modules like I think we could do all this in another PR though. |
This fixes some inconsistencies in the code, splits the language properties into separate files (similar to how the Agda standard library does it) and tries to make it easier to use.