[m-dev.] For review: new DD front end architecture
Mark Anthony BROWN
dougl at cs.mu.OZ.AU
Tue Dec 7 02:25:10 AEDT 1999
Hi,
This is for review by anyone.
Cheers,
Mark.
Estimated hours taken: 120
Implement the new architecture for the front end of the
declarative debugger. Disable declarative debugging if conservative
GC is not being used since this change relies on it. The benefits
of declarative debugging in non-GC grades, if any, are not worth the
extra maintenance required to support it.
browser/declarative_analyser.m:
New module which handles the analysis of EDTs, which was
previously done in browser/declarative_debugger.m.
browser/declarative_debugger.m:
- Change the interface according to the new design.
- Export types of the form decl_*, rather than edt_*.
- Move the EDT analysis to the new module.
- Handle the interaction between the analyser and the oracle.
- Don't interact directly with the user, but go via the oracle.
- New diagnoser state type.
- Update the EDT instance to conform to the other changes.
browser/declarative_oracle.m:
- Replace oracle_answer type with oracle_response.
- Allow the oracle to work with a queue of questions rather
than one at a time.
- Add new predicates to manipulate the knowledge base.
browser/declarative_user.m:
- Export the user_state type.
- Handle some user commands in this module.
- Handle questions properly (apart from printing atoms).
browser/browser_library.m:
Add the new module.
trace/mercury_trace_declarative.c:
- Initialise the front end state just once per session.
- Make the step size much larger, since implicit subtrees
are not fully supported yet.
- Correct the types in a format specifier.
trace/mercury_trace_declarative.c:
trace/mercury_trace_internal.c:
trace/mercury_trace_internal.h:
- Disable declarative debugging unless conservative GC is used.
Index: browser/browser_library.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/browser_library.m,v
retrieving revision 1.7
diff -u -r1.7 browser_library.m
--- browser_library.m 1999/11/30 00:04:23 1.7
+++ browser_library.m 1999/11/30 14:39:17
@@ -15,7 +15,7 @@
:- import_module browse, frame, help, parse, util.
:- import_module debugger_interface.
:- import_module declarative_debugger, declarative_oracle, declarative_user.
-:- import_module declarative_execution.
+:- import_module declarative_execution, declarative_analyser.
:- import_module interactive_query, dl, name_mangle.
:- import_module collect_lib.
Index: browser/declarative_debugger.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_debugger.m,v
retrieving revision 1.6
diff -u -r1.6 declarative_debugger.m
--- declarative_debugger.m 1999/11/30 00:04:24 1.6
+++ declarative_debugger.m 1999/11/30 14:39:17
@@ -21,98 +21,200 @@
:- module declarative_debugger.
:- interface.
-:- import_module io, list, bool.
+:- import_module io, list, bool, std_util.
:- import_module declarative_execution.
% This type represents the possible truth values for nodes
% in the EDT.
%
-:- type edt_truth == bool.
+:- type decl_truth == bool.
- % Values of this type represent EDT nodes. This representation
+ % This type represents the bugs which can be diagnosed.
+ % The parameter of the constructor is the type of EDT nodes.
+ %
+:- type decl_bug(T)
+ ---> e_bug(T) % An EDT whose root node is incorrect,
+ % but whose children are all correct.
+
+ ; i_bug(T). % An EDT whose root node is incorrect, and
+ % which has no incorrect children but at
+ % least one inadmissible one.
+
+ % Values of this type represent goal behaviour. This representation
% is used by the front end (in this module), as well as the
% oracle and user interface.
%
-:- type edt_node
+:- type decl_question
% The node is a suspected wrong answer. The
% argument is the atom in its final state of
% instantiatedness (ie. at the EXIT event).
%
- ---> wrong_answer(edt_atom)
+ ---> wrong_answer(decl_atom)
% The node is a suspected missing answer. The
% first argument is the atom in its initial state
% of instantiatedness (ie. at the CALL event),
% and the second argument is the list of solutions.
%
- ; missing_answer(edt_atom, list(edt_atom)).
+ ; missing_answer(decl_atom, list(decl_atom)).
-:- type edt_atom == trace_atom.
+:- type decl_answer == pair(decl_question, decl_truth).
- % This typeclass represents a declarative view of execution.
- %
-:- typeclass mercury_edt(S, T) where [
- pred edt_root(S, T, edt_node),
- mode edt_root(in, in, out) is det,
-
- pred edt_children(S, T, list(T)),
- mode edt_children(in, in, out) is det
-].
+:- type decl_atom == trace_atom.
% The diagnoser eventually responds with a value of this type
- % when it is called.
+ % after it is called.
%
% XXX need to have a case for expanding an implicit tree.
%
:- type diagnoser_response
- ---> bug_found(edt_node)
+ ---> bug_found
; no_bug_found.
-
-:- type diagnoser_state.
-:- pred diagnoser_state_init(diagnoser_state).
-:- mode diagnoser_state_init(out) is det.
+:- type diagnoser_state(R).
-:- pred diagnosis(io__input_stream, io__output_stream, S, trace_node(R),
- diagnoser_response, diagnoser_state, diagnoser_state,
- io__state, io__state) <= execution_tree(S, R).
-:- mode diagnosis(in, in, in, in, out, in, out, di, uo) is det.
+:- pred diagnoser_state_init(io__input_stream, io__output_stream,
+ diagnoser_state(R)).
+:- mode diagnoser_state_init(in, in, out) is det.
+
+:- pred diagnosis(S, R, diagnoser_response, diagnoser_state(R),
+ diagnoser_state(R), io__state, io__state)
+ <= execution_tree(S, R).
+:- mode diagnosis(in, in, out, in, out, di, uo) is det.
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module require, int, char.
-:- import_module declarative_oracle, declarative_user.
+:- import_module declarative_analyser, declarative_oracle.
+
+:- type diagnoser_state(R)
+ ---> diagnoser(
+ analyser_state(edt_node(R)),
+ oracle_state
+ ).
+
+:- pred diagnoser_get_analyser(diagnoser_state(R),
+ analyser_state(edt_node(R))).
+:- mode diagnoser_get_analyser(in, out) is det.
+
+diagnoser_get_analyser(diagnoser(Analyser, _), Analyser).
+
+:- pred diagnoser_set_analyser(diagnoser_state(R), analyser_state(edt_node(R)),
+ diagnoser_state(R)).
+:- mode diagnoser_set_analyser(in, in, out) is det.
+
+diagnoser_set_analyser(diagnoser(_, B), A, diagnoser(A, B)).
+
+:- pred diagnoser_get_oracle(diagnoser_state(R), oracle_state).
+:- mode diagnoser_get_oracle(in, out) is det.
+
+diagnoser_get_oracle(diagnoser(_, Oracle), Oracle).
+
+:- pred diagnoser_set_oracle(diagnoser_state(R), oracle_state,
+ diagnoser_state(R)).
+:- mode diagnoser_set_oracle(in, in, out) is det.
+
+diagnoser_set_oracle(diagnoser(A, _), B, diagnoser(A, B)).
+
+diagnoser_state_init(InStr, OutStr, Diagnoser) :-
+ analyser_state_init(Analyser),
+ oracle_state_init(InStr, OutStr, Oracle),
+ Diagnoser = diagnoser(Analyser, Oracle).
+
+diagnosis(Store, NodeId, Response, Diagnoser0, Diagnoser) -->
+ { diagnoser_get_analyser(Diagnoser0, Analyser0) },
+ { start_analysis(wrap(Store), dynamic(NodeId), AnalyserResponse,
+ Analyser0, Analyser) },
+ { diagnoser_set_analyser(Diagnoser0, Analyser, Diagnoser1) },
+ handle_analyser_response(Store, AnalyserResponse, Response,
+ Diagnoser1, Diagnoser).
+
+:- pred handle_analyser_response(S, analyser_response(edt_node(R)),
+ diagnoser_response, diagnoser_state(R), diagnoser_state(R),
+ io__state, io__state) <= execution_tree(S, R).
+:- mode handle_analyser_response(in, in, out, in, out, di, uo) is det.
-:- type diagnoser_state == oracle_state.
+handle_analyser_response(_, no_suspects, no_bug_found, D, D) -->
+ [].
+
+handle_analyser_response(Store, bug_found(Bug), Response, D, D) -->
+ confirm_bug(Store, Bug, Confirmed),
+ {
+ Confirmed = yes,
+ Response = bug_found
+ ;
+ Confirmed = no,
+ Response = no_bug_found
+ }.
+
+handle_analyser_response(Store, oracle_queries(Queries), Response,
+ Diagnoser0, Diagnoser) -->
+
+ { diagnoser_get_oracle(Diagnoser0, Oracle0) },
+ query_oracle(Queries, OracleResponse, Oracle0, Oracle),
+ { diagnoser_set_oracle(Diagnoser0, Oracle, Diagnoser1) },
+ handle_oracle_response(Store, OracleResponse, Response, Diagnoser1,
+ Diagnoser).
+
+handle_analyser_response(_, require_explicit(_), _, _, _) -->
+ { error("diagnosis: implicit representation not yet implemented") }.
+
+:- pred handle_oracle_response(S, oracle_response, diagnoser_response,
+ diagnoser_state(R), diagnoser_state(R), io__state, io__state)
+ <= execution_tree(S, R).
+:- mode handle_oracle_response(in, in, out, in, out, di, uo) is det.
+
+handle_oracle_response(Store, oracle_answers(Answers), Response, Diagnoser0,
+ Diagnoser) -->
+
+ { diagnoser_get_analyser(Diagnoser0, Analyser0) },
+ { continue_analysis(wrap(Store), Answers, AnalyserResponse,
+ Analyser0, Analyser) },
+ { diagnoser_set_analyser(Diagnoser0, Analyser, Diagnoser1) },
+ handle_analyser_response(Store, AnalyserResponse, Response,
+ Diagnoser1, Diagnoser).
+
+handle_oracle_response(_, no_oracle_answers, no_bug_found, D, D) -->
+ [].
-:- pragma export(diagnoser_state_init(out),
- "MR_DD_diagnoser_state_init").
+handle_oracle_response(_, abort_diagnosis, no_bug_found, D, D) -->
+ io__write_string("Diagnosis aborted.\n").
+
+:- pred confirm_bug(S, decl_bug(edt_node(R)), bool, io__state, io__state)
+ <= execution_tree(S, R).
+:- mode confirm_bug(in, in, out, di, uo) is det.
-diagnoser_state_init(Oracle) :-
- oracle_state_init(Oracle).
-
-diagnosis(MdbIn, MdbOut, Store, Node, Response, State0, State) -->
- io__set_input_stream(MdbIn, OldIn),
- io__set_output_stream(MdbOut, OldOut),
- analyse_edt(wrap(Store), Node, Response, State0, State),
- io__set_input_stream(OldIn, _),
- io__set_output_stream(OldOut, _).
+confirm_bug(_, Bug, yes) -->
+ io__write(Bug), % XXX this doesn't work very well.
+ io__nl.
+ % Export a monomorphic version of diagnosis_state_init/4, to
+ % make it easier to call from C code.
+ %
+:- pred diagnoser_state_init_store(io__input_stream, io__output_stream,
+ diagnoser_state(trace_node_id)).
+:- mode diagnoser_state_init_store(in, in, out) is det.
+
+:- pragma export(diagnoser_state_init_store(in, in, out),
+ "MR_DD_decl_diagnosis_state_init").
+
+diagnoser_state_init_store(InStr, OutStr, Diagnoser) :-
+ diagnoser_state_init(InStr, OutStr, Diagnoser).
+
% Export a monomorphic version of diagnosis/9, to make it
% easier to call from C code.
%
-:- pred diagnosis_store(io__input_stream, io__output_stream,
- trace_node_store, trace_node(trace_node_id),
- diagnoser_response, diagnoser_state, diagnoser_state,
+:- pred diagnosis_store(trace_node_store, trace_node_id, diagnoser_response,
+ diagnoser_state(trace_node_id), diagnoser_state(trace_node_id),
io__state, io__state).
-:- mode diagnosis_store(in, in, in, in, out, in, out, di, uo) is det.
+:- mode diagnosis_store(in, in, out, in, out, di, uo) is det.
-:- pragma export(diagnosis_store(in, in, in, in, out, in, out, di, uo),
+:- pragma export(diagnosis_store(in, in, out, in, out, di, uo),
"MR_DD_decl_diagnosis").
-diagnosis_store(In, Out, Store, Node, Response, State0, State) -->
- diagnosis(In, Out, Store, Node, Response, State0, State).
+diagnosis_store(Store, Node, Response, State0, State) -->
+ diagnosis(Store, Node, Response, State0, State).
%-----------------------------------------------------------------------------%
@@ -121,7 +223,10 @@
% any instance of execution tree.
%
-:- instance mercury_edt(wrap(S), trace_node(R)) <= execution_tree(S, R)
+:- type edt_node(R)
+ ---> dynamic(R).
+
+:- instance mercury_edt(wrap(S), edt_node(R)) <= execution_tree(S, R)
where [
pred(edt_root/3) is trace_root,
pred(edt_children/3) is trace_children
@@ -130,12 +235,13 @@
% The wrap/1 around the first argument of the instance is
% required by the language.
%
-:- type wrap(T) ---> wrap(T).
+:- type wrap(S) ---> wrap(S).
-:- pred trace_root(wrap(S), trace_node(R), edt_node) <= execution_tree(S, R).
+:- pred trace_root(wrap(S), edt_node(R), decl_question) <= execution_tree(S, R).
:- mode trace_root(in, in, out) is det.
-trace_root(wrap(Store), Node, Root) :-
+trace_root(wrap(Store), dynamic(Ref), Root) :-
+ det_trace_node_from_id(Store, Ref, Node),
(
Node = fail(_, CallId)
->
@@ -151,7 +257,7 @@
error("trace_root: not an EXIT or FAIL node")
).
-:- pred get_answers(S, R, list(edt_atom), list(edt_atom))
+:- pred get_answers(S, R, list(decl_atom), list(decl_atom))
<= execution_tree(S, R).
:- mode get_answers(in, in, in, out) is det.
@@ -165,11 +271,18 @@
As = As0
).
-:- pred trace_children(wrap(S), trace_node(R), list(trace_node(R)))
+:- pred trace_children(wrap(S), edt_node(R), list(edt_node(R)))
<= execution_tree(S, R).
-:- mode trace_children(in, in, out) is det.
+:- mode trace_children(in, in, out) is semidet.
-trace_children(wrap(Store), Node, Children) :-
+trace_children(wrap(Store), dynamic(Ref), Children) :-
+
+ % This is meant to fail if the children are implicit,
+ % but this is not yet implemented.
+ %
+ semidet_succeed,
+
+ det_trace_node_from_id(Store, Ref, Node),
(
Node = fail(PrecId, _)
->
@@ -182,7 +295,7 @@
error("trace_children: not an EXIT or FAIL node")
).
-:- pred wrong_answer_children(S, R, list(trace_node(R)), list(trace_node(R)))
+:- pred wrong_answer_children(S, R, list(edt_node(R)), list(edt_node(R)))
<= execution_tree(S, R).
:- mode wrong_answer_children(in, in, in, out) is det.
@@ -197,14 +310,14 @@
;
Node = exit(_, Call, _, _),
call_node_from_id(Store, Call, call(Prec, _, _)),
- wrong_answer_children(Store, Prec, [Node | Ns0], Ns)
+ wrong_answer_children(Store, Prec, [dynamic(NodeId) | Ns0], Ns)
;
Node = redo(_, _),
error("wrong_answer_children: unexpected REDO node")
;
Node = fail(_, Call),
call_node_from_id(Store, Call, call(Prec, _, _)),
- wrong_answer_children(Store, Prec, [Node | Ns0], Ns)
+ wrong_answer_children(Store, Prec, [dynamic(NodeId) | Ns0], Ns)
;
Node = cond(Prec, _, Flag),
(
@@ -240,7 +353,7 @@
wrong_answer_children(Store, Back, Ns1, Ns)
).
-:- pred missing_answer_children(S, R, list(trace_node(R)), list(trace_node(R)))
+:- pred missing_answer_children(S, R, list(edt_node(R)), list(edt_node(R)))
<= execution_tree(S, R).
:- mode missing_answer_children(in, in, in, out) is det.
@@ -261,7 +374,7 @@
;
call_node_from_id(Store, Call, call(Prec, _, _))
),
- wrong_answer_children(Store, Prec, [Node | Ns0], Ns)
+ wrong_answer_children(Store, Prec, [dynamic(NodeId) | Ns0], Ns)
;
Node = redo(_, Exit),
exit_node_from_id(Store, Exit, exit(Prec, _, _, _)),
@@ -276,7 +389,8 @@
;
Next = Back
),
- missing_answer_children(Store, Next, [Node | Ns0], Ns)
+ missing_answer_children(Store, Next, [dynamic(NodeId) | Ns0],
+ Ns)
;
Node = cond(Prec, _, Flag),
(
@@ -310,130 +424,4 @@
neg_node_from_id(Store, Neg, neg(Back, _, _)),
missing_answer_children(Store, Back, Ns1, Ns)
).
-
-
-%-----------------------------------------------------------------------------%
-
- %
- % This section implements the analysis.
- % It is passed an EDT, which is analysed to find a cause of the bug,
- % and this bug is then presented to the user.
- %
- % The current implementation uses a simple top-down strategy to
- % analyse the EDT.
- %
-
- %
- % This is what the analysis can currently find.
- %
-
-:- type declarative_bug(T) % <= evaluation_tree(T)
- ---> not_found
- %
- % An e_bug is an EDT whose root node is incorrect, but
- % whose children are all correct.
- %
- ; e_bug(T).
-
-
-:- pred analyse_edt(S, T, diagnoser_response, oracle_state,
- oracle_state, io__state, io__state) <= mercury_edt(S, T).
-:- mode analyse_edt(in, in, out, in, out, di, uo) is det.
-
-analyse_edt(Store, EDT, no_bug_found, Oracle0, Oracle) -->
- { edt_root(Store, EDT, RootNode) },
- query_oracle(RootNode, Answer, Oracle0, Oracle1),
- (
- { Answer = truth_value(yes) },
- { Bug = not_found },
- { Oracle = Oracle1 }
- ;
- { Answer = truth_value(no) },
- analyse_edt_2(Store, EDT, Bug, Oracle1, Oracle)
- ;
- { Answer = deferred(_) },
- { Bug = not_found },
- { Oracle = Oracle1 }
- ),
- report_bug(Store, Bug).
-
-
- %
- % Assumes the root note is not valid.
- %
-:- pred analyse_edt_2(S, T, declarative_bug(T), oracle_state, oracle_state,
- io__state, io__state) <= mercury_edt(S, T).
-:- mode analyse_edt_2(in, in, out, in, out, di, uo) is det.
-
-analyse_edt_2(Store, EDT, Bug, Oracle0, Oracle) -->
- { edt_children(Store, EDT, Children) },
- analyse_children(Store, Children, e_bug(EDT), Bug, Oracle0, Oracle).
-
-
-:- pred analyse_children(S, list(T), declarative_bug(T), declarative_bug(T),
- oracle_state, oracle_state, io__state, io__state)
- <= mercury_edt(S, T).
-:- mode analyse_children(in, in, in, out, in, out, di, uo) is det.
-
-analyse_children(_, [], Bug, Bug, Oracle, Oracle) -->
- [].
-analyse_children(Store, [Child | Children], Bug0, Bug, Oracle0, Oracle) -->
- { edt_root(Store, Child, ChildNode) },
- query_oracle(ChildNode, Answer, Oracle0, Oracle1),
- (
- { Answer = truth_value(yes) },
- analyse_children(Store, Children, Bug0, Bug, Oracle1, Oracle)
- ;
- { Answer = truth_value(no) },
- analyse_edt_2(Store, Child, Bug, Oracle1, Oracle)
- ;
- { Answer = deferred(_) },
- { append(Children, [Child], NewChildren) },
- analyse_children(Store, NewChildren, Bug0, Bug, Oracle1,
- Oracle)
- ).
-
-
-:- pred report_bug(S, declarative_bug(T), io__state, io__state)
- <= mercury_edt(S, T).
-:- mode report_bug(in, in, di, uo) is det.
-
-report_bug(_, not_found) -->
- io__write_string("Bug not found.\n").
-report_bug(Store, e_bug(EDT)) -->
- io__write_string("Incorrect instance found:\n\n"),
- write_root_node(Store, EDT),
- { edt_children(Store, EDT, Children0) },
- (
- { Children0 = [Child | Children1] }
- ->
- io__write_string(" :-\n"),
- { list__reverse(Children1, Children) },
- write_children(Store, Children),
- io__write_char('\t'),
- write_root_node(Store, Child)
- ;
- []
- ),
- io__write_string(".\n\n").
-
-
-:- pred write_children(S, list(T), io__state, io__state) <= mercury_edt(S, T).
-:- mode write_children(in, in, di, uo) is det.
-
-write_children(_, []) -->
- [].
-write_children(Store, [Child | Children]) -->
- io__write_char('\t'),
- write_root_node(Store, Child),
- io__write_string(",\n"),
- write_children(Store, Children).
-
-
-:- pred write_root_node(S, T, io__state, io__state) <= mercury_edt(S, T).
-:- mode write_root_node(in, in, di, uo) is det.
-
-write_root_node(Store, EDT) -->
- { edt_root(Store, EDT, RootNode) },
- write_edt_node(RootNode).
Index: browser/declarative_oracle.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_oracle.m,v
retrieving revision 1.4
diff -u -r1.4 declarative_oracle.m
--- declarative_oracle.m 1999/08/20 06:47:24 1.4
+++ declarative_oracle.m 1999/11/30 14:39:17
@@ -3,7 +3,7 @@
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%-----------------------------------------------------------------------------%
-% File: declarative_debugger.m
+% File: declarative_oracle.m
% Author: Mark Brown
% Purpose:
% This module implements the oracle for a Mercury declarative debugger.
@@ -24,92 +24,100 @@
:- module declarative_oracle.
:- interface.
-:- import_module io.
-:- import_module declarative_debugger, declarative_user.
+:- import_module declarative_debugger.
+:- import_module list, io.
+ % A response that the oracle gives to the caller.
%
+:- type oracle_response
+ ---> oracle_answers(list(decl_answer))
+ ; no_oracle_answers
+ ; abort_diagnosis.
+
% The oracle state. This is threaded around the declarative
% debugger.
%
:- type oracle_state.
+ % Produce a new oracle state.
%
- % A response that the oracle gives to the caller. This is
- % a truth value, if available, or else an indication of why
- % the query cannot be answered yet. For deferred answers
- % the argument is the user response, which will not be a truth
- % value (since, if it was, the truth_value/1 constructor would
- % be used).
- %
-:- type oracle_answer
- ---> truth_value(edt_truth)
- ; deferred(user_response).
+:- pred oracle_state_init(io__input_stream, io__output_stream, oracle_state).
+:- mode oracle_state_init(in, in, out) is det.
- %
% Query the oracle about the program being debugged. The first
- % argument is a node in the evaluation tree, the second argument
- % is the oracle response. The oracle state is threaded through
- % so its contents can be updated after user responses.
+ % argument is a queue of nodes in the evaluation tree, the second
+ % argument is the oracle response to any of these. The oracle
+ % state is threaded through so its contents can be updated after
+ % user responses.
%
-:- pred query_oracle(edt_node, oracle_answer, oracle_state, oracle_state,
- io__state, io__state).
+:- pred query_oracle(list(decl_question), oracle_response, oracle_state,
+ oracle_state, io__state, io__state).
:- mode query_oracle(in, out, in, out, di, uo) is det.
- %
- % Produce a new oracle state.
- %
-:- pred oracle_state_init(oracle_state).
-:- mode oracle_state_init(out) is det.
-
%-----------------------------------------------------------------------------%
:- implementation.
-:- import_module bool, list, char, require, std_util, string, map.
-:- import_module declarative_user, util, browse.
+:- import_module declarative_user, util.
+:- import_module bool, std_util, map, set.
+query_oracle(Queries, Response, Oracle0, Oracle) -->
+ { get_oracle_kb(Oracle0, KB0) },
+ { list__filter_map(query_oracle_kb(KB0), Queries, Answers) },
+ (
+ { Answers = [] }
+ ->
+ { get_oracle_user(Oracle0, User0) },
+ query_user(Queries, UserResponse, User0, User),
+ {
+ UserResponse = user_answer(Answer),
+ assert_oracle_kb(Answer, KB0, KB),
+ Response = oracle_answers([Answer])
+ ;
+ UserResponse = no_user_answer,
+ Response = no_oracle_answers,
+ KB = KB0
+ ;
+ UserResponse = abort_diagnosis,
+ Response = abort_diagnosis,
+ KB = KB0
+ },
+ { set_oracle_kb(Oracle0, KB, Oracle1) },
+ { set_oracle_user(Oracle1, User, Oracle) }
+ ;
+ { Response = oracle_answers(Answers) },
+ { Oracle = Oracle0 }
+ ).
+
:- type oracle_state
---> oracle(
-% browser_state, % XXX not used yet
- oracle_kb
+ oracle_kb, % Knowledge base.
+ user_state % User interface.
).
-oracle_state_init(oracle(KB)) :-
- oracle_kb_init(KB).
+oracle_state_init(InStr, OutStr, Oracle) :-
+ user_state_init(InStr, OutStr, User),
+ oracle_kb_init(KB),
+ Oracle = oracle(KB, User).
-
:- pred get_oracle_kb(oracle_state, oracle_kb).
:- mode get_oracle_kb(in, out) is det.
-get_oracle_kb(oracle(KB), KB).
+get_oracle_kb(oracle(KB, _), KB).
:- pred set_oracle_kb(oracle_state, oracle_kb, oracle_state).
:- mode set_oracle_kb(in, in, out) is det.
-set_oracle_kb(oracle(_), KB, oracle(KB)).
+set_oracle_kb(oracle(_, UI), KB, oracle(KB, UI)).
-query_oracle(Node, Answer, Oracle0, Oracle) -->
- (
- { query_oracle_kb(Node, Oracle0, KBTruth, _KBAssumption) }
- ->
- { Answer = truth_value(KBTruth) },
- { Oracle = Oracle0 }
- ;
- query_user(Node, Answer),
- {
- Answer = truth_value(Truth),
- %
- % We don't need to check the consistency of this
- % assertion because we only get here if the KB
- % didn't know the answer already.
- %
- add_oracle_assumption(Node, Truth, _Assumption,
- Oracle0, Oracle)
- ;
- Answer = deferred(_),
- Oracle = Oracle0
- }
- ).
+:- pred get_oracle_user(oracle_state, user_state).
+:- mode get_oracle_user(in, out) is det.
+
+get_oracle_user(oracle(_, UI), UI).
+
+:- pred set_oracle_user(oracle_state, user_state, oracle_state).
+:- mode set_oracle_user(in, in, out) is det.
+set_oracle_user(oracle(KB, _), UI, oracle(KB, UI)).
%-----------------------------------------------------------------------------%
@@ -117,62 +125,138 @@
% This section implements the oracle knowledge base, which
% stores anything that the debugger knows about the intended
% interpretation. This can be used to check the correctness
- % of an EDT node. The KB stores items of knowledge, called
- % oracle assumptions, and these can be referred to from outside
- % this module by the use of an identifier.
+ % of an EDT node.
%
- %
% The type of the knowledge base. Other fields may be added in
% the future, such as for assertions made on-the-fly by the user,
% or assertions in the program text.
%
:- type oracle_kb
---> oracle_kb(
- %
+
% For ground atoms, the knowledge is represented directly
% with a map. This is used, for example, in the common
% case that the user supplies a truth value for a
% "wrong answer" node.
%
- map(edt_node, edt_truth)
+ map(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.
+ %
+ map(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.
+ %
+ map(decl_atom, set(decl_atom))
).
+:- pred oracle_kb_init(oracle_kb).
+:- mode oracle_kb_init(out) is det.
- %
- % The type of identifiers for the oracle assumptions.
- %
-:- type oracle_assumption
- %
- % Truth value came from a table of ground atoms.
- %
- ---> ground(edt_node).
+oracle_kb_init(oracle_kb(G, Y, N)) :-
+ map__init(G),
+ map__init(Y),
+ map__init(N).
+:- pred get_kb_ground_map(oracle_kb, map(decl_atom, decl_truth)).
+:- mode get_kb_ground_map(in, out) is det.
-:- pred query_oracle_kb(edt_node, oracle_state, edt_truth, oracle_assumption).
-:- mode query_oracle_kb(in, in, out, out) is semidet.
+get_kb_ground_map(oracle_kb(Map, _, _), Map).
-query_oracle_kb(Node, Oracle, Truth, Assumption) :-
- get_oracle_kb(Oracle, oracle_kb(NodeMap)),
- map__search(NodeMap, Node, Truth),
- Assumption = ground(Node).
+:- pred set_kb_ground_map(oracle_kb, map(decl_atom, decl_truth), oracle_kb).
+:- mode set_kb_ground_map(in, in, out) is det.
+set_kb_ground_map(oracle_kb(_, Y, N), G, oracle_kb(G, Y, N)).
-:- pred add_oracle_assumption(edt_node, edt_truth, oracle_assumption,
- oracle_state, oracle_state).
-:- mode add_oracle_assumption(in, in, out, in, out) is det.
+:- pred get_kb_complete_map(oracle_kb, map(decl_atom, set(decl_atom))).
+:- mode get_kb_complete_map(in, out) is det.
-add_oracle_assumption(Node, Truth, Assumption, Oracle0, Oracle) :-
- get_oracle_kb(Oracle0, oracle_kb(NodeMap0)),
- map__set(NodeMap0, Node, Truth, NodeMap),
- set_oracle_kb(Oracle0, oracle_kb(NodeMap), Oracle),
- Assumption = ground(Node).
+get_kb_complete_map(oracle_kb(_, Map, _), Map).
+:- pred set_kb_complete_map(oracle_kb, map(decl_atom, set(decl_atom)),
+ oracle_kb).
+:- mode set_kb_complete_map(in, in, out) is det.
-:- pred oracle_kb_init(oracle_kb).
-:- mode oracle_kb_init(out) is det.
+set_kb_complete_map(oracle_kb(G, _, N), Y, oracle_kb(G, Y, N)).
+
+:- pred get_kb_incomplete_map(oracle_kb, map(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, map(decl_atom, set(decl_atom)),
+ oracle_kb).
+:- mode set_kb_incomplete_map(in, in, out) is det.
-oracle_kb_init(oracle_kb(NodeMap)) :-
- map__init(NodeMap).
+set_kb_incomplete_map(oracle_kb(G, Y, _), N, oracle_kb(G, Y, N)).
+%-----------------------------------------------------------------------------%
+
+:- pred query_oracle_kb(oracle_kb, decl_question, decl_answer).
+:- mode query_oracle_kb(in, in, out) is semidet.
+
+query_oracle_kb(KB, Node, Node - Truth) :-
+ Node = wrong_answer(Atom),
+ get_kb_ground_map(KB, Map),
+ map__search(Map, Atom, Truth).
+
+query_oracle_kb(KB, Node, Node - Truth) :-
+ Node = missing_answer(Call, Solns),
+ set__list_to_set(Solns, Ss),
+ get_kb_complete_map(KB, CMap),
+ (
+ map__search(CMap, Call, CSs),
+ set__subset(CSs, Ss)
+ ->
+ Truth = yes
+ ;
+ get_kb_incomplete_map(KB, IMap),
+ map__search(IMap, Call, ISs),
+ set__subset(Ss, ISs),
+ Truth = no
+ ).
+
+ % assert_oracle_kb/3 assumes that the asserted fact is consistent
+ % with the current knowledge base. This will generally be the
+ % case, since the user will never be asked questions which
+ % the knowledge base knows anything about.
+ %
+:- pred assert_oracle_kb(decl_answer, oracle_kb, oracle_kb).
+:- mode assert_oracle_kb(in, in, out) is det.
+
+assert_oracle_kb(wrong_answer(Atom) - Truth, KB0, KB) :-
+ get_kb_ground_map(KB0, Map0),
+ map__det_insert(Map0, Atom, Truth, Map),
+ set_kb_ground_map(KB0, Map, KB).
+
+assert_oracle_kb(missing_answer(Call, Solns) - yes, KB0, KB) :-
+ get_kb_complete_map(KB0, Map0),
+ set__list_to_set(Solns, Ss0),
+ (
+ map__search(Map0, Call, OldSs)
+ ->
+ % The sets are both complete, so their
+ % intersection must be also.
+ %
+ set__intersect(OldSs, Ss0, Ss),
+ map__set(Map0, Call, Ss, Map)
+ ;
+ map__det_insert(Map0, Call, Ss0, Map)
+ ),
+ set_kb_complete_map(KB0, Map, KB).
+
+assert_oracle_kb(missing_answer(Call, Solns) - no, KB0, KB) :-
+ get_kb_incomplete_map(KB0, Map0),
+ set__list_to_set(Solns, Ss),
+ %
+ % XXX should also keep the old incomplete set around, too.
+ % It can still give us information that the new one can't.
+ %
+ map__set(Map0, Call, Ss, Map),
+ set_kb_incomplete_map(KB0, Map, KB).
Index: browser/declarative_user.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_user.m,v
retrieving revision 1.2
diff -u -r1.2 declarative_user.m
--- declarative_user.m 1999/11/30 00:04:26 1.2
+++ declarative_user.m 1999/11/30 14:39:17
@@ -14,94 +14,155 @@
:- module declarative_user.
:- interface.
-:- import_module declarative_debugger, declarative_oracle.
+:- import_module declarative_debugger.
+:- import_module list, io.
- %
+:- type user_response
+ ---> user_answer(decl_answer)
+ ; no_user_answer
+ ; abort_diagnosis.
+
+:- type user_state.
+
+:- pred user_state_init(io__input_stream, io__output_stream, user_state).
+:- mode user_state_init(in, in, out) is det.
+
% This predicate handles the interactive part of the declarative
% debugging process. The user is presented with an EDT node,
% and is asked to respond about the truth of the node in the
% intended interpretation.
- %
-
-:- pred query_user(edt_node, oracle_answer, io__state, io__state).
-:- mode query_user(in, out, di, uo) is det.
-
- %
- % Display the node in user readable form on the current
- % output stream.
%
-:- pred write_edt_node(edt_node, io__state, io__state).
-:- mode write_edt_node(in, di, uo) is det.
+:- pred query_user(list(decl_question), user_response, user_state, user_state,
+ io__state, io__state).
+:- mode query_user(in, out, in, out, di, uo) is det.
+
+% :- pred confirm_user(list(decl_answer), user_response, user_state, user_state,
+% io__state, io__state).
+% :- mode confirm_user(in, out, in, out, di, uo) is det.
- %
- % These are the responses the user can give.
- %
-:- type user_response
- ---> yes % The node is correct.
- ; no % The node is incorrect.
- ; inadmissible % The node is inadmissible.
- ; do_not_know % The user has no answer.
- ; browse % Browse the data before answering.
- ; tree % Browse the EDT.
- ; help % Request help before answering.
- ; illegal_command. % None of the above.
-
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module declarative_execution, util.
-:- import_module std_util, io, bool, list, char, string.
+:- import_module std_util, char, string, bool.
-query_user(Node, Answer) -->
- write_edt_node(Node),
- io__nl,
- get_command("Valid? ", Command),
+:- type user_state
+ ---> user(
+ io__input_stream,
+ io__output_stream
+ ).
+
+user_state_init(InStr, OutStr, User) :-
+ User = user(InStr, OutStr).
+
+query_user(Nodes, Response, User0, User) -->
+ query_user_2(Nodes, [], Response, User0, User).
+
+:- pred query_user_2(list(decl_question), list(decl_question), user_response,
+ user_state, user_state, io__state, io__state).
+:- mode query_user_2(in, in, out, in, out, di, uo) is det.
+
+query_user_2([], _, no_user_answer, User, User) -->
+ [].
+query_user_2([Node | Nodes], Skipped, Response, User0, User) -->
+ write_decl_question(Node, User0),
+ { decl_question_prompt(Node, Question) },
+ get_command(Question, Command, User0, User1),
(
{ Command = yes },
- { Answer = truth_value(yes) }
+ { Response = user_answer(Node - yes) },
+ { User = User1 }
;
{ Command = no },
- { Answer = truth_value(no) }
+ { Response = user_answer(Node - no) },
+ { User = User1 }
;
{ Command = inadmissible },
- io__write_string("Sorry, not implemented.\n"),
- query_user(Node, Answer)
+ io__write_string("Sorry, not implemented,\n"),
+ query_user_2([Node | Nodes], Skipped, Response, User1, User)
+ ;
+ { Command = skip },
+ query_user_2(Nodes, [Node | Skipped], Response, User1, User)
;
- { Command = do_not_know },
- { Answer = deferred(do_not_know) }
+ { Command = restart },
+ { reverse_and_append(Skipped, [Node | Nodes], Questions) },
+ query_user_2(Questions, [], Response, User1, User)
;
{ Command = browse },
- io__write_string("Sorry, not implemented.\n"),
- query_user(Node, Answer)
+ browse_edt_node(Node, User1, User2),
+ query_user_2([Node | Nodes], Skipped, Response, User2, User)
;
- { Command = tree },
- io__write_string("Sorry, not implemented.\n"),
- query_user(Node, Answer )
+ { Command = abort },
+ { Response = abort_diagnosis },
+ { User = User1 }
;
{ Command = help },
- io__write_strings([
- "According to the intended interpretation",
- " of the program, answer one of:\n",
- "\ty\tyes\n",
- "\tn\tno\n",
-% "\ti\tinadmissible (not yet)\n",
- "\td\tdon't know\n",
-% "\tb\tbrowse the atom arguments (not yet)\n",
-% "\tt\tprint the evaluation tree (not yet)\n",
- "\th, ?\tthis help message\n"
- ]),
- query_user(Node, Answer )
+ user_help_message(User1),
+ query_user_2([Node | Nodes], Skipped, Response, User1, User)
;
{ Command = illegal_command },
io__write_string("Unknown command, 'h' for help.\n"),
- query_user(Node, Answer)
+ query_user_2([Node | Nodes], Skipped, Response, User1, User)
).
+:- pred decl_question_prompt(decl_question, string).
+:- mode decl_question_prompt(in, out) is det.
-:- pred get_command(string, user_response, io__state, io__state).
-:- mode get_command(in, out, di, uo) is det.
+decl_question_prompt(wrong_answer(_), "Valid? ").
+decl_question_prompt(missing_answer(_, _), "Complete? ").
-get_command(Prompt, Command) -->
+:- pred browse_edt_node(decl_question, user_state, user_state,
+ io__state, io__state).
+:- mode browse_edt_node(in, in, out, di, uo) is det.
+
+browse_edt_node(_Node, User, User) -->
+ io__write_string("Sorry, not implemented.\n").
+
+ % Reverse the first argument and append the second to it.
+ %
+:- pred reverse_and_append(list(T), list(T), list(T)).
+:- mode reverse_and_append(in, in, out) is det.
+
+reverse_and_append([], Bs, Bs).
+reverse_and_append([A | As], Bs, Cs) :-
+ reverse_and_append(As, [A | Bs], Cs).
+
+
+%-----------------------------------------------------------------------------%
+
+:- type user_command
+ ---> yes % The node is correct.
+ ; no % The node is incorrect.
+ ; inadmissible % The node is inadmissible.
+ ; skip % The user has no answer.
+ ; restart % Ask the skipped questions again.
+ ; browse % Browse the data before answering.
+ ; abort % Abort this diagnosis session.
+ ; help % Request help before answering.
+ ; illegal_command. % None of the above.
+
+:- pred user_help_message(user_state, io__state, io__state).
+:- mode user_help_message(in, di, uo) is det.
+
+user_help_message(user(_, OutStr)) -->
+ io__write_strings(OutStr, [
+ "According to the intended interpretation of the program,",
+ " answer one of:\n",
+ "\ty\tyes\t\tthe node is correct\n",
+ "\tn\tno\t\tthe node is incorrect\n",
+% "\ti\tinadmissible\tthe input arguments are out of range\n",
+ "\ts\tskip\t\tskip this question\n",
+ "\tr\trestart\t\task the skipped questions again\n",
+% "\tb\tbrowse\t\tbrowse the atom\n",
+ "\ta\tabort\t\tabort this diagnosis session\n",
+ "\th, ?\thelp\t\tthis help message\n"
+ ]).
+
+:- pred get_command(string, user_command, user_state, user_state,
+ io__state, io__state).
+:- mode get_command(in, out, in, out, di, uo) is det.
+
+get_command(Prompt, Command, User, User) -->
util__trace_getline(Prompt, Result),
( { Result = ok(String) },
{ string__to_char_list(String, Line) },
@@ -116,56 +177,53 @@
{ io__error_message(Error, Msg) },
io__write_string(Msg),
io__nl,
- get_command(Prompt, Command)
+ { Command = abort }
; { Result = eof },
- % XXX this should definitely be handled better.
- { Command = illegal_command }
+ { Command = abort }
).
-:- pred command_chars(list(char), user_response).
+:- pred command_chars(list(char), user_command).
:- mode command_chars(in, out) is semidet.
command_chars(['y' | _], yes).
command_chars(['n' | _], no).
command_chars(['i' | _], inadmissible).
-command_chars(['d' | _], do_not_know).
+command_chars(['s' | _], skip).
+command_chars(['r' | _], restart).
command_chars(['b' | _], browse).
-command_chars(['t' | _], tree).
+command_chars(['a' | _], abort).
command_chars(['h' | _], help).
command_chars(['?' | _], help).
+%-----------------------------------------------------------------------------%
-write_edt_node(Node) -->
- {
- Node = wrong_answer(atom(Name, Args))
- ;
- % XXX this is wrong, but most of the module is
- % going to be re-written again soon anyway, so I
- % won't fix it yet.
- %
- Node = missing_answer(atom(Name, Args), _)
- },
- io__write_string(Name),
- (
- { Args = [Arg1 | Args0] }
- ->
- io__write_char('('),
- io__print(Arg1),
- write_args_rest(Args0),
- io__write_char(')')
- ;
- []
- ).
+ % Display the node in user readable form on the current
+ % output stream.
+ %
+:- pred write_decl_question(decl_question, user_state, io__state, io__state).
+:- mode write_decl_question(in, in, di, uo) is det.
+write_decl_question(wrong_answer(Atom), User) -->
+ { User = user(_, OutStr) },
+ write_decl_atom(OutStr, "", Atom).
+
+write_decl_question(missing_answer(Call, Solns), User) -->
+ { User = user(_, OutStr) },
+ write_decl_atom(OutStr, "Call ", Call),
+ io__write_string(OutStr, "Solutions:\n"),
+ list__foldl(write_decl_atom(OutStr, "\t"), Solns).
+
+:- pred write_decl_atom(io__output_stream, string, decl_atom,
+ io__state, io__state).
+:- mode write_decl_atom(in, in, in, di, uo) is det.
-:- pred write_args_rest(list(univ), io__state, io__state).
-:- mode write_args_rest(in, di, uo) is det.
+write_decl_atom(OutStr, Indent, Atom) -->
+ io__write_string(OutStr, Indent),
-write_args_rest([]) -->
- [].
-write_args_rest([Arg | Args]) -->
- io__write_string(", "),
- io__print(Arg),
- write_args_rest(Args).
+ % XXX this looks horrible, but works for now. We should
+ % call the browser to print this.
+ %
+ io__write(OutStr, Atom),
+ io__nl.
Index: trace/mercury_trace_declarative.c
===================================================================
RCS file: /home/mercury1/repository/mercury/trace/mercury_trace_declarative.c,v
retrieving revision 1.12
diff -u -r1.12 mercury_trace_declarative.c
--- mercury_trace_declarative.c 1999/11/30 00:04:59 1.12
+++ mercury_trace_declarative.c 1999/12/06 05:12:10
@@ -51,7 +51,7 @@
** macro gives the default depth limit (relative to the starting depth).
*/
-#define MR_EDT_DEPTH_STEP_SIZE 8
+#define MR_EDT_DEPTH_STEP_SIZE 128
/*
** The declarative debugger back end is controlled by the
@@ -79,10 +79,14 @@
/*
** The front end state is stored here in between calls to it.
+** MR_trace_decl_ensure_init should be called before using the state.
*/
-static Word MR_trace_front_end_state = (Word) NULL;
+static Word MR_trace_front_end_state;
+static void
+MR_trace_decl_ensure_init(void);
+
/*
** MR_trace_current_node always contains the last node allocated,
** or NULL if the collection has just started.
@@ -182,9 +186,9 @@
if (event_info->MR_event_number > MR_edt_last_event) {
/* This shouldn't ever be reached. */
fprintf(MR_mdb_err, "Warning: missed final event.\n");
- fprintf(MR_mdb_err, "event %d\nlast event %d\n",
- event_info->MR_event_number,
- MR_edt_last_event);
+ fprintf(MR_mdb_err, "event %ld\nlast event %ld\n",
+ (long) event_info->MR_event_number,
+ (long) MR_edt_last_event);
MR_trace_decl_mode = MR_TRACE_INTERACTIVE;
return MR_trace_event_internal(cmd, TRUE, event_info);
}
@@ -779,6 +783,29 @@
return arglist;
}
+static void
+MR_trace_decl_ensure_init(void)
+{
+ static bool done = FALSE;
+ static MercuryFile mdb_in;
+ static MercuryFile mdb_out;
+
+ mdb_in.file = MR_mdb_in;
+ mdb_in.line_number = 1;
+ mdb_out.file = MR_mdb_out;
+ mdb_out.line_number = 1;
+
+ if (! done) {
+ MR_TRACE_CALL_MERCURY(
+ MR_DD_decl_diagnosis_state_init(
+ (Word) &mdb_in,
+ (Word) &mdb_out,
+ &MR_trace_front_end_state);
+ );
+ done = TRUE;
+ }
+}
+
bool
MR_trace_start_decl_debug(const char *outfile, MR_Trace_Cmd_Info *cmd,
MR_Event_Info *event_info, MR_Event_Details *event_details,
@@ -823,18 +850,14 @@
}
}
+ MR_trace_decl_ensure_init();
+
MR_edt_last_event = event_info->MR_event_number;
MR_edt_min_depth = event_info->MR_call_depth;
MR_edt_max_depth = event_info->MR_call_depth + MR_EDT_DEPTH_STEP_SIZE;
MR_trace_node_store = 0;
MR_trace_current_node = (MR_Trace_Node) NULL;
- if (MR_trace_front_end_state == (Word) NULL) {
- MR_TRACE_CALL_MERCURY(
- MR_DD_diagnoser_state_init(&MR_trace_front_end_state);
- );
- }
-
cmd->MR_trace_cmd = MR_CMD_GOTO;
cmd->MR_trace_stop_event = MR_trace_event_number + 1;
cmd->MR_trace_strict = FALSE;
@@ -846,21 +869,20 @@
static void
MR_decl_diagnosis(MR_Trace_Node root)
{
- MercuryFile mdb_in, mdb_out;
Word response;
- mdb_in.file = MR_mdb_in;
- mdb_in.line_number = 1;
- mdb_out.file = MR_mdb_out;
- mdb_out.line_number = 1;
-
MR_TRACE_CALL_MERCURY(
- MR_DD_decl_diagnosis((Word) &mdb_in, (Word) &mdb_out,
- MR_trace_node_store, root, &response,
+ MR_DD_decl_diagnosis(MR_trace_node_store, root, &response,
MR_trace_front_end_state,
&MR_trace_front_end_state
);
);
+
+ /*
+ ** XXX We don't do anything with the response yet.
+ ** We should set the current event to the call of the buggy node
+ ** (if there is one), or we should handle requests for subtrees.
+ */
}
static void
Index: trace/mercury_trace_declarative.h
===================================================================
RCS file: /home/mercury1/repository/mercury/trace/mercury_trace_declarative.h,v
retrieving revision 1.5
diff -u -r1.5 mercury_trace_declarative.h
--- mercury_trace_declarative.h 1999/11/30 00:04:59 1.5
+++ mercury_trace_declarative.h 1999/11/30 14:39:45
@@ -50,11 +50,11 @@
#define MR_TRACE_STATUS_FAILED (Word) 1
#define MR_TRACE_STATUS_UNDECIDED (Word) 2
-#define MR_trace_atom(atom, name, args) \
- do { \
- tag_incr_hp((atom), MR_mktag(0), 2); \
- MR_field(MR_mktag(0), (atom), 0) = (Word) (name); \
- MR_field(MR_mktag(0), (atom), 1) = (args); \
+#define MR_trace_atom(atom, name, args) \
+ do { \
+ tag_incr_hp((atom), MR_mktag(0), 2); \
+ MR_field(MR_mktag(0), (atom), (Integer) 0) = (Word) (name); \
+ MR_field(MR_mktag(0), (atom), (Integer) 1) = (args); \
} while(0)
#endif /* MERCURY_TRACE_DECLARATIVE_H */
New module:
%-----------------------------------------------------------------------------%
% Copyright (C) 1999 The University of Melbourne.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%-----------------------------------------------------------------------------%
% File: declarative_analyser.m
% Author: Mark Brown
%
% This module defines Evaluation Dependency Trees (EDTs), and
% implements an analysis algorithm which finds bugs in such trees.
%
:- module declarative_analyser.
:- interface.
:- import_module list.
:- import_module declarative_debugger.
% This typeclass defines how EDTs may be accessed by this module.
% An EDT is a tree of nodes, each of which contains a question
% about the truth of an assertion. The children of a node may
% not be immediately accessible if the sub-tree beneath that
% node is represented implicitly. In this case, the analyser
% must request that it be made explicit before continuing.
%
:- typeclass mercury_edt(S, T) where [
% Gives the root node of an EDT.
%
pred edt_root(S, T, decl_question),
mode edt_root(in, in, out) is det,
% Gives the list of children of a tree. If the tree is
% represented implicitly, then the procedure fails.
%
pred edt_children(S, T, list(T)),
mode edt_children(in, in, out) is semidet
].
:- type analyser_response(T)
% There are no suspects left, and no incorrect
% nodes have been found.
%
---> no_suspects
% A suspect who is guilty.
%
; bug_found(decl_bug(T))
% The analyser desires answers to any of a list
% of queries.
%
; oracle_queries(list(decl_question))
% The analyser requires the given implicit sub-tree
% to be made explicit.
%
; require_explicit(T).
:- type analyser_state(T).
:- pred analyser_state_init(analyser_state(T)).
:- mode analyser_state_init(out) is det.
% Perform analysis on the given EDT, which may be a new tree
% to diagnose, or a sub-tree that was required to be made
% explicit.
%
:- pred start_analysis(S, T, analyser_response(T), analyser_state(T),
analyser_state(T)) <= mercury_edt(S, T).
:- mode start_analysis(in, in, out, in, out) is det.
% Continue analysis after the oracle has responded with some
% answers.
%
:- pred continue_analysis(S, list(decl_answer), analyser_response(T),
analyser_state(T), analyser_state(T)) <= mercury_edt(S, T).
:- mode continue_analysis(in, in, out, in, out) is det.
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module std_util, bool, require.
% The analyser state represents a set of suspects. We
% consider one incorrect node at a time, and store its suspect
% children.
%
:- type analyser_state(T)
---> analyser(
% Current incorrect node (initially `no').
%
maybe(T),
% Current suspects.
%
list(suspect(T))
).
% A suspect is a suspect tree along with its corresponding
% root node.
%
:- type suspect(T) == pair(T, decl_question).
analyser_state_init(analyser(no, [])).
start_analysis(Store, Tree, Response, _, Analyser) :-
edt_root(Store, Tree, Root),
Response = oracle_queries([Root]),
Analyser = analyser(no, [Tree - Root]).
continue_analysis(Store, Answers, Response, Analyser0, Analyser) :-
(
find_incorrect_suspect(Answers, Analyser0, Node)
->
make_new_suspects(Store, Node, Response, Analyser)
;
remove_suspects(Answers, Response, Analyser0, Analyser)
).
% Find an answer which is `no' and find the suspect that
% corresponds to it, or else fail.
%
:- pred find_incorrect_suspect(list(decl_answer), analyser_state(T), T).
:- mode find_incorrect_suspect(in, in, out) is semidet.
find_incorrect_suspect([Answer | Answers], Analyser, Child) :-
Analyser = analyser(_, Suspects),
(
Answer = Node - no,
find_matching_suspects(Node, Suspects, [Match | _], _)
->
Match = Child - _
;
find_incorrect_suspect(Answers, Analyser, Child)
).
% Create a new suspect list from the given tree, which is
% assumed to have an incorrect root.
%
:- pred make_new_suspects(S, T, analyser_response(T), analyser_state(T))
<= mercury_edt(S, T).
:- mode make_new_suspects(in, in, out, out) is det.
make_new_suspects(Store, Tree, Response, Analyser) :-
(
edt_children(Store, Tree, Children)
->
make_suspects(Store, Children, Suspects, Queries),
Analyser = analyser(yes(Tree), Suspects),
(
Queries = []
->
Response = bug_found(e_bug(Tree))
;
Response = oracle_queries(Queries)
)
;
Response = require_explicit(Tree),
Analyser = analyser(yes(Tree), [])
).
:- pred make_suspects(S, list(T), list(suspect(T)), list(decl_question))
<= mercury_edt(S, T).
:- mode make_suspects(in, in, out, out) is det.
make_suspects(_, [], [], []).
make_suspects(Store, [Tree | Trees], [Tree - Root | Ss], [Root | Qs]) :-
edt_root(Store, Tree, Root),
make_suspects(Store, Trees, Ss, Qs).
% Go through the answers (none of which should be `no') and
% remove the corresponding children from the suspect list.
%
:- pred remove_suspects(list(decl_answer), analyser_response(T),
analyser_state(T), analyser_state(T)).
:- mode remove_suspects(in, out, in, out) is det.
remove_suspects([], Response, Analyser, Analyser) :-
Analyser = analyser(MaybeTree, Suspects),
(
Suspects = []
->
(
MaybeTree = yes(Tree)
->
Response = bug_found(e_bug(Tree))
;
Response = no_suspects
)
;
list__map(snd, Suspects, Queries),
Response = oracle_queries(Queries)
).
remove_suspects([Node - yes | Answers], Response, Analyser0, Analyser) :-
Analyser0 = analyser(MaybeTree, Suspects0),
find_matching_suspects(Node, Suspects0, _, Suspects),
Analyser1 = analyser(MaybeTree, Suspects),
remove_suspects(Answers, Response, Analyser1, Analyser).
remove_suspects([_ - no | _], _, _, _) :-
error("remove_suspects: unexpected incorrect node").
:- pred find_matching_suspects(decl_question, list(suspect(T)),
list(suspect(T)), list(suspect(T))).
:- mode find_matching_suspects(in, in, out, out) is det.
find_matching_suspects(Node, Suspects, Matches, NoMatches) :-
P = (pred(A::in) is semidet :- A = _ - Node),
list__filter(P, Suspects, Matches, NoMatches).
--
Mark Brown, PhD student )O+ | "Another of Fortran's breakthroughs
(m.brown at cs.mu.oz.au) | was the GOTO statement, which was...
Dept. of Computer Science and Software | uniquely simple and understandable"
Engineering, University of Melbourne | -- IEEE, 1994
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list