Nothing Special   »   [go: up one dir, main page]
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

Fix #405: support --functor in the Agda backend #406

Merged
merged 7 commits into from
Dec 23, 2021
Merged

Fix #405: support --functor in the Agda backend #406

merged 7 commits into from
Dec 23, 2021

Conversation

andreasabel
Copy link
Member
@andreasabel andreasabel commented Dec 21, 2021 •
edited
Loading

Fix #405: support --functor in the Agda backend

TODO:

  • define pragmas
  • changelog
  • docs

@andreasabel
Fix #405: support --functor in the Agda backend
d3fd356 
This updates the generated abstract syntax (AST.agda) so that data
types are parametrized, and instantiated to #BNFCPosition.
@andreasabel
Testing #405: use --functor with --agda in system testsuite
7ded4a4
@andreasabel andreasabel added Agda Issues of the Agda backend position Concerning position information in parsed AST labels Dec 21, 2021
@andreasabel andreasabel added this to the 2.9.4 milestone Dec 21, 2021
@andreasabel andreasabel self-assigned this Dec 21, 2021
@andreasabel
Copy link
Member Author

@depsterr: Does this fit your needs?

@rachelambda
Copy link

This seems perfect! Thanks for the quick fix, much appreciated!

@andreasabel
Re #405 (Agda/Functor): fix problem with underscores in category names
1eab993 
Underscores are placeholders in Agda, so e.g. the name Foo_' is
invalid, since ' by itself is not a valid name.
@andreasabel
Re #405: implement define for Agda/Functor by parametrizing Haskell's
80ccbfa 
Generalize `definedRules` to `definedRules'` using a configuration
record that is instantiated to both Haskell and Agda.
@andreasabel
CHANGELOG #405
af2cd4d
@andreasabel
Agda makefile: use ${AGDA} instead of just agda
c745f36
@andreasabel
Document --agda --functor (#405)
a964b7c 
Also, observe that the Agda backend needs at least Agda 2.6.0.
@andreasabel andreasabel merged commit 7d7b714 into master Dec 23, 2021
@andreasabel andreasabel deleted the issue405 branch December 23, 2021 13:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@andreasabel andreasabel

Labels
Agda Issues of the Agda backend position Concerning position information in parsed AST
Projects
None yet
Milestone
2.9.4
Development

Successfully merging this pull request may close these issues.

--functor and --agda cannot be used simultaneously
2 participants
@andreasabel @rachelambda