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.

Sign up for GitHub

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

Jump to bottom

Check that all used definitions are actually defined in the Haskell code #119

Closed
jespercockx opened this issue Nov 11, 2022 · 1 comment · Fixed by #332
Closed

Check that all used definitions are actually defined in the Haskell code #119

jespercockx opened this issue Nov 11, 2022 · 1 comment · Fixed by #332
Assignees
@jespercockx
Labels
enhancement New feature or request error-reporting
Milestone
1.4

Comments

@jespercockx
Copy link
Member

@flupe mentioned to me that it would be a good idea to check that all defined symbols that are used in the generated Haskell code are also actually defined in the Haskell code. This would require some kind of "foreign" pragma for annotating a function that is already defined in the Haskell code.
@jespercockx jespercockx added enhancement New feature or request error-reporting labels Nov 11, 2022
@jespercockx jespercockx modified the milestone: 1.0 Nov 11, 2022
@jespercockx jespercockx added this to the 1.1 milestone Apr 12, 2023
@jespercockx jespercockx mentioned this issue Jul 27, 2023
Closed
@jespercockx jespercockx modified the milestones: 1.1, 1.2 Oct 6, 2023
@jespercockx jespercockx modified the milestones: 1.2, 1.3 Nov 27, 2023
@jespercockx
Copy link
Member Author

Alternatively we could use the following criterion for which functions are allowed to appear in compiled Haskell code:

  • has a COMPILE AGDA2HS pragma,
  • OR is a builtin function of agda2hs,
  • OR is defined in a module starting with Haskell.Prim

If we have the full set of allowed functions, we could also make a call to dontReduceDefs allowedFunctions (normalise v) to try to make the disallowed functions disappear. If that doesn't work, we should throw an error.

@jespercockx jespercockx modified the milestones: 1.3, 1.4 Mar 22, 2024
@jespercockx jespercockx mentioned this issue May 24, 2024
Closed
jespercockx added a commit to jespercockx/agda2hs that referenced this issue Jun 9, 2024
@jespercockx
[ fix agda#119 ] Raise a warning when an unknown name appears in gene…
f8ceb8f 
…rated Haskell code
@jespercockx jespercockx mentioned this issue Jun 9, 2024
Merged
@jespercockx jespercockx self-assigned this Jun 9, 2024
jespercockx added a commit to jespercockx/agda2hs that referenced this issue Jun 9, 2024
@jespercockx
[ fix agda#119 ] Raise a warning when an unknown name appears in gene…
1b1005e 
…rated Haskell code
jespercockx added a commit to jespercockx/agda2hs that referenced this issue Sep 19, 2024
@jespercockx
[ fix agda#119 ] Raise a warning when an unknown name appears in gene…
2ffeca0 
…rated Haskell code
jespercockx added a commit to jespercockx/agda2hs that referenced this issue Sep 24, 2024
@jespercockx
[ fix agda#119 ] Throw an error when an unknown name appears in gener…
85afb90 
…ated Haskell code
jespercockx added a commit to jespercockx/agda2hs that referenced this issue Sep 25, 2024
@jespercockx
[ fix agda#119 ] Throw an error when an unknown name appears in gener…
602d7f0 
…ated Haskell code
jespercockx added a commit that referenced this issue Oct 10, 2024
@jespercockx
[ fix #119 ] Throw an error when an unknown name appears in generated…
62617a5 
… Haskell code
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jespercockx jespercockx

Labels
enhancement New feature or request error-reporting
Projects
None yet
Milestone
1.4
1 participant
@jespercockx