For review: declarative debugging back end (3/3)

[Mark Anthony BROWN]

Note for reviewers:  the following module contains large commented out
sections.  These parts are not yet used, but show roughly how I intend the
module to work (in the near future).

%-----------------------------------------------------------------------------%
% Copyright (C) 1998 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: evaluation_tree.m
% Author: dougl
% Stability: low
%
% Purpose:
% 	This module defines the interface to a Mercury Evaluation
% 	Dependence Tree (EDT), a data structure that holds the representation
% 	of a justification of program behaviour in terms of the declarative
% 	semantics of the language.
%
% 	An EDT for which the top node represents an incorrect result
% 	exhibits a "symptom" (eg: wrong answer, missing answer, etc); an
% 	EDT which exhibits a symptom, but which contains no direct
% 	children that exhibit symptoms, is an "error" (eg: incorrect
% 	clause instance, uncovered atom, etc).
%
% Rationale:
% 	An EDT can be used by a declarative debugger to search for
% 	errors in terms of symptoms.  This is achieved with a two level
% 	architecture: a back end generates EDTs for a running program,
% 	and a front end searches them for errors.
%
%	To support this, the interface to an EDT is decoupled from its
%	implementation.  The front end of a declarative debugger should
%	use the interface provided for the type evaluation_tree/1 and the
%	typeclass evaluation_atom/1, and their associated access procedures,
%	to analyse the EDT.  The back end should provide an instance
%	of evaluation_atom (NB: this is the purpose of the compiler
%	module evaluation_tree_gen.m).
%
%	The chief advantage of this decoupling is that a debuggee module
%	(back end) is free to vary the implementation of atoms without
%	affecting the debugger (ie the compiled debugger does not depend
%	on the debuggee's representation of atoms).  In particular, this
%	allows a debugger to be written, compiled and distributed _before_
%	the debuggee is written, without resorting to the use of the
%	ground representation.
%
% Design:
% 	The decoupling is achieved by parametrizing most of the types in
% 	this module with the type used to represent atoms, which must be
% 	an instance of the evaluation_atom typeclass.  This module uses
% 	one of the type variables 'A' or 'E' whenever such a type is
% 	expected.

:- module evaluation_tree.
:- interface.

:- import_module io, std_util, list.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% This section declares data common to the front and back ends.
%

	%
	% An evaluation_tree holds an EDT for Mercury.
	%
	% 	*_wrong		An EDT that can be used for wrong answer
	% 			analysis.  For these EDTs, a goal
	% 			behaviour is a computed answer (an
	% 			evaluation_atom in its final state), and
	% 			a goal justification is a proof_tree.
	%
	%	*_miss		An EDT that can be used for missing
	%			answer analysis.  In this case, a goal
	%			behaviour is an evaluation_atom in its
	%			initial state and a set of computed
	%			answers, and a goal justification is
	%			a miss_tree.
	%
	% 	analyse_*	A pair representing a goal behaviour
	% 			and a goal justification.
	%
	%	interface_*	A node representing a goal behaviour.
	%			The justification is not explicitly
	%			represented, but we assume that all 
	%			children were symptom-free.
	%
	%	implicit_*	A node representing a goal behaviour.
	%			The justification is not explicitly
	%			represented, and we make no assumptions
	%			about it.
	%
	%	assumed		The EDT is assumed to be symptom-free.
	%
	
:- type evaluation_tree(A)
	--->	analyse_wrong(wrong_node(A), proof_tree(A))
	;	analyse_miss(miss_node(A), miss_tree(A))
	;	interface_wrong(wrong_node(A))
	;	interface_miss(miss_node(A))
	;	implicit_wrong(wrong_node(A))
	;	implicit_miss(miss_node(A))
	;	assumed.


	%
	% The elements of type *_node represent goal behaviours for the
	% kinds of analysis that EDTs are used for.
	%
	% For wrong answer analysis, we store the computed answer.
	%
	
:- type wrong_node(A) == A.

	%
	% For missing answer analysis, we store the atom in its initial
	% instantiatedness, along with the set of its computed answers,
	% represented as a list.
	%
	
:- type miss_node(A) == pair(A, list(A)).

	%
	% The front end can request an analysis of a particular atom.
	% The back end should generate an element of the following type
	% (and inst).
	%
	
:- type analysis(A)
	--->	nondet_wrong(pred(evaluation_tree(A)))
	;	multi_wrong(pred(evaluation_tree(A)))
	;	semidet_wrong(pred(evaluation_tree(A)))
	;	det_wrong(pred(evaluation_tree(A)))
	;	wrong_io(pred(evaluation_tree(A), io__state, io__state))
	;	miss(pred(evaluation_tree(A)))
	;	miss_io(pred(evaluation_tree(A), io__state, io__state))
	;	unavailable.

:- inst analysis =
	bound(		nondet_wrong(pred(out) is nondet)
		;	multi_wrong(pred(out) is multi)
		;	semidet_wrong(pred(out) is semidet)
		;	det_wrong(pred(out) is det)
		;	wrong_io(pred(out, di, uo) is det)
		;	miss(pred(out) is det)
		;	miss_io(pred(out, di, uo) is det)
		;	unavailable
	).

	%
	% The back end must provide a way of converting terms in the ground
	% representation to atoms.  The following is the result type of
	% such a conversion.
	%

:- type atom_result(A)
	--->	ok(A)
	;	type_error
	;	mode_error
	;	undefined_atom
	;	not_an_atom.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% This section contains the interface to the front end.
%

:- type evaluation_node(A)
	--->	wrong(wrong_node(A))
	;	miss(miss_node(A))
	;	interface_wrong(wrong_node(A))
	;	interface_miss(miss_node(A))
	;	assumed.

:- type evaluation_node_type
	--->	explicit
	;	implicit
	;	interface
	;	assumed.

/*
	% 
	% These procedures are used for traversing an evaluation_tree.
	%
	
:- pred root(evaluation_tree(A), evaluation_node(A), evaluation_node_type)
		<= evaluation_atom(A).
:- mode root(in, out, out) is det.

:- pred local_child(evaluation_tree(A), evaluation_tree(A))
		<= evaluation_atom(A).
:- mode local_child(in, out) is nondet.

	%
	% Each atom is in one of the following states.
	%

:- type inst_state
	--->	initial		% The atom represents the inputs to a call.
	;	final.		% The atom represents a computed answer.

	%
	% These procedures convert terms using the ground representation
	% into atoms.  Note that the type variable 'A' is universally
	% quantified.  This means that the context of the caller
	% determines the value of A; these procedures attempt to match
	% the term against those atoms that can be represented by A.
	%

:- pred find_matching_atom_and_mode(inst_state, int, term, atom_result(A))
		<= evaluation_atom(A).
:- mode find_matching_atom_and_mode(in, in, in, out) is det.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% This section contains the interface that the back end must
% conform to.
%

	%
	% A module that can act as a back end (ie, generate
	% evaluation_trees) is free to choose any type to represent atoms.
	% The module must provide an interface that makes the type an
	% instance of the following typeclass.
	%
	
:- typeclass evaluation_atom(A) where [
	pred atom_to_wrong_analysis(A::in, analysis(A)::out(analysis)) is det,
	pred atom_to_miss_analysis(A::in, analysis(A)::out(analysis)) is det,
	pred term_to_atom(term::in, atom_result(A)::out) is det,
	pred atom_to_term(A::in, term::out) is det
].

*/

	%
	% For wrong answer analysis, the goal justification is a
	% proof_tree for a computed answer.
	%
	
:- type proof_tree(A)
	--->	local_call(evaluation_tree(A))
%	;	some [E] external_call(evaluation_tree(E))
%			<= evaluation_atom(E)
	;	conj(list(proof_tree(A)))
	;	disj(int, proof_tree(A))
	;	switch(int, proof_tree(A))
	;	if_then(proof_tree(A), proof_tree(A))
	;	else(miss_tree(A), proof_tree(A))
	;	not(miss_tree(A))
	;	trivial.

	%
	% For missing answer analysis also, the goal justification is a
	% tree that corresponds to the structure of the program.  It is
	% the dual of the above structure: it represents which atoms
	% were _not_ computed answers.
	%
	
:- type miss_tree(A)
	--->	local_call(evaluation_tree(A))
%	;	some [E] external_call(evaluation_tree(E))
%			<= evaluation_atom(E)
	;	conj(list(miss_tree(A)))
	;	disj(list(miss_tree(A)))
	;	switch(list(miss_tree(A)))
	;	if_then(miss_tree(A), miss_tree(A))
	;	else(proof_tree(A), miss_tree(A))
	;	not(proof_tree(A))
	;	trivial.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

/*

:- implementation.
:- import_module string, int.

root(analyse_wrong(Node, _), wrong(Node), explicit).
root(analyse_miss(Node, _), miss(Node), explicit).
root(interface_wrong(Node), interface_wrong(Node), interface).
root(interface_miss(Node), interface_miss(Node), interface).
root(implicit_wrong(Node), wrong(Node), implicit).
root(implicit_miss(Node), miss(Node), implicit).
root(assumed, assumed, assumed).

local_child(analyse_wrong(_, ProofTree), Child) :-
	proof_tree_child(ProofTree, Child).
local_child(analyse_miss(_, MissTree), Child) :-
	miss_tree_child(MissTree, Child).
	%
	% XXX  Here we should implement the implicit representation
	% of subtrees transparently.  If the caller asks for the child
	% of a implicit_{wrong, miss} node, then we should call
	% atom_to_{wrong, miss}_analysis, then call the resulting
	% closure to create the tree explicitly.
	%

:- pred proof_tree_child(proof_tree(A), evaluation_tree(A)).
:- mode proof_tree_child(in, out) is nondet.

proof_tree_child(local_call(C), C).
proof_tree_child(conj(Ps), C) :-
	list__member(P, Ps),
	proof_tree_child(P, C).
proof_tree_child(disj(_, P), C) :-
	proof_tree_child(P, C).
proof_tree_child(switch(_, P), C) :-
	proof_tree_child(P, C).
proof_tree_child(if_then(P, _), C) :-
	proof_tree_child(P, C).
proof_tree_child(if_then(_, P), C) :-
	proof_tree_child(P, C).
proof_tree_child(else(M, _), C) :-
	miss_tree_child(M, C).
proof_tree_child(else(_, P), C) :-
	proof_tree_child(P, C).
proof_tree_child(not(M), C) :-
	miss_tree_child(M, C).

:- pred miss_tree_child(miss_tree(A), evaluation_tree(A)).
:- mode miss_tree_child(in, out) is nondet.

miss_tree_child(local_call(C), C).
miss_tree_child(conj(Ms), C) :-
	list__member(M, Ms),
	miss_tree_child(M, C).
miss_tree_child(disj(Ms), C) :-
	list__member(M, Ms),
	miss_tree_child(M, C).
miss_tree_child(switch(Ms), C) :-
	list__member(M, Ms),
	miss_tree_child(M, C).
miss_tree_child(if_then(M, _), C) :-
	miss_tree_child(M, C).
miss_tree_child(if_then(_, M), C) :-
	miss_tree_child(M, C).
miss_tree_child(else(P, _), C) :-
	proof_tree_child(P, C).
miss_tree_child(else(_, M), C) :-
	miss_tree_child(M, C).
miss_tree_child(not(P), C) :-
	proof_tree_child(P, C).

%-----------------------------------------------------------------------------%

find_matching_atom_and_mode(InstState, ModeNum, Term0, AtomResult) :-
	( Term0 = term__functor(term__atom(Atom0), Args, Context) ->
		add_mode_suffix(Atom0, ModeNum, Atom1),
		add_inst_state_suffix(Atom1, InstState, Atom),
		Term = term__functor(term__atom(Atom), Args, Context),
		term_to_atom(Term, AtomResult)
	;
		AtomResult = not_an_atom
	).


:- pred add_mode_suffix(string, int, string).
:- mode add_mode_suffix(in, in, out) is det.

add_mode_suffix(Name0, ModeNum, Name) :-
	string__format("%s_%i", [s(Name0), i(ModeNum)], Name).

:- pred add_inst_state_suffix(string, inst_state, string).
:- mode add_inst_state_suffix(in, in, out) is det.

add_inst_state_suffix(Name0, InstState, Name) :-
	(
		InstState = initial,
		Suffix = "_initial"
	;
		InstState = final,
		Suffix = "_final"
	),
	string__append(Name0, Suffix, Name).
	
*/

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
% Copyright (C) 1998 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%

% File: proof_tree.m
% Author: dougl
% Purpose:
%
% This module is an HLDS transformation that implements the proof tree
% generation required by evaluation_tree_gen.m for declarative
% debugging (of wrong answers).
%
% For each predicate that is to be debugged, a new predicate is created.
% This has one procedure for each procedure of the original.  The new versions
% are the same except that they have an extra argument (with mode out)
% containing the proof tree, and that they call the debugging versions of
% subgoals whenever possible.  In particular, the determinism does not
% change, and there is a one to one correspondence between the original
% modes and the new modes.
%
% The transformation can be described by the following relations.
%
% 	pw : Procedure -> Procedure
%
% 		pw[[ Proc ]] denotes the transformed version of Proc.
%
% 	gw : Procedure x Var -> Procedure
%
% 		gw[[ Goal, Proof ]] denotes Goal transformed so as to
% 		produce a proof tree in Proof.
%
% 	cw : Atom x Var -> Atom
%
% 		cw[[ Call, EDT ]] denotes a call to the version of Call
% 		which produces an evaluation tree in EDT.
%
% 	aw : Atom x Var -> Atom
%
% 		aw[[ Atom, EDT ]] is the same as Atom, but has EDT as
% 		an extra argument.
%
% The relations also refer to gm, which is the same as gw except that
% the structure produced is a miss tree rather than a proof tree.
%
% pw[[ Head :- Body ]] =
% 	aw[[ Head, EDT ]] :- (gw[[ Body, P ]], EDT = analyse_wrong(Head, P))
%
% gw[[ (G1, ..., Gn), P ]] =
% 	(gw[[ G1, P1 ]], ..., gw[[ Gn, Pn ]], P = conj([Pn, ..., P1]))
% gw[[ (G1; ...; Gn), P ]] =
% 	(((gw[[ G1, Pd ]], Arm = 1); ...; (gw[[ Gn, PD ]], Arm = n)),
% 	P = disj(Arm, PD))
% gw[[ (some Vs G), P ]] =
% 	(some Vs gw[[ G, P ]])
% gw[[ (not G), P) ]] =
% 	(not G, gm[[ G, M ]], P = not(M))
% gw[[ (Term1 = Term2), P ]] =
% 	(Term1 = Term2, P = trivial)
% gw[[ (Cond -> Then ; Else), P ]] =
% 	(gw[[ Cond, PC ]] -> (gw[[ Then, PT ]], P = if_then(PC, PT))
% 		; (gm[[ Cond, MC ]], gw[[ Else, PE ]], P = else(MC, PE)))
% gw[[ call(Closure, ...), P ]] =
% 	(call(Closure, ...), P = trivial)
% gw[[ LocalCall, P ]] =
% 	(cw[[ Call, EDT ]], P = local_call(EDT))
% gw[[ ExternalCall, P ]] =
% 	(ExternalCall, EDT = assumed, P = external_call(EDT))
%
% cw[[ Call, EDT ]] =
% 	aw[[ Call, EDT ]]		, if Call is a proc with
% 					  a wrong answer version
% 	(Call, EDT = assumed)		, otherwise
%
% aw[[ foo(A1, ..., An), EDT ]] =
% 	foo(A1, ..., An, EDT)
%
% XXXs:
%
%     - The transformation as described does not do anything useful for
%       higher order calls or calls to external predicates (it treats
%       them as it will treat builtins in future).  This means that any
%       front end will act as if it assumes such calls are correct, and
%       it will not search them for bug instances.  This will change
%       when more support for external calls (firstly) and higher order
%       calls (secondly) is added.
%
%     - According to the above transformation, proof trees will in
%       general contain a large number of trivial subtrees which are
%       usually not useful.  As an optimisation, the actual
%       transformation avoids building trivial subtrees where possible.
%       The consequence of this is that proof trees built for
%       conjunctions will _not_ always be of the form conj([Pn, ..., P1]).
%       Some of the subtrees will not be included in the list, so it
%       could be of the form (say) conj([P6, P5, P3, P1]).  However, a
%       front end can still use this effectively if we record which
%       conjunct corresponds to each list member, or if we always decide
%       in a consistent way which ones to exclude.
% 			
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- module proof_tree.
:- interface.

:- import_module hlds_module, hlds_pred, evaluation_tree_util.

	%
	% Perform the transformation on the proc referred to by the
	% edt_proc_info.
	%
:- pred proof_tree__create_proc(module_info, edt_info, edt_proc_info,
		module_info).
:- mode proof_tree__create_proc(in, in, in, out) is det.

	%
	% Make a predicate with the required signature.  Used by the
	% first pass of the evaluation_tree compiler phase.
	%
:- pred make_wrong_answer_pred_stub(edt_info, module_info, pred_id, pred_info).
:- mode make_wrong_answer_pred_stub(in, in, in, out) is det.

	%
	% Make the procedure which converts an atom to a closure with
	% that atom as a goal.
	%

:- pred proof_tree__make_wrong_analysis_pred(module_info, edt_info, pred_info).
:- mode proof_tree__make_wrong_analysis_pred(in, in, out) is det.

%-----------------------------------------------------------------------------%

:- implementation.

:- import_module hlds_goal, hlds_data, prog_data, (inst), globals, instmap.

:- import_module map, std_util, term, list, require, int, varset, set.

proof_tree__create_proc(Module0, EDTInfo, EDTProcInfo, Module) :-

	edt_proc_info_get_wrong_proc(EDTProcInfo, WrongPredId, WrongProcId),
	module_info_preds(Module0, PredTable0),
	map__lookup(PredTable0, WrongPredId, WrongPredInfo0),
	pred_info_procedures(WrongPredInfo0, WrongProcs0),
	map__lookup(WrongProcs0, WrongProcId, ProcInfo0),

	transform_proc(EDTInfo, EDTProcInfo, ProcInfo0, ProcInfo),

	map__det_update(WrongProcs0, WrongProcId, ProcInfo, WrongProcs),
	pred_info_set_procedures(WrongPredInfo0, WrongProcs, WrongPredInfo),
	map__det_update(PredTable0, WrongPredId, WrongPredInfo, PredTable),
	module_info_set_preds(Module0, PredTable, Module).


:- pred transform_proc(edt_info, edt_proc_info, proc_info, proc_info).
:- mode transform_proc(in, in, in, out) is det.

transform_proc(EDTInfo, EDTProcInfo, ProcInfo0, ProcInfo) :-
	proc_info_goal(ProcInfo0, Goal0),
	Goal0 = GoalExpr0 - GoalInfo0,

	transform_goal(EDTInfo, ProcInfo0, ProcInfo1, GoalExpr0, GoalInfo0,
			MaybeProofVar, GoalExpr1, GoalInfo1),
	maybe_add_trivial_proof(EDTInfo, ProcInfo1, ProcInfo2, GoalExpr1,
			GoalInfo1, GoalExpr2, GoalInfo2, MaybeProofVar,
			ProofVar),

	goal_to_conj_list(GoalExpr2 - GoalInfo2, GoalList0),
	make_node_construction(EDTInfo, EDTProcInfo, ProcInfo2, ProcInfo3,
			NodeVar, NodeConsGoals),

		%
		% We use the unmodified hlds_goal_info as input here
		% because the proof_tree variable is not nonlocal in the
		% outer conjunction.
		%
	create_evaluation_tree_head_var(EDTInfo, ProcInfo3, ProcInfo4,
			GoalInfo0, GoalInfo, EDTVar),
	evaluation_tree_ctor_analyse_wrong(EDTConsId),
	make_simple_construction(EDTVar, EDTConsId, [NodeVar, ProofVar],
			EDTConsGoal),

	list__append(NodeConsGoals, [EDTConsGoal], GoalList1),
	list__append(GoalList0, GoalList1, GoalList),
	Goal = conj(GoalList) - GoalInfo,
	proc_info_set_goal(ProcInfo4, Goal, ProcInfo).


:- pred make_node_construction(edt_info, edt_proc_info, proc_info, proc_info,
		var, hlds_goals).
:- mode make_node_construction(in, in, in, out, out, out) is det.

make_node_construction(EDTInfo, EDTProcInfo, ProcInfo0, ProcInfo, Var,
		Goals) :-

		%
		% For wrong answer analysis, a node is just an atom in
		% its final instantiatedness state.
		%
	make_final_atom_construction(EDTInfo, EDTProcInfo, ProcInfo0, ProcInfo,
			Var, Goals).


:- pred transform_goal(edt_info, proc_info, proc_info, hlds_goal_expr,
		hlds_goal_info, maybe(var), hlds_goal_expr, hlds_goal_info).
:- mode transform_goal(in, in, out, in, in, out, out, out) is det.

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		yes(ProofVar), GoalExpr, GoalInfo) :-

	GoalExpr0 = conj(Goals0),

	create_proof_tree_list_var(EDTInfo, ProcInfo0, ProcInfo1,
			ProofListVar0),
	library_ctor_list_nil(NilConsId),
	make_simple_construction(ProofListVar0, NilConsId, [], InitGoal),

	transform_conj_list(EDTInfo, ProcInfo1, ProcInfo2, ProofListVar0, 
			ProofListVar, Goals0, [InitGoal], Goals1),

	create_proof_tree_var(EDTInfo, ProcInfo2, ProcInfo, GoalInfo0,
			GoalInfo, ProofVar),

	proof_tree_ctor_conj(ConjConsId),
	make_simple_construction(ProofVar, ConjConsId, [ProofListVar],
			NewGoal),
	list__append(Goals1, [NewGoal], Goals),
	GoalExpr = conj(Goals).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		yes(ProofVar), GoalExpr, GoalInfo) :-

	GoalExpr0 = call(PredId, ProcId, Args, BuiltinState, Context,
			SymName),

	transform_call(EDTInfo, ProcInfo0, ProcInfo, PredId, ProcId, Args,
			BuiltinState, Context, SymName, GoalInfo0, ProofVar,
			GoalExpr, GoalInfo).

transform_goal(_EDTInfo, ProcInfo, ProcInfo, GoalExpr, GoalInfo, no,
		GoalExpr, GoalInfo) :-

	GoalExpr = higher_order_call(_, _, _, _, _, _).

transform_goal(_EDTInfo, ProcInfo, ProcInfo, GoalExpr, GoalInfo, no,
		GoalExpr, GoalInfo) :-

	GoalExpr = class_method_call(_, _, _, _, _, _).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		yes(ProofVar), GoalExpr, GoalInfo) :-
	
	GoalExpr0 = switch(SwitchVar, CanFail, Cases0, StoreMap),

	create_proof_tree_var(EDTInfo, ProcInfo0, ProcInfo1, GoalInfo0,
			GoalInfo, ProofVar),
	list__map_foldl(transform_switch_case(EDTInfo, ProofVar),
			Cases0, Cases, ProcInfo1, ProcInfo),
	GoalExpr = switch(SwitchVar, CanFail, Cases, StoreMap).

transform_goal(_EDTInfo, ProcInfo, ProcInfo, GoalExpr, GoalInfo, no,
		GoalExpr, GoalInfo) :-
	
	GoalExpr = unify(_, _, _, _, _).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0, 
		yes(ProofVar), GoalExpr, GoalInfo) :-
	
	GoalExpr0 = disj(Goals0, StoreMap),

	create_proof_tree_var(EDTInfo, ProcInfo0, ProcInfo1, GoalInfo0,
			GoalInfo, ProofVar),
	list__map_foldl(transform_disjunct(EDTInfo, ProofVar),
			Goals0, Goals, ProcInfo1, ProcInfo),
	GoalExpr = disj(Goals, StoreMap).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		yes(ProofVar), GoalExpr, GoalInfo) :-

	GoalExpr0 = not(NegatedGoalExpr - NegatedGoalInfo),

	transform_negated_context(EDTInfo, ProcInfo0, ProcInfo1, 
			NegatedGoalExpr, NegatedGoalInfo, MissTreeVar,
			NewGoal1),
	create_proof_tree_var(EDTInfo, ProcInfo1, ProcInfo, GoalInfo0,
			GoalInfo, ProofVar),
	proof_tree_ctor_not(NotConsId),
	make_simple_construction(ProofVar, NotConsId, [MissTreeVar], NewGoal2),
	GoalList = [GoalExpr0 - GoalInfo0, NewGoal1, NewGoal2],
	GoalExpr = conj(GoalList).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		MaybeProofVar, GoalExpr, GoalInfo) :-

	GoalExpr0 = some(Vars, GoalExpr1 - GoalInfo1),
	transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr1, GoalInfo1,
			MaybeProofVar, GoalExpr2, GoalInfo2),
	GoalExpr = some(Vars, GoalExpr2 - GoalInfo2),
	(
		MaybeProofVar = yes(ProofVar)
	->
		goal_info_set_nonlocal_grounded(GoalInfo0, ProofVar, GoalInfo)
	;
		GoalInfo = GoalInfo0
	).

transform_goal(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		yes(ProofVar), GoalExpr, GoalInfo) :-
			
	GoalExpr0 = if_then_else(Locals, CondGoal, ThenGoal, ElseGoal,
			StoreMap),

	transform_if_then_else(EDTInfo, ProcInfo0, ProcInfo, Locals,
			CondGoal, ThenGoal, ElseGoal, StoreMap, GoalInfo0,
			ProofVar, GoalExpr, GoalInfo).

transform_goal(_EDTInfo, ProcInfo, ProcInfo, GoalExpr, GoalInfo, no,
		GoalExpr, GoalInfo) :-

	GoalExpr = pragma_c_code(_, _, _, _, _, _, _).

transform_goal(_EDTInfo, ProcInfo, ProcInfo, GoalExpr, GoalInfo, no,
		GoalExpr, GoalInfo) :-

	GoalExpr = par_conj(_, _).


:- pred transform_conj_list(edt_info, proc_info, proc_info, var, var,
		hlds_goals, hlds_goals, hlds_goals).
:- mode transform_conj_list(in, in, out, in, out, in, in, out) is det.

transform_conj_list(EDTInfo, ProcInfo0, ProcInfo, ProofListVar0, ProofListVar,
		[InGoal | InGoals], OutGoals0, OutGoals) :-

	InGoal = GoalExpr0 - GoalInfo0,
	transform_goal(EDTInfo, ProcInfo0, ProcInfo1, GoalExpr0, GoalInfo0,
			MaybeProofVar, GoalExpr1, GoalInfo1),
	Goal1 = GoalExpr1 - GoalInfo1,
	prepend_goal_to_rev_goal_list(Goal1, OutGoals0, OutGoals1),

	(
		MaybeProofVar = yes(ProofVar)
	->
		create_proof_tree_list_var(EDTInfo, ProcInfo1, ProcInfo2,
				ProofListVar1),
		library_ctor_list_cons(ListConsId),
		make_simple_construction(ProofListVar1, ListConsId,
				[ProofVar, ProofListVar0], NewGoal),
		prepend_goal_to_rev_goal_list(NewGoal, OutGoals1, OutGoals2),
		LastProof = ProofListVar1
	;
		ProcInfo2 = ProcInfo1,
		OutGoals2 = OutGoals1,
		LastProof = ProofListVar0
	),

	transform_conj_list(EDTInfo, ProcInfo2, ProcInfo, LastProof,
			ProofListVar, InGoals, OutGoals2, OutGoals).

transform_conj_list(_EDTInfo, ProcInfo, ProcInfo, ProofVar, ProofVar, 
		[], OutGoals0, OutGoals) :-

		%
		% OutGoals0 has accumulated the goals in reverse order, so
		% at the end we reverse again before returning.
		%
	list__reverse(OutGoals0, OutGoals).


:- pred transform_call(edt_info, proc_info, proc_info, pred_id, proc_id,
		list(var), builtin_state, maybe(call_unify_context), sym_name,
		hlds_goal_info, var, hlds_goal_expr, hlds_goal_info).
:- mode transform_call(in, in, out, in, in, in, in, in, in, in, out, out, out)
		is det.

transform_call(EDTInfo, ProcInfo0, ProcInfo, PredId0, ProcId0, Args0,
		BuiltinState, Context, SymName0, GoalInfo0, ProofVar,
		GoalExpr, GoalInfo) :-

	create_evaluation_tree_var(EDTInfo, ProcInfo0, ProcInfo1, GoalInfo0,
			GoalInfo1, EDTVar),
	create_proof_tree_var(EDTInfo, ProcInfo1, ProcInfo, GoalInfo1,
			GoalInfo, ProofVar),

		%
		% Here we assume that the call is local.  If the call is
		% actually external, then at the moment we treat it as
		% if it is assumed correct.
		%
	proof_tree_ctor_local_call(CallConsId),
	make_simple_construction(ProofVar, CallConsId, [EDTVar], NewGoal0),
	GoalList0 = [NewGoal0],

	edt_info_proc_analysis(EDTInfo, PredId0, ProcId0, Analysis),
	((
		Analysis = wrong_answer_analysis(PredId, ProcId)
	;
		Analysis = full_analysis(PredId, ProcId, _, _)
	) ->
		list__append(Args0, [EDTVar], Args),
		wrong_answer_sym_name_mangle(SymName0, SymName),
		NewGoalExpr = call(PredId, ProcId, Args, BuiltinState,
				Context, SymName),

			%
			% GoalInfo1 has EDTVar added to the nonlocals,
			% and going to ground in the instmap_delta.
			%
		GoalList = [NewGoalExpr - GoalInfo1 | GoalList0]
	;
		evaluation_tree_ctor_assumed(AssumedConsId),
		make_simple_construction(EDTVar, AssumedConsId, [],
				NewGoal1),
		GoalList1 = [NewGoal1 | GoalList0],
		GoalExpr0 = call(PredId0, ProcId0, Args0, BuiltinState,
				Context, SymName0),
		GoalList = [GoalExpr0 - GoalInfo0 | GoalList1]
	),
	GoalExpr = conj(GoalList).


:- pred transform_switch_case(edt_info, var, case, case, proc_info, proc_info).
:- mode transform_switch_case(in, in, in, out, in, out) is det.

transform_switch_case(EDTInfo, ProofVar, Case0, Case, ProcInfo0, ProcInfo) :-
	Case0 = case(ConsId, GoalExpr0 - GoalInfo0),
	transform_goal(EDTInfo, ProcInfo0, ProcInfo1, GoalExpr0, GoalInfo0,
			MaybeCaseProofVar, GoalExpr1, GoalInfo1),
	maybe_add_trivial_proof(EDTInfo, ProcInfo1, ProcInfo2, GoalExpr1,
			GoalInfo1, GoalExpr2, GoalInfo2, MaybeCaseProofVar,
			CaseProofVar),

	goal_to_conj_list(GoalExpr2 - GoalInfo2, GoalList0),
	make_arm_id_construction(GoalInfo0, ProcInfo2, ProcInfo, ArmIdVar,
			NewGoal1),

	proof_tree_ctor_switch(SwitchConsId),
	make_simple_construction(ProofVar, SwitchConsId,
			[ArmIdVar, CaseProofVar], NewGoal2),
	list__append(GoalList0, [NewGoal1, NewGoal2], GoalList),
		%
		% We must update the nonlocals and instmap_delta for
		% this switch arm.
		%
	goal_info_set_nonlocal_grounded(GoalInfo0, ProofVar, GoalInfo),
	Case = case(ConsId, conj(GoalList) - GoalInfo).


:- pred transform_disjunct(edt_info, var, hlds_goal, hlds_goal, proc_info,
		proc_info).
:- mode transform_disjunct(in, in, in, out, in, out) is det.

transform_disjunct(EDTInfo, ProofVar, Goal0, Goal, ProcInfo0, ProcInfo) :-
	Goal0 = GoalExpr0 - GoalInfo0,
	transform_goal(EDTInfo, ProcInfo0, ProcInfo1, GoalExpr0, GoalInfo0,
			MaybeDisjProofVar, GoalExpr1, GoalInfo1),
	maybe_add_trivial_proof(EDTInfo, ProcInfo1, ProcInfo2, GoalExpr1,
			GoalInfo1, GoalExpr2, GoalInfo2, MaybeDisjProofVar,
			DisjProofVar),

	goal_to_conj_list(GoalExpr2 - GoalInfo2, GoalList0),
	make_arm_id_construction(GoalInfo0, ProcInfo2, ProcInfo, ArmIdVar,
			NewGoal1),

	proof_tree_ctor_disj(DisjConsId),
	make_simple_construction(ProofVar, DisjConsId,
			[ArmIdVar, DisjProofVar], NewGoal2),
	list__append(GoalList0, [NewGoal1, NewGoal2], GoalList),
		%
		% We must update the nonlocals and instmap_delta for
		% this disjunct.
		%
	goal_info_set_nonlocal_grounded(GoalInfo0, ProofVar, GoalInfo),
	Goal = conj(GoalList) - GoalInfo.


:- pred make_arm_id_construction(hlds_goal_info, proc_info, proc_info, var,
		hlds_goal).
:- mode make_arm_id_construction(in, in, out, out, out) is det.

make_arm_id_construction(GoalInfo, ProcInfo0, ProcInfo, ArmIdVar, NewGoal) :-
	create_int_var(ProcInfo0, ArmIdVar, ProcInfo),
	get_arm_identifier(GoalInfo, ArmId),
	make_simple_construction(ArmIdVar, int_const(ArmId), [], NewGoal).


:- pred get_arm_identifier(hlds_goal_info, int).
:- mode get_arm_identifier(in, out) is det.

get_arm_identifier(GoalInfo, ArmId) :-
	goal_info_get_goal_path(GoalInfo, GoalPath),
	(
		(
			GoalPath = [switch(ArmId0) | _]
		;
			GoalPath = [disj(ArmId0) | _]
		)
	->
		ArmId = ArmId0
	;
		error("get_arm_identifier: not a switch or disj")
	).


:- pred transform_if_then_else(edt_info, proc_info, proc_info, list(var),
		hlds_goal, hlds_goal, hlds_goal, store_map, hlds_goal_info,
		var, hlds_goal_expr, hlds_goal_info).
:- mode transform_if_then_else(in, in, out, in, in, in, in, in, in, out, out,
		out) is det.

transform_if_then_else(EDTInfo, ProcInfo0, ProcInfo, Locals0, CondGoal0,
		ThenGoal0, ElseGoal0, StoreMap, GoalInfo0, ProofVar,
		GoalExpr, GoalInfo) :-

	create_proof_tree_var(EDTInfo, ProcInfo0, ProcInfo1, GoalInfo0,
			GoalInfo, ProofVar),

	CondGoal0 = CondGoalExpr0 - CondGoalInfo0,
	transform_goal(EDTInfo, ProcInfo1, ProcInfo2, CondGoalExpr0,
			CondGoalInfo0, MaybeCondProofVar, CondGoalExpr1,
			CondGoalInfo1),
	maybe_add_trivial_proof(EDTInfo, ProcInfo2, ProcInfo3, CondGoalExpr1,
			CondGoalInfo1, CondGoalExpr, CondGoalInfo,
			MaybeCondProofVar, CondProofVar),
	Locals = [CondProofVar | Locals0],
	CondGoal = CondGoalExpr - CondGoalInfo,

	ThenGoal0 = ThenGoalExpr0 - ThenGoalInfo0,
		%
		% We can throw out the hlds_goal_info because the
		% proof_tree for the `then' branch is not nonlocal -- it
		% is used immediately to construct the proof_tree for
		% the entire goal.
		%
	transform_goal(EDTInfo, ProcInfo3, ProcInfo4, ThenGoalExpr0,
			ThenGoalInfo0, MaybeThenProofVar, ThenGoalExpr1, _),
	maybe_add_trivial_proof(EDTInfo, ProcInfo4, ProcInfo5, ThenGoalExpr1,
			ThenGoalInfo0, ThenGoalExpr2, _, MaybeThenProofVar,
			ThenProofVar),
		%
		% The proof_tree variables for the condition and for the
		% entire if_then_else are nonlocal to the `then' branch.
		%
	goal_info_add_nonlocal(ThenGoalInfo0, CondProofVar, ThenGoalInfo1),
	goal_info_set_nonlocal_grounded(ThenGoalInfo1, ProofVar,
			ThenGoalInfo2),
	ThenGoal2 = ThenGoalExpr2 - ThenGoalInfo2,
	proof_tree_ctor_if_then(IfThenConsId),
	make_simple_construction(ProofVar, IfThenConsId,
			[CondProofVar, ThenProofVar], ExtraThenGoal),
	conjoin_goals(ThenGoal2, ExtraThenGoal, ThenGoal),

	ElseGoal0 = ElseGoalExpr0 - ElseGoalInfo0,
		%
		% We can throw out the hlds_goal_info because the
		% proof_tree for the `else' branch is not nonlocal -- it
		% is used immediately to construct the proof_tree for
		% the entire goal.
		%
	transform_goal(EDTInfo, ProcInfo5, ProcInfo6, ElseGoalExpr0,
			ElseGoalInfo0, MaybeElseProofVar, ElseGoalExpr1, _),
	maybe_add_trivial_proof(EDTInfo, ProcInfo6, ProcInfo7, ElseGoalExpr1,
			ElseGoalInfo0, ElseGoalExpr2, _, MaybeElseProofVar,
			ElseProofVar),
		%
		% This variable is nonlocal to the `else' goal as well
		% as the entire if_then_else.
		%
	goal_info_set_nonlocal_grounded(ElseGoalInfo0, ProofVar,
			ElseGoalInfo2),
	ElseGoal2 = ElseGoalExpr2 - ElseGoalInfo2,

	transform_negated_context(EDTInfo, ProcInfo7, ProcInfo, ElseGoalExpr2,
			ElseGoalInfo2, MissTreeVar, ExtraElseGoal1),
	conjoin_goals(ElseGoal2, ExtraElseGoal1, ElseGoal3),

	proof_tree_ctor_else(ElseConsId),
	make_simple_construction(ProofVar, ElseConsId,
			[MissTreeVar, ElseProofVar], ExtraElseGoal2),
	conjoin_goals(ElseGoal3, ExtraElseGoal2, ElseGoal),

	GoalExpr = if_then_else(Locals, CondGoal, ThenGoal, ElseGoal,
			StoreMap).


:- pred transform_negated_context(edt_info, proc_info, proc_info,
		hlds_goal_expr, hlds_goal_info, var, hlds_goal).
:- mode transform_negated_context(in, in, out, in, in, out, out) is det.

transform_negated_context(EDTInfo, ProcInfo0, ProcInfo, _NegatedGoalExpr,
		NegatedGoalInfo, MissTreeVar, Goal) :-

	create_miss_tree_var(EDTInfo, ProcInfo0, ProcInfo, NegatedGoalInfo, _,
			MissTreeVar),
		%
		% XXX For the moment, miss_trees are always trivial.
		%
	miss_tree_ctor_trivial(TrivialConsId),
	make_simple_construction(MissTreeVar, TrivialConsId, [], Goal).


:- pred maybe_add_trivial_proof(edt_info, proc_info, proc_info, hlds_goal_expr,
		hlds_goal_info, hlds_goal_expr, hlds_goal_info, maybe(var),
		var).
:- mode maybe_add_trivial_proof(in, in, out, in, in, out, out, in, out) is det.

maybe_add_trivial_proof(EDTInfo, ProcInfo0, ProcInfo, GoalExpr0, GoalInfo0,
		GoalExpr, GoalInfo, MaybeProofVar, ProofVar) :-

	(
		MaybeProofVar = yes(ProofVar0)
	->
		ProcInfo = ProcInfo0,
		GoalExpr = GoalExpr0,
		GoalInfo = GoalInfo0,
		ProofVar = ProofVar0
	;
		create_proof_tree_var(EDTInfo, ProcInfo0, ProcInfo,
				GoalInfo0, _, ProofVar),

		proof_tree_ctor_trivial(TrivialConsId),
		make_simple_construction(ProofVar, TrivialConsId, [],
				ExtraGoal),
		conjoin_goals(GoalExpr0 - GoalInfo0, ExtraGoal,
				GoalExpr - GoalInfo)
	).


%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

make_wrong_answer_pred_stub(EDTInfo, Module, PredId, NewPredInfo) :-
	module_info_pred_info(Module, PredId, PredInfo),

        pred_info_arg_types(PredInfo, ArgTypeVarSet, ExistQTVars, ArgTypes0),
	pred_info_clauses_info(PredInfo, ClausesInfo),
	pred_info_context(PredInfo, Context),
	pred_info_module(PredInfo, ModuleName),
	pred_info_name(PredInfo, PredName0),
	pred_info_arity(PredInfo, Arity0),
	pred_info_import_status(PredInfo, ImportStatus),
	pred_info_get_goal_type(PredInfo, GoalType),
	pred_info_get_markers(PredInfo, Markers),
	pred_info_get_is_pred_or_func(PredInfo, PredOrFunc),
        pred_info_get_class_context(PredInfo, ClassContext),
        pred_info_get_constraint_proofs(PredInfo, ClassProofs),

		%
		% The new predicate has an extra argument.
		%
	Arity = Arity0 + 1,
	edt_info_evaluation_tree_type(EDTInfo, EDTType),
	list__append(ArgTypes0, [EDTType], ArgTypes),

	wrong_answer_name_mangle(PredName0, PredName),

		%
		% This creates a predicate with no procedures.  We will
		% add them later.
		%
	pred_info_init(ModuleName, unqualified(PredName), Arity, ArgTypeVarSet,
		ExistQTVars, ArgTypes, true, Context, ClausesInfo,
		ImportStatus, Markers, GoalType, PredOrFunc, ClassContext,
		ClassProofs, NewPredInfo).

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

proof_tree__make_wrong_analysis_pred(Module, EDTInfo, PredInfo) :-
	edt_info_get_module_name(EDTInfo, ModuleName),
	wrong_analysis_pred_sym_name(ModuleName, SymName),
	make_wrong_analysis_proc(EDTInfo, ProcInfo0, AtomType, AnalysisType),
	make_wrong_analysis_proc_body(Module, EDTInfo, ProcInfo0, ProcInfo),
	varset__init(TVarSet),
	generated_code_context(Context),
	init_markers(PredMarkers),
	ClassConstraints = constraints([], []),
	pred_info_create(ModuleName, SymName, TVarSet, [],
			[AtomType, AnalysisType], true, Context, exported,
			PredMarkers, predicate, ClassConstraints, ProcInfo, _,
			PredInfo).

:- pred make_wrong_analysis_proc(edt_info, proc_info, (type), (type)).
:- mode make_wrong_analysis_proc(in, out, out, out) is det.

make_wrong_analysis_proc(EDTInfo, ProcInfo, AtomType, AnalysisType) :-
	ground_inst(Ground),
	Arity = 2,
	edt_info_evaluation_atom_type(EDTInfo, AtomType),
	edt_info_analysis_type(EDTInfo, AnalysisType),
	generated_code_context(Context),
	local_analysis_inst(AnalysisInst),

	HeadModes = [(Ground -> Ground), (free -> AnalysisInst)],
	edt_info_get_globals(EDTInfo, Globals),
	globals__get_args_method(Globals, ArgsMethod),
	proc_info_init(Arity, HeadModes, no, no, no, Context, ArgsMethod,
			ProcInfo0),
	proc_info_set_inferred_determinism(ProcInfo0, semidet, ProcInfo1),
	proc_info_headvars(ProcInfo1, HeadVars),
	(
		HeadVars = [H1, H2]
	->
		map__from_assoc_list([H1 - AtomType, H2 - AnalysisType],
				VarTypes),
		proc_info_set_vartypes(ProcInfo1, VarTypes, ProcInfo)
	;
		error("make_wrong_analysis_proc: wrong arity")
	).


:- pred make_wrong_analysis_proc_body(module_info, edt_info, proc_info,
		proc_info).
:- mode make_wrong_analysis_proc_body(in, in, in, out) is det.

make_wrong_analysis_proc_body(Module, EDTInfo, ProcInfo0, ProcInfo) :-
	proc_info_headvars(ProcInfo0, HeadVars),
	(
		HeadVars = [H1, H2]
	->
		HeadVar1 = H1,
		HeadVar2 = H2
	;
		error("make_wrong_analysis_proc_body: wrong arity")
	),
	edt_info_get_proc_map(EDTInfo, ProcMap),
	map__values(ProcMap, EDTProcInfos),
	list__map_foldl(make_wrong_analysis_case(Module, EDTInfo, HeadVar1,
			HeadVar2), EDTProcInfos, AtomCases, ProcInfo0,
			ProcInfo1),
	map__init(StoreMap),
	GoalExpr = switch(HeadVar1, can_fail, AtomCases, StoreMap),

	set__list_to_set(HeadVars, NonLocals),
	ground_inst(Ground),
	instmap_delta_from_assoc_list([HeadVar2 - Ground], InstMapDelta),
	goal_info_init(NonLocals, InstMapDelta, semidet, GoalInfo),

	proc_info_set_goal(ProcInfo1, GoalExpr - GoalInfo, ProcInfo).


:- pred make_wrong_analysis_case(module_info, edt_info, var, var,
		edt_proc_info, case, proc_info, proc_info).
:- mode make_wrong_analysis_case(in, in, in, in, in, out, in, out) is det.

make_wrong_analysis_case(Module, EDTInfo, HeadVar1, HeadVar2, EDTProcInfo,
		Case, ProcInfo0, ProcInfo) :-
	(
		wrong_analysis_is_available(EDTProcInfo)
	->
		make_wrong_analysis_case_1(Module, EDTInfo, HeadVar1, HeadVar2,
				EDTProcInfo, Case, ProcInfo0, ProcInfo)
	;
		analysis_ctor_unavailable(AnalysisConsId),
		make_simple_construction(HeadVar2, AnalysisConsId, [], Goal),
		edt_proc_info_initial_cons_id(EDTProcInfo, AtomConsId),
		Case = case(AtomConsId, Goal),
		ProcInfo = ProcInfo0
	).

	%
	% This predicate temporarily exists to allow us to restrict
	% what can be attempted while functionality is still being
	% added.  This predicate will ultimately be of no purpose and
	% will be removed.
	%
:- pred wrong_analysis_is_available(edt_proc_info).
:- mode wrong_analysis_is_available(in) is semidet.

wrong_analysis_is_available(EDTProcInfo) :-
	edt_proc_info_get_atom_descriptor(EDTProcInfo, AtomDesc),
	not (some [Arg] (
		list__member(Arg, AtomDesc),
		Arg \= direct_var(_, _, _)
	)).

:- pred make_wrong_analysis_case_1(module_info, edt_info, var, var,
		edt_proc_info, case, proc_info, proc_info).
:- mode make_wrong_analysis_case_1(in, in, in, in, in, out, in, out) is det.

make_wrong_analysis_case_1(Module, EDTInfo, HeadVar1, HeadVar2, EDTProcInfo,
		Case, ProcInfo0, ProcInfo) :-

	set__list_to_set([HeadVar1, HeadVar2], NonLocals),
	ground_inst(Ground),
	instmap_delta_from_assoc_list([HeadVar2 - Ground], InstMapDelta),
	goal_info_init(NonLocals, InstMapDelta, semidet, GoalInfo),

	make_atom_deconstruction(EDTInfo, EDTProcInfo, HeadVar1, ArgVars,
			ProcInfo0, ProcInfo1, ArgGoals),
		
		%
		% XXX We should be more accurate with the determinism
		% here, rather than just treating everything as nondet.
		%
	make_wrong_closure_construction(Module, EDTInfo, EDTProcInfo, ArgVars,
			nondet, ProcInfo1, ProcInfo, ClosureVar, ClosureGoal),
	analysis_ctor_nondet_wrong(AnalysisConsId),
	make_simple_construction(HeadVar2, AnalysisConsId, [ClosureVar],
			AnalysisGoal),

	edt_proc_info_initial_cons_id(EDTProcInfo, InitialConsId),
	list__append(ArgGoals, [ClosureGoal, AnalysisGoal], GoalList),
	CaseGoal = conj(GoalList) - GoalInfo,
	Case = case(InitialConsId, CaseGoal).

:- pred make_wrong_closure_construction(module_info, edt_info, edt_proc_info, 
		list(var), determinism, proc_info, proc_info, var, hlds_goal).
:- mode make_wrong_closure_construction(in, in, in, in, in, in, out, out, out)
		is det.

make_wrong_closure_construction(Module, EDTInfo, EDTProcInfo, ArgVars, Detism,
		ProcInfo0, ProcInfo, ClosureVar, Goal) :-

	create_closure_var(EDTInfo, ProcInfo0, ProcInfo1, ClosureVar),
	set__list_to_set([ClosureVar | ArgVars], NonLocals),
	ground_inst(Ground),
	instmap_delta_from_assoc_list([ClosureVar - Ground], InstMapDelta),
	goal_info_init(NonLocals, InstMapDelta, det, GoalInfo),

		%
		% We can throw out the modified hlds_goal_info because this
		% proof_tree variable is lambda quantified, not nonlocal.
		%

	create_evaluation_tree_var(EDTInfo, ProcInfo1, ProcInfo, GoalInfo, _,
			LambdaVar),
	edt_proc_info_get_wrong_proc(EDTProcInfo, PredId, ProcId),
		
		%
		% SymName is only used for hlds dumps.
		%
	module_info_pred_info(Module, PredId, PredInfo),
	pred_info_name(PredInfo, PredName),
	SymName = unqualified(PredName),
	make_closure_construction(ClosureVar, SymName, PredId, ProcId,
			LambdaVar, ArgVars, Detism, GoalExpr),
	Goal = GoalExpr - GoalInfo.

:- pred make_atom_deconstruction(edt_info, edt_proc_info, var, list(var), 
		proc_info, proc_info, hlds_goals).
:- mode make_atom_deconstruction(in, in, in, out, in, out, out) is det.

make_atom_deconstruction(EDTInfo, EDTProcInfo, AtomVar, ArgVars, ProcInfo0,
		ProcInfo, Goals) :-

	edt_proc_info_get_atom_descriptor(EDTProcInfo, AtomDesc),
	make_call_arguments(EDTInfo, AtomDesc, ArgVars, ConsVars, ProcInfo0,
			ProcInfo, ArgGoals),
	edt_proc_info_initial_cons_id(EDTProcInfo, ConsId),
	make_simple_deconstruction(AtomVar, ConsId, ConsVars, Goal1),
	Goals = [Goal1 | ArgGoals].

:- pred make_call_arguments(edt_info, atom_descriptor, list(var), list(var),
		proc_info, proc_info, hlds_goals).
:- mode make_call_arguments(in, in, out, out, in, out, out) is det.

make_call_arguments(_, [], [], [], ProcInfo, ProcInfo, []).

make_call_arguments(EDTInfo, [AtomArg | AtomArgs], [ArgVar | ArgVars],
		[ConsVar | ConsVars], ProcInfo0, ProcInfo, Goals) :-

	AtomArg = direct_var(_, _, ArgType), 
	proc_info_create_var_from_type(ProcInfo0, ArgType, ArgVar, ProcInfo1),
	ConsVar = ArgVar,
	make_call_arguments(EDTInfo, AtomArgs, ArgVars, ConsVars, ProcInfo1,
			ProcInfo, Goals).

make_call_arguments(EDTInfo, [AtomArg | AtomArgs], [ArgVar | ArgVars],
		[ConsVar | ConsVars], ProcInfo0, ProcInfo, Goals) :-

	AtomArg = univ_var(_, _, ArgType),
	proc_info_create_var_from_type(ProcInfo0, ArgType, ArgVar, ProcInfo1),
	create_univ_var(ProcInfo1, ConsVar, ProcInfo2),
		%
		% XXX this actually needs to call univ_value
		%
	make_from_univ_call(EDTInfo, ArgVar, ConsVar, Goal0),
	make_call_arguments(EDTInfo, AtomArgs, ArgVars, ConsVars, ProcInfo2,
			ProcInfo, Goals0),
	Goals = [Goal0 | Goals0].


make_call_arguments(EDTInfo, [AtomArg | AtomArgs], ArgVars, ConsVars, 
		ProcInfo0, ProcInfo, Goals) :-

	AtomArg = io_state_di(_, _),
	make_call_arguments(EDTInfo, AtomArgs, ArgVars, ConsVars, ProcInfo0,
			ProcInfo, Goals).

make_call_arguments(EDTInfo, [AtomArg | AtomArgs], ArgVars, ConsVars,
		ProcInfo0, ProcInfo, Goals) :-
	
	AtomArg = io_state_uo(_, _),
	make_call_arguments(EDTInfo, AtomArgs, ArgVars, ConsVars, ProcInfo0,
			ProcInfo, Goals).