Closed
Conversation
The existing monadic-translator interface code does a bit of guessing of various constant names, and needs to set the translator use_full_type_names setting to false to make the naming predictable enough. This makes the monadic translator incompatible with various translation contexts. Some of this code can be replaced by use of get_type_inv and other query functions to fetch the relevant constants. This seems to allow the monadic translator to run with use_full_type_names present, and doesn't seem to break anything.
The monadic translator code uses parsing to set up quite a few terms, some of which were never added to a Syntax library, some of which were. This seems to make the system fragile in scenarios where an Ancestor include set (or explicit set_grammar_ancestry) hasn't included all the expected constants. Replace most of them with use of relevant Syntax lib or term poked from a def theorem or similar. Doesn't seem to break anything, and gets me a couple of steps further into an experiment (which is still incomplete and not ready to be a selftest).
Contributor
Author
|
Fails, and the same failure is present on my list-sort branch/PR. Will close this and try to fix it there. |
Contributor
|
Is this superseded by #1348 ? |
Contributor
Author
|
Yeah, whatever is broken also affects #1348 , so I'll try to fix them together. |
Contributor
Author
|
Oh, sorry, I misread which one you were talking about. There was a bug in my actual changes here that I've fixed in #1349 . Meanwhile Ramana and/or an AI has re-discovered and/or superseded a lot of my parser fixes in #1348 . In either case this PR gets retired. Probably #1348 and #1349 will conflict with each other and I or the AI will need to do some merge-conflict-squashing, but that's no big deal. |
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
2 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.
Some fixes to the monadic translator libs to be a little less fragile.
It seems that the examples still run and some corner cases are fixed, to my initial test. Let's see what the regression thinks.