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

Remove nat magic #3184

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Remove nat magic #3184

wants to merge 2 commits into from

Conversation

Z-snails
Copy link
Collaborator

@Z-snails Z-snails commented Jan 1, 2024

Description

Remove compiler magic around Nat.

This uses %transform rules, which are currently fragile (see #3183) so it doesn't work currently.
Once that issue is fixed, then this should work well.

Should this change go in the CHANGELOG?

Yes, I will do this later

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG.md (and potentially also
    CONTRIBUTORS.md).

-- TODO: next release remove this and use %builtin pragma
natHack : List Magic
natHack =
[ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k)
Copy link
Collaborator

Choose a reason for hiding this comment

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

This makes Nat -> integer a no-op right? Is that optimization captured anymore once this code is removed?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes that optimisation is captured already by a different, much more general optimisation I added.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants