note
	description: "Translates Eiffel to IV AST nodes."
	date: "$Date$"
	revision: "$Revision$"

class
	E2B_TRANSLATOR

inherit

	SHARED_WORKBENCH

	E2B_SHARED_CONTEXT

create
	make

feature {NONE} -- Initialization

	make (a_boogie_universe: IV_UNIVERSE)
			-- Initialize translator.
		do
			translation_pool.reset
				-- Add types and features used by every system
			if attached helper.set_any_type as t then
				translation_pool.add_type (t)
			end
		end

feature -- Status report

	has_next_step: BOOLEAN
			-- Is there another step in the translation?
		do
			Result := translation_pool.has_untranslated_elements
		end

feature -- Element change

	add_input (a_input: E2B_TRANSLATOR_INPUT)
			-- Add all classes and featurse from `a_input' to be translated.
		do
			across a_input.class_list as i loop
				add_class (i.item)
			end
			across a_input.feature_list as i loop
				add_feature (i.item)
			end
			across a_input.feature_of_type_list as i loop
				add_feature_of_type (i.item.f, i.item.t)
			end
			across a_input.class_check_list as i loop
				translation_pool.add_class_check (i.item)
			end
		end

	add_class (a_class: CLASS_C)
			-- Add `a_class' to be translated.
		local
			l_feature: FEATURE_I
		do
			if not helper.is_class_logical (a_class) then
				translation_pool.add_class_check (helper.constraint_type (a_class))
			end
			if a_class.has_feature_table then
				from
					a_class.feature_table.start
				until
					a_class.feature_table.after
				loop
					l_feature := a_class.feature_table.item_for_iteration
					if helper.verify_feature_in_class (l_feature, a_class) then
						add_feature_of_type (l_feature, a_class.actual_type)
					end
					a_class.feature_table.forth
				end
			end
		end

	add_feature (a_feature: FEATURE_I)
			-- Add `a_feature' to be translated.
		require
			a_feature_attached: attached a_feature
		do
			add_feature_of_type (a_feature, system.class_of_id (a_feature.written_in).actual_type)
		end

	add_feature_of_type (a_feature: FEATURE_I; a_context_type: CL_TYPE_A)
			-- Add `a_feature' in context of type `a_context_type' to be translated.
		require
			a_feature_attached: attached a_feature
			a_context_type_attached: attached a_context_type
		do
			translation_pool.add_feature (a_feature, helper.constraint_type (a_context_type.base_class))
		end

feature -- Basic operations

	step
			-- Do one step of the translation.
		require
			has_next_step: has_next_step
		local
			l_unit: E2B_TRANSLATION_UNIT
			l_failed: BOOLEAN
			l_error: E2B_AUTOPROOF_ERROR
		do
			if l_failed then
				if l_unit /= Void then
					translation_pool.mark_translated (l_unit)
					create l_error
					l_error.set_type ("Internal Error")
					if attached {E2B_TU_CLASS} l_unit as x then
						l_error.set_class (x.class_type.base_class)
					elseif attached {E2B_TU_FEATURE} l_unit as x then
						l_error.set_class (x.type.base_class)
						l_error.set_feature (x.feat)
					end
					l_error.set_message (messages.internal_translation_error (l_unit.id))
					autoproof_errors.extend (l_error)
				end
			else
				check translation_pool.has_untranslated_elements end
				l_unit := translation_pool.next_untranslated_element
				l_unit.translate
				translation_pool.mark_translated (l_unit)
			end
		rescue
			l_failed := True
			retry
		end

end