indexing
	description: "Describes a type of objects in a running program"

class interface
	EIFFEL_TYPE

creation 
	make

feature -- basic description of the type

	attributes: ARRAY [EIFFEL_ATTRIBUTE]
			-- flat form or attributes

	direct_parents: ARRAY [EIFFEL_TYPE]
			-- direct parents of this class

	generics: ARRAY [EIFFEL_TYPE]
			-- Void if not generic

	name: STRING
			-- name of this class

	routines: ARRAY [EIFFEL_ROUTINE]
			-- flat form of routines
	
feature -- creation routines and invariants

	creation_procedures: ARRAY [EIFFEL_PROCEDURE]
			-- creation routines (could be Void)

	invariants: ARRAY [EIFFEL_ASSERTION]
			-- short for invariants
	
feature -- different views of routines

	functions: ARRAY [EIFFEL_FUNCTION]
			-- flat form of functions

	procedures: ARRAY [EIFFEL_PROCEDURE]
			-- flat form of procedures
	
feature -- instance creation

	create_instance (creation_routine_name: STRING; arguments: ARRAY [ANY]): ANY
		require
			type_not_deferred: not is_deferred;
			name_not_void: creation_routine_name /= void
		ensure
			result_exists: Result /= void;
			correct_type: has_instance (Result);
			valid_invariant: valid_invariant (Result)
	
feature -- queries about the kind of class this is

	is_deferred: BOOLEAN

	is_expanded: BOOLEAN

	is_generic: BOOLEAN
	
feature -- validity and conformance checks

	conforms_to_type (other: like Current): BOOLEAN
			-- does this "type" conform to "other"
		require
			other_not_void: other /= void

	has_instance (object: ANY): BOOLEAN
			-- is the "object" an instance of this type (descendant
			-- types count)
		require
			object_not_void: object /= void

	valid_invariant (object: ANY): BOOLEAN
			-- Return the result of testing the invariant on 'object'
		require
			object_not_void: object /= void
	
invariant

	name_not_void: name /= void;
	deferred_implies_no_creation_routines: is_deferred implies creation_procedures = void;
	consistent_generic: is_generic implies ((generics /= void) and then (generics.count >= 1));
	consistent_routines: (routines /= void) implies ((functions /= void) or (procedures /= void));
	creation_and_procedures: (creation_procedures /= void) implies (procedures /= void);
	consistent_deferred: is_expanded implies not is_deferred;

end -- class EIFFEL_TYPE