agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

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

Open jespercockx opened this issue 8 months ago • 0 comments

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 avatar Jun 09 '24 10:06 jespercockx