Lem concurrency interface v2 #1548
Conversation
(continues to work with Isabelle 2025)
src/lib/outcome_rewrites.ml
Outdated
| let instantiate target ast = | ||
| (* Some backends will need the instantiations to hook up to a particular interface *) | ||
| let keep_original_defs = String.compare target "coq" == 0 in | ||
| let keep_original_defs = String.compare target "coq" == 0 || String.compare target "lem" == 0 in |
There was a problem hiding this comment.
In general I don't love hard-coding target specific behaviours into rewrites like this. I think the cleaner thing to do would be to add a flag to the target struct in target.ml that can be set by Target.register similar to the supports_abstract_types flag. Then here we would use Target.get and query that flag.
There was a problem hiding this comment.
I just had a go at this, but hit a dependency cycle Outcome_rewrites -> Target -> Rewrites -> Outcome_rewrites. I guess we could do some refactoring, or maybe just adding a boolean flag to the outcomes rewrite using Bool_rewriter is simpler?
There was a problem hiding this comment.
Maybe not worth refactoring it for now then
There was a problem hiding this comment.
Although a boolean flag on the rewrite might be better if it's easy to do
There was a problem hiding this comment.
Seems easy, I've pushed a commit.
Test Results 16 files 36 suites 0s ⏱️ Results for commit 8c034c4. ♻️ This comment has been updated with latest results. |
| [ | ||
| ("move_termination_measures", []); | ||
| ("instantiate_outcomes", [String_arg "lean"]); | ||
| ("instantiate_outcomes", [String_arg "lean"; Bool_arg false]); |
There was a problem hiding this comment.
When rebasing, you'll want to change this because Lean now supports v2.
| ("instantiate_outcomes", [String_arg "lean"; Bool_arg false]); | |
| ("instantiate_outcomes", [String_arg "lean"; Bool_arg true]); |
3 participants
Add a Lem implementation of the concurrency interface v2 and use it when translation Sail specs targeting that interface. For detecting the interface parameters, we reuse the code also used by the Rocq interface. This requires not removing the outcome and instantiation declarations during rewriting, which needs a tweak to the monomorphisation rewrite to accept those declarations without throwing an error; we just ignore those declarations during monomorphisation for now (additional definitions generated by the outcome instantiation rewrite continue to be handled).