Add the notion of a DeepThunk and generation for this#35
Draft
Equilibris wants to merge 5 commits intomainfrom
Draft
Add the notion of a DeepThunk and generation for this#35Equilibris wants to merge 5 commits intomainfrom
DeepThunk and generation for this#35Equilibris wants to merge 5 commits intomainfrom
Conversation
Owner
|
See comments on the other PR, they also apply here |
Equilibris
force-pushed
the
codef-3-deepThunk
branch
from
02fbbf2 to
563190b
Compare
Equilibris
changed the title
DeepThunk and generation for this
Equilibris
force-pushed
the
codef-3-deepThunk
branch
from
6d85d1c to
5befbab
Compare
Equilibris
commented
Aug 15, 2024
| @@ -0,0 +1,66 @@ | |||
| import Qpf.Macro.Data.Replace | |||
Collaborator
Author
There was a problem hiding this comment.
Should this maybe be a separate PR?
Contributor
There was a problem hiding this comment.
I agree. It seems like this functionality was just lifted from another file ("Ind.lean") and so it is a non-functional refactoring. I think it would be good to make a small pr of the form "[NFC] Chore: refactor Recursive form functionality into a separate file".
AtticusKuhn
approved these changes
Aug 15, 2024
Contributor
There was a problem hiding this comment.
I don't really understand this code at a deep level. There seem to be a lot of macros and quotations and syntaxes.
I think at a high level, this PR would be easier to understand if you split this PR up into at least three separate PRs:
- Refactor "RecursionForm" into a separate file
- Add the notion of a "DeepThunk"
- Add syntax support for Deepthunks in the quotations.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
When it comes to expressing co-recursive functions, a state type is required to seed the progress. This state often also stores at what point the expression is in. This can be for a corec function on streams that repeats each element once more can have a state of a boolean and the stream that flips the boolean every other emission. This behaviour can be a bit funny to encode correctly in general corec functions so we use DeepThunk (the trace) to construct it instead. Generation of these objects takes a bit of work as seen in Ind.lean but the general categorical object resides in DeepThunk.lean.
Additionally, to this we split some files out and move some code around. This might be worth doing in a separate PR though.