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

Implement the backend #28

Open
5 tasks
jespercockx opened this issue Aug 1, 2024 · 0 comments
Open
5 tasks

Implement the backend #28

jespercockx opened this issue Aug 1, 2024 · 0 comments

Comments

@jespercockx
Copy link
Owner

jespercockx commented Aug 1, 2024

One of the main goals of the project is to have a backend for Agda proper that uses Agda Core to type-check the elaborated internal syntax of a module. Steps that we need to take to get this to work:

  • Implement the translation from Agda Terms to Agda Core Terms.
  • Implement a translation from an Agda Signature to an Agda Core GlobalScope + Signature for it.
  • Implement a translation from Agda's CompiledClauses to an Agda Core Term using TCases for each node in the case tree.
  • Implement the actual backend functionality that calls the typechecker on each term in a definition.
  • Add test cases
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

No branches or pull requests

1 participant