ir: Allow Ir.init to reference active REPLs by name#205
ir: Allow Ir.init to reference active REPLs by name#205ike-mulder-aws wants to merge 1 commit intoawslabs:mainfrom
Conversation
Add get_theory_or_repl that checks the REPL table first (extracting the final theory state) before falling back to Thy_Info.get_theory. This lets Ir.init create REPLs whose parent theories come from other active REPLs, not just heap/loaded theories. Signed-off-by: Ike Mulder <ikemul@amazon.com>
ike-mulder-aws
force-pushed
the
ir-init-repl-refs
branch
from
782e0ab to
f4c29a6
Compare
| theory), then fall back to Thy_Info.get_theory for heap/loaded theories. *) | ||
| fun get_theory_or_repl name = | ||
| case Symtab.lookup (Synchronized.value repl_tab) name of | ||
| SOME r => Toplevel.theory_of (last_state r) |
There was a problem hiding this comment.
(How) Is this different from forking a REPL from the last state in the parent REPL? I would prefer the latter as it retains the dependency between the REPLs.
There was a problem hiding this comment.
Separately, here we 'close' the parent REPL into a theory; should this be a separate step?
There was a problem hiding this comment.
Is this different from forking a REPL from the last state in the parent REPL?
It's different because this allows you to merge multiple REPLs and/or loaded theories into a new theory. I see the tests don't showcase this - I'll change that.
Separately, here we 'close' the parent REPL into a theory; should this be a separate step?
You mean, make the Toplevel.theory_of (last_state r) available separately, so that you'd be able to do get the same functionality in multiple I/R commands? That'd work for me too. I think it'd require a separate table of 'saved/closed' REPLs, since I don't think we can save the REPLs as regular theories - but I haven't looked into this much
There was a problem hiding this comment.
It's different because this allows you to merge multiple REPLs and/or loaded theories into a new theory. I see the tests don't showcase this - I'll change that.
Ah yes, that's right 👍 Thanks!
There was a problem hiding this comment.
I think it'd require a separate table of 'saved/closed' REPLs, since I don't think we can save the REPLs as regular theories - but I haven't looked into this much
Yes, I was wondering if it's worth having such a table of theories, either coming from load_theory or theories obtained by closing REPLs.
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
I'd like to understand and ideally document better the motivation for this change, esp. its relation to the existing Ir.fork command which, I think, effectively subsumes the functionality added here.
Also, do you foresee this to be used in interactive or non-interactive sessions, or both? If it's only for non-interactive sessions, we may want to hide the functionality in the interactive case, to prevent confusing the MCP client (cf. is_interactive_session)
|
I don't think |
2 participants
Add get_theory_or_repl that checks the REPL table first (extracting the final theory state) before falling back to Thy_Info.get_theory. This lets Ir.init create REPLs whose parent theories come from other active REPLs, not just heap/loaded theories.
Issue #, if available:
Description of changes:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.