saw-script interpreter typechecks one line at a time #2158
Assignees
Labels
needs design
Technical design work is needed for issue to progress
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Milestone
Comments
sauclovian-g
added
type: bug
|
There are additional problems, such as that it turns out the type signatures in the list of builtin primitives are not checked. (Accordingly, at least one of them is wrong.) I think this needs to be fixed so that parsed but not typechecked text is not available to the interpreter code. |
sauclovian-g
added a commit
that referenced
this issue
Dec 18, 2024
…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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The saw-script interpreter typechecks one statement at a time when executing at the top level (either the TopLevel top level or the ProofScript top level, I think) ... and this is not easily fixed because it does special things with top-level binds that ought to be happening in the typechecker instead, except that the AST representation can't represent them so something needs to give.
It also just doesn't check some statements before executing them.
This is all made worse by the corresponding assumption in the typechecker that statements happen only inside do-blocks.
With #2157 the overtly incorrect behavior where top-level typedefs were just not checked at all has been corrected, but because of these complications that was done as a patch rather than a fix.
The text was updated successfully, but these errors were encountered: