Hanno Becker (Jan 07 2023 at 19:09): Hanno Becker (Jan 07 2023 at 19:09):Hi! I noticed that Method.parse returns a Method.text object rather than a method -- the latter is only obtained upon calling evaluate: text -> Proof.context -> method. What is the reason for this indirection?
Manuel Eberl (Jan 07 2023 at 19:25):Seems to me that Method.text is an AST and Method.method is the actual method. And getting from the AST to the method requires a context.
Hanno Becker (Feb 19 2023 at 20:25):Hi Manuel! It makes sense that going from the AST to the actual method is context dependent, but it doesn't explain the prominence of the AST-type text throughout the code base. Why not parse into a method directly (and ask for a Proof.context argument to do that)?
Manuel Eberl (Feb 21 2023 at 11:40):I cannot say for sure, but my guess would be that maybe the parsing might happen at a point when no context is available yet, e.g. because you want to be able to parse a theory even without having a context.
Manuel Eberl (Feb 21 2023 at 11:41):The context will, after all, only be available after processing the entire theory and all its dependencies, which might take minutes or even hours. But I really don't know, I didn't look at it in detail and I never really did any programming in that area of the Isabelle code base.
Manuel Eberl (Feb 21 2023 at 11:42):For a definite answer to those questions, it is best to ask on the mailing list. These things are typically decisions made by Makarius, and he refuses to use Zulip.
Hanno Becker (Mar 03 2023 at 08:10):Thank you @Manuel Eberl !
Hanno Becker (Mar 14 2023 at 05:07):Late note on this one: The lazy evaluation of method texts appears useful to allow updates to e.g. named theorem lists used in the method, after the definition of the method. If the method text was interpreted at definition time, it would be bound to the state of the named theorem list at that point, which is not what you want.
On the flipside, it probably also means that if you reference another method in the definition which is then re-defined elsewhere, the meaning of your method text changes as well.
Wolfgang Jeltsch (Mar 14 2023 at 11:36):Hanno Becker said:
On the flipside, it probably also means that if you reference another method in the definition which is then re-defined elsewhere, the meaning of your method text changes as well.
That’s not necessarily the case with laziness. If some sort of closure is formed, then redefining internally used methods does not change the meaning of your calling method. That said, I don’t know whether Eisbach really forms closures; it might very well be that it doesn’t. However, is it really possible to redefine methods (as opposed to define methods of the same name in a different namespace)?
Last updated: Apr 30 2024 at 01:06 UTC