Further typechecker and interpreter cleanup #2165
Open
Conversation
This file contains 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
Make it clearer what you might need to fix in your code. (Mostly, typos in type names.) Also note that we haven't found any way to do anything overtly unsound with the incorrect behavior, only trigger panics.
…binds.
This corrects certain weirdnesses that were probably intended as
ease-of-use affordances for the repl but also affect scripts. In
particular:
- monadic actions need to be in TopLevel (or in ProofScript for
the ProofScript repl);
- monadic actions that are polymorphic in their monad are run
in TopLevel or ProofScript instead of being gratuitiously
rejected;
- the interpreter no longer wraps pieces of the bind in a
Decl for typechecking, which is the first step on cleaning
up the interpreter's typechecking notions (#2158).
The downside is that you can no longer directly eval non-monadic
expressions in the repl without prefixing them with "return". This is
not terrible, but we should at least consider adding repl-specific
affordances to allow that again once the code is in shape to be able
to do it reasonably.
Another oddity is that previously if you eval'd a monadic action that
was in some other monad (e.g. LLVMSetup) at the syntactic top level it
would, instead of giving a type error, just not evaluate it and then
print "<monadic>" as the result. If for some reason you really want
to do this you can also get the old behavior by prefixing the lot with
"return".
Note that all this applied to the _syntactic_ top level, and not binds
within do-blocks, whether or not they were within functions, and
regardless of whether they were in the TopLevel monad.
Include some tests and a CHANGES entry. Closes #2162.
sauclovian-g
added
type: bug
In particular the interpreter used to allow "x <- e;" for a pure term e as long as it was at the syntactic top level; this should have been "let x = e;" and now it will be rejected. The failures so far (except for one) have been linked to three specific saw-script builtins: unfold_term, parse_core_mod, and mir_find_adt. I've checked all uses I can find of these. There might be more cases lurking though. Also update the CHANGES entry to specifically mention this behavior, since it's quite conceivable that downstream users will have their own instances of this problem.
…mples. Properly part of the previous commit.
Pass in the position from the original StmtBind instead of tossing it out and then using PosRepl instead.
There is no reason any more (if there ever was) to yoink the type out of the pattern and graft a copy onto the expression as an explicit type annotation. Commit this separately just in case there's something subtle happening and we end up wanting to be able to bisect to it later.
Move it all to a single subsection of processStmtBind. Also, don't print the types of functions when we weren't asked to print.
There's no point finding a position to cons up an LName if the position is then going to just be discarded.
Now it's in interpretStmt and that's the first step to having only one typechecker call in interpretStmt. Which is in turn the first step on typechecking _before_ we start interpreting.
…oup. This should have no effect, but commit it separately anyway in case we ever need to bisect it. This makes the checkDeclGroup entry point to the typechecker no longer used, so remove it.
The position we've been passing to checkStmt is now always just the position _of_ the statement. The typechecker can get this on its own. Leave a note for later that this is not really the right position to use for the purposes the typechecker uses this position for (the monad context the statement appears in) and that should be sorted out better. But it's probably not worth trying to do so until the interfacing to the typechecker is rationalized.
|
For the record, I decided to go ahead and push the further cleanup I'd been doing while deciding what to do about the failure in s2n. The changes coming (to make the new failures warnings for the time being) really want to sit on top of that cleanup: currently the typechecker cannot produce warnings and making it able to do so affects the interpreter -> typechecker interface, which is now a lot less fraught. |
Statements of the forms x <- e; x <- s; s; where e is a non-monadic term and s is a monadic term in the wrong monad are now accepted with a warning instead of causing a fatal type error. Note that statements of the form e; which also used to be accepted will now fail. The chance of this appearing in the wild is low. While I've fixed all the fallout in the saw tree, the amount (and nature) suggests that downstream users will also have cases to fix and we should allow time for this before making it a hard fail. Add tests for all these forms.
1. Don't allow the wrong monad in a bind whose pattern is a tuple pattern. The old saw produces a type error for that so we don't have to allow it now. 2. For binds in the wrong monad, unify the pattern type with the full wrong monadic type of the expression, not just the associated value type. This assigns the variables in the pattern types in the wrong monad, which matches both the historical behavior and also what happens inside the interpreter during execution. It also turns out that binds in the wrong monad with an explicit type signature expecting the bind to work didn't typecheck in the old saw. So we don't need to make that work as part of the workarounds either. Add three more test cases...
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
No description provided.