Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bugfix: modules associated with inductive types should be declared after their inductive types #2768

Merged
merged 7 commits into from
May 14, 2024

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz commented May 7, 2024

  • Closes Internal-to-Core translation is limited to type-declaring axioms #2763.
  • Fixes a bug in the scoper, likely introduced in Per-module compilation #2468 by making later declarations depend on earlier ones. The problem was that the inductive modules were always added at the beginning of a section, which resulted in an incorrect definition dependency graph (an inductive type depended on its associated projections).
  • Now inductive modules are added just after a group of inductive definitions, before the next function definition. This implies that inductive type definitions which depend on each other cannot be separated by function definitions. Existing Juvix code needs to be adjusted.
  • The behaviour is now equivalent to "manually" inserting module declarations with projections after each group of inductive definitions.

@lukaszcz lukaszcz added this to the 0.6.2 milestone May 7, 2024
@lukaszcz lukaszcz self-assigned this May 7, 2024
@lukaszcz lukaszcz marked this pull request as ready for review May 7, 2024 16:58
@lukaszcz lukaszcz force-pushed the bugfix-internal-to-core-axioms branch from 8359160 to 145dc31 Compare May 8, 2024 14:19
@lukaszcz lukaszcz force-pushed the bugfix-internal-to-core-axioms branch 2 times, most recently from 87f82d1 to daf68f0 Compare May 14, 2024 07:53
@janmasrovira janmasrovira force-pushed the bugfix-internal-to-core-axioms branch from daf68f0 to bb46fb1 Compare May 14, 2024 08:53
Copy link
Collaborator

@janmasrovira janmasrovira left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I struggled to understand what was happening only by looking at the code. I think that adding some comments will be helpful

@lukaszcz lukaszcz force-pushed the bugfix-internal-to-core-axioms branch from 9166444 to 0143476 Compare May 14, 2024 15:48
@lukaszcz
Copy link
Collaborator Author

I struggled to understand what was happening only by looking at the code. I think that adding some comments will be helpful

Okay, I added some comments

@paulcadman paulcadman force-pushed the bugfix-internal-to-core-axioms branch from 2077e99 to 76e10fa Compare May 14, 2024 16:46
@lukaszcz lukaszcz merged commit d59d02c into main May 14, 2024
4 checks passed
@lukaszcz lukaszcz deleted the bugfix-internal-to-core-axioms branch May 14, 2024 17:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Internal-to-Core translation is limited to type-declaring axioms
2 participants