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

[ fix #119 ] Raise a warning when an unknown name appears in generated Haskell code #332

Merged
merged 2 commits into from
Oct 10, 2024

Conversation

jespercockx
Copy link
Member

@jespercockx jespercockx commented Jun 9, 2024

This fixes #119 by raising a warning when an unknown name appears in the generated Haskell code. The following names are considered as "known":

  • Names that have a COMPILE pragma
  • Names that have an associated rewrite rule in the agda2hs config
  • Names that are defined in a primitive module (i.e. anything in the agda2hs library)
  • Names of record fields that represent a type class
  • Names of constructors of datatypes that have a COMPILE pragma
  • Names that are defined in a where module of a known definition

For the test suite, I didn't figure out yet how to capture the warning message. At the moment, the test just produces "unexpected success". If anyone has an idea how to set up the test for the warning, that's very welcome. (Otherwise I'll take a look at how Agda itself does it).

@jespercockx
Copy link
Member Author

Since 1.3 has been released, I will go ahead and merge this now so it can get some testing before the next release.

@jespercockx jespercockx merged commit 62617a5 into agda:master Oct 10, 2024
6 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.

Check that all used definitions are actually defined in the Haskell code
1 participant