agda2hs
agda2hs copied to clipboard
[ fix #119 ] Raise a warning when an unknown name appears in generated Haskell code
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).