hat-detect, Algorithmic Debugging for hat
ART Memo 20, Version 0
Thorsten Brehm, April 23rd, 2001


INTRODUCTION

The program hat-detect enables the user to perform algorithmic
debugging on hat trace files. The tool does not need any
additional information, except the recorded trace file, which
is used for hat-observer or hat-browse.


EXAMPLE OF USAGE:

- Compile your program with "hmake -T".
- Run your program.
- use hat-detect to start the algorithmic debugging on the recorded
  trace file.
  e.g.
       hat-detect tracefile
- the tool starts to scan the file, finding all CAFs. The CAFs are
  stored in a separate file, which will allow a quicker response
  of the tool when used again on an unchanged hat trace file.
- The tool will then ask about every single CAF, whether its result
  is correct or not. You may answer any question with yes ('y'),
  no ('n') or '?' if you are unsure. If you answer no or '?',
  the tool will search the CAF's children and ask you about
  these reductions.
- If you determined an reduction to be wrong (answering "no"),
  but you find all its child reduction's are correct (or,
  if there aren't any child reductions) the tool will identify
  a bug in the program at the definition of the applied
  function. If you were unsure about this reduction (hence,
  have answered with "?"), you will be asked to reconsider this
  reductin at this point.
- You can switch between normal and verbose mode by using the
  "v" or "verbose" command. Function applications within
  arguments of the shown reduction will be displayed in verbose
  mode, but are shown as underscores in normal mode.

KNOWN PROBLEMS AND BUGS:

1 First response time on startup of the tool is low, when the trace
  file is very large. In order to ask about the CAFs in the correct
  order of dependency, the tool needs to search the entire trace
  file.

2 A major problem occurred with applications used within the condition
  of an "if" or "guard" clause. Due to optimisations on the
  transformation, the trace file did no longer contain the necessary
  SATs to show the correct result of such an application. This
  problem was solved by a modification to the transformation.
  
3 Problem with locally defined functions. There is not enough
  information in hat files about lambda functions and locally
  defined functions. Therefore, reductions of these functions
  are not shown in hat-detect. However, as they  may be passed
  as higher order parameters to top-level functions, they may
  still occur in a question.

SOLUTIONS:

1 In order to show the CAFs in the correct order of dependency
  (e.g. the "main" CAF should be shown last), it is necessary to
  check the entire file. As there is no direct way to locate CAFs
  in the file, there does not seem to be an alternative to a
  search. As the same tool might be used several times on the
  same trace file, the CAFs locations are stored in a separate
  file. They are reused, when hat-detect is invoked again and
  the trace file was not modified (checked by file's time).

2 SATs for applications within conditions are not necessary for
  hat's redex trail browser, but they are necessary to find the
  result of an application. Both tools, hat-detect as well as
  hat-observe rely on the possibility to obtain the result
  of an application, in order to show a reduction. Hence, SATs
  need to be available for any application, and needed to be
  reintroduced.

3 The only way to fully enable the user to answer question's
  about a reduction is to provide him with all the necessary
  information. Hence, the only perfect solution to this
  problem is to obtain the necessary information from the
  trace file - which probably means that more information
  needed to be added to it.


REMARKS:

1 Finding the result for an application for a given application
  node in the hat file has shown to be a bit unreliable, as
  corresponding SATs for applications have to be searched in
  the trace file. In some special cases, necessary SATs were
  not present in the file or at least not at the right place.
  As finding an application's result turned out to be a very
  frequent operation for tools like hat-detect and hat-observe,
  the proposal to join SAT nodes with application nodes (see
  ART memo 19) would indeed show an advantage for the new
  tools working on the trace file - in reliablity as well a
  speed.