# A global static type
#
# MType are global to the model; it means that a `MType` is not bound to a
# specific `MModule`.
# This characteristic helps the reasoning about static types in a program
# since a single `MType` object always denote the same type.
#
# However, because a `MType` is global, it does not really have properties
# nor have subtypes to a hierarchy since the property and the class hierarchy
# depends of a module.
# Moreover, virtual types an formal generic parameter types also depends on
# a receiver to have sense.
#
# Therefore, most method of the types require a module and an anchor.
# The module is used to know what are the classes and the specialization
# links.
# The anchor is used to know what is the bound of the virtual types and formal
# generic parameter types.
#
# MType are not directly usable to get properties. See the `anchor_to` method
# and the `MClassType` class.
#
# FIXME: the order of the parameters is not the best. We mus pick on from:
#  * foo(mmodule, anchor, othertype)
#  * foo(othertype, anchor, mmodule)
#  * foo(anchor, mmodule, othertype)
#  * foo(othertype, mmodule, anchor)
abstract class MType
	super MEntity

	redef fun name do return to_s

	# Return true if `self` is an subtype of `sup`.
	# The typing is done using the standard typing policy of Nit.
	#
	# REQUIRE: `anchor == null implies not self.need_anchor and not sup.need_anchor`
	# REQUIRE: `anchor != null implies self.can_resolve_for(anchor, null, mmodule) and sup.can_resolve_for(anchor, null, mmodule)`
	fun is_subtype(mmodule: MModule, anchor: nullable MClassType, sup: MType): Bool
	do
		var sub = self
		if sub == sup then return true

		#print "1.is {sub} a {sup}? ===="

		if anchor == null then
			assert not sub.need_anchor
			assert not sup.need_anchor
		else
			# First, resolve the formal types to the simplest equivalent forms in the receiver
			assert sub.can_resolve_for(anchor, null, mmodule)
			sub = sub.lookup_fixed(mmodule, anchor)
			assert sup.can_resolve_for(anchor, null, mmodule)
			sup = sup.lookup_fixed(mmodule, anchor)
		end

		# Does `sup` accept null or not?
		# Discard the nullable marker if it exists
		var sup_accept_null = false
		if sup isa MNullableType then
			sup_accept_null = true
			sup = sup.mtype
		else if sup isa MNotNullType then
			sup = sup.mtype
		else if sup isa MNullType then
			sup_accept_null = true
		end

		# Can `sub` provide null or not?
		# Thus we can match with `sup_accept_null`
		# Also discard the nullable marker if it exists
		var sub_reject_null = false
		if sub isa MNullableType then
			if not sup_accept_null then return false
			sub = sub.mtype
		else if sub isa MNotNullType then
			sub_reject_null = true
			sub = sub.mtype
		else if sub isa MNullType then
			return sup_accept_null
		end
		# Now the case of direct null and nullable is over.

		# If `sub` is a formal type, then it is accepted if its bound is accepted
		while sub isa MFormalType do
			#print "3.is {sub} a {sup}?"

			# A unfixed formal type can only accept itself
			if sub == sup then return true

			assert anchor != null
			sub = sub.lookup_bound(mmodule, anchor)
			if sub_reject_null then sub = sub.as_notnull

			#print "3.is {sub} a {sup}?"

			# Manage the second layer of null/nullable
			if sub isa MNullableType then
				if not sup_accept_null and not sub_reject_null then return false
				sub = sub.mtype
			else if sub isa MNotNullType then
				sub_reject_null = true
				sub = sub.mtype
			else if sub isa MNullType then
				return sup_accept_null
			end
		end
		#print "4.is {sub} a {sup}? <- no more resolution"

		if sub isa MBottomType or sub isa MErrorType then
			return true
		end

		assert sub isa MClassType else print_error "{sub} <? {sup}" # It is the only remaining type

		# Handle sup-type when the sub-type is class-based (other cases must have be identified before).
		if sup isa MFormalType or sup isa MNullType or sup isa MBottomType or sup isa MErrorType then
			# These types are not super-types of Class-based types.
			return false
		end

		assert sup isa MClassType else print_error "got {sup} {sub.inspect}" # It is the only remaining type

		# Now both are MClassType, we need to dig

		if sub == sup then return true

		if anchor == null then anchor = sub # UGLY: any anchor will work
		var resolved_sub = sub.anchor_to(mmodule, anchor)
		var res = resolved_sub.collect_mclasses(mmodule).has(sup.mclass)
		if not res then return false
		if not sup isa MGenericType then return true
		var sub2 = sub.supertype_to(mmodule, anchor, sup.mclass)
		assert sub2.mclass == sup.mclass
		for i in [0..sup.mclass.arity[ do
			var sub_arg = sub2.arguments[i]
			var sup_arg = sup.arguments[i]
			res = sub_arg.is_subtype(mmodule, anchor, sup_arg)
			if not res then return false
		end
		return true
	end

	# The base class type on which self is based
	#
	# This base type is used to get property (an internally to perform
	# unsafe type comparison).
	#
	# Beware: some types (like null) are not based on a class thus this
	# method will crash
	#
	# Basically, this function transform the virtual types and parameter
	# types to their bounds.
	#
	# Example
	#
	#     class A end
	#     class B super A end
	#     class X end
	#     class Y super X end
	#     class G[T: A]
	#       type U: X
	#     end
	#     class H
	#       super G[B]
	#       redef type U: Y
	#     end
	#
	# Map[T,U]  anchor_to  H  #->  Map[B,Y]
	#
	# Explanation of the example:
	# In H, T is set to B, because "H super G[B]", and U is bound to Y,
	# because "redef type U: Y". Therefore, Map[T, U] is bound to
	# Map[B, Y]
	#
	# REQUIRE: `self.need_anchor implies anchor != null`
	# ENSURE: `not self.need_anchor implies result == self`
	# ENSURE: `not result.need_anchor`
	fun anchor_to(mmodule: MModule, anchor: nullable MClassType): MType
	do
		if not need_anchor then return self
		assert anchor != null and not anchor.need_anchor
		# Just resolve to the anchor and clear all the virtual types
		var res = self.resolve_for(anchor, null, mmodule, true)
		assert not res.need_anchor
		return res
	end

	# Does `self` contain a virtual type or a formal generic parameter type?
	# In order to remove those types, you usually want to use `anchor_to`.
	fun need_anchor: Bool do return true

	# Return the supertype when adapted to a class.
	#
	# In Nit, for each super-class of a type, there is a equivalent super-type.
	#
	# Example:
	#
	# ~~~nitish
	#     class G[T, U] end
	#     class H[V] super G[V, Bool] end
	#
	# H[Int]  supertype_to  G  #->  G[Int, Bool]
	# ~~~
	#
	# REQUIRE: `super_mclass` is a super-class of `self`
	# REQUIRE: `self.need_anchor implies anchor != null and self.can_resolve_for(anchor, null, mmodule)`
	# ENSURE: `result.mclass = super_mclass`
	fun supertype_to(mmodule: MModule, anchor: nullable MClassType, super_mclass: MClass): MClassType
	do
		if super_mclass.arity == 0 then return super_mclass.mclass_type
		if self isa MClassType and self.mclass == super_mclass then return self
		var resolved_self
		if self.need_anchor then
			assert anchor != null
			resolved_self = self.anchor_to(mmodule, anchor)
		else
			resolved_self = self
		end
		var supertypes = resolved_self.collect_mtypes(mmodule)
		for supertype in supertypes do
			if supertype.mclass == super_mclass then
				# FIXME: Here, we stop on the first goal. Should we check others and detect inconsistencies?
				return supertype.resolve_for(self, anchor, mmodule, false)
			end
		end
		abort
	end

	# Replace formals generic types in self with resolved values in `mtype`
	# If `cleanup_virtual` is true, then virtual types are also replaced
	# with their bounds.
	#
	# This function returns self if `need_anchor` is false.
	#
	# ## Example 1
	#
	# ~~~
	# class G[E] end
	# class H[F] super G[F] end
	# class X[Z] end
	# ~~~
	#
	#  * Array[E].resolve_for(H[Int])  #->  Array[Int]
	#  * Array[E].resolve_for(G[Z], X[Int]) #->  Array[Z]
	#
	# Explanation of the example:
	#  * Array[E].need_anchor is true because there is a formal generic parameter type E
	#  * E makes sense for H[Int] because E is a formal parameter of G and H specialize G
	#  * Since "H[F] super G[F]", E is in fact F for H
	#  * More specifically, in H[Int], E is Int
	#  * So, in H[Int], Array[E] is Array[Int]
	#
	# This function is mainly used to inherit a signature.
	# Because, unlike `anchor_to`, we do not want a full resolution of
	# a type but only an adapted version of it.
	#
	# ## Example 2
	#
	# ~~~
	# class A[E]
	#     fun foo(e:E):E is abstract
	# end
	# class B super A[Int] end
	# ~~~
	#
	# The signature on foo is (e: E): E
	# If we resolve the signature for B, we get (e:Int):Int
	#
	# ## Example 3
	#
	# ~~~nitish
	# class A[E]
	#     fun foo(e:E):E is abstract
	# end
	# class C[F]
	#     var a: A[Array[F]]
	#     fun bar do a.foo(x) # <- x is here
	# end
	# ~~~
	#
	# The first question is: is foo available on `a`?
	#
	# The static type of a is `A[Array[F]]`, that is an open type.
	# in order to find a method `foo`, whe must look at a resolved type.
	#
	#   A[Array[F]].anchor_to(C[nullable Object])  #->  A[Array[nullable Object]]
	#
	# the method `foo` exists in `A[Array[nullable Object]]`, therefore `foo` exists for `a`.
	#
	# The next question is: what is the accepted types for `x`?
	#
	# the signature of `foo` is `foo(e:E)`, thus we must resolve the type E
	#
	#   E.resolve_for(A[Array[F]],C[nullable Object])  #->  Array[F]
	#
	# The resolution can be done because `E` make sense for the class A (see `can_resolve_for`)
	#
	# FIXME: the parameter `cleanup_virtual` is just a bad idea, but having
	# two function instead of one seems also to be a bad idea.
	#
	# REQUIRE: `can_resolve_for(mtype, anchor, mmodule)`
	# ENSURE: `not self.need_anchor implies result == self`
	fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract

	# Resolve formal type to its verbatim bound.
	# If the type is not formal, just return self
	#
	# The result is returned exactly as declared in the "type" property (verbatim).
	# So it could be another formal type.
	#
	# In case of conflicts or inconsistencies in the model, the method returns a `MErrorType`.
	fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType do return self

	# Resolve the formal type to its simplest equivalent form.
	#
	# Formal types are either free or fixed.
	# When it is fixed, it means that it is equivalent with a simpler type.
	# When a formal type is free, it means that it is only equivalent with itself.
	# This method return the most simple equivalent type of `self`.
	#
	# This method is mainly used for subtype test in order to sanely compare fixed.
	#
	# By default, return self.
	# See the redefinitions for specific behavior in each kind of type.
	#
	# In case of conflicts or inconsistencies in the model, the method returns a `MErrorType`.
	fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType do return self

	# Is the type a `MErrorType` or contains an `MErrorType`?
	#
	# `MErrorType` are used in result with conflict or inconsistencies.
	#
	# See `is_legal_in` to check conformity with generic bounds.
	fun is_ok: Bool do return true

	# Is the type legal in a given `mmodule` (with an optional `anchor`)?
	#
	# A type is valid if:
	#
	# * it does not contain a `MErrorType` (see `is_ok`).
	# * its generic formal arguments are within their bounds.
	fun is_legal_in(mmodule: MModule, anchor: nullable MClassType): Bool do return is_ok

	# Can the type be resolved?
	#
	# In order to resolve open types, the formal types must make sence.
	#
	# ## Example
	#
	#     class A[E]
	#     end
	#     class B[F]
	#     end
	#
	# ~~~nitish
	# E.can_resolve_for(A[Int])  #->  true, E make sense in A
	#
	# E.can_resolve_for(B[Int])  #->  false, E does not make sense in B
	#
	# B[E].can_resolve_for(A[F], B[Object])  #->  true,
	# # B[E] is a red hearing only the E is important,
	# # E make sense in A
	# ~~~
	#
	# REQUIRE: `anchor != null implies not anchor.need_anchor`
	# REQUIRE: `mtype.need_anchor implies anchor != null and mtype.can_resolve_for(anchor, null, mmodule)`
	# ENSURE: `not self.need_anchor implies result == true`
	fun can_resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule): Bool is abstract

	# Return the nullable version of the type
	# If the type is already nullable then self is returned
	fun as_nullable: MType
	do
		var res = self.as_nullable_cache
		if res != null then return res
		res = new MNullableType(self)
		self.as_nullable_cache = res
		return res
	end

	# Remove the base type of a decorated (proxy) type.
	# Is the type is not decorated, then self is returned.
	#
	# Most of the time it is used to return the not nullable version of a nullable type.
	# In this case, this just remove the `nullable` notation, but the result can still contains null.
	# For instance if `self isa MNullType` or self is a formal type bounded by a nullable type.
	# If you really want to exclude the `null` value, then use `as_notnull`
	fun undecorate: MType
	do
		return self
	end

	# Returns the not null version of the type.
	# That is `self` minus the `null` value.
	#
	# For most types, this return `self`.
	# For formal types, this returns a special `MNotNullType`
	fun as_notnull: MType do return self

	private var as_nullable_cache: nullable MType = null


	# The depth of the type seen as a tree.
	#
	# * A -> 1
	# * G[A] -> 2
	# * H[A, B] -> 2
	# * H[G[A], B] -> 3
	#
	# Formal types have a depth of 1.
	# Only `MClassType` and `MFormalType` nodes are counted.
	fun depth: Int
	do
		return 1
	end

	# The length of the type seen as a tree.
	#
	# * A -> 1
	# * G[A] -> 2
	# * H[A, B] -> 3
	# * H[G[A], B] -> 4
	#
	# Formal types have a length of 1.
	# Only `MClassType` and `MFormalType` nodes are counted.
	fun length: Int
	do
		return 1
	end

	# Compute all the classdefs inherited/imported.
	# The returned set contains:
	#  * the class definitions from `mmodule` and its imported modules
	#  * the class definitions of this type and its super-types
	#
	# This function is used mainly internally.
	#
	# REQUIRE: `not self.need_anchor`
	fun collect_mclassdefs(mmodule: MModule): Set[MClassDef] is abstract

	# Compute all the super-classes.
	# This function is used mainly internally.
	#
	# REQUIRE: `not self.need_anchor`
	fun collect_mclasses(mmodule: MModule): Set[MClass] is abstract

	# Compute all the declared super-types.
	# Super-types are returned as declared in the classdefs (verbatim).
	# This function is used mainly internally.
	#
	# REQUIRE: `not self.need_anchor`
	fun collect_mtypes(mmodule: MModule): Set[MClassType] is abstract

	# Is the property in self for a given module
	# This method does not filter visibility or whatever
	#
	# REQUIRE: `not self.need_anchor`
	fun has_mproperty(mmodule: MModule, mproperty: MProperty): Bool
	do
		assert not self.need_anchor
		return self.collect_mclassdefs(mmodule).has(mproperty.intro_mclassdef)
	end
end