Debugging SML

For local contextual information, you can use the print_all function provided by the structure I within each contextual information's structure.

For example, RippleCInfo.print_all_rst rst will print out the rippling information for every goal in the reasoning state rst.

There is course the print for a given goal: RippleCInfo.print_rst rst gname which will print out the rippling information for goal gname in the reasoning state rst.

Generally all kinds of data have a pretty and print function. Look in the source code and if they are not there, add them!

Signatures and Structures

A common problem is that to replay an error that occurs in a function in a signature constrained structure which has non-exported helper functions. For most of the structures in IsaPlanner (and I encourage you do do this for your code) I write a structure DB_StructureName which is not constrained by the signature, and then use StructureName : SignatureName = DB_StructureName to do the corresponding type-check for the structure against the signature. This ensures intermodule dependencies while providing the flexibility to debug your code by calling signature-hidden functions.

To see the signature of a structure, you can type: structure Foo = StructureName;. This works because the interactive ML shell spits out signatures of newly defined structures. Thus you can now see the signature, of Foo which is defined to be equal to StructureName;, printed by the interactive ML shell.

Exceptions to Dive Into Code

A handy trick to find bugs in the middle of some complicated bit of code is to make ML throw a customised exception. Make it do this at the just before you think the problem is ocuring and make the type of the exception hold the information you want to look at in more detail. For example, in unification, we might want to look at the terms being unified. You can then handle the exception at the top level and pull out the parameters.

Continuing the above example:

• exception my_exp of Term.term * Term.term;

defines an exception of a pair of terms which we want to look at, because we believe the bug in the code is related to these. We then add a raise my_exp (t1,t2) to the complicated bit of code in the internals of our program.

• Seq.list_of (Res.restr_res thrm goal ppl) is the buggy function call that will then raise the exception.

• To then run the code and get the variables as if we were right in the middle of the complicated code, we can do the following:

val (t1,t2) = the ((Seq.list_of (Res.restr_res thrm goal ppl); NONE) handle my_exp x => SOME x);

Now we have t1 and t2 bound to the values of where we think the error is likely to be. This is better than simply pretty printing as it allows a much more detailed analysis of the data. It also allows you to run functions on the extracted internal values of where the code is behaving strangely.

Isabelle Terms

Isabelle terms get big and complicated and often it is hard to identify where what it is about a term that is causing a problem. A useful trick is to use the TermDbg.writeterm function on the problematic term. This pretty prints the term in a way that you can then paste back in to reconstruct. This allows you to break up you term easily and paste bits of it in to try to narrow down issues with you term. Unlike the pretty printer, it also shows you exactly what your term really is so that you can mentally trace what is going on in you term manipulation code.

This function is also useful to hand-construction of complicated terms, which you sometimes want for pattern matching. You can read in a term from a string, or get it from an existing theorem, print them out using TermDbg.writeterm and then copy and paste the bits you want, or use this to make new terms by pasting different parts together.

Warning: if you combine terms by hand, you are likely to create badly formed terms. You can check your terms with: Thm.cterm_of