[m-dev.] proposed command set for the internal trace based debugger

[Fergus Henderson]

On 02-Jun-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> > > You seem to have omitted the REDO port.  That one's pretty important.
> > 
> > Our execution mechanism optimizes away the REDO port.
> > Instead, execution jumps directly to the place where execution will
> > resume (i.e. a DISJ port).  
> 
> That sounds like what you should show, then.  But how is this different from
> a REDO port anyway?  Let me put it this way:  I don't want to step through a
> hundred redo-fail pairs.  Arriving immediately at the first REDO port that
> has a chance of succeeding is fine with me.  That's what the Quintus
> debugger does, too. 

It's not just skipping REDO-FAIL pairs, you also skipped some unmatched REDOs.
Also the DISJ port which you jump to may not be in the same predicate. 
So if you have a spypoint on a predicate, you won't necessarily
catch all the REDOs into that predicate.

For example:

	:- mode p(out) is nondet.
	p(X) :- q(X).

	:- mode q(out) is nondet.
	q(1).
	q(2).

	main --> ( { p(X), X > 1 } -> print(X), nl ; print("no"), nl ).

The trace for this, with "REDO" ports inserted, looks like this:

       1:      1  1 CALL CCMUL foo:main/2-0 
       2:      2  2 CALL NON   foo:p/1-0 
       3:      3  3 CALL NON   foo:q/1-0 
       4:      3  3 DISJ NON   foo:q/1-0 d1;
       5:      3  3 EXIT NON   foo:q/1-0 
       6:      2  2 EXIT NON   foo:p/1-0 
[[[   R1:      2  2 REDO NON   foo:p/1-0		]]]
[[[   R2:      3  3 REDO NON   foo:q/1-0		]]]
       7:      3  3 DISJ NON   foo:q/1-0 d2;
       8:      3  3 EXIT NON   foo:q/1-0 
       9:      2  2 EXIT NON   foo:p/1-0 
      10:      1  1 THEN CCMUL foo:main/2-0 t;
      11:      1  1 EXIT CCMUL foo:main/2-0 

The lines marked [[[...]]] are the ones that the current debugger
does not print.

If I had set a spypoint on p/1, this would cause the debugger
to stop at events 2 (CALL), 6 (EXIT), and 9 (EXIT).

If, for example, the first answer that p/1 returns is
correct but the second is incorrect, this may be a bit difficult
to debug, since I have no way of stopping on re-entry to p/1
to get control at the point where it starts computing the
second answer -- I can only stop on the EXIT port, once it
has already computed the answer.

Thus I think it may be worthwhile for us to implement a proper REDO port.
There is no point in including REDO-FAIL pairs for attempts to
retry goals that didn't create any choice points, but for goals
that did create choice points, a proper REDO port would be useful.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.