Debugging Reasoning Techniques

Failure and Ending

Be aware that a technique is said to fail if SOME sequence of new states which is empty. This is in contrast to ending where it returns NONE. Each reasoning technique is responsible for setting the continuation. When it has successfully finish what it is intended to do, it should set the continuation to NONE.

Interactive Tracing of Techniques

The code for the tracer, which is the way I tend to find errors in Techniques is in the structure PPInterface. This lives in the file interface/interface.ML.

Bugs Outside the Tracer's Visibility

A common problem with debugging Reasoning Techniques is that the bug happens in the construction of a new state which the tracer cannot show you because an exception is raised or because it results in the empty sequence of new states.

No new states where I expect them

This is the easier of the difficulties: trace through to the state where the problem occurs. At this point exit the tracer. This returns the reasoning state you were looking at. Bind this to a top-level ML value, I usually use val rst = it;

Now you can run the sub-functions on that reasoning state. I usually do this by pasting the function in line by line.

Exceptions

This is a big trickier, and frustrating when you spend time to trace to the right point and then get an exception. However, the tracer always holds the last successful reasoning state that was being looked at (or searched through in if you stepped-over or searched through). You can get this using: PPInterface.get_last_rst(); and bind it to a top level value and then start pasting in the function that raises the exception line by line.

Bugs sliding past exception handlers

Lasy evaluation of ML sequences sometimes causes bugs to show up in places you do not expect them to. A good way to check/force the issue for debugging is to modify the code by adding explicit unfolding and refolding of the lazily evaluated list: ((Seq.of_list o Seq.list_of) your Seq.eq returning code) handle ... .