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

Add support for custom tuples #342

Merged
merged 3 commits into from
Jul 23, 2024
Merged

Conversation

jespercockx
Copy link
Member

This PR addresses the first point in #105 by adding support for compiling an Agda record type to a Haskell tuple. The feature is designed to be pretty flexible, so you can compile any record type and agda2hs will just take the (compiled) field types as the tuple components. It also allows defining unboxed tuples, which was previously not supported by agda2hs. However, there are no checks in place that the rules for unboxed tuples are followed, so it might generate invalid Haskell code if used improperly.

@jespercockx jespercockx requested a review from omelkonian July 23, 2024 10:08
@jespercockx
Copy link
Member Author

At the moment, tuple projections are not yet supported, and I'm not sure what's the best way to handle them. Here are two options:

  1. Generate projection functions for each projection of the record type (but then there will be many redundant copies of the projections if you have a lot of tuple types)
  2. Compile projections to built-in functions fst and snd (but what to do about tuples with more than 2 components?)

A hybrid (2 for binary tuples, 1 for everything else) is also possible in theory.

@jespercockx
Copy link
Member Author

jespercockx commented Jul 23, 2024

One more option I just thought of: take option 1 except that for binary tuple types, we check that the projections are called fst and snd, and we don't generate any code in that case.

EDIT: actually, record projections are not compiled unless they have their own COMPILE pragma, so perhaps there is nothing that really needs to be changed. If users want to define their own record types that use Haskell's built-in fst and snd projections, they can do so by declaring rewrite rules for the projections.

jespercockx added a commit to jespercockx/agda-core that referenced this pull request Jul 23, 2024
@jespercockx jespercockx merged commit 3ca7265 into agda:master Jul 23, 2024
7 checks passed
@jespercockx jespercockx added this to the 1.3 milestone Sep 24, 2024
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.

Add support for user-definable tuples (WAS: User-definable functions for builtin Haskell syntax)
1 participant