[m-rev.] a proof tree monitor

[Erwan Jahier]

I wrote that a long time ago too, and I think it is worth including it in the
cvs repository as a more involved monitor example you can define with collect. 

I am not 100 % confident that it is the best/simple way to compute a proof
tree from the trace, but at least it works. Maybe Mark would have some comments
about that code if he wishes.

--
Estimated hours taken: 20
branches: main.

Add a monitor that computes the program execution proof tree.

extras/morphine/source/collect__proof_tree:
	A new monitor that computes the program execution proof tree
	(New file).

extras/morphine/source/control_flow.op:
	Add support for calling the proof_tree monitor from Morphine.

Index: extras/morphine/source/collect__proof_tree
===================================================================
RCS file: collect__proof_tree
diff -N collect__proof_tree
--- /dev/null	Wed Nov 15 09:24:47 2000
+++ collect__proof_tree	Thu Jul 12 21:39:55 2001
@@ -0,0 +1,398 @@
+%------------------------------------------------------------------------------%
+% 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, 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 = [] ->
+			( map__update(ProofT0, CurrentCN, 
+				leaf(CurrentCN, CurrentPred), ProofT1) ->
+				ProofT = ProofT1
+			;
+			        map__det_insert(ProofT0, CurrentCN, 
+				        leaf(CurrentCN, CurrentPred), ProofT)
+		        ) 
+		;
+			list__map(map__lookup(ProofT0), ListCN, ListTrees),
+			( map__update(ProofT0, CurrentCN, 
+				tree(CurrentCN, CurrentPred, ListTrees), 
+				ProofT1) ->
+				ProofT = ProofT1
+			;
+			        map__det_insert(ProofT0, CurrentCN, 
+				    tree(CurrentCN, CurrentPred, ListTrees), 
+				    ProofT)
+			)
+		),
+		AllSolList = AllSolList0
+	;
+		Port = fail
+	->
+		stack__top_det(CallStack, 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.
+		        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 to the 
+		% 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)
+		;
+		        remove_sol_if_branch(GoalPath, CurrentCN,
+		                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_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),
+	        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_if_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, 
+	ProofT0, ProofT) :-
+	( if string__remove_suffix(GoalPath, "e;", GoalPathIfBranch) then
+                % 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 
+		% that, we use the goal path information.
+		list__filter(remove_this_goal_path(GoalPathIfBranch), 
+	                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).
+
+:- 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).
+
+:- 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", Index0) then
+                Index = Index0 
+	  else
+                error("No disjunctions is find 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") 
+	).
Index: extras/morphine/source/control_flow.op
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/morphine/source/control_flow.op,v
retrieving revision 1.5
diff -u -d -u -r1.5 control_flow.op
--- extras/morphine/source/control_flow.op	2001/07/12 07:32:09	1.5
+++ extras/morphine/source/control_flow.op	2001/07/12 11:39:55
@@ -257,3 +257,225 @@
 	).   
 
 
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+opium_command(
+	name		: proof_tree,
+	arg_list	: [ProgramCall],
+	arg_type_list	: [is_mercury_program_call],
+	abbrev		: pt,
+	interface	: button,
+	command_type	: opium,
+	implementation	: proof_tree_Op,
+	parameters	: [ps_viewer],
+	message		:
+"Computes the program proof tree."
+	).
+
+proof_tree_Op(Program) :-
+	run(Program),
+	generate_filename(Program, ".pt.dot", ".pt.ps", DotFile, PsFile),
+	generate_proof_tree_graph(Graph),
+	display_graph(Graph, DotFile, PsFile).
+
+%
+%:- pred generate_dynamic_call_graph(graph).
+%:- mode generate_dynamic_call_graph(out) is det.
+%
+
+generate_proof_tree_graph(G) :-
+	getenv("MERCURY_MORPHINE_DIR", MorphineDir),
+	append_strings(MorphineDir, "/source/collect__proof_tree", 
+		CollectFile),
+	collect(CollectFile, Result),
+	( Result = ct(ProofTree), ! ; Result = pb(Msg), print(Msg), abort), 
+	tree_to_graph(0:toplevel, ProofTree, G).
+
+tree_to_graph(Father, leaf(CN, PredUniv), [arc(Father, CN:Pred)]) :-
+	remove_type_pred(PredUniv, Pred).
+tree_to_graph(Father, tree(CN, PredUniv, TreeList), Graph) :-
+	remove_type_pred(PredUniv, Pred),
+	maplist(tree_to_graph(CN:Pred), TreeList, GraphList),
+	list_of_list_to_list(GraphList, Graph0),
+	Graph = [arc(Father, CN:Pred) | Graph0].
+
+remove_type_pred(p(NameStr, _Arity, ArgUnivList), Pred) :-
+	maplist(remove_type_arg, ArgUnivList, ArgList),
+	( string(NameStr) -> atom_string(Name, NameStr) ; Name = NameStr),
+	append([Name], ArgList, NameArgList),
+	Pred =.. NameArgList.
+
+remove_type_arg(univ_cons(state('<<c_pointer>>')), '-'). % We don't display that
+remove_type_arg(univ_cons(Arg), Arg).
+
+
+list_of_list_to_list([], []).
+list_of_list_to_list([List], List).
+list_of_list_to_list([List1, List2 | Tail], LList) :-
+	append(List1, List2, List),
+	LList0 = [List | Tail],
+	list_of_list_to_list(LList0, LList).
+
+
-- 
R1.


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