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 fixity declarations #158

Merged
merged 1 commit into from
Dec 22, 2023
Merged

Conversation

flupe
Copy link
Contributor

@flupe flupe commented Mar 9, 2023

Implements #41.

WIP, I have yet to fix infix applications parentheses.

@flupe flupe linked an issue Mar 9, 2023 that may be closed by this pull request
@jespercockx jespercockx added this to the 1.0 milestone Mar 17, 2023
@flupe
Copy link
Contributor Author

flupe commented Mar 20, 2023

Kinda hitting a roadblock here. Currently pretty-printing infix applications (1 + 2 - 5 instead of 1 + (2 - 5)) is done by processing the generated Haskell syntax and accounting for the default fixities of things in the prelude (this mapping is exported by the Haskell syntax library we use).

My PR works but fixity of custom operators is ignored and each application sees its children parenthesized (which is fine).

In order to also pretty-print custom operators, I wanted the post-processing pass to rely on a mapping from names to fixity of things in scope of the current module. I thought this info could be found in _scopeFixities from ScopeInfo, info we retrieve from iInsideScope of the module Interface that we get when compiling the module. To my surprise, this mapping is always empty, which I find surprising.

Looking for some comments on this, @jespercockx ? The lazy way out is to not pretty-print properly custom operators, which is arguably fine is the point of Agda2HS is to make it easy to bind to generated Haskell, not make said Haskell particularly pretty.

@jespercockx
Copy link
Member

Hm that's a bit surprising indeed, I'm not sure why the fixity information is absent. I guess this will require some detective work in the Agda codebase itself to figure out where the fixity information is going to.

I put this PR on the 1.0 milestone because I assumed it was (almost) ready, but since it isn't I propose we keep the current situation as it is.

@jespercockx jespercockx removed this from the 1.0 milestone Mar 20, 2023
@jespercockx jespercockx added this to the 1.1 milestone Apr 12, 2023
@flupe flupe modified the milestones: 1.1, 1.2 Oct 12, 2023
@jespercockx jespercockx modified the milestones: 1.2, 1.3 Nov 27, 2023
@flupe
Copy link
Contributor Author

flupe commented Dec 13, 2023

Just rebased this PR on current master. Just wanted to note that it does work currently (you can introduce your own fixity). The only caveat is that your custom declarations won't be used when pretty-printing the generated Haskell code, but it will generate correct Haskell.

Maybe we can merge and save the problem of pretty-printing custom fixities for later? @jespercockx

@flupe flupe marked this pull request as ready for review December 21, 2023 08:56
@jespercockx
Copy link
Member

Sounds good, thanks for the PR!

@jespercockx jespercockx merged commit bda9466 into agda:master Dec 22, 2023
7 checks passed
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.

fixity declarations
2 participants