APPS WITH SATS -- A KEY TO HAT-OBSERVE AND HAT-DETECT ART Memo 16 (Version 0) Colin Runciman, 27 March 2001 INTRODUCTION In discussions at the end of Claus Reinke's recent visit we were once again asking ourselves whether redex trails could be used to support tracing in the style of Hood and Freja. Our intuition was `almost' -- but there is perhaps some information missing. This memo suggests that a lot could be done with .hat files just as they are now -- though two minor amendements could help. APPLICATIONS AND RESULTS In Hood, we have found that observations of functions -- tables showing the arguments to and results from functions that actually occur in a computation -- are the most useful. In Freja, the whole scheme of algorithmic debugging is based around the presentation of equations of the form `function application = result' which the user is invited to confirm or deny as the behaviour they intend. So, we need to extract details of function applications with their associated results. If one only examines the type definitions for redex trails, or considers them as graphs, it is fairly clear how to extract details of function applications, but far from clear how to find the result from a given application. In the .hat file, however, the SAT for the function result is right next to the APP for its application! (Addresses are more powerful than pointers!) To my knowledge, we are not yet exploiting this fact in any way -- though Olaf has noticed that SATs occur with APPs and wondered about combining the writing operations for the two nodes to gain efficiency. HAT-OBSERVE I shall give the name hat-observe to a (hypothetical) tool for Hood-like observations from a .hat file. A basic version of hat-observe could be implemented very quickly in C by adapting routines already found in hat-stack, hat-check and hat-connect. What I have in mind is the usage `hat-observe f' where f is the name of a top-level function. The result would be a pretty-printed tabulation of all recorded applications of f and the associated results. The applications could be found just by a sequential scan looking at all APP nodes -- hat-check has shown that this can be quite quick, even for large files. Note the restriction to `top-level' functions, to avoid the problems that Hood has, confusing different instances of the same local function. I don't think we have any way to enforce this restriction at the moment, but it would not be difficult to add a bit to the name-table entries representing the top-level/local distinction. HAT-DETECT Similarly, hat-detect is a provisional name for a tool that tracks down bugs, locating them in the bodies of named functions, using something like the algorithmic debugging scheme in Freja. Again a quick prototype could re-use C routines we already have. It is not quite as straightforward as hat-observe, but not too bad: * Where to start? As main is monadic, the equational presentation needs some thought -- can basic monadic actions be reconstructed as a do-expression? To begin with, could just assume a single `interact' (as Freja does, in effect). * How to find the `children' of an application-result equation that the user says is faulty? In the first instance, the children can be found by a sequential scan, looking for APPs with the desired parent. Any such children must come later in the .hat file than their parent. * What about locally-defined names? As with hat-observe, the easy way round this problem is to say that only top-level functions are first-class citizens. Locating a fault to within a named top-level function, with a counter-example, may be enough in most cases. It would be easy to add functionality to the basic dialogue of equations and yes/no answers: extensions such as asserting that statically untrusted functions are now trusted. SUMMARY It seems that with fairly modest effort, we could prototype tools hat-observe and hat-detect to provide a useful subset of Hood and Freja functionality. It would be helpful to make one small modification to .hat files: add a bit-marker to indicate names defined at top-level. COROLLARY Despite what I wrote in Memo 15 (Version 1), perhaps it is not such a good idea to eliminate SATs after all! However, we might consider incorporating SAT pointers in APP-node variants, rather than having separate SAT nodes.