Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML - How to handle ERROR exception

Email Gateway (Aug 22 2022 at 18:43):

From: Janik Benzin <janik.benzin@rwth-aachen.de>
Hi all,

I would like to learn a bit more about the ML basis of Isabelle.
Recently, I have tried to catch and handle the user exception "ERROR of
string" defined in exn.ML in the following example:

ML {*
type isar_record = {context: Proof.context, facts: thm list, goal:
thm}

fun goal_display ctxt (isar_goal:isar_record) =
Pretty.writeln(Goal_Display.pretty_goal ctxt (#goal(isar_goal)))
handle Exn.ERROR _ => ();
*}

Now I would like to insert the function using ML_val and antiquotations
anywhere in a theory file, i.e. inside and outside of proofs:

ML_val {*
goal_display @{context} @{Isar.goal}
*}

However, the exception ERROR "No proof state" is printed as an error
message in Isabelle, although I’ve installed the corresponding error
handler. Am I doing something wrong here?

Thank you for your time and help!

Best regards,
Janik Benzin

Email Gateway (Aug 22 2022 at 18:44):

From: Makarius <makarius@sketis.net>
On 08/11/2018 20:25, Janik Benzin wrote:

I would like to learn a bit more about the ML basis of Isabelle.
Recently, I have tried to catch and handle the user exception "ERROR of
string" defined in exn.ML in the following example:

The "implementation" manual contains a lot of explanations about
Isabelle/ML in chapter 0. Section 0.5 is about exceptions in particular:
these clear guidelines help to work with various kinds of errors robustly.

ML {*
type isar_record = {context: Proof.context, facts: thm list, goal:
thm}

fun goal_display ctxt (isar_goal:isar_record) =
Pretty.writeln(Goal_Display.pretty_goal ctxt (#goal(isar_goal)))
handle Exn.ERROR _ => ();
*}

BTW, when you find yourself defining record-type aliases such as
isar_record above there is something wrong with your function
signatures. In the Isabelle/Pure implementation, types are defined in a
manner to minimize redundant type constraints: ML is essentially
implicitly typed LISP, and the Isabelle/ML IDE tells you what the
inferred types are -- you rarely write anything in the source.

So here is the example written in a more standard way:

ML ‹
fun goal_display ctxt goal =
Pretty.writeln (Goal_Display.pretty_goal ctxt goal)
handle ERROR _ => ();
›

ML_val ‹goal_display (#goal @{Isar.goal})›

ML_val {*
goal_display @{context} @{Isar.goal}
*}

However, the exception ERROR "No proof state" is printed as an error
message in Isabelle, although I’ve installed the corresponding error
handler. Am I doing something wrong here?

The error is produced statically by the @{Isar.goal} antiquotation,
because the context of the ML_val command lacks a goal state.

Such confusions about the origin of exceptions belong to the nature of
exceptions: it requires care to write programs correctly in that respect
(section 0.5 of the "implementation" manual and the body of
Isabelle/Pure ML sources should provide some idea how to do it).

Makarius

Last updated: Nov 21 2024 at 12:39 UTC