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

[Mark Anthony BROWN]

%-----------------------------------------------------------------------------%
% 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: evaluation_tree_util.m
% Author: dougl
% Purpose:
%	This module provides basic data structures and procedures to
%	support the generation of Evaluation Dependency Trees (EDTs) for
%	Mercury programs.  It is used by:
%
%		evaluation_tree_gen.m
%		proof_tree.m
%
%	This module contains:
%
%		- Data structures to support the compiler stage for EDT
%		  generation, and access procedures for these structures.
%		- Hard coded procedures that mimic the contents of
%		  evaluation_tree.m in the library directory.
%		- Data structures to record which variant of the
%		  transformations is to be used for each procedure.
%		- Support predicates that are common to all EDT
%		  transformations, but too specific to be put in
%		  goal_util.m

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

:- module evaluation_tree_util.
:- interface.

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

:- import_module std_util, list, term, bool, io, map, varset.

	%
	% Data structures for the compiler phase.
	%

	%
	% An edt_info contains all the information required by the
	% compiler to transform one module.  Each edt_info is built
	% in one pass of the module, and can then be used for
	% transformations to support wrong answer analysis or missing
	% answer analysis.
	%

:- type edt_info
	---> edt_info(
		module_name,
		globals,
		map(pred_proc_id, edt_proc_info),
				% Associates each procedure with details
				% of its alternative versions.
		list(constructor),
				% The constructors for evaluation_atoms
				% that can be created by this module.
		pred_id,	% type_to_univ/2.
		proc_id,	% forward mode of type_to_univ/2.
		maybe(pred_proc_id)
				% main/2 (if it exists in this module).
	).


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

:- pred edt_info_get_module_name(edt_info, module_name).
:- mode edt_info_get_module_name(in, out) is det.

:- pred edt_info_get_globals(edt_info, globals).
:- mode edt_info_get_globals(in, out) is det.

:- pred edt_info_get_atom_ctors(edt_info, list(constructor)).
:- mode edt_info_get_atom_ctors(in, out) is det.

:- pred edt_info_add_atom_ctor(edt_info, constructor, edt_info).
:- mode edt_info_add_atom_ctor(in, in, out) is det.

:- pred edt_info_get_proc_map(edt_info, map(pred_proc_id, edt_proc_info)).
:- mode edt_info_get_proc_map(in, out) is det.

:- pred edt_info_add_proc(edt_info, pred_proc_id, edt_proc_info, edt_info).
:- mode edt_info_add_proc(in, in, in, out) is det.

:- pred edt_info_univ_pred_proc_id(edt_info, pred_id, proc_id).
:- mode edt_info_univ_pred_proc_id(in, out, out) is det.

:- pred edt_info_set_main_pred_proc_id(edt_info, pred_id, proc_id, edt_info).
:- mode edt_info_set_main_pred_proc_id(in, in, in, out) is det.

:- pred maybe_write_edt_info(bool, module_info, edt_info, io__state,
		io__state).
:- mode maybe_write_edt_info(in, in, in, di, uo) is det.

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

	%
	% An edt_proc_info contains data that applies to just one
	% procedure.  This information is collected in the first pass
	% and is used by subsequent passes.
	%

:- type edt_proc_info
	---> edt_proc_info(
		pred_id,		% Id of the wrong answer version.
		proc_id,
		maybe(pred_proc_id),	% Id of the missing answer version,
					% if it exists.
		cons_id,		% The constructor for initial atoms
					% of this procedure.
		cons_id,		% The constructor for final atoms of
					% this procedure.
		atom_descriptor		% How the node arguments are built.
	).


:- pred edt_proc_info_init(pred_id, proc_id, cons_id, cons_id, atom_descriptor,
		edt_proc_info).
:- mode edt_proc_info_init(in, in, in, in, in, out) is det.

:- pred edt_proc_info_get_wrong_proc(edt_proc_info, pred_id, proc_id).
:- mode edt_proc_info_get_wrong_proc(in, out, out) is det.

:- pred edt_proc_info_get_miss_proc(edt_proc_info, pred_id, proc_id).
:- mode edt_proc_info_get_miss_proc(in, out, out) is semidet.

:- pred edt_proc_info_get_atom_descriptor(edt_proc_info, atom_descriptor).
:- mode edt_proc_info_get_atom_descriptor(in, out) is det.

:- pred edt_proc_info_initial_cons_id(edt_proc_info, cons_id).
:- mode edt_proc_info_initial_cons_id(in, out) is det.

:- pred edt_proc_info_final_cons_id(edt_proc_info, cons_id).
:- mode edt_proc_info_final_cons_id(in, out) is det.

:- pred write_edt_proc_info(module_info, pair(pred_proc_id, edt_proc_info),
		io__state, io__state).
:- mode write_edt_proc_info(in, in, di, uo) is det.


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

	%
	% Hard coded data.
	%
	% The evaluation tree transformation adds to the HLDS references to
	% fixed modules that are part of the library.  This section
	% hard codes the constants that are used.
	%
	% The information here corresponds to the contents of
	% library/evaluation_tree.  Any changes made to this section should
	% be reflected there, and vice versa.
	%


	%
	% Name of the module that defines the back end interface
	% (library/evaluation_tree.m).
	%

:- pred evaluation_tree_interface_module(module_specifier).
:- mode evaluation_tree_interface_module(out) is det.

	%
	% Types defined in the library module.
	%

:- pred evaluation_tree_type_id(type_id).
:- mode evaluation_tree_type_id(out) is det.

:- pred proof_tree_type_id(type_id).
:- mode proof_tree_type_id(out) is det.

:- pred miss_tree_type_id(type_id).
:- mode miss_tree_type_id(out) is det.

:- pred evaluation_atom_type(module_name, (type)).
:- mode evaluation_atom_type(in, out) is det.

:- pred evaluation_atom_type_name(module_name, sym_name).
:- mode evaluation_atom_type_name(in, out) is det.

	%
	% Constructors for evaluation_tree/1.
	%
	
:- pred evaluation_tree_ctor_analyse_wrong(cons_id).
:- mode evaluation_tree_ctor_analyse_wrong(out) is det.

:- pred evaluation_tree_ctor_analyse_miss(cons_id).
:- mode evaluation_tree_ctor_analyse_miss(out) is det.

:- pred evaluation_tree_ctor_implicit_wrong(cons_id).
:- mode evaluation_tree_ctor_implicit_wrong(out) is det.

:- pred evaluation_tree_ctor_implicit_miss(cons_id).
:- mode evaluation_tree_ctor_implicit_miss(out) is det.

:- pred evaluation_tree_ctor_interface_wrong(cons_id).
:- mode evaluation_tree_ctor_interface_wrong(out) is det.

:- pred evaluation_tree_ctor_interface_miss(cons_id).
:- mode evaluation_tree_ctor_interface_miss(out) is det.

:- pred evaluation_tree_ctor_assumed(cons_id).
:- mode evaluation_tree_ctor_assumed(out) is det.

	%
	% Constructors for proof_tree/1.
	%

:- pred proof_tree_ctor_local_call(cons_id).
:- mode proof_tree_ctor_local_call(out) is det.

:- pred proof_tree_ctor_conj(cons_id).
:- mode proof_tree_ctor_conj(out) is det.

:- pred proof_tree_ctor_disj(cons_id).
:- mode proof_tree_ctor_disj(out) is det.

:- pred proof_tree_ctor_switch(cons_id).
:- mode proof_tree_ctor_switch(out) is det.

:- pred proof_tree_ctor_if_then(cons_id).
:- mode proof_tree_ctor_if_then(out) is det.

:- pred proof_tree_ctor_else(cons_id).
:- mode proof_tree_ctor_else(out) is det.

:- pred proof_tree_ctor_not(cons_id).
:- mode proof_tree_ctor_not(out) is det.

:- pred proof_tree_ctor_trivial(cons_id).
:- mode proof_tree_ctor_trivial(out) is det.

	%
	% Constructors for miss_tree/1.
	%

:- pred miss_tree_ctor_local_call(cons_id).
:- mode miss_tree_ctor_local_call(out) is det.

:- pred miss_tree_ctor_conj(cons_id).
:- mode miss_tree_ctor_conj(out) is det.

:- pred miss_tree_ctor_disj(cons_id).
:- mode miss_tree_ctor_disj(out) is det.

:- pred miss_tree_ctor_switch(cons_id).
:- mode miss_tree_ctor_switch(out) is det.

:- pred miss_tree_ctor_if_then(cons_id).
:- mode miss_tree_ctor_if_then(out) is det.

:- pred miss_tree_ctor_else(cons_id).
:- mode miss_tree_ctor_else(out) is det.

:- pred miss_tree_ctor_not(cons_id).
:- mode miss_tree_ctor_not(out) is det.

:- pred miss_tree_ctor_trivial(cons_id).
:- mode miss_tree_ctor_trivial(out) is det.

	%
	% Constructors for analysis/1.
	%

:- pred analysis_ctor_nondet_wrong(cons_id).
:- mode analysis_ctor_nondet_wrong(out) is det.

:- pred analysis_ctor_unavailable(cons_id).
:- mode analysis_ctor_unavailable(out) is det.

	%
	% Some fixed types in the library.
	%

:- pred library_type_univ(type).
:- mode library_type_univ(out) is det.

	%
	% Constructors for list:list/1.
	%

:- pred library_ctor_list_cons(cons_id).
:- mode library_ctor_list_cons(out) is det.

:- pred library_ctor_list_nil(cons_id).
:- mode library_ctor_list_nil(out) is det.

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

	%
	% This is used to store how the module represents atoms.
	%

:- type atom_descriptor == list(atom_arg_descriptor).

:- type atom_arg_descriptor
	--->	direct_var(int, var, (type))
	;	univ_var(int, var, (type))
	;	io_state_di(int, var)
	;	io_state_uo(int, var).

:- pred write_atom_descriptor(varset, atom_descriptor, io__state, io__state).
:- mode write_atom_descriptor(in, in, di, uo) is det.

	%
	% This is used to specify the transformation that will be
	% performed on a call inside a goal.
	%
	
:- type analysis
	--->	no_analysis
	;	wrong_answer_analysis(pred_id, proc_id)
	;	full_analysis(pred_id, proc_id, pred_id, proc_id).

:- pred edt_info_proc_analysis(edt_info, pred_id, proc_id, analysis).
:- mode edt_info_proc_analysis(in, in, in, out) is det.

	%
	% Hard coded strategies of the transformations.
	%

:- pred wrong_answer_sym_name_mangle(sym_name, sym_name).
:- mode wrong_answer_sym_name_mangle(in, out) is det.

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

:- pred wrong_analysis_pred_sym_name(module_name, sym_name).
:- mode wrong_analysis_pred_sym_name(in, out) is det.

:- pred local_evaluation_tree_type(module_name, (type)).
:- mode local_evaluation_tree_type(in, out) is det.

:- pred local_evaluation_atom_type(module_name, (type)).
:- mode local_evaluation_atom_type(in, out) is det.

:- pred local_evaluation_atom_sym_name(module_name, sym_name).
:- mode local_evaluation_atom_sym_name(in, out) is det.

:- pred local_analysis_type(module_name, (type)).
:- mode local_analysis_type(in, out) is det.

:- pred local_analysis_inst((inst)).
:- mode local_analysis_inst(out) is det.

	%
	% This is the context we will use for any code added by the
	% transformations.
	%

:- pred generated_code_context(term__context).
:- mode generated_code_context(out) is det.

:- pred dummy_type_id(type_id).
:- mode dummy_type_id(out) is det.

:- pred ground_inst(inst).
:- mode ground_inst(out) is det.


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

	%
	% New types in the transformed program.  These types depend on
	% the module being debugged, hence they must be passed an
	% edt_info.
	%

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

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

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

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

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

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

	%
	% HLDS manipulation predicates.  These can be used to support
	% transformations for both wrong answer analysis and missing 
	% answer analysis.
	%

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

:- pred make_evaluation_atom_type_defn(edt_info, tvarset, type_defn).
:- mode make_evaluation_atom_type_defn(in, out, out) is det.

:- pred make_simple_construction(var, cons_id, list(var), hlds_goal).
:- mode make_simple_construction(in, in, in, out) is det.

:- pred make_simple_deconstruction(var, cons_id, list(var), hlds_goal).
:- mode make_simple_deconstruction(in, in, in, out) is det.

:- pred make_closure_construction(var, sym_name, pred_id, proc_id, var,
		list(var), determinism, hlds_goal_expr).
:- mode make_closure_construction(in, in, in, in, in, in, in, out) is det.

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

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

	%
	% Procedures to create new variables in the transformed part
	% of the HLDS.  Those procedures which take an hlds_goal_info
	% as an input argument add the new variable (say V) to the
	% set of nonlocals, and add {V -> ground} to the instmap_delta.
	%

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

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

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

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

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

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

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

:- pred create_int_var(proc_info, var, proc_info).
:- mode create_int_var(in, out, out) is det.

:- pred create_univ_var(proc_info, var, proc_info).
:- mode create_univ_var(in, out, out) is det.

	%
	% Some basic manipulation routines for the HLDS.
	%

:- pred prepend_goal_to_rev_goal_list(hlds_goal, hlds_goals, hlds_goals).
:- mode prepend_goal_to_rev_goal_list(in, in, out) is det.

:- pred goal_info_add_nonlocal(hlds_goal_info, var, hlds_goal_info).
:- mode goal_info_add_nonlocal(in, in, out) is det.

:- pred goal_info_set_nonlocal_grounded(hlds_goal_info, var, hlds_goal_info).
:- mode goal_info_set_nonlocal_grounded(in, in, out) is det.

:- pred goal_info_set_var_new_inst(hlds_goal_info, var, (inst),
		hlds_goal_info).
:- mode goal_info_set_var_new_inst(in, in, in, out) is det.


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

:- implementation.

:- import_module type_util, prog_out, mercury_to_mercury, hlds_out, instmap.

:- import_module string, require, set.

edt_info_init(Module, EDTInfo) :-
	module_info_name(Module, ModuleName),
	module_info_globals(Module, Globals),
	map__init(Map),

	module_info_get_predicate_table(Module, PredTable),
	StdUtil = unqualified("std_util"),
	(
		predicate_table_search_pred_m_n_a(PredTable, StdUtil,
				"type_to_univ", 2, TypeToUnivPredIds),
		TypeToUnivPredIds = [TypeToUnivPredId0 | _]
	->
		TypeToUnivPredId = TypeToUnivPredId0,
		proc_id_to_int(TypeToUnivProcId, 0)
			% XXX That should not be hard coded
	;
		error("edt_info_init: std_util:type_to_univ/2 not found")
	),
	EDTInfo = edt_info(ModuleName, Globals, Map, [], TypeToUnivPredId,
			TypeToUnivProcId, no).

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

% :- type edt_info
%	---> edt_info(
% A		module_name,	% module name
% B		globals,	% global compiler options
% C		map(pred_proc_id, proc_proof_info),
%				% Associates each procedure with details
%				% of its alternative versions.
% D		list(constructor),
%				% The constructors for evaluation_atoms
%				% that can be created by this module.
% E		pred_id,	% type_to_univ/2
% F		proc_id,	% forward mode of type_to_univ/2.
% G		maybe(pred_proc_id)
%				% main/2 (if it exists in this module).
%	).

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

	%
	% Predicates which access the edt_info data structure.
	%

edt_info_get_module_name(EDTInfo, A) :-
	EDTInfo = edt_info(A, _, _, _, _, _, _).

edt_info_get_globals(EDTInfo, B) :-
	EDTInfo = edt_info(_, B, _, _, _, _, _).

edt_info_get_proc_map(EDTInfo, C) :-
	EDTInfo = edt_info(_, _, C, _, _, _, _).

edt_info_get_atom_ctors(EDTInfo, D) :-
	EDTInfo = edt_info(_, _, _, D, _, _, _).

edt_info_univ_pred_proc_id(EDTInfo, E, F) :-
	EDTInfo = edt_info(_, _, _, _, E, F, _).

	%
	% Predicates which modify the edt_info structure.
	%

edt_info_add_atom_ctor(EDTInfo0, AtomCtor, EDTInfo) :-
	EDTInfo0 = edt_info(A, B, C, D0, E, F, G),
	D = [AtomCtor | D0],
	EDTInfo  = edt_info(A, B, C, D, E, F, G).

edt_info_add_proc(EDTInfo0, PredProcId, EDTProcInfo, EDTInfo) :-
	EDTInfo0 = edt_info(A, B, Map0, D, E, F, G),
	map__det_insert(Map0, PredProcId, EDTProcInfo, Map),
	EDTInfo  = edt_info(A, B, Map, D, E, F, G).

edt_info_set_main_pred_proc_id(EDTInfo0, PredId, ProcId, EDTInfo) :-
	EDTInfo0 = edt_info(A, B, C, D, E, F, _),
	EDTInfo  = edt_info(A, B, C, D, E, F, yes(proc(PredId, ProcId))).

maybe_write_edt_info(no, _, _) -->
	[].
maybe_write_edt_info(yes, Module, EDTInfo) -->
	{ EDTInfo = edt_info(Name, _Globals, Map, Ctors, _UnivPred,
			_UnivProc, _MaybeMain) },
	io__write_string("% EDT Info for module "),
	prog_out__write_sym_name(Name),
	io__write_string(":\n"),
	io__write_string("%   edt_proc_infos:\n"),
	{ map__to_assoc_list(Map, EDTProcInfos) },
	list__foldl(write_edt_proc_info(Module), EDTProcInfos),
	io__write_string("%   Constructors:\n"),
	{ varset__init(TypeVars) },
	list__foldl(write_atom_constructor(TypeVars), Ctors).

:- pred write_atom_constructor(varset, constructor, io__state, io__state).
:- mode write_atom_constructor(in, in, di, uo) is det.

write_atom_constructor(TypeVars, Ctor) -->
	io__write_string("%       "),
	mercury_output_ctor(Ctor, TypeVars),
	io__nl.

edt_proc_info_init(PredId, ProcId, InitialConsId, FinalConsId, AtomDesc,
		EDTProcInfo) :-
	
	EDTProcInfo = edt_proc_info(PredId, ProcId, no, InitialConsId,
			FinalConsId, AtomDesc).

edt_proc_info_get_wrong_proc(EDTProcInfo, PredId, ProcId) :-
	EDTProcInfo = edt_proc_info(PredId, ProcId, _, _, _, _).

edt_proc_info_get_miss_proc(EDTProcInfo, PredId, ProcId) :-
	EDTProcInfo = edt_proc_info(_, _, yes(proc(PredId, ProcId)), _, _, _).

edt_proc_info_get_atom_descriptor(EDTProcInfo, AtomDesc) :-
	EDTProcInfo = edt_proc_info(_, _, _, _, _, AtomDesc).

edt_proc_info_initial_cons_id(EDTProcInfo, ConsId) :-
	EDTProcInfo = edt_proc_info(_, _, _, ConsId, _, _).

edt_proc_info_final_cons_id(EDTProcInfo, ConsId) :-
	EDTProcInfo = edt_proc_info(_, _, _, _, ConsId, _).

write_edt_proc_info(Module, PredProcId - EDTProcInfo) -->
	{ PredProcId = proc(PredId, ProcId) },
	{ EDTProcInfo = edt_proc_info(_, _, _, _, _, AtomDesc) },
	{ module_info_pred_info(Module, PredId, PredInfo) },
	{ pred_info_arg_types(PredInfo, VarSet, _, _) },
	io__write_string("%   "),
	hlds_out__write_pred_proc_id(Module, PredId, ProcId),
	io__write_string(":\n"),
	write_atom_descriptor(VarSet, AtomDesc).


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

evaluation_tree_interface_module(unqualified("evaluation_tree")).


evaluation_tree_type_id(SymName - Arity) :-
	evaluation_tree_interface_module(Module),
	SymName = qualified(Module, "evaluation_tree"),
	Arity = 1.


proof_tree_type_id(SymName - Arity) :-
	evaluation_tree_interface_module(Module),
	SymName = qualified(Module, "proof_tree"),
	Arity = 1.

evaluation_atom_type(Module, AtomType) :-
	evaluation_atom_type_name(Module, SymName),
	construct_type(SymName - 0, [], AtomType).


evaluation_atom_type_name(Module, SymName) :-
	SymName = qualified(Module, "atom").


miss_tree_type_id(SymName - Arity) :-
	evaluation_tree_interface_module(Module),
	SymName = qualified(Module, "miss_tree"),
	Arity = 1.


evaluation_tree_ctor_analyse_wrong(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "analyse_wrong").

evaluation_tree_ctor_analyse_miss(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "analyse_miss").


evaluation_tree_ctor_implicit_wrong(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "implicit_wrong").

evaluation_tree_ctor_implicit_miss(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "implicit_miss").


evaluation_tree_ctor_interface_wrong(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "interface_wrong").

evaluation_tree_ctor_interface_miss(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "interface_miss").


evaluation_tree_ctor_assumed(cons(SymName, Arity)) :-
	Arity = 0,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "assumed").


proof_tree_ctor_local_call(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "local_call").

proof_tree_ctor_conj(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "conj").

proof_tree_ctor_switch(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "switch").


proof_tree_ctor_disj(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "disj").


proof_tree_ctor_not(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "not").


proof_tree_ctor_if_then(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "if_then").


proof_tree_ctor_else(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "else").


proof_tree_ctor_trivial(cons(SymName, Arity)) :-
	Arity = 0,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "trivial").


miss_tree_ctor_local_call(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "local_call").

miss_tree_ctor_conj(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "conj").

miss_tree_ctor_switch(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "switch").

miss_tree_ctor_disj(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "disj").

miss_tree_ctor_not(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "not").

miss_tree_ctor_if_then(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "if_then").

miss_tree_ctor_else(cons(SymName, Arity)) :-
	Arity = 2,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "else").

miss_tree_ctor_trivial(cons(SymName, Arity)) :-
	Arity = 0,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "trivial").

analysis_ctor_nondet_wrong(cons(SymName, Arity)) :-
	Arity = 1,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "nondet_wrong").

analysis_ctor_unavailable(cons(SymName, Arity)) :-
	Arity = 0,
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "unavailable").

library_type_univ(UnivType) :-
	StdUtil = unqualified("std_util"),
	UnivTypeId = qualified(StdUtil, "univ") - 0,
	construct_type(UnivTypeId, [], UnivType).

library_ctor_list_cons(cons(SymName, Arity)) :-
	Arity = 2,
	Module = unqualified("list"),
	SymName = qualified(Module, ".").


library_ctor_list_nil(cons(SymName, Arity)) :-
	Arity = 0,
	Module = unqualified("list"),
	SymName = qualified(Module, "[]").

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

write_atom_descriptor(VarSet, AtomDesc) -->
	io__write_string("%       "),
	(
		{ AtomDesc = [Arg | Args] }
	->
		io__write_char('['),
		write_atom_argument(VarSet, Arg),
		write_atom_arguments(VarSet, Args),
		io__write_string("]\n")
	;
		io__write_string("[]\n")
	).

:- pred write_atom_arguments(varset, list(atom_arg_descriptor), io__state,
		io__state).
:- mode write_atom_arguments(in, in, di, uo) is det.

write_atom_arguments(_, []) -->
	[].
write_atom_arguments(VarSet, [Arg | Args]) -->
	io__write_string(", "),
	write_atom_argument(VarSet, Arg),
	write_atom_arguments(VarSet, Args).

:- pred write_atom_argument(varset, atom_arg_descriptor, io__state, io__state).
:- mode write_atom_argument(in, in, di, uo) is det.

write_atom_argument(VarSet, direct_var(_Pos, _Var, Type)) -->
	io__write_string("direct("),
	mercury_output_term(Type, VarSet, no),
	io__write_char(')').
write_atom_argument(VarSet, univ_var(_Pos, _Var, Type)) -->
	io__write_string("univ("),
	mercury_output_term(Type, VarSet, no),
	io__write_char(')').
write_atom_argument(_VarSet, io_state_di(_, _)) -->
	io__write_string("io_di").
write_atom_argument(_VarSet, io_state_uo(_, _)) -->
	io__write_string("io_uo").

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

edt_info_proc_analysis(EDTInfo, PredId, ProcId, Analysis) :-
	edt_info_get_proc_map(EDTInfo, ProcMap),
	(
		map__search(ProcMap, proc(PredId, ProcId), EDTProcInfo)
	->
		edt_proc_info_get_wrong_proc(EDTProcInfo, WrongPredId,
				WrongProcId),
		(
			edt_proc_info_get_miss_proc(EDTProcInfo, MissPredId,
					MissProcId)
		->
			Analysis = full_analysis(WrongPredId, WrongProcId,
					MissPredId, MissProcId)
		;
			Analysis = wrong_answer_analysis(WrongPredId,
					WrongProcId)
		)
	;
		Analysis = no_analysis
	).


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

	%
	% For the moment, this will be a very simple transformation.
	%
wrong_answer_name_mangle(Name0, Name) :-
	string__append(Name0, "_wrong", Name).
	
wrong_answer_sym_name_mangle(SymName0, SymName) :-
	(
		SymName0 = unqualified(Name0),
		wrong_answer_name_mangle(Name0, Name),
		SymName = unqualified(Name)
	;
		SymName0 = qualified(Module, Name0),
		wrong_answer_name_mangle(Name0, Name),
		SymName = qualified(Module, Name)
	).

wrong_analysis_pred_sym_name(ModuleName, SymName) :-
	SymName = qualified(ModuleName, "atom_to_wrong_analysis").

local_evaluation_tree_type(Module, TreeType) :-
	local_evaluation_atom_type(Module, AtomType),
	evaluation_tree_type_id(TypeId),
	construct_type(TypeId, [AtomType], TreeType).

local_evaluation_atom_type(Module, AtomType) :-
	local_evaluation_atom_sym_name(Module, SymName),
	construct_type(SymName - 0, [], AtomType).

local_evaluation_atom_sym_name(ModuleName, SymName) :-
	SymName = qualified(ModuleName, "evaluation_atom").

local_analysis_type(Module, AnalysisType) :-
	local_evaluation_atom_type(Module, AtomType),
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "analysis"),
	construct_type(SymName - 1, [AtomType], AnalysisType).

local_analysis_inst(AnalysisInst) :-
	evaluation_tree_interface_module(LibModule),
	SymName = qualified(LibModule, "analysis"),
	InstName = user_inst(SymName, []),
	AnalysisInst = defined_inst(InstName).

generated_code_context(Context) :-
	term__context_init(Context).

dummy_type_id(unqualified("") - 0).

ground_inst(ground(shared, no)).

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

edt_info_evaluation_tree_type(EDTInfo, Type) :-
	evaluation_tree_type_id(EDTTypeId),
	edt_info_evaluation_atom_type(EDTInfo, AtomType),
	construct_type(EDTTypeId, [AtomType], Type).

edt_info_proof_tree_type(EDTInfo, Type) :-
	proof_tree_type_id(ProofTreeTypeId),
	edt_info_evaluation_atom_type(EDTInfo, AtomType),
	construct_type(ProofTreeTypeId, [AtomType], Type).

edt_info_miss_tree_type(EDTInfo, Type) :-
	miss_tree_type_id(MissTreeTypeId),
	edt_info_evaluation_atom_type(EDTInfo, AtomType),
	construct_type(MissTreeTypeId, [AtomType], Type).

edt_info_evaluation_atom_type(EDTInfo, Type) :-
	edt_info_get_module_name(EDTInfo, Module),
	local_evaluation_atom_type(Module, Type).

edt_info_analysis_type(EDTInfo, Type) :-
	edt_info_get_module_name(EDTInfo, Module),
	local_analysis_type(Module, Type).

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

make_final_atom_construction(EDTInfo, EDTProcInfo, ProcInfo0, ProcInfo, 
		AtomVar, Goals) :-

	edt_proc_info_get_atom_descriptor(EDTProcInfo, AtomDesc),
	make_atom_cons_args(EDTInfo, AtomDesc, ArgVars, ProcInfo0, ProcInfo1,
			[], Goals0),
	create_evaluation_atom_var(EDTInfo, ProcInfo1, ProcInfo, AtomVar),
	edt_proc_info_final_cons_id(EDTProcInfo, ConsId),
	make_simple_construction(AtomVar, ConsId, ArgVars, ExtraGoal),
	list__append(Goals0, [ExtraGoal], Goals).

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

make_atom_cons_args(_EDTInfo, [], [], ProcInfo, ProcInfo, Goals, Goals).
make_atom_cons_args(EDTInfo, [AtomArg | AtomArgs], ArgVars, ProcInfo0,
		ProcInfo, Goals0, Goals) :-

	make_atom_cons_arg(EDTInfo, AtomArg, MaybeArgVar, ProcInfo0, ProcInfo1,
			Goals0, Goals1),
	make_atom_cons_args(EDTInfo, AtomArgs, ArgVars0, ProcInfo1, ProcInfo,
			Goals1, Goals),
	(
		MaybeArgVar = yes(ArgVar)
	->
		ArgVars = [ArgVar | ArgVars0]
	;
		ArgVars = ArgVars0
	).

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

make_atom_cons_arg(_EDTInfo, direct_var(_, Var, _), yes(Var), Proc, Proc,
		Goals, Goals).
make_atom_cons_arg(EDTInfo, univ_var(_, Var, _), yes(UnivVar), Proc0, Proc,
		Goals0, Goals) :-

	create_univ_var(Proc0, UnivVar, Proc),
	make_to_univ_call(EDTInfo, Var, UnivVar, Goal),
	Goals = [Goal | Goals0].

make_atom_cons_arg(_EDTInfo, io_state_di(_, _), no, Proc, Proc, Goals, Goals).
make_atom_cons_arg(_EDTInfo, io_state_uo(_, _), no, Proc, Proc, Goals, Goals).


make_evaluation_atom_type_defn(EDTInfo, TVarSet, TypeDefn) :-
	edt_info_get_atom_ctors(EDTInfo, Ctors),
	edt_info_get_module_name(EDTInfo, Module),
	local_evaluation_atom_sym_name(Module, SymName),
	TypeDefn = du_type(SymName, [], Ctors, no),
	varset__init(TVarSet).

make_simple_construction(LVar, ConsId, Args, Goal) :-
	Ground = ground(shared, no),

	UnifyRHS = functor(ConsId, Args),
	UnifyMode = ((free -> Ground) - (Ground -> Ground)),

	UniMode = ((free - Ground) -> (Ground - Ground)),
	list__length(Args, Arity),
	list__duplicate(Arity, UniMode, UniModes),
	Unification = construct(LVar, ConsId, Args, UniModes),

	Context = unify_context(explicit, []),
	GoalExpr = unify(LVar, UnifyRHS, UnifyMode, Unification, Context),

	set__list_to_set([LVar | Args], NonLocals),
	instmap_delta_from_assoc_list([LVar - Ground], InstMapDelta),
	Detism = det,
	goal_info_init(NonLocals, InstMapDelta, Detism, GoalInfo),

	Goal = GoalExpr - GoalInfo.

make_simple_deconstruction(LVar, ConsId, Args, Goal) :-
	Ground = ground(shared, no),

	UnifyRHS = functor(ConsId, Args),
	UnifyMode = ((Ground -> Ground) - (free -> Ground)),
	UniMode = ((Ground - free) -> (Ground - Ground)),
	list__length(Args, Arity),
	list__duplicate(Arity, UniMode, UniModes),
	Unification = deconstruct(LVar, ConsId, Args, UniModes, cannot_fail),
	Context = unify_context(explicit, []),
	GoalExpr = unify(LVar, UnifyRHS, UnifyMode, Unification, Context),

	set__list_to_set([LVar | Args], NonLocals),
	Map = lambda([Var::in, VarInst::out] is det,
			(VarInst = Var - Ground)
	),
	list__map(Map, Args, InstMapAssocList),
	instmap_delta_from_assoc_list(InstMapAssocList, InstMapDelta),
	Detism = det,
	goal_info_init(NonLocals, InstMapDelta, Detism, GoalInfo),

	Goal = GoalExpr - GoalInfo.

make_closure_construction(LVar, SymName, PredId, ProcId, LambdaVar, ArgVars,
		Detism, GoalExpr) :-

	ground_inst(Ground),
	list__append(ArgVars, [LambdaVar], CallArgs),
	LambdaGoalExpr = call(PredId, ProcId, CallArgs, not_builtin, no,
			SymName),
	set__list_to_set(CallArgs, NonLocals),
	instmap_delta_from_assoc_list([LambdaVar - Ground], InstMapDelta),
	goal_info_init(NonLocals, InstMapDelta, Detism, LambdaGoalInfo),
	LambdaGoal = LambdaGoalExpr - LambdaGoalInfo,

	UnifyRHS = lambda_goal(predicate, ArgVars, [LambdaVar],
			[(free -> Ground)], nondet, LambdaGoal),
	UnifyMode = ((free -> Ground) - (Ground -> Ground)),
	UniMode = ((Ground - Ground) -> (Ground - Ground)),
	list__length(ArgVars, Arity),
	list__duplicate(Arity, UniMode, UniModes),
	ConsId = pred_const(PredId, ProcId),
	Unification = construct(LVar, ConsId, ArgVars, UniModes),
	Context = unify_context(explicit, []),
	GoalExpr = unify(LVar, UnifyRHS, UnifyMode, Unification, Context).


make_to_univ_call(EDTInfo, LVar, RVar, Goal) :-
	proc_id_to_int(ProcId, 1),
	make_univ_call(EDTInfo, ProcId, LVar, RVar, RVar, Goal).

make_from_univ_call(EDTInfo, LVar, RVar, Goal) :-
	proc_id_to_int(ProcId, 2),
	make_univ_call(EDTInfo, ProcId, LVar, RVar, LVar, Goal).

:- pred make_univ_call(edt_info, proc_id, var, var, var, hlds_goal).
:- mode make_univ_call(in, in, in, in, in, out) is det.

make_univ_call(EDTInfo, ProcId, Var, UnivVar, BoundVar, GoalExpr - GoalInfo) :-

	edt_info_univ_pred_proc_id(EDTInfo, PredId, _),
	Args = [Var, UnivVar],
	BuiltinState = not_builtin,
	SymName = unqualified("type_to_univ"),
	GoalExpr = call(PredId, ProcId, Args, BuiltinState, no, SymName),
	set__list_to_set(Args, NonLocals),
	Ground = ground(shared, no),
	instmap_delta_from_assoc_list([BoundVar - Ground], InstMapDelta),
	Detism = det,
	goal_info_init(NonLocals, InstMapDelta, Detism, GoalInfo).


create_evaluation_tree_head_var(EDTInfo, ProcInfo0, ProcInfo, GoalInfo0,
		GoalInfo, EDTVar) :-

	create_evaluation_tree_var(EDTInfo, ProcInfo0, ProcInfo1, GoalInfo0,
			GoalInfo1, EDTVar),
	goal_info_add_nonlocal(GoalInfo1, EDTVar, GoalInfo),

	proc_info_headvars(ProcInfo1, HeadVars0),
	proc_info_argmodes(ProcInfo1, ArgModes0),
	proc_info_varset(ProcInfo1, VarSet0),
	list__append(HeadVars0, [EDTVar], HeadVars),
	ground_inst(Ground),
	EDTMode = (free -> Ground),
	list__append(ArgModes0, [EDTMode], ArgModes),
	varset__name_var(VarSet0, EDTVar, "HeadEDT", VarSet),
	proc_info_set_headvars(ProcInfo1, HeadVars, ProcInfo2),
	proc_info_set_argmodes(ProcInfo2, ArgModes, ProcInfo3),
	proc_info_set_varset(ProcInfo3, VarSet, ProcInfo).

create_evaluation_tree_var(EDTInfo, ProcInfo0, ProcInfo, GoalInfo0, GoalInfo,
		EDTVar) :-

	edt_info_evaluation_tree_type(EDTInfo, EDTType),
	create_new_variable(EDTType, "EDT", ProcInfo0, ProcInfo, GoalInfo0,
			GoalInfo, EDTVar).

create_evaluation_atom_var(EDTInfo, ProcInfo0, ProcInfo, AtomVar) :-
	edt_info_evaluation_atom_type(EDTInfo, AtomType),
	proc_info_create_var_from_type(ProcInfo0, AtomType, AtomVar,
			ProcInfo1),
	proc_info_varset(ProcInfo1, VarSet0),
	varset__name_var(VarSet0, AtomVar, "Atom", VarSet),
	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo).

create_proof_tree_var(EDTInfo, ProcInfo0, ProcInfo, GoalInfo0, GoalInfo,
		ProofVar) :-

	edt_info_proof_tree_type(EDTInfo, ProofType),
	create_new_variable(ProofType, "Proof", ProcInfo0, ProcInfo,
			GoalInfo0, GoalInfo, ProofVar).

create_miss_tree_var(EDTInfo, ProcInfo0, ProcInfo, GoalInfo0, GoalInfo,
		MissTreeVar) :-

	edt_info_miss_tree_type(EDTInfo, MissTreeType),
	create_new_variable(MissTreeType, "MissTree", ProcInfo0, ProcInfo,
			GoalInfo0, GoalInfo, MissTreeVar).

create_proof_tree_list_var(EDTInfo, ProcInfo0, ProcInfo, ProofListVar) :-
	edt_info_proof_tree_type(EDTInfo, ProofType),
	ListSymName = qualified(unqualified("list"), "list"),
	ListArity = 1,
	ListTypeId = ListSymName - ListArity,
	construct_type(ListTypeId, [ProofType], ProofListType),
	proc_info_create_var_from_type(ProcInfo0, ProofListType, ProofListVar,
			ProcInfo1),
	proc_info_varset(ProcInfo1, VarSet0),
	varset__name_var(VarSet0, ProofListVar, "Proofs", VarSet),
	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo).

create_closure_var(EDTInfo, ProcInfo0, ProcInfo, ClosureVar) :-
	edt_info_evaluation_tree_type(EDTInfo, EDTType),
	generated_code_context(Context),
	ClosureType = term__functor(term__atom("pred"), [EDTType], Context),
	proc_info_create_var_from_type(ProcInfo0, ClosureType, ClosureVar, 
			ProcInfo).

:- pred create_new_variable((type), string, proc_info, proc_info,
		hlds_goal_info, hlds_goal_info, var).
:- mode create_new_variable(in, in, in, out, in, out, out) is det.

create_new_variable(VarType, VarName, ProcInfo0, ProcInfo, GoalInfo0, GoalInfo,
		NewVar) :-

	proc_info_create_var_from_type(ProcInfo0, VarType, NewVar, ProcInfo1),
	proc_info_varset(ProcInfo1, VarSet0),
	varset__name_var(VarSet0, NewVar, VarName, VarSet),
	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo),
	goal_info_set_nonlocal_grounded(GoalInfo0, NewVar, GoalInfo).


create_int_var(ProcInfo0, IntVar, ProcInfo) :-
	IntTypeId = qualified(unqualified("mercury_builtin"), "int") - 0,
	construct_type(IntTypeId, [], IntType),
	proc_info_create_var_from_type(ProcInfo0, IntType, IntVar, ProcInfo1),
	proc_info_varset(ProcInfo1, VarSet0),
	varset__name_var(VarSet0, IntVar, "ArmId", VarSet),
	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo).


create_univ_var(ProcInfo0, UnivVar, ProcInfo) :-
	UnivTypeId = qualified(unqualified("std_util"), "univ") - 0,
	construct_type(UnivTypeId, [], UnivType),
	proc_info_create_var_from_type(ProcInfo0, UnivType, UnivVar,
			ProcInfo1),
	proc_info_varset(ProcInfo1, VarSet0),
	varset__name_var(VarSet0, UnivVar, "Univ", VarSet),
	proc_info_set_varset(ProcInfo1, VarSet, ProcInfo).


prepend_goal_to_rev_goal_list(Goal0, Goals0, Goals) :-
	(
		Goal0 = conj(SubGoals) - _
	->
		list__reverse(SubGoals, RevSubGoals),
		list__append(RevSubGoals, Goals0, Goals)
	;
		Goals = [Goal0 | Goals0]
	).

goal_info_add_nonlocal(GoalInfo0, NewVar, GoalInfo) :-
	goal_info_get_nonlocals(GoalInfo0, NonLocals0),
	set__insert(NonLocals0, NewVar, NonLocals),
	goal_info_set_nonlocals(GoalInfo0, NonLocals, GoalInfo).

goal_info_set_nonlocal_grounded(GoalInfo0, NewVar, GoalInfo) :-
	goal_info_add_nonlocal(GoalInfo0, NewVar, GoalInfo1),
	ground_inst(NewInst),
	goal_info_set_var_new_inst(GoalInfo1, NewVar, NewInst, GoalInfo).

goal_info_set_var_new_inst(GoalInfo0, Var, NewInst, GoalInfo) :-
	goal_info_get_instmap_delta(GoalInfo0, InstMapDelta0),
	instmap_delta_insert(InstMapDelta0, Var, NewInst, InstMapDelta),
	goal_info_set_instmap_delta(GoalInfo0, InstMapDelta, GoalInfo).

:- end_module evaluation_tree_util.