[m-rev.] a proof tree monitor

[Mark Brown]

On 12-Jul-2001, Erwan Jahier <Erwan.Jahier at irisa.fr> wrote:
> 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. 

Definitely.

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

Sure.  I have a couple of comments about the code.

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

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.

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

> +		;
> +			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)
> +			)

Ditto.

> +		),
> +		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),

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

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

s/previous disjunction/condition/

I suspect this code would have the same bug as with disjunctions.

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