Email Gateway (Aug 22 2022 at 09:18): Email Gateway (Aug 22 2022 at 09:18):From: Matthias Schlaipfer <matthias.schlaipfer@tuwien.ac.at>
Hello,
I am trying to understand the implementation of program extraction in
Isabelle. I am wondering whether it is possible to access the
instantiated proof terms (like the output of the Isar commands prf or
full_prf) in the extract/extr functions in Pure/Proof/extraction.ml.
I tried printing them for better understanding and thought it should be
possible similar as in string_of_prfs (in Pure/Isar/isar_cmd.ML), but I
don't know how to access the context, or if it is even possible at this
point.
Is there an easy way to access the instantiated proof terms in the extr
functions?
Thank you and best regards,
Matthias
Email Gateway (Aug 22 2022 at 10:09):From: Makarius <makarius@sketis.net>
On Mon, 20 Apr 2015, Matthias Schlaipfer wrote:
I am trying to understand the implementation of program extraction in
Isabelle. I am wondering whether it is possible to access the instantiated
proof terms (like the output of the Isar commands prf or full_prf) in the
extract/extr functions in Pure/Proof/extraction.ml.I tried printing them for better understanding and thought it should be
possible similar as in string_of_prfs (in Pure/Isar/isar_cmd.ML), but I don't
know how to access the context, or if it is even possible at this point.
I am not quite sure what you are trying to do, but here are some general
hints.
The formal Proof.context is easily accessible to any tool that is somehow
integrated in the system. If you just experiment with Isabelle/ML (e.g.
via 'ML' or 'ML_file') you can access the compile-time context via the
@{context} antiquotation. If you implement a diagnostic print command,
you can use e.g. Toplevel.context_of to get a proper run-time context.
Sometimes old tools operate on a global theory instead of a proper local
Proof.context. If you have already some (ctxt: Proof.context), you pass
(Proof_Context.theory_of ctxt) to such a tool.
In rare situations, e.g. inside some old style hook that only provides a
(thy: theory) value, you can use (Proof_Context.init_global thy) as last
resort.
Is there an easy way to access the instantiated proof terms in the extr
functions?
I don't quite understand that. Can you point to the precise spot in the
Isabelle sources where you are looking at?
Makarius
Last updated: Nov 21 2024 at 12:39 UTC