Support _ghost_stmt in _pure functions#76
Conversation
Add a GhostStmt case to emit_pure_body that emits ghost statements as 'let _ = <code> in <rest>' in Pure functions, matching the standard F* pattern for sequencing lemma calls in a pure context. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
| Doc::text("let") | ||
| .append(Doc::line()) | ||
| .append("_") | ||
| .append(Doc::line()) | ||
| .append("=") | ||
| .group() | ||
| .nest(2) | ||
| .append(Doc::line().append(ghost_doc).nest(2)) | ||
| .append(Doc::line()) | ||
| .append("in") | ||
| .append(Doc::line().append(rest).nest(2)), |
There was a problem hiding this comment.
So this produces let _ = ... in. Is this what we want?
(I honestly don't know, maybe it's actually better than ...;?)
There was a problem hiding this comment.
Using ; in a branch of ìf ... then ... else would require enclosing that branch with parentheses, which is not required with let _ = ... in .
| /* This test is not in pure_fn.c because it also needs shift operations. | ||
| Thus, it is not purely a unit test */ |
There was a problem hiding this comment.
Don't read too much into the organization of the test directory, this mostly happened by accident and not by design. My favorite parts are where an agent keeps appending to the same test file for the whole session, even though the features are completely unrelated.
But if you want concrete guidelines, I'd suggest the following:
- Keep tests independent and medium-sized (F* takes over a second to check a single test).
- Don't include unnecessary details beyond the feature that you want to test (tests rot and it's easier to keep them fresh when you can see at a glance what it's testing).
In this case, I would suggest the following function as a test:
_pure int pure_ghost_stmt()
_ensures(false)
{
_ghost_stmt(assume False);
return 1;
}This test is short and self-contained enough that it can easily go in the pure_fn.c file.
2 participants
Add a GhostStmt case to emit_pure_body that emits ghost statements as
let _ = <code> in <rest>in Pure functions, matching the standard F* pattern for sequencing lemma calls in a pure context.Co-authored-by Copilot (except the unit tests, which I wrote by hand.)