[m-rev.] a proof tree monitor
Erwan Jahier
Erwan.Jahier at irisa.fr
Tue Jul 17 02:48:34 AEST 2001
Mark wrote:
| > + Port = exit
| > + ->
| > + stack__top_det(CallStack, FatherCN),
| > + map__det_remove(GoalSuccT0, FatherCN, CNListF0, GoalSuccT1),
| > + list__merge_and_remove_dups([CurrentCN - GoalPath], CNListF0,
| > + CNListF),
|
| Hmm, I'm not completely sure that this is the right thing to do here.
| As I understand the code, the order that these call_paths are added to
| goal_successors_table is significant because when backtracking occurs,
| you will need to remove all of the entries since the last choice point.
| However, using list__merge_and_remove_dups will not preserve the order
| that you need, so I can't see how you will be able to remove the correct
| parts of the previous branch when backtracking occurs.
No, the order is unsignificant here; in order to know which branches I remove
on backtracking, I use the goal_path and the call number. More precisely:
1) at fail events, I remove the solution corresponding to the current call
number
2) at redo events, I remove the solution which call numbers are bigger than the
current one (this is needed because deterministic procs do not produce any
fail events, so case 1) won't remove them).
3) at disj ports, I remove the solution which goal path occur after in the
goal.
| > + map__det_insert(GoalSuccT1, FatherCN, CNListF, GoalSuccT),
| > + %
| > + % Update the proof tree Table. To do that, we retrieve the
| > + % list of successors of the current goal, we retrieve their
| > + % proof trees, and then we build the proof tree of the
| > + % current goal.
| > + %
| > + map__lookup(GoalSuccT, CurrentCN, ListCP),
| > + %
| > + % we remove the goal path from that list of call_path
| > + %
| > + list__map(remove_goal_path, ListCP, ListCN),
| > + ( ListCN = [] ->
| > + ( map__update(ProofT0, CurrentCN,
| > + leaf(CurrentCN, CurrentPred), ProofT1) ->
| > + ProofT = ProofT1
| > + ;
| > + map__det_insert(ProofT0, CurrentCN,
| > + leaf(CurrentCN, CurrentPred), ProofT)
| > + )
|
| You can update maps this way using map__set.
yop, thanks.
| > +:- pred remove_goal_path(call_path, call_number).
| > +:- mode remove_goal_path(in, out) is det.
| > +remove_goal_path(CallNumber - _GoalPath, CallNumber).
| > +
| > +
| > +:- pred remove_sol_failing_branch(goal_path_string, call_number,
| > + goal_successors_table, goal_successors_table,
| > + proof_tree_table, proof_tree_table).
| > +:- mode remove_sol_failing_branch(in, in, in, out, in, out) is det.
| > +remove_sol_failing_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
| > + ProofT0, ProofT) :-
| > + ( if get_goal_path_previous_disj(GoalPath, GoalPathPrevDisj) then
| > + % Get the succesors list of the father of the current goal.
| > + map__lookup(GoalSuccT0, CurrentCN, SuccList),
| > + % From this list of successors, we want to remove all the
| > + % call_path that were in the previous disjunction; to do
| > + % that, we use the goal path information.
| > + list__filter(remove_this_goal_path(GoalPathPrevDisj),
| > + SuccList, NewSuccList),
|
| I'm not 100% sure, but I think this is a bug. The problem is that there
| could have been any number of internal events after the disjunction,
| which would overwrite the "current" goal path with the goal path for
| that internal event.
No. I maintain a stack of goal path in order to always have the rigth goal path
(cf update_goal_path).
| Any calls that now occur will be stored in the
| goal successors table with the new event. However, when we backtrack to
| the disjunction and select a later disjunct, those calls will be
| backtracked over but they will not be removed from the goal successors
| table because they are associated with a different goal path. The end
| result would be a proof tree that has extra children that should not be
| there.
|
| Could you please test the proof tree monitor on a program that contains
| the following code snippet?
|
| p(A, B) :-
| (
| q(A)
| ;
| r(A)
| ),
| (
| s(B)
| ;
| t(B)
| ).
|
| I'd be interested in checking the proof trees generated for the third
| and fourth solutions to p.
Indeed it is wrong, but maybe not the way you thought (cf foo.bad.ps in
attachement).
My code is wrong for all solutions predicates; it is not really a surprise
since I have added the code to handle them yesterday, whereas the rest of the
code was written 9 months ago... If I have the call solution(p, Sol), then I
have the following trace:
2 call solutions
3 call p
...
3 exit p ---> first sol
3 redo p
3 call p
...
3 exit p ---> second sol
3 redo p
5 fail p ---> p fails !!!
2 exit solutions
The code I have added yesterday was to take care not removing the solutions
of p when p fails. But the data structure I used was not designed to collect
several solutions of the same call. indeed, I had:
:- type proof_tree_table == map(call_number, proof_tree).
whereas I should have something along:
:- type proof_tree_table == map(call_number, list(proof_tree)).
Thefore I have changed that (see the diff below).
[... more testing ...]
Well, I found another bug in the code ; I do not remove the rigth branches
when I enter the branch of a disjunction (of course, this bug could not
appeared as long as I was restricting myself to program without all solutions
predicates...).
Any case, thanks Mark!
I have appended below the diff and the relative diff as well as a few monitor
results (foo.bad.ps was the result of my first version, foo.pt.ps is the
current one, queens2.pt.ps is the result of the current version applied on the
queens program).
Index: extras/morphine/source/collect__proof_tree
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/morphine/source/collect__proof_tree,v
retrieving revision 1.1
diff -u -d -u -r1.1 collect__proof_tree
--- extras/morphine/source/collect__proof_tree 2001/07/12 15:54:04 1.1
+++ extras/morphine/source/collect__proof_tree 2001/07/16 16:42:54
@@ -10,7 +10,8 @@
% Note that it only works if the internal events have been generated in
% the trace. Also, the Morphine parameter collect_arg should be set to `yes'.
%
-% Bug: not/1 is not handled (I should do something at `neg_*' events to fix that).
+% Bug: not/1 is not handled (I should do something at `neg_*' events to fix
+% that).
%
:- import_module list, string, require, map, stack, term, std_util.
@@ -51,7 +52,6 @@
).
:- type collected_type ---> pb(string) ; ct(proof_tree).
-
:- type call_path == pair(call_number, goal_path_string).
@@ -63,7 +63,7 @@
leaf(call_number, predicate)
; tree(call_number, predicate, list(proof_tree)).
-:- type proof_tree_table == map(call_number, proof_tree).
+:- type proof_tree_table == map(call_number, list(proof_tree)).
%-----------------------------------------------------------------------%
@@ -116,45 +116,54 @@
% we remove the goal path from that list of call_path
%
list__map(remove_goal_path, ListCP, ListCN),
- ( ListCN = [] ->
- ( map__update(ProofT0, CurrentCN,
- leaf(CurrentCN, CurrentPred), ProofT1) ->
- ProofT = ProofT1
- ;
- map__det_insert(ProofT0, CurrentCN,
- leaf(CurrentCN, CurrentPred), ProofT)
- )
+
+ ( ListCN = [] ->
+ % The current goal is a success leaf
+ % (i.e., it has no child)
+ ProofTreeCGoal = leaf(CurrentCN, CurrentPred)
;
- list__map(map__lookup(ProofT0), ListCN, ListTrees),
- ( map__update(ProofT0, CurrentCN,
- tree(CurrentCN, CurrentPred, ListTrees),
- ProofT1) ->
- ProofT = ProofT1
+ list__map(map__lookup(ProofT0), ListCN, ListListTrees),
+ % If the goal is an all sol pred, ListListTrees should
+ % contain the list of the solution of the goal it
+ % calls; otherwise, it should contain the list of its
+ % children solutions
+ list__condense(ListListTrees, ListTrees),
+ ProofTreeCGoal =
+ tree(CurrentCN, CurrentPred, ListTrees)
+ ),
+ ( map__search(ProofT0, CurrentCN, ProofTL0) ->
+ ( member(FatherCN, AllSolList0) ->
+ append([ProofTreeCGoal], ProofTL0, ProofTL),
+ map__set(ProofT0, CurrentCN, ProofTL, ProofT)
;
- map__det_insert(ProofT0, CurrentCN,
- tree(CurrentCN, CurrentPred, ListTrees),
- ProofT)
+ % If a goal is not called from an all solution
+ % predicate, we only keep the current solution
+ map__set(ProofT0, CurrentCN,
+ [ProofTreeCGoal], ProofT)
)
+ ;
+ map__set(ProofT0, CurrentCN, [ProofTreeCGoal], ProofT)
),
AllSolList = AllSolList0
;
Port = fail
->
- stack__top_det(CallStack, FatherCN),
+ stack__top_det(CallStack0, FatherCN),
( member(FatherCN, AllSolList0) ->
- % for all solutions predicates (such as std_util__solutions/2)
- % we must not remove the previous solutions of the goal.
- % Indeed, the all solutions predicates call the goal they
- % search all the solution of until it fails; therefore that
- % would mean that we would always remove those solutions.
+ % for all sol procs (such as std_util__solutions/2)
+ % we must not remove the previous solutions of
+ % the goal. Indeed, all solutions predicates
+ % call the goal they search all the solution of
+ % until it fails; therefore that would mean that we
+ % would always remove those solutions.
GoalSuccT = GoalSuccT0,
ProofT = ProofT0
;
map__lookup(GoalSuccT0, CurrentCN, SuccList),
remove_proof_trees(ProofT0, SuccList, ProofT),
map__lookup(GoalSuccT0, FatherCN, SuccListFather0),
- list__filter(remove_current_cn(CurrentCN), SuccListFather0,
- SuccListFather),
+ list__filter(remove_current_cn(CurrentCN),
+ SuccListFather0, SuccListFather),
map__det_update(GoalSuccT0, FatherCN, SuccListFather,
GoalSuccT)
),
@@ -165,23 +174,43 @@
%
% We need to remove the solutions of the previous (failing
% branch) disjunction, i.e., we remove form the successors
- % tables all the branches from the father goal to the
- % goal of the previous disjunction. We also have to remove
- % the proof trees of those goals.
+ % tables all the branches from the father goal of the
+ % previous disjunction. We also have to remove the proof
+ % trees of those goals.
%
% We also need to remove the solutions produced in the if
% branch for the same reasons as above (actually, it is
% natural since `if A then B else C' <=> `A, !, B ; C'.).
%
- ( Port = disj ->
- remove_sol_failing_branch(GoalPath, CurrentCN,
- GoalSuccT0, GoalSuccT, ProofT0, ProofT)
+ stack__top_det(CallStack, FatherCN),
+ ( member(FatherCN, AllSolList0) ->
+ GoalSuccT = GoalSuccT0,
+ ProofT = ProofT0
;
- remove_sol_if_branch(GoalPath, CurrentCN,
+ ( Port = disj ->
+ remove_sol_disj_branch(GoalPath, CurrentCN,
+ GoalSuccT0, GoalSuccT, ProofT0, ProofT)
+ ;
+ remove_sol_then_branch(GoalPath, CurrentCN,
GoalSuccT0, GoalSuccT, ProofT0, ProofT)
+ )
),
AllSolList = AllSolList0
;
+ Port = redo
+ ->
+ % Deterministic proc won't produce any fail event on
+ % backtraking; thefore we need to remove solutions here too.
+ stack__top_det(CallStack0, FatherCN),
+ ( member(FatherCN, AllSolList0) ->
+ GoalSuccT = GoalSuccT0,
+ ProofT = ProofT0
+ ;
+ remove_sol_at_redo_port(CurrentCN, FatherCN,
+ GoalSuccT0, GoalSuccT, ProofT0, ProofT)
+ ),
+ AllSolList = AllSolList0
+ ;
% Bug XXX I probably should do something at ports
% neg_enter, neg_success, and neg_failure.
%
@@ -215,19 +244,40 @@
remove_goal_path(CallNumber - _GoalPath, CallNumber).
-:- pred remove_sol_failing_branch(goal_path_string, call_number,
+:- pred remove_sol_at_redo_port(call_number, call_number,
goal_successors_table, goal_successors_table,
proof_tree_table, proof_tree_table).
-:- mode remove_sol_failing_branch(in, in, in, out, in, out) is det.
-remove_sol_failing_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
+:- mode remove_sol_at_redo_port(in, in, in, out, in, out) is det.
+remove_sol_at_redo_port(CurrentCN, FatherCN, GoalSuccT0, GoalSuccT,
+ ProofT0, ProofT) :-
+ % Get the successors list of the father of the current goal.
+ map__lookup(GoalSuccT0, FatherCN, SuccList),
+ list__filter(call_number_is_bigger(CurrentCN), SuccList, NewSuccList),
+ map__det_update(GoalSuccT0, FatherCN, NewSuccList, GoalSuccT),
+ % We also remove the corresponding proof trees
+ list__delete_elems(SuccList, NewSuccList, FailList),
+ remove_proof_trees(ProofT0, FailList, ProofT).
+
+:- pred call_number_is_bigger(call_number, call_path).
+:- mode call_number_is_bigger(in, in) is semidet.
+call_number_is_bigger(CN1, CN2 - _GoalPath2) :-
+ CN1 > CN2.
+
+
+:- pred remove_sol_disj_branch(goal_path_string, call_number,
+ goal_successors_table, goal_successors_table,
+ proof_tree_table, proof_tree_table).
+:- mode remove_sol_disj_branch(in, in, in, out, in, out) is det.
+remove_sol_disj_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
ProofT0, ProofT) :-
- ( if get_goal_path_previous_disj(GoalPath, GoalPathPrevDisj) then
- % Get the succesors list of the father of the current goal.
+ ( if get_goal_path_previous_disj(GoalPath, GoalPathPrev) then
+ % Get the successors list of the father of the current goal.
map__lookup(GoalSuccT0, CurrentCN, SuccList),
% From this list of successors, we want to remove all the
- % call_path that were in the previous disjunction; to do
+ % call_path that were in the previous disjunction, as well as
+ % the solutions that were produced after; to do
% that, we use the goal path information.
- list__filter(remove_this_goal_path(GoalPathPrevDisj),
+ list__filter(goal_path_is_after(GoalPathPrev),
SuccList, NewSuccList),
map__det_update(GoalSuccT0, CurrentCN, NewSuccList, GoalSuccT),
% We also remove the corresponding proof trees
@@ -238,19 +288,21 @@
ProofT = ProofT0
).
-:- pred remove_sol_if_branch(goal_path_string, call_number,
+:- pred remove_sol_then_branch(goal_path_string, call_number,
goal_successors_table, goal_successors_table,
proof_tree_table, proof_tree_table).
-:- mode remove_sol_if_branch(in, in, in, out, in, out) is det.
-remove_sol_if_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
+:- mode remove_sol_then_branch(in, in, in, out, in, out) is det.
+remove_sol_then_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
ProofT0, ProofT) :-
( if string__remove_suffix(GoalPath, "e;", GoalPathIfBranch) then
+ append(GoalPathIfBranch, "t;", GoalPathThenBranch),
% Get the succesors list of the current of the current goal.
map__lookup(GoalSuccT0, CurrentCN, SuccList),
% From this list of successors, we want to remove all the
- % call_path that were in the previous disjunction; to do
+ % call_path that were in the then branch, as well as
+ % the solutions that were produced after; to do
% that, we use the goal path information.
- list__filter(remove_this_goal_path(GoalPathIfBranch),
+ list__filter(goal_path_is_after(GoalPathThenBranch),
SuccList, NewSuccList),
map__det_update(GoalSuccT0, CurrentCN, NewSuccList, GoalSuccT),
% We also remove the corresponding proof trees
@@ -261,34 +313,81 @@
).
-:- pred remove_proof_trees(proof_tree_table, list(call_path), proof_tree_table).
+:- pred remove_proof_trees(proof_tree_table, list(call_path),
+ proof_tree_table).
:- mode remove_proof_trees(in, in, out) is det.
remove_proof_trees(ProofT0, [], ProofT0).
remove_proof_trees(ProofT0, [CN-_|Tail], ProofT) :-
map__det_remove(ProofT0, CN, _, ProofT1),
remove_proof_trees(ProofT1, Tail, ProofT).
-:- pred remove_this_goal_path(goal_path_string, call_path).
-:- mode remove_this_goal_path(in, in) is semidet.
-% We check whether Path1 is a sub path of Path2
-remove_this_goal_path(Path1, _ - Path2) :-
- string__append(Path1, _, Path2).
+% goal_path_is_after(Path1, _ - Path2) is true iff Path1
+% occurs <<after>> Path2 in the goal.
+%
+% The idea is that when we enter the branch of a disjunction,
+% we need to remove all the solutions that were produced after
+% as well as the solutions that were produced in the previous disjunction.
+%
+% Ex: goal_path_is_after("d3;c4;d3;d3", _ - "d3;c4;d2;t")
+% goal_path_is_after("d3;e;c6;d9", _ - "d4;e;")
+:- pred goal_path_is_after(goal_path_string, call_path).
+:- mode goal_path_is_after(in, in) is semidet.
+goal_path_is_after(GoalPath1, _CN2 - GoalPath2) :-
+ string__words(is_semi_column, GoalPath1) = ListPath1,
+ string__words(is_semi_column, GoalPath2) = ListPath2,
+ goal_path_is_after2(ListPath1, ListPath2).
+
+:- pred is_semi_column(char::in) is semidet.
+is_semi_column(';').
+
+:- pred goal_path_is_after2(list(string)::in, list(string)::in) is semidet.
+goal_path_is_after2([Path1|Tail1], [Path2|Tail2]) :-
+ ( Path1 = Path2 ->
+ goal_path_is_after2(Tail1, Tail2)
+ ;
+ atomic_path_is_after(Path1, Path2)
+ ).
+
+:- pred atomic_path_is_after(string::in, string::in) is semidet.
+% atomic_path_is_after(Path1, Path2) succeeds iff Path1 < Path2
+atomic_path_is_after(Path1, Path2) :-
+ (
+ Path2 = ""
+ ->
+ % "s2;d2;d4;" is after "s2;d2;"
+ true
+ ;
+ append(L, Int1Str, Path1),
+ append(L, Int2Str, Path2),
+ ( L = "c" ; L = "d"),
+ string__det_to_int(Int1Str) = Int1,
+ string__det_to_int(Int2Str) = Int2
+ ->
+ Int1 > Int2
+ ;
+ ( Path1 = "e" ; Path1 = "t"), Path2 = "?"
+ ).
+
+
:- pred remove_current_cn(call_number, call_path).
:- mode remove_current_cn(in, in) is semidet.
remove_current_cn(N1, N2 - _) :-
not (N1 = N2).
+
:- pred get_goal_path_previous_disj(goal_path_string, goal_path_string).
:- mode get_goal_path_previous_disj(in, out) is semidet.
-% Takes a goal path of the form "<path>, di" (where i>0), and outputs the
-% goal path "<path>, di-1" if i>1, fails otherwise
+% Takes a goal path of the form "<path>;di;" (where i>0), and outputs the
+% goal path "<path>;di-1;" if i>1, fails otherwise
get_goal_path_previous_disj(GoalPath, GoalPathPrev) :-
reverse_string(GoalPath, GoalPathRev),
- ( if string__sub_string_search(GoalPathRev, "d", Index0) then
- Index = Index0
- else
- error("No disjunctions is find in this string")
+ ( if
+ string__sub_string_search(GoalPathRev, "d", Index1)
+ then
+ Index = Index1
+ else
+ error("No disjunction is found in this string")
),
string__split(GoalPathRev, Index, NRevStr0, GoalPathTailRev),
% remove the ";"
@@ -305,7 +404,6 @@
string__int_to_string(NPrev, NPrevStr),
string__append_list([GoalPathTail, NPrevStr, ";"], GoalPathPrev).
-
:- pred reverse_string(string, string).
:- mode reverse_string(in, out) is det.
reverse_string(String, StringRev) :-
@@ -390,7 +488,7 @@
post_process(ct(_, _, _, _, _, _, ProofTreeTable), ProofTree) :-
- ( map__to_assoc_list(ProofTreeTable, [1 - ProofTree0 | _]) ->
+ ( map__to_assoc_list(ProofTreeTable, [1 - [ProofTree0] | _]) ->
ProofTree = ct(ProofTree0)
;
% Should not occur
-------------- next part --------------
%------------------------------------------------------------------------------%
% Copyright (C) 2001 INRIA/IFSIC.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file License in the Morphine distribution.
%
% Author : Erwan Jahier <jahier at irisa.fr>
%
% Computes the proof tree.
%
% Note that it only works if the internal events have been generated in
% the trace. Also, the Morphine parameter collect_arg should be set to `yes'.
%
% Bug: not/1 is not handled (I should do something at `neg_*' events to fix
% that).
%
:- import_module list, string, require, map, stack, term, std_util.
:- type accumulator_type --->
ct(
% We need that stack to be able to get the
% call number of the caller.
%
stack(call_number),
% We need the goal path and 2 stacks to be able
% to get the goal path at internal events.
%
goal_path_string,
stack(goal_path_string),
stack(goal_path_string),
% Each goal is indexed by its call number. We use
% that call number to build a table that
% contains the list of the goal direct successors
% that succeed. Each call number is associated with
% a goal path so that we know in which branch each
% success node was produced; this is necessary to be
% able to remove success nodes that do not
% contribute to the final solution.
%
goal_successors_table,
% list of call numbers corresponding to all solution
% predicates. Indeed, such predicates need to be handled
% differently because the goal they search the solutions of
% ends up to fail although it has produced solutions.
list(call_number),
% Table of proof trees indexed by call numbers.
proof_tree_table
).
:- type collected_type ---> pb(string) ; ct(proof_tree).
:- type call_path == pair(call_number, goal_path_string).
:- type goal_successors_table == map(call_number, list(call_path)).
:- type predicate ---> p(proc_name, arity, list(univ)).
:- type proof_tree --->
leaf(call_number, predicate)
; tree(call_number, predicate, list(proof_tree)).
:- type proof_tree_table == map(call_number, list(proof_tree)).
%-----------------------------------------------------------------------%
initialize(ct(CallStack, "", GpDetStack, GpNonDetStack, GoalSuccTable, [],
ProofTable)) :-
stack__init(CallStack0),
stack__push(CallStack0, 0, CallStack),
stack__init(GpDetStack),
stack__init(GpNonDetStack),
map__init(GoalSuccTable0),
map__det_insert(GoalSuccTable0, 0, [], GoalSuccTable),
map__init(ProofTable).
filter(Event, Acc0, Acc, continue) :-
Acc0 = ct(CallStack0, GoalPath0, GpDetStack0, GpNonDetStack0,
GoalSuccT0, AllSolList0, ProofT0),
Port = port(Event),
CurrentCN = call(Event),
Arg = arguments(Event),
CurrentPred = p(proc_name(Event), proc_arity(Event), Arg),
update_goal_path(Event, GoalPath0, GoalPath, GpDetStack0, GpDetStack,
GpNonDetStack0, GpNonDetStack),
update_call_stack(Port, CurrentCN, CallStack0, CallStack),
(
Port = call
->
map__det_insert(GoalSuccT0, CurrentCN, [], GoalSuccT),
( is_a_all_solutions_predicate(proc_name(Event)) ->
AllSolList = [CurrentCN | AllSolList0]
;
AllSolList = AllSolList0
),
ProofT = ProofT0
;
Port = exit
->
stack__top_det(CallStack, FatherCN),
map__det_remove(GoalSuccT0, FatherCN, CNListF0, GoalSuccT1),
list__merge_and_remove_dups([CurrentCN - GoalPath], CNListF0,
CNListF),
map__det_insert(GoalSuccT1, FatherCN, CNListF, GoalSuccT),
%
% Update the proof tree Table. To do that, we retrieve the
% list of successors of the current goal, we retrieve their
% proof trees, and then we build the proof tree of the
% current goal.
%
map__lookup(GoalSuccT, CurrentCN, ListCP),
%
% we remove the goal path from that list of call_path
%
list__map(remove_goal_path, ListCP, ListCN),
( ListCN = [] ->
% The current goal is a success leaf
% (i.e., it has no child)
ProofTreeCGoal = leaf(CurrentCN, CurrentPred)
;
list__map(map__lookup(ProofT0), ListCN, ListListTrees),
% If the goal is an all sol pred, ListListTrees should
% contain the list of the solution of the goal it
% calls; otherwise, it should contain the list of its
% children solutions
list__condense(ListListTrees, ListTrees),
ProofTreeCGoal =
tree(CurrentCN, CurrentPred, ListTrees)
),
( map__search(ProofT0, CurrentCN, ProofTL0) ->
( member(FatherCN, AllSolList0) ->
append([ProofTreeCGoal], ProofTL0, ProofTL),
map__set(ProofT0, CurrentCN, ProofTL, ProofT)
;
% If a goal is not called from an all solution
% predicate, we only keep the current solution
map__set(ProofT0, CurrentCN,
[ProofTreeCGoal], ProofT)
)
;
map__set(ProofT0, CurrentCN, [ProofTreeCGoal], ProofT)
),
AllSolList = AllSolList0
;
Port = fail
->
stack__top_det(CallStack0, FatherCN),
( member(FatherCN, AllSolList0) ->
% for all sol procs (such as std_util__solutions/2)
% we must not remove the previous solutions of
% the goal. Indeed, all solutions predicates
% call the goal they search all the solution of
% until it fails; therefore that would mean that we
% would always remove those solutions.
GoalSuccT = GoalSuccT0,
ProofT = ProofT0
;
map__lookup(GoalSuccT0, CurrentCN, SuccList),
remove_proof_trees(ProofT0, SuccList, ProofT),
map__lookup(GoalSuccT0, FatherCN, SuccListFather0),
list__filter(remove_current_cn(CurrentCN),
SuccListFather0, SuccListFather),
map__det_update(GoalSuccT0, FatherCN, SuccListFather,
GoalSuccT)
),
AllSolList = AllSolList0
;
( Port = disj ; Port = ite_else )
->
%
% We need to remove the solutions of the previous (failing
% branch) disjunction, i.e., we remove form the successors
% tables all the branches from the father goal of the
% previous disjunction. We also have to remove the proof
% trees of those goals.
%
% We also need to remove the solutions produced in the if
% branch for the same reasons as above (actually, it is
% natural since `if A then B else C' <=> `A, !, B ; C'.).
%
stack__top_det(CallStack, FatherCN),
( member(FatherCN, AllSolList0) ->
GoalSuccT = GoalSuccT0,
ProofT = ProofT0
;
( Port = disj ->
remove_sol_disj_branch(GoalPath, CurrentCN,
GoalSuccT0, GoalSuccT, ProofT0, ProofT)
;
remove_sol_then_branch(GoalPath, CurrentCN,
GoalSuccT0, GoalSuccT, ProofT0, ProofT)
)
),
AllSolList = AllSolList0
;
Port = redo
->
% Deterministic proc won't produce any fail event on
% backtraking; thefore we need to remove solutions here too.
stack__top_det(CallStack0, FatherCN),
( member(FatherCN, AllSolList0) ->
GoalSuccT = GoalSuccT0,
ProofT = ProofT0
;
remove_sol_at_redo_port(CurrentCN, FatherCN,
GoalSuccT0, GoalSuccT, ProofT0, ProofT)
),
AllSolList = AllSolList0
;
% Bug XXX I probably should do something at ports
% neg_enter, neg_success, and neg_failure.
%
GoalSuccT = GoalSuccT0,
ProofT = ProofT0,
AllSolList = AllSolList0
),
Acc = ct(CallStack, GoalPath, GpDetStack, GpNonDetStack,
GoalSuccT, AllSolList, ProofT).
:- pred is_a_all_solutions_predicate(string::in) is semidet.
is_a_all_solutions_predicate("solutions").
is_a_all_solutions_predicate("std_util__solutions").
is_a_all_solutions_predicate("solutions_set").
is_a_all_solutions_predicate("std_util__solutions_set").
is_a_all_solutions_predicate("unsorted_solutions").
is_a_all_solutions_predicate("std_util__unsorted_solutions").
is_a_all_solutions_predicate("aggregate").
is_a_all_solutions_predicate("std_util__aggregate").
is_a_all_solutions_predicate("aggregate2").
is_a_all_solutions_predicate("std_util__aggregate2").
is_a_all_solutions_predicate("unsorted_aggregate").
is_a_all_solutions_predicate("std_util__unsorted_aggregate").
is_a_all_solutions_predicate("do_while").
is_a_all_solutions_predicate("std_util__do_while").
:- pred remove_goal_path(call_path, call_number).
:- mode remove_goal_path(in, out) is det.
remove_goal_path(CallNumber - _GoalPath, CallNumber).
:- pred remove_sol_at_redo_port(call_number, call_number,
goal_successors_table, goal_successors_table,
proof_tree_table, proof_tree_table).
:- mode remove_sol_at_redo_port(in, in, in, out, in, out) is det.
remove_sol_at_redo_port(CurrentCN, FatherCN, GoalSuccT0, GoalSuccT,
ProofT0, ProofT) :-
% Get the successors list of the father of the current goal.
map__lookup(GoalSuccT0, FatherCN, SuccList),
list__filter(call_number_is_bigger(CurrentCN), SuccList, NewSuccList),
map__det_update(GoalSuccT0, FatherCN, NewSuccList, GoalSuccT),
% We also remove the corresponding proof trees
list__delete_elems(SuccList, NewSuccList, FailList),
remove_proof_trees(ProofT0, FailList, ProofT).
:- pred call_number_is_bigger(call_number, call_path).
:- mode call_number_is_bigger(in, in) is semidet.
call_number_is_bigger(CN1, CN2 - _GoalPath2) :-
CN1 > CN2.
:- pred remove_sol_disj_branch(goal_path_string, call_number,
goal_successors_table, goal_successors_table,
proof_tree_table, proof_tree_table).
:- mode remove_sol_disj_branch(in, in, in, out, in, out) is det.
remove_sol_disj_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
ProofT0, ProofT) :-
( if get_goal_path_previous_disj(GoalPath, GoalPathPrev) then
% Get the successors list of the father of the current goal.
map__lookup(GoalSuccT0, CurrentCN, SuccList),
% From this list of successors, we want to remove all the
% call_path that were in the previous disjunction, as well as
% the solutions that were produced after; to do
% that, we use the goal path information.
list__filter(goal_path_is_after(GoalPathPrev),
SuccList, NewSuccList),
map__det_update(GoalSuccT0, CurrentCN, NewSuccList, GoalSuccT),
% We also remove the corresponding proof trees
list__delete_elems(SuccList, NewSuccList, FailList),
remove_proof_trees(ProofT0, FailList, ProofT)
else
GoalSuccT = GoalSuccT0,
ProofT = ProofT0
).
:- pred remove_sol_then_branch(goal_path_string, call_number,
goal_successors_table, goal_successors_table,
proof_tree_table, proof_tree_table).
:- mode remove_sol_then_branch(in, in, in, out, in, out) is det.
remove_sol_then_branch(GoalPath, CurrentCN, GoalSuccT0, GoalSuccT,
ProofT0, ProofT) :-
( if string__remove_suffix(GoalPath, "e;", GoalPathIfBranch) then
append(GoalPathIfBranch, "t;", GoalPathThenBranch),
% Get the succesors list of the current of the current goal.
map__lookup(GoalSuccT0, CurrentCN, SuccList),
% From this list of successors, we want to remove all the
% call_path that were in the then branch, as well as
% the solutions that were produced after; to do
% that, we use the goal path information.
list__filter(goal_path_is_after(GoalPathThenBranch),
SuccList, NewSuccList),
map__det_update(GoalSuccT0, CurrentCN, NewSuccList, GoalSuccT),
% We also remove the corresponding proof trees
list__delete_elems(SuccList, NewSuccList, FailList),
remove_proof_trees(ProofT0, FailList, ProofT)
else
error("Not an ite_else event")
).
:- pred remove_proof_trees(proof_tree_table, list(call_path),
proof_tree_table).
:- mode remove_proof_trees(in, in, out) is det.
remove_proof_trees(ProofT0, [], ProofT0).
remove_proof_trees(ProofT0, [CN-_|Tail], ProofT) :-
map__det_remove(ProofT0, CN, _, ProofT1),
remove_proof_trees(ProofT1, Tail, ProofT).
% goal_path_is_after(Path1, _ - Path2) is true iff Path1
% occurs <<after>> Path2 in the goal.
%
% The idea is that when we enter the branch of a disjunction,
% we need to remove all the solutions that were produced after
% as well as the solutions that were produced in the previous disjunction.
%
% Ex: goal_path_is_after("d3;c4;d3;d3", _ - "d3;c4;d2;t")
% goal_path_is_after("d3;e;c6;d9", _ - "d4;e;")
:- pred goal_path_is_after(goal_path_string, call_path).
:- mode goal_path_is_after(in, in) is semidet.
goal_path_is_after(GoalPath1, _CN2 - GoalPath2) :-
string__words(is_semi_column, GoalPath1) = ListPath1,
string__words(is_semi_column, GoalPath2) = ListPath2,
goal_path_is_after2(ListPath1, ListPath2).
:- pred is_semi_column(char::in) is semidet.
is_semi_column(';').
:- pred goal_path_is_after2(list(string)::in, list(string)::in) is semidet.
goal_path_is_after2([Path1|Tail1], [Path2|Tail2]) :-
( Path1 = Path2 ->
goal_path_is_after2(Tail1, Tail2)
;
atomic_path_is_after(Path1, Path2)
).
:- pred atomic_path_is_after(string::in, string::in) is semidet.
% atomic_path_is_after(Path1, Path2) succeeds iff Path1 < Path2
atomic_path_is_after(Path1, Path2) :-
(
Path2 = ""
->
% "s2;d2;d4;" is after "s2;d2;"
true
;
append(L, Int1Str, Path1),
append(L, Int2Str, Path2),
( L = "c" ; L = "d"),
string__det_to_int(Int1Str) = Int1,
string__det_to_int(Int2Str) = Int2
->
Int1 > Int2
;
( Path1 = "e" ; Path1 = "t"), Path2 = "?"
).
:- pred remove_current_cn(call_number, call_path).
:- mode remove_current_cn(in, in) is semidet.
remove_current_cn(N1, N2 - _) :-
not (N1 = N2).
:- pred get_goal_path_previous_disj(goal_path_string, goal_path_string).
:- mode get_goal_path_previous_disj(in, out) is semidet.
% Takes a goal path of the form "<path>;di;" (where i>0), and outputs the
% goal path "<path>;di-1;" if i>1, fails otherwise
get_goal_path_previous_disj(GoalPath, GoalPathPrev) :-
reverse_string(GoalPath, GoalPathRev),
( if
string__sub_string_search(GoalPathRev, "d", Index1)
then
Index = Index1
else
error("No disjunction is found in this string")
),
string__split(GoalPathRev, Index, NRevStr0, GoalPathTailRev),
% remove the ";"
string__append(";", NRevStr, NRevStr0),
% check that it is not the first disjunction
not (NRevStr = "1"),
reverse_string(GoalPathTailRev, GoalPathTail),
reverse_string(NRevStr, NStr),
( if string__to_int(NStr, N0) then
NPrev is N0 - 1
else
error("Should be an integer")
),
string__int_to_string(NPrev, NPrevStr),
string__append_list([GoalPathTail, NPrevStr, ";"], GoalPathPrev).
:- pred reverse_string(string, string).
:- mode reverse_string(in, out) is det.
reverse_string(String, StringRev) :-
% Is this the most efficient way to do that?
string__to_char_list(String, Char),
string__from_rev_char_list(Char, StringRev).
:- pred update_goal_path(event::in,
goal_path_string::in, goal_path_string::out,
% To get rigth goal path
% at call ports.
stack(goal_path_string)::in, stack(goal_path_string)::out,
% To get rigth goal path
% at exit and fail ports.
stack(goal_path_string)::in, stack(goal_path_string)::out
% To get rigth goal path
% at redo ports.
) is det.
% For efficiency, this should be interwined inside filter. I did not
% do that for the sake of clarity and reusability.
% Hopefully, the deforestration optimisation should be able to
% work here.
update_goal_path(Event, GoalPath0, GoalPath, DetStack0, DetStack,
NonDetStack0, NonDetStack) :-
Port = port(Event),
Det = determinism(Event),
(
Port = call
->
stack__push(DetStack0, GoalPath0, DetStack),
NonDetStack = NonDetStack0,
GoalPath = GoalPath0
;
Port = exit
->
stack__pop_det(DetStack0, GoalPath, DetStack),
( nondet_or_multi(Det) ->
% Only nondet and multi proc have redo ports
stack__push(NonDetStack0, GoalPath, NonDetStack)
;
NonDetStack = NonDetStack0
)
;
Port = redo
->
stack__pop_det(NonDetStack0, GoalPath, NonDetStack),
stack__push(DetStack0, GoalPath, DetStack)
;
Port = fail
->
stack__pop_det(DetStack0, GoalPath, DetStack),
NonDetStack = NonDetStack0
;
% At internal events, the goal path is available
GoalPath = goal_path(Event),
NonDetStack = NonDetStack0,
DetStack = DetStack0
).
:- pred nondet_or_multi(determinism::in) is semidet.
nondet_or_multi(3). % nondet
nondet_or_multi(7). % multi
:- pred update_call_stack(trace_port_type, call_number, stack(call_number),
stack(call_number)).
:- mode update_call_stack(in, in, in, out) is det.
update_call_stack(Port, Current, CallStack0, CallStack) :-
(
( Port = call ; Port = redo )
->
stack__push(CallStack0, Current, CallStack)
;
( Port = exit ; Port = fail )
->
stack__pop_det(CallStack0, _, CallStack)
;
CallStack = CallStack0
).
post_process(ct(_, _, _, _, _, _, ProofTreeTable), ProofTree) :-
( map__to_assoc_list(ProofTreeTable, [1 - [ProofTree0] | _]) ->
ProofTree = ct(ProofTree0)
;
% Should not occur
ProofTree = pb("map__to_assoc_list failed \n")
).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: queens2.pt.ps
Type: application/postscript
Size: 29485 bytes
Desc: queens2.pt.ps
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20010716/632046fb/attachment.ps>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: foo.pt.ps
Type: application/postscript
Size: 8094 bytes
Desc: foo.pt.ps
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20010716/632046fb/attachment-0001.ps>
-------------- next part --------------
:- module foo.
:- interface.
:- import_module io.
:- pred main(io__state, io__state).
:- mode main(di, uo) is det.
:- implementation.
:- import_module list, int, std_util.
main -->
{ foo__solutions(p, Solutions) },
print( Solutions).
:- pred p(pair(int)::out) is multi.
p(A-B) :-
(
q(A)
;
r(A)
),
(
s(B)
;
t(B)
).
:- pred q(int::out) is det.
:- pred r(int::out) is det.
:- pred s(int::out) is det.
:- pred t(int::out) is det.
q(1).
r(2).
s(3).
t(4).
%-----------------------------------------------------------------------%
%
% This is to be able to see the call to solutions/2 in the trace.
:- pred foo__solutions(pred(T), list(T)).
:- mode foo__solutions(pred(out) is multi, out) is det.
:- mode foo__solutions(pred(out) is nondet, out) is det.
foo__solutions(Pred, List) :-
std_util__solutions(Pred, List).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: foo.bad.ps
Type: application/postscript
Size: 5151 bytes
Desc: foo.bad.ps
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20010716/632046fb/attachment-0002.ps>
-------------- next part --------------
R1.
More information about the reviews
mailing list