[m-dev.] For review: declarative debugging back end (3/3)

[Fergus Henderson]

On 14-Jul-1998, Mark Anthony BROWN <dougl at cs.mu.OZ.AU> wrote:
> % File: evaluation_tree.m
> % Author: dougl
> % Stability: low
> %
> % Purpose:
> % 	This module defines the interface to a Mercury Evaluation
> % 	Dependence Tree (EDT), a data structure that holds the representation
> % 	of a justification of program behaviour in terms of the declarative
> % 	semantics of the language.
> %
> % 	An EDT for which the top node represents an incorrect result
> % 	exhibits a "symptom" (eg: wrong answer, missing answer, etc); an
> % 	EDT which exhibits a symptom, but which contains no direct
> % 	children that exhibit symptoms, is an "error" (eg: incorrect
> % 	clause instance, uncovered atom, etc).
> %
> % Rationale:
> % 	An EDT can be used by a declarative debugger to search for
> % 	errors in terms of symptoms.

You should mention "declarative debugger" somewhere in the first
few lines, so that someone who is not interested in this stuff
can figure it what it is for without having to read down that far.

For example, you could add something like

	% Summary:
	%	This module defines an interface intended to be used by
	%	a (not yet implemented) declarative debugger for Mercury.

at the start.

> This is achieved with a two level
> % 	architecture: a back end generates EDTs for a running program,
> % 	and a front end searches them for errors.
> %
> %	To support this, the interface to an EDT is decoupled from its
> %	implementation.  The front end of a declarative debugger should
> %	use the interface provided for the type evaluation_tree/1 and the
> %	typeclass evaluation_atom/1, and their associated access procedures,
> %	to analyse the EDT.  The back end should provide an instance
> %	of evaluation_atom (NB: this is the purpose of the compiler
> %	module evaluation_tree_gen.m).
> %
> %	The chief advantage of this decoupling is that a debuggee module
> %	(back end) is free to vary the implementation of atoms without
> %	affecting the debugger (ie the compiled debugger does not depend
> %	on the debuggee's representation of atoms).  In particular, this
> %	allows a debugger to be written, compiled and distributed _before_
> %	the debuggee is written, without resorting to the use of the
> %	ground representation.

Huh?

You must still be using a ground representation.
The typeclass interface specifies that the representation must be ground!

> % Design:
> % 	The decoupling is achieved by parametrizing most of the types in
> % 	this module with the type used to represent atoms, which must be
> % 	an instance of the evaluation_atom typeclass.  This module uses
> % 	one of the type variables 'A' or 'E' whenever such a type is
> % 	expected.

What do `A' and `E' stand for?

(It might be clearer to use `Atom' or `AtomType' instead of `A'.
Then again, it might not.)

> 	%
> 	% The front end can request an analysis of a particular atom.
> 	% The back end should generate an element of the following type
> 	% (and inst).
> 	%
> 	
> :- type analysis(A)
> 	--->	nondet_wrong(pred(evaluation_tree(A)))
> 	;	multi_wrong(pred(evaluation_tree(A)))
> 	;	semidet_wrong(pred(evaluation_tree(A)))
> 	;	det_wrong(pred(evaluation_tree(A)))
> 	;	wrong_io(pred(evaluation_tree(A), io__state, io__state))
> 	;	miss(pred(evaluation_tree(A)))
> 	;	miss_io(pred(evaluation_tree(A), io__state, io__state))
> 	;	unavailable.

You should document the meanings of all of these.

miss_io, in particular, is quite mysterious to me.

> %-----------------------------------------------------------------------------%
> %
> % This section contains the interface that the back end must
> % conform to.
> %

You separated this section from the "interface to the back end" section,
but I think they should be together.

In particular, it's hard to understand the `analysis' type unless you
see how it is used.

> 	%
> 	% For wrong answer analysis, the goal justification is a
> 	% proof_tree for a computed answer.
> 	%
> 	
> :- type proof_tree(A)
> 	--->	local_call(evaluation_tree(A))
> %	;	some [E] external_call(evaluation_tree(E))
> %			<= evaluation_atom(E)
> 	;	conj(list(proof_tree(A)))
> 	;	disj(int, proof_tree(A))
> 	;	switch(int, proof_tree(A))
> 	;	if_then(proof_tree(A), proof_tree(A))
> 	;	else(miss_tree(A), proof_tree(A))
> 	;	not(miss_tree(A))
> 	;	trivial.

You should document what the `int's represent.

> 	%
> 	% For missing answer analysis also, the goal justification is a
> 	% tree that corresponds to the structure of the program.  It is
> 	% the dual of the above structure: it represents which atoms
> 	% were _not_ computed answers.
> 	%
> 	
> :- type miss_tree(A)
> 	--->	local_call(evaluation_tree(A))
> %	;	some [E] external_call(evaluation_tree(E))
> %			<= evaluation_atom(E)
> 	;	conj(list(miss_tree(A)))

Shouldn't that be `conj(int)'?

[... to be continued ...] 

-- 
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.