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

Index free syntax #204

Open
wants to merge 26 commits into
base: master
Choose a base branch
from
Open

Index free syntax #204

wants to merge 26 commits into from

Conversation

andrevidela
Copy link
Collaborator

@andrevidela andrevidela commented Dec 25, 2019

This PR add support for a new index-free syntax which more closely resembles ml-style languages with data constructors:

List a := nil : 1 | cons : a * List a

fix #164
fix #175
fix #23

Copy link
Member

@epost epost left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very cool André! 👍

Typedefs_Syntax.md Outdated Show resolved Hide resolved
Typedefs_Syntax.md Outdated Show resolved Hide resolved
Typedefs_Syntax.md Outdated Show resolved Hide resolved
Typedefs_Syntax.md Outdated Show resolved Hide resolved
Typedefs_Syntax.md Outdated Show resolved Hide resolved
src/Typedefs/Syntax/Compiler.idr Outdated Show resolved Hide resolved
src/Typedefs/Syntax/Compiler.idr Outdated Show resolved Hide resolved
src/Typedefs/Syntax/Compiler.idr Outdated Show resolved Hide resolved
src/Typedefs/Syntax/Compiler.idr Outdated Show resolved Hide resolved
src/Typedefs/Syntax/Compiler.idr Outdated Show resolved Hide resolved
@andrevidela
Copy link
Collaborator Author

The merge for this is going to take a bit longer than expected

@andrevidela
Copy link
Collaborator Author

Actually this is going to take a lot more work than expected. Indeed this is not compatible anymore with the current master in which we only allow to generate code for TDefs with resolved references.

This commit, is the culprit and makes the change from TNamed to TNamedR. I tried using the existing references compiler but the type signatures don't quite match.

So either we rewrite the reference compiler or we rewrite the syntax compiler. Eitherway, it's not a trivial and easy task

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants