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

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).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.