More, on backtracking problem..

[brad@cs.adelaide.edu.au (Bradley Alexander)]

Hello, 
      I've tried to narrow the scope of the debugger problem down
further and have found some interesting behaviour.

I have (by using the fail button on the debugger) found that my
definition backtracks almost to the first rule invoked. This 
is convenient because it allows me to describe the problem using 
just two typol rules. The following is a description of what happens.


I have an Adl program of the general form (in abstract syntax)

  let( decls[....], <expression> )

The expression part has been deliberatley badly typed so that
the type checker that I've defined for Adl will fail (it is 
an "if" expression with consequent and alternative of differing
types). The problem that I was trying to solve was that my
typechecker made more attempts than I thought the rules would
allow to prove the program correct (i.e. it seemed that I had
multiple solutions to some rules that I didn't want). 

When I execute the typechecker on this program in debug mode I 
first encounter the rule..

 eval_type(typenv[] |- E => T)
 -----------------------------
  |- E;

The next rule used (and the only one applicable at this point) is
in the set eval_type, it is:


 TE |- D:TE' & TE' |- E => T
 ----------------------------
  TE |- let(D,E) => T;

The top line of the rule is (or should be) irrelevant because I
press the "fail" button at this point. The debugger displays
"fail" in its status panel. 

Next I press the "step" button and instead of redisplaying the 
first rule with "fail" in the status panel the debugger behaves as
if I have pressed go and another potential solution is found
because it makes four attempts (on this particular program) to find
the solution (I'm able to tell because I've inserted write() statements 
in my typol definition).

If I press fail when the first rule is displayed then the program
fails without attempting any other rules.

Is it possible that there could be some feature in the definition of
the rule handling the "let" that causes this behaviour (The debugger
is usually very reliable).

Thanks,

Brad Alexander.