Debugging Tree Rewriting

By default, Prop generates a macro DEBUG_C for each rewrite class named C. The user can redefine this macro in order to trace the replacements that are performed during the execution of a set of rewriting rules. The default definition of DEBUG_C is as follows:

i.e. it simply returns the value of R.

The arguments to the macro are as follows:

• R is the new replacement term.
• redex is the current redex, before the replacement has been performed.
• filename is the file name of the current rewriting rule.
• linenumber is the location of the current rewriting rule.
• ruletext is a string that describes the current rule.

In order to activate tracing, the user can redefine the macro DEBUG_FOO (for rewrite class FOO) as follows:

#define DEBUG_FOO(a,b,c,d,e) print_rule(a,b,c,d,e)

template <class T>
  T print_rule(T replacement, T redex,
               const char * file_name,
               int line, const char * rule_text)
  { cerr << file_name << ':' << line << ": " << rule_text
         << " redex = " << redex << " replacement = " << replacement
         << endl;
    return replacement;
  }

Note that these definitions must appear before the rewrite FOO declaration.