[m-rev.] for review: higher order declarative debugging

[Mark Brown]

On 02-May-2002, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> On 02-May-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > There is still a problem in that the
> > declarative debugger back end does not filter out external events for
> > higher order calls.
> 
> I don't understand this comment. What problem are you referring to?
> 
> > +:- type decl_atom_map(V) == tree234_cc(decl_atom, V).
> > +
> 
> Please don't embed the key type in there. In my change to add I/O actions
> to the declarative debugger, I am already distinguishing between decl_atoms
> that correspond to exits from those that correspond to calls, since only the
> former can have a sequence of associated I/O actions. This means that different
> maps in the oracle state have different key types. A definition such as
> 
> :- type map_cc(K, V) == tree234_cc(K, V).
> 
> would be much more appropriate.
> 
> > +% since this is the determinism of compare_representation.  Semidet
> > +% predicates, however, are now cc_multi.
> 
> That last sentence should be something like
> 
> Even predicates that used to be semidet are now cc_multi, since ...
> 
> Apart from those comments, the diff is fine. The sooner you commit it,
> the fewer conflicts I will get in declarative_oracle.m.
> 
> Zoltan.

Thanks.  I'll commit it now, with the following modification:

--- log1	Thu May  2 17:16:02 2002
+++ log	Thu May  2 17:17:40 2002
@@ -11,8 +11,10 @@
 This completes the changes to the declarative debugger to support the
 debugging of higher order code.  (There is still a problem in that the
 declarative debugger back end does not filter out external events for
-higher order calls.  But that is an unrelated problem, which I will
-deal with separately.)
+higher order calls.  This means that the declarative debugger asks
+questions about what are effectively calls to call/N, which is not
+necessary since we assume that call/N is correct.  This is a problem
+unrelated to this change, so I will deal with it separately.)
 
 browser/tree234_cc.m:
 	The new sub-module of mdb, which implements the 234-trees.
diff -u browser/declarative_oracle.m browser/declarative_oracle.m
--- browser/declarative_oracle.m
+++ browser/declarative_oracle.m
@@ -154,27 +154,27 @@
 		% case that the user supplies a truth value for a
 		% "wrong answer" node.
 		%
-		decl_atom_map(decl_truth),
+		map_cc(decl_atom, decl_truth),
 
 		% Mapping from call atoms to their solution sets.
 		% The sets in this map are all complete---but they may
 		% contain wrong answers.
 		%
-		decl_atom_map(set(decl_atom)),
+		map_cc(decl_atom, set(decl_atom)),
 
 		% Mapping from call atoms to their solution sets.
 		% The sets in this map are all incomplete---there
 		% exists a correct solution which is not in the set.
 		%
-		decl_atom_map(set(decl_atom)),
+		map_cc(decl_atom, set(decl_atom)),
 
 		% Mapping from call atoms to information about which
 		% exceptions are possible or impossible.
 		%
-		decl_atom_map(known_exceptions)
+		map_cc(decl_atom, known_exceptions)
 	).
 
-:- type decl_atom_map(V) == tree234_cc(decl_atom, V).
+:- type map_cc(K, V) == tree234_cc(K, V).
 
 :- type known_exceptions
 	--->	known_excp(
@@ -191,44 +191,44 @@
 	tree234_cc__init(N),
 	tree234_cc__init(X).
 
-:- pred get_kb_ground_map(oracle_kb, decl_atom_map(decl_truth)).
+:- pred get_kb_ground_map(oracle_kb, map_cc(decl_atom, decl_truth)).
 :- mode get_kb_ground_map(in, out) is det.
 
 get_kb_ground_map(oracle_kb(Map, _, _, _), Map).
 
-:- pred set_kb_ground_map(oracle_kb, decl_atom_map(decl_truth), oracle_kb).
+:- pred set_kb_ground_map(oracle_kb, map_cc(decl_atom, decl_truth), oracle_kb).
 :- mode set_kb_ground_map(in, in, out) is det.
 
 set_kb_ground_map(oracle_kb(_, Y, N, X), G, oracle_kb(G, Y, N, X)).
 
-:- pred get_kb_complete_map(oracle_kb, decl_atom_map(set(decl_atom))).
+:- pred get_kb_complete_map(oracle_kb, map_cc(decl_atom, set(decl_atom))).
 :- mode get_kb_complete_map(in, out) is det.
 
 get_kb_complete_map(oracle_kb(_, Map, _, _), Map).
 
-:- pred set_kb_complete_map(oracle_kb, decl_atom_map(set(decl_atom)),
+:- pred set_kb_complete_map(oracle_kb, map_cc(decl_atom, set(decl_atom)),
 		oracle_kb).
 :- mode set_kb_complete_map(in, in, out) is det.
 
 set_kb_complete_map(oracle_kb(G, _, N, X), Y, oracle_kb(G, Y, N, X)).
 
-:- pred get_kb_incomplete_map(oracle_kb, decl_atom_map(set(decl_atom))).
+:- pred get_kb_incomplete_map(oracle_kb, map_cc(decl_atom, set(decl_atom))).
 :- mode get_kb_incomplete_map(in, out) is det.
 
 get_kb_incomplete_map(oracle_kb(_, _, Map, _), Map).
 
-:- pred set_kb_incomplete_map(oracle_kb, decl_atom_map(set(decl_atom)),
+:- pred set_kb_incomplete_map(oracle_kb, map_cc(decl_atom, set(decl_atom)),
 		oracle_kb).
 :- mode set_kb_incomplete_map(in, in, out) is det.
 
 set_kb_incomplete_map(oracle_kb(G, Y, _, X), N, oracle_kb(G, Y, N, X)).
 
-:- pred get_kb_exceptions_map(oracle_kb, decl_atom_map(known_exceptions)).
+:- pred get_kb_exceptions_map(oracle_kb, map_cc(decl_atom, known_exceptions)).
 :- mode get_kb_exceptions_map(in, out) is det.
 
 get_kb_exceptions_map(oracle_kb(_, _, _, Map), Map).
 
-:- pred set_kb_exceptions_map(oracle_kb, decl_atom_map(known_exceptions),
+:- pred set_kb_exceptions_map(oracle_kb, map_cc(decl_atom, known_exceptions),
 		oracle_kb).
 :- mode set_kb_exceptions_map(in, in, out) is det.
 
diff -u browser/tree234_cc.m browser/tree234_cc.m
--- browser/tree234_cc.m
+++ browser/tree234_cc.m
@@ -19,9 +19,11 @@
 % behaviour may be acceptable.
 %
 % A flow on effect is that most of the det predicates are now cc_multi,
-% since this is the determinism of compare_representation.  Semidet
-% predicates, however, are now cc_multi.  They return all outputs in a
-% maybe type, which indicates success or failure.
+% since this is the determinism of compare_representation.  Even
+% predicates that used to be semidet are now cc_multi, since they need
+% to be called just after calls to other committed choice procedures
+% which means that they are not allowed to fail.  They return all outputs
+% in a maybe type, which indicates success or failure.
 % 
 % main author: conway.
 % stability: medium.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------