Skip to content

Where clauses fix#58

Draft
flupe wants to merge 4 commits intomasterfrom
issue52
Draft

Where clauses fix#58
flupe wants to merge 4 commits intomasterfrom
issue52

Conversation

@flupe
Copy link
Copy Markdown
Collaborator

@flupe flupe commented Feb 24, 2026

The easy fix is to suffix all names with the (unique) name id.
Will do more tests to see if this also solves the problem with where clauses.

However, this means we give up on (approximate) 1:1 name correspondence.
I'm willing to lose this if this means we ensure compilation is correct, and with the custom re-mapping feature this probably isn't too bad, but idk.

@omelkonian
Copy link
Copy Markdown
Collaborator

For what it's worth, that's what we're also doing in agda2train.

@flupe
Copy link
Copy Markdown
Collaborator Author

flupe commented Feb 25, 2026

Ah nice, then let's do that. Although I think we can also only do that for names that have been Agda-generated (with, \where, etc) and keep the others. Let's try and see if this breaks things.

I noticed the only \where functions that are inlined are the non-recursive one, whereas we decided to never compile them, so I'm working on fixing that.
Now Fannkuch compiles.
But still doesn't evaluate...

@flupe flupe marked this pull request as draft February 25, 2026 13:12
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

Successfully merging this pull request may close these issues.

2 participants