model: add new type `MNotNullType` to force that null is excluded from a type.

[nit.git] / src / model / model.nit

# This file is part of NIT ( http://www.nitlanguage.org ).
#
# Copyright 2012 Jean Privat <jean@pryen.org>
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#     http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# Classes, types and properties
#
# All three concepts are defined in this same module because these are strongly connected:
# * types are based on classes
# * classes contains properties
# * some properties are types (virtual types)
#
# TODO: liearization, extern stuff
# FIXME: better handling of the types
module model

import mmodule
import mdoc
import ordered_tree
private import more_collections

redef class Model
        # All known classes
        var mclasses = new Array[MClass]

        # All known properties
        var mproperties = new Array[MProperty]

        # Hierarchy of class definition.
        #
        # Each classdef is associated with its super-classdefs in regard to
        # its module of definition.
        var mclassdef_hierarchy = new POSet[MClassDef]

        # Class-type hierarchy restricted to the introduction.
        #
        # The idea is that what is true on introduction is always true whatever
        # the module considered.
        # Therefore, this hierarchy is used for a fast positive subtype check.
        #
        # This poset will evolve in a monotonous way:
        # * Two non connected nodes will remain unconnected
        # * New nodes can appear with new edges
        private var intro_mtype_specialization_hierarchy = new POSet[MClassType]

        # Global overlapped class-type hierarchy.
        # The hierarchy when all modules are combined.
        # Therefore, this hierarchy is used for a fast negative subtype check.
        #
        # This poset will evolve in an anarchic way. Loops can even be created.
        #
        # FIXME decide what to do on loops
        private var full_mtype_specialization_hierarchy = new POSet[MClassType]

        # Collections of classes grouped by their short name
        private var mclasses_by_name = new MultiHashMap[String, MClass]

        # Return all class named `name`.
        #
        # If such a class does not exist, null is returned
        # (instead of an empty array)
        #
        # Visibility or modules are not considered
        fun get_mclasses_by_name(name: String): nullable Array[MClass]
        do
                return mclasses_by_name.get_or_null(name)
        end

        # Collections of properties grouped by their short name
        private var mproperties_by_name = new MultiHashMap[String, MProperty]

        # Return all properties named `name`.
        #
        # If such a property does not exist, null is returned
        # (instead of an empty array)
        #
        # Visibility or modules are not considered
        fun get_mproperties_by_name(name: String): nullable Array[MProperty]
        do
                return mproperties_by_name.get_or_null(name)
        end

        # The only null type
        var null_type = new MNullType(self)

        # Build an ordered tree with from `concerns`
        fun concerns_tree(mconcerns: Collection[MConcern]): ConcernsTree do
                var seen = new HashSet[MConcern]
                var res = new ConcernsTree

                var todo = new Array[MConcern]
                todo.add_all mconcerns

                while not todo.is_empty do
                        var c = todo.pop
                        if seen.has(c) then continue
                        var pc = c.parent_concern
                        if pc == null then
                                res.add(null, c)
                        else
                                res.add(pc, c)
                                todo.add(pc)
                        end
                        seen.add(c)
                end

                return res
        end
end

# An OrderedTree that can be easily refined for display purposes
class ConcernsTree
        super OrderedTree[MConcern]
end

redef class MModule
        # All the classes introduced in the module
        var intro_mclasses = new Array[MClass]

        # All the class definitions of the module
        # (introduction and refinement)
        var mclassdefs = new Array[MClassDef]

        # Does the current module has a given class `mclass`?
        # Return true if the mmodule introduces, refines or imports a class.
        # Visibility is not considered.
        fun has_mclass(mclass: MClass): Bool
        do
                return self.in_importation <= mclass.intro_mmodule
        end

        # Full hierarchy of introduced ans imported classes.
        #
        # Create a new hierarchy got by flattening the classes for the module
        # and its imported modules.
        # Visibility is not considered.
        #
        # Note: this function is expensive and is usually used for the main
        # module of a program only. Do not use it to do you own subtype
        # functions.
        fun flatten_mclass_hierarchy: POSet[MClass]
        do
                var res = self.flatten_mclass_hierarchy_cache
                if res != null then return res
                res = new POSet[MClass]
                for m in self.in_importation.greaters do
                        for cd in m.mclassdefs do
                                var c = cd.mclass
                                res.add_node(c)
                                for s in cd.supertypes do
                                        res.add_edge(c, s.mclass)
                                end
                        end
                end
                self.flatten_mclass_hierarchy_cache = res
                return res
        end

        # Sort a given array of classes using the linearization order of the module
        # The most general is first, the most specific is last
        fun linearize_mclasses(mclasses: Array[MClass])
        do
                self.flatten_mclass_hierarchy.sort(mclasses)
        end

        # Sort a given array of class definitions using the linearization order of the module
        # the refinement link is stronger than the specialisation link
        # The most general is first, the most specific is last
        fun linearize_mclassdefs(mclassdefs: Array[MClassDef])
        do
                var sorter = new MClassDefSorter(self)
                sorter.sort(mclassdefs)
        end

        # Sort a given array of property definitions using the linearization order of the module
        # the refinement link is stronger than the specialisation link
        # The most general is first, the most specific is last
        fun linearize_mpropdefs(mpropdefs: Array[MPropDef])
        do
                var sorter = new MPropDefSorter(self)
                sorter.sort(mpropdefs)
        end

        private var flatten_mclass_hierarchy_cache: nullable POSet[MClass] = null

        # The primitive type `Object`, the root of the class hierarchy
        var object_type: MClassType = self.get_primitive_class("Object").mclass_type is lazy

        # The type `Pointer`, super class to all extern classes
        var pointer_type: MClassType = self.get_primitive_class("Pointer").mclass_type is lazy

        # The primitive type `Bool`
        var bool_type: MClassType = self.get_primitive_class("Bool").mclass_type is lazy

        # The primitive type `Int`
        var int_type: MClassType = self.get_primitive_class("Int").mclass_type is lazy

        # The primitive type `Char`
        var char_type: MClassType = self.get_primitive_class("Char").mclass_type is lazy

        # The primitive type `Float`
        var float_type: MClassType = self.get_primitive_class("Float").mclass_type is lazy

        # The primitive type `String`
        var string_type: MClassType = self.get_primitive_class("String").mclass_type is lazy

        # The primitive type `NativeString`
        var native_string_type: MClassType = self.get_primitive_class("NativeString").mclass_type is lazy

        # A primitive type of `Array`
        fun array_type(elt_type: MType): MClassType do return array_class.get_mtype([elt_type])

        # The primitive class `Array`
        var array_class: MClass = self.get_primitive_class("Array") is lazy

        # A primitive type of `NativeArray`
        fun native_array_type(elt_type: MType): MClassType do return native_array_class.get_mtype([elt_type])

        # The primitive class `NativeArray`
        var native_array_class: MClass = self.get_primitive_class("NativeArray") is lazy

        # The primitive type `Sys`, the main type of the program, if any
        fun sys_type: nullable MClassType
        do
                var clas = self.model.get_mclasses_by_name("Sys")
                if clas == null then return null
                return get_primitive_class("Sys").mclass_type
        end

        # The primitive type `Finalizable`
        # Used to tag classes that need to be finalized.
        fun finalizable_type: nullable MClassType
        do
                var clas = self.model.get_mclasses_by_name("Finalizable")
                if clas == null then return null
                return get_primitive_class("Finalizable").mclass_type
        end

        # Force to get the primitive class named `name` or abort
        fun get_primitive_class(name: String): MClass
        do
                var cla = self.model.get_mclasses_by_name(name)
                if cla == null then
                        if name == "Bool" and self.model.get_mclasses_by_name("Object") != null then
                                # Bool is injected because it is needed by engine to code the result
                                # of the implicit casts.
                                var c = new MClass(self, name, null, enum_kind, public_visibility)
                                var cladef = new MClassDef(self, c.mclass_type, new Location(null, 0,0,0,0))
                                cladef.set_supertypes([object_type])
                                cladef.add_in_hierarchy
                                return c
                        end
                        print("Fatal Error: no primitive class {name}")
                        exit(1)
                end
                if cla.length != 1 then
                        var msg = "Fatal Error: more than one primitive class {name}:"
                        for c in cla do msg += " {c.full_name}"
                        print msg
                        #exit(1)
                end
                return cla.first
        end

        # Try to get the primitive method named `name` on the type `recv`
        fun try_get_primitive_method(name: String, recv: MClass): nullable MMethod
        do
                var props = self.model.get_mproperties_by_name(name)
                if props == null then return null
                var res: nullable MMethod = null
                for mprop in props do
                        assert mprop isa MMethod
                        var intro = mprop.intro_mclassdef
                        for mclassdef in recv.mclassdefs do
                                if not self.in_importation.greaters.has(mclassdef.mmodule) then continue
                                if not mclassdef.in_hierarchy.greaters.has(intro) then continue
                                if res == null then
                                        res = mprop
                                else if res != mprop then
                                        print("Fatal Error: ambigous property name '{name}'; conflict between {mprop.full_name} and {res.full_name}")
                                        abort
                                end
                        end
                end
                return res
        end
end

private class MClassDefSorter
        super Comparator
        redef type COMPARED: MClassDef
        var mmodule: MModule
        redef fun compare(a, b)
        do
                var ca = a.mclass
                var cb = b.mclass
                if ca != cb then return mmodule.flatten_mclass_hierarchy.compare(ca, cb)
                return mmodule.model.mclassdef_hierarchy.compare(a, b)
        end
end

private class MPropDefSorter
        super Comparator
        redef type COMPARED: MPropDef
        var mmodule: MModule
        redef fun compare(pa, pb)
        do
                var a = pa.mclassdef
                var b = pb.mclassdef
                var ca = a.mclass
                var cb = b.mclass
                if ca != cb then return mmodule.flatten_mclass_hierarchy.compare(ca, cb)
                return mmodule.model.mclassdef_hierarchy.compare(a, b)
        end
end

# A named class
#
# `MClass` are global to the model; it means that a `MClass` is not bound to a
# specific `MModule`.
#
# This characteristic helps the reasoning about classes in a program since a
# single `MClass` object always denote the same class.
#
# The drawback is that classes (`MClass`) contain almost nothing by themselves.
# These do not really have properties nor belong to a hierarchy since the property and the
# hierarchy of a class depends of the refinement in the modules.
#
# Most services on classes require the precision of a module, and no one can asks what are
# the super-classes of a class nor what are properties of a class without precising what is
# the module considered.
#
# For instance, during the typing of a source-file, the module considered is the module of the file.
# eg. the question *is the method `foo` exists in the class `Bar`?* must be reformulated into
# *is the method `foo` exists in the class `Bar` in the current module?*
#
# During some global analysis, the module considered may be the main module of the program.
class MClass
        super MEntity

        # The module that introduce the class
        # While classes are not bound to a specific module,
        # the introducing module is used for naming an visibility
        var intro_mmodule: MModule

        # The short name of the class
        # In Nit, the name of a class cannot evolve in refinements
        redef var name: String

        # The canonical name of the class
        #
        # It is the name of the class prefixed by the full_name of the `intro_mmodule`
        # Example: `"owner::module::MyClass"`
        redef var full_name is lazy do
                return "{self.intro_mmodule.namespace_for(visibility)}::{name}"
        end

        redef var c_name is lazy do
                return "{intro_mmodule.c_namespace_for(visibility)}__{name.to_cmangle}"
        end

        # The number of generic formal parameters
        # 0 if the class is not generic
        var arity: Int is noinit

        # Each generic formal parameters in order.
        # is empty if the class is not generic
        var mparameters = new Array[MParameterType]

        # Initialize `mparameters` from their names.
        protected fun setup_parameter_names(parameter_names: nullable Array[String]) is
                autoinit
        do
                if parameter_names == null then
                        self.arity = 0
                else
                        self.arity = parameter_names.length
                end

                # Create the formal parameter types
                if arity > 0 then
                        assert parameter_names != null
                        var mparametertypes = new Array[MParameterType]
                        for i in [0..arity[ do
                                var mparametertype = new MParameterType(self, i, parameter_names[i])
                                mparametertypes.add(mparametertype)
                        end
                        self.mparameters = mparametertypes
                        var mclass_type = new MGenericType(self, mparametertypes)
                        self.mclass_type = mclass_type
                        self.get_mtype_cache[mparametertypes] = mclass_type
                else
                        self.mclass_type = new MClassType(self)
                end
        end

        # The kind of the class (interface, abstract class, etc.)
        # In Nit, the kind of a class cannot evolve in refinements
        var kind: MClassKind

        # The visibility of the class
        # In Nit, the visibility of a class cannot evolve in refinements
        var visibility: MVisibility

        init
        do
                intro_mmodule.intro_mclasses.add(self)
                var model = intro_mmodule.model
                model.mclasses_by_name.add_one(name, self)
                model.mclasses.add(self)
        end

        redef fun model do return intro_mmodule.model

        # All class definitions (introduction and refinements)
        var mclassdefs = new Array[MClassDef]

        # Alias for `name`
        redef fun to_s do return self.name

        # The definition that introduces the class.
        #
        # Warning: such a definition may not exist in the early life of the object.
        # In this case, the method will abort.
        var intro: MClassDef is noinit

        # Return the class `self` in the class hierarchy of the module `mmodule`.
        #
        # SEE: `MModule::flatten_mclass_hierarchy`
        # REQUIRE: `mmodule.has_mclass(self)`
        fun in_hierarchy(mmodule: MModule): POSetElement[MClass]
        do
                return mmodule.flatten_mclass_hierarchy[self]
        end

        # The principal static type of the class.
        #
        # For non-generic class, mclass_type is the only `MClassType` based
        # on self.
        #
        # For a generic class, the arguments are the formal parameters.
        # i.e.: for the class Array[E:Object], the `mclass_type` is Array[E].
        # If you want Array[Object] the see `MClassDef::bound_mtype`
        #
        # For generic classes, the mclass_type is also the way to get a formal
        # generic parameter type.
        #
        # To get other types based on a generic class, see `get_mtype`.
        #
        # ENSURE: `mclass_type.mclass == self`
        var mclass_type: MClassType is noinit

        # Return a generic type based on the class
        # Is the class is not generic, then the result is `mclass_type`
        #
        # REQUIRE: `mtype_arguments.length == self.arity`
        fun get_mtype(mtype_arguments: Array[MType]): MClassType
        do
                assert mtype_arguments.length == self.arity
                if self.arity == 0 then return self.mclass_type
                var res = get_mtype_cache.get_or_null(mtype_arguments)
                if res != null then return res
                res = new MGenericType(self, mtype_arguments)
                self.get_mtype_cache[mtype_arguments.to_a] = res
                return res
        end

        private var get_mtype_cache = new HashMap[Array[MType], MGenericType]

        # Is there a `new` factory to allow the pseudo instantiation?
        var has_new_factory = false is writable
end


# A definition (an introduction or a refinement) of a class in a module
#
# A `MClassDef` is associated with an explicit (or almost) definition of a
# class. Unlike `MClass`, a `MClassDef` is a local definition that belong to
# a specific class and a specific module, and contains declarations like super-classes
# or properties.
#
# It is the class definitions that are the backbone of most things in the model:
# ClassDefs are defined with regard with other classdefs.
# Refinement and specialization are combined to produce a big poset called the `Model::mclassdef_hierarchy`.
#
# Moreover, the extension and the intention of types is defined by looking at the MClassDefs.
class MClassDef
        super MEntity

        # The module where the definition is
        var mmodule: MModule

        # The associated `MClass`
        var mclass: MClass is noinit

        # The bounded type associated to the mclassdef
        #
        # For a non-generic class, `bound_mtype` and `mclass.mclass_type`
        # are the same type.
        #
        # Example:
        # For the classdef Array[E: Object], the bound_mtype is Array[Object].
        # If you want Array[E], then see `mclass.mclass_type`
        #
        # ENSURE: `bound_mtype.mclass == self.mclass`
        var bound_mtype: MClassType

        # The origin of the definition
        var location: Location

        # Internal name combining the module and the class
        # Example: "mymodule#MyClass"
        redef var to_s: String is noinit

        init
        do
                self.mclass = bound_mtype.mclass
                mmodule.mclassdefs.add(self)
                mclass.mclassdefs.add(self)
                if mclass.intro_mmodule == mmodule then
                        assert not isset mclass._intro
                        mclass.intro = self
                end
                self.to_s = "{mmodule}#{mclass}"
        end

        # Actually the name of the `mclass`
        redef fun name do return mclass.name

        # The module and class name separated by a '#'.
        #
        # The short-name of the class is used for introduction.
        # Example: "my_module#MyClass"
        #
        # The full-name of the class is used for refinement.
        # Example: "my_module#intro_module::MyClass"
        redef var full_name is lazy do
                if is_intro then
                        # public gives 'p#A'
                        # private gives 'p::m#A'
                        return "{mmodule.namespace_for(mclass.visibility)}#{mclass.name}"
                else if mclass.intro_mmodule.mproject != mmodule.mproject then
                        # public gives 'q::n#p::A'
                        # private gives 'q::n#p::m::A'
                        return "{mmodule.full_name}#{mclass.full_name}"
                else if mclass.visibility > private_visibility then
                        # public gives 'p::n#A'
                        return "{mmodule.full_name}#{mclass.name}"
                else
                        # private gives 'p::n#::m::A' (redundant p is omitted)
                        return "{mmodule.full_name}#::{mclass.intro_mmodule.name}::{mclass.name}"
                end
        end

        redef var c_name is lazy do
                if is_intro then
                        return "{mmodule.c_namespace_for(mclass.visibility)}___{mclass.c_name}"
                else if mclass.intro_mmodule.mproject == mmodule.mproject and mclass.visibility > private_visibility then
                        return "{mmodule.c_name}___{mclass.name.to_cmangle}"
                else
                        return "{mmodule.c_name}___{mclass.c_name}"
                end
        end

        redef fun model do return mmodule.model

        # All declared super-types
        # FIXME: quite ugly but not better idea yet
        var supertypes = new Array[MClassType]

        # Register some super-types for the class (ie "super SomeType")
        #
        # The hierarchy must not already be set
        # REQUIRE: `self.in_hierarchy == null`
        fun set_supertypes(supertypes: Array[MClassType])
        do
                assert unique_invocation: self.in_hierarchy == null
                var mmodule = self.mmodule
                var model = mmodule.model
                var mtype = self.bound_mtype

                for supertype in supertypes do
                        self.supertypes.add(supertype)

                        # Register in full_type_specialization_hierarchy
                        model.full_mtype_specialization_hierarchy.add_edge(mtype, supertype)
                        # Register in intro_type_specialization_hierarchy
                        if mclass.intro_mmodule == mmodule and supertype.mclass.intro_mmodule == mmodule then
                                model.intro_mtype_specialization_hierarchy.add_edge(mtype, supertype)
                        end
                end

        end

        # Collect the super-types (set by set_supertypes) to build the hierarchy
        #
        # This function can only invoked once by class
        # REQUIRE: `self.in_hierarchy == null`
        # ENSURE: `self.in_hierarchy != null`
        fun add_in_hierarchy
        do
                assert unique_invocation: self.in_hierarchy == null
                var model = mmodule.model
                var res = model.mclassdef_hierarchy.add_node(self)
                self.in_hierarchy = res
                var mtype = self.bound_mtype

                # Here we need to connect the mclassdef to its pairs in the mclassdef_hierarchy
                # The simpliest way is to attach it to collect_mclassdefs
                for mclassdef in mtype.collect_mclassdefs(mmodule) do
                        res.poset.add_edge(self, mclassdef)
                end
        end

        # The view of the class definition in `mclassdef_hierarchy`
        var in_hierarchy: nullable POSetElement[MClassDef] = null

        # Is the definition the one that introduced `mclass`?
        fun is_intro: Bool do return mclass.intro == self

        # All properties introduced by the classdef
        var intro_mproperties = new Array[MProperty]

        # All property definitions in the class (introductions and redefinitions)
        var mpropdefs = new Array[MPropDef]
end

# 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"

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

                # A unfixed formal type can only accept itself
                if sup isa MFormalType then
                        return false
                end

                if sup isa MNullType then
                        # `sup` accepts only null
                        return false
                end

                assert sup isa MClassType # 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 res == false 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 res == false 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]
        #
        # ENSURE: `not self.need_anchor implies result == self`
        # ENSURE: `not result.need_anchor`
        fun anchor_to(mmodule: MModule, anchor: MClassType): MType
        do
                if not need_anchor then return self
                assert 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 conflict, the method aborts.
        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.
        fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType do return self

        # 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

        # Return the not nullable version of the type
        # Is the type is already not nullable, then self is returned.
        #
        # Note: 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.
        fun as_notnullable: 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.
        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.
        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

# A type based on a class.
#
# `MClassType` have properties (see `has_mproperty`).
class MClassType
        super MType

        # The associated class
        var mclass: MClass

        redef fun model do return self.mclass.intro_mmodule.model

        # TODO: private init because strongly bounded to its mclass. see `mclass.mclass_type`

        # The formal arguments of the type
        # ENSURE: `result.length == self.mclass.arity`
        var arguments = new Array[MType]

        redef fun to_s do return mclass.to_s

        redef fun full_name do return mclass.full_name

        redef fun c_name do return mclass.c_name

        redef fun need_anchor do return false

        redef fun anchor_to(mmodule: MModule, anchor: MClassType): MClassType
        do
                return super.as(MClassType)
        end

        redef fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MClassType do return self

        redef fun can_resolve_for(mtype, anchor, mmodule) do return true

        redef fun collect_mclassdefs(mmodule)
        do
                assert not self.need_anchor
                var cache = self.collect_mclassdefs_cache
                if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
                return cache[mmodule]
        end

        redef fun collect_mclasses(mmodule)
        do
                if collect_mclasses_last_module == mmodule then return collect_mclasses_last_module_cache
                assert not self.need_anchor
                var cache = self.collect_mclasses_cache
                if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
                var res = cache[mmodule]
                collect_mclasses_last_module = mmodule
                collect_mclasses_last_module_cache = res
                return res
        end

        private var collect_mclasses_last_module: nullable MModule = null
        private var collect_mclasses_last_module_cache: Set[MClass] is noinit

        redef fun collect_mtypes(mmodule)
        do
                assert not self.need_anchor
                var cache = self.collect_mtypes_cache
                if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
                return cache[mmodule]
        end

        # common implementation for `collect_mclassdefs`, `collect_mclasses`, and `collect_mtypes`.
        private fun collect_things(mmodule: MModule)
        do
                var res = new HashSet[MClassDef]
                var seen = new HashSet[MClass]
                var types = new HashSet[MClassType]
                seen.add(self.mclass)
                var todo = [self.mclass]
                while not todo.is_empty do
                        var mclass = todo.pop
                        #print "process {mclass}"
                        for mclassdef in mclass.mclassdefs do
                                if not mmodule.in_importation <= mclassdef.mmodule then continue
                                #print "  process {mclassdef}"
                                res.add(mclassdef)
                                for supertype in mclassdef.supertypes do
                                        types.add(supertype)
                                        var superclass = supertype.mclass
                                        if seen.has(superclass) then continue
                                        #print "    add {superclass}"
                                        seen.add(superclass)
                                        todo.add(superclass)
                                end
                        end
                end
                collect_mclassdefs_cache[mmodule] = res
                collect_mclasses_cache[mmodule] = seen
                collect_mtypes_cache[mmodule] = types
        end

        private var collect_mclassdefs_cache = new HashMap[MModule, Set[MClassDef]]
        private var collect_mclasses_cache = new HashMap[MModule, Set[MClass]]
        private var collect_mtypes_cache = new HashMap[MModule, Set[MClassType]]

end

# A type based on a generic class.
# A generic type a just a class with additional formal generic arguments.
class MGenericType
        super MClassType

        redef var arguments

        # TODO: private init because strongly bounded to its mclass. see `mclass.get_mtype`

        init
        do
                assert self.mclass.arity == arguments.length

                self.need_anchor = false
                for t in arguments do
                        if t.need_anchor then
                                self.need_anchor = true
                                break
                        end
                end

                self.to_s = "{mclass}[{arguments.join(", ")}]"
        end

        # The short-name of the class, then the full-name of each type arguments within brackets.
        # Example: `"Map[String, List[Int]]"`
        redef var to_s: String is noinit

        # The full-name of the class, then the full-name of each type arguments within brackets.
        # Example: `"standard::Map[standard::String, standard::List[standard::Int]]"`
        redef var full_name is lazy do
                var args = new Array[String]
                for t in arguments do
                        args.add t.full_name
                end
                return "{mclass.full_name}[{args.join(", ")}]"
        end

        redef var c_name is lazy do
                var res = mclass.c_name
                # Note: because the arity is known, a prefix notation is enough
                for t in arguments do
                        res += "__"
                        res += t.c_name
                end
                return res.to_s
        end

        redef var need_anchor: Bool is noinit

        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                if not need_anchor then return self
                assert can_resolve_for(mtype, anchor, mmodule)
                var types = new Array[MType]
                for t in arguments do
                        types.add(t.resolve_for(mtype, anchor, mmodule, cleanup_virtual))
                end
                return mclass.get_mtype(types)
        end

        redef fun can_resolve_for(mtype, anchor, mmodule)
        do
                if not need_anchor then return true
                for t in arguments do
                        if not t.can_resolve_for(mtype, anchor, mmodule) then return false
                end
                return true
        end


        redef fun depth
        do
                var dmax = 0
                for a in self.arguments do
                        var d = a.depth
                        if d > dmax then dmax = d
                end
                return dmax + 1
        end

        redef fun length
        do
                var res = 1
                for a in self.arguments do
                        res += a.length
                end
                return res
        end
end

# A formal type (either virtual of parametric).
#
# The main issue with formal types is that they offer very little information on their own
# and need a context (anchor and mmodule) to be useful.
abstract class MFormalType
        super MType

        redef var as_notnull = new MNotNullType(self) is lazy
end

# A virtual formal type.
class MVirtualType
        super MFormalType

        # The property associated with the type.
        # Its the definitions of this property that determine the bound or the virtual type.
        var mproperty: MVirtualTypeProp

        redef fun model do return self.mproperty.intro_mclassdef.mmodule.model

        redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        do
                return lookup_single_definition(mmodule, resolved_receiver).bound.as(not null)
        end

        private fun lookup_single_definition(mmodule: MModule, resolved_receiver: MType): MVirtualTypeDef
        do
                assert not resolved_receiver.need_anchor
                var props = self.mproperty.lookup_definitions(mmodule, resolved_receiver)
                if props.is_empty then
                        abort
                else if props.length == 1 then
                        return props.first
                end
                var types = new ArraySet[MType]
                var res  = props.first
                for p in props do
                        types.add(p.bound.as(not null))
                        if not res.is_fixed then res = p
                end
                if types.length == 1 then
                        return res
                end
                abort
        end

        # A VT is fixed when:
        # * the VT is (re-)defined with the annotation `is fixed`
        # * the VT is (indirectly) bound to an enum class (see `enum_kind`) since there is no subtype possible
        # * the receiver is an enum class since there is no subtype possible
        redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
                resolved_receiver = resolved_receiver.as_notnullable
                assert resolved_receiver isa MClassType # It is the only remaining type

                var prop = lookup_single_definition(mmodule, resolved_receiver)
                var res = prop.bound.as(not null)

                # Recursively lookup the fixed result
                res = res.lookup_fixed(mmodule, resolved_receiver)

                # 1. For a fixed VT, return the resolved bound
                if prop.is_fixed then return res

                # 2. For a enum boud, return the bound
                if res isa MClassType and res.mclass.kind == enum_kind then return res

                # 3. for a enum receiver return the bound
                if resolved_receiver.mclass.kind == enum_kind then return res

                return self
        end

        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                if not cleanup_virtual then return self
                assert can_resolve_for(mtype, anchor, mmodule)
                # self is a virtual type declared (or inherited) in mtype
                # The point of the function it to get the bound of the virtual type that make sense for mtype
                # But because mtype is maybe a virtual/formal type, we need to get a real receiver first
                #print "{class_name}: {self}/{mtype}/{anchor}?"
                var resolved_receiver
                if mtype.need_anchor then
                        assert anchor != null
                        resolved_receiver = mtype.resolve_for(anchor, null, mmodule, true)
                else
                        resolved_receiver = mtype
                end
                # Now, we can get the bound
                var verbatim_bound = lookup_bound(mmodule, resolved_receiver)
                # The bound is exactly as declared in the "type" property, so we must resolve it again
                var res = verbatim_bound.resolve_for(mtype, anchor, mmodule, cleanup_virtual)

                return res
        end

        redef fun can_resolve_for(mtype, anchor, mmodule)
        do
                if mtype.need_anchor then
                        assert anchor != null
                        mtype = mtype.anchor_to(mmodule, anchor)
                end
                return mtype.has_mproperty(mmodule, mproperty)
        end

        redef fun to_s do return self.mproperty.to_s

        redef fun full_name do return self.mproperty.full_name

        redef fun c_name do return self.mproperty.c_name
end

# The type associated to a formal parameter generic type of a class
#
# Each parameter type is associated to a specific class.
# It means that all refinements of a same class "share" the parameter type,
# but that a generic subclass has its own parameter types.
#
# However, in the sense of the meta-model, a parameter type of a class is
# a valid type in a subclass. The "in the sense of the meta-model" is
# important because, in the Nit language, the programmer cannot refers
# directly to the parameter types of the super-classes.
#
# Example:
#
#     class A[E]
#         fun e: E is abstract
#     end
#     class B[F]
#         super A[Array[F]]
#     end
#
# In the class definition B[F], `F` is a valid type but `E` is not.
# However, `self.e` is a valid method call, and the signature of `e` is
# declared `e: E`.
#
# Note that parameter types are shared among class refinements.
# Therefore parameter only have an internal name (see `to_s` for details).
class MParameterType
        super MFormalType

        # The generic class where the parameter belong
        var mclass: MClass

        redef fun model do return self.mclass.intro_mmodule.model

        # The position of the parameter (0 for the first parameter)
        # FIXME: is `position` a better name?
        var rank: Int

        redef var name

        redef fun to_s do return name

        redef var full_name is lazy do return "{mclass.full_name}::{name}"

        redef var c_name is lazy do return mclass.c_name + "__" + "#{name}".to_cmangle

        redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
                resolved_receiver = resolved_receiver.as_notnullable
                assert resolved_receiver isa MClassType # It is the only remaining type
                var goalclass = self.mclass
                if resolved_receiver.mclass == goalclass then
                        return resolved_receiver.arguments[self.rank]
                end
                var supertypes = resolved_receiver.collect_mtypes(mmodule)
                for t in supertypes do
                        if t.mclass == goalclass then
                                # Yeah! c specialize goalclass with a "super `t'". So the question is what is the argument of f
                                # FIXME: Here, we stop on the first goal. Should we check others and detect inconsistencies?
                                var res = t.arguments[self.rank]
                                return res
                        end
                end
                abort
        end

        # A PT is fixed when:
        # * Its bound is a enum class (see `enum_kind`).
        #   The PT is just useless, but it is still a case.
        # * More usually, the `resolved_receiver` is a subclass of `self.mclass`,
        #   so it is necessarily fixed in a `super` clause, either with a normal type
        #   or with another PT.
        #   See `resolve_for` for examples about related issues.
        redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
                resolved_receiver = resolved_receiver.as_notnullable
                assert resolved_receiver isa MClassType # It is the only remaining type
                var res = self.resolve_for(resolved_receiver.mclass.mclass_type, resolved_receiver, mmodule, false)
                return res
        end

        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                assert can_resolve_for(mtype, anchor, mmodule)
                #print "{class_name}: {self}/{mtype}/{anchor}?"

                if mtype isa MGenericType and mtype.mclass == self.mclass then
                        var res = mtype.arguments[self.rank]
                        if anchor != null and res.need_anchor then
                                # Maybe the result can be resolved more if are bound to a final class
                                var r2 = res.anchor_to(mmodule, anchor)
                                if r2 isa MClassType and r2.mclass.kind == enum_kind then return r2
                        end
                        return res
                end

                # self is a parameter type of mtype (or of a super-class of mtype)
                # The point of the function it to get the bound of the virtual type that make sense for mtype
                # But because mtype is maybe a virtual/formal type, we need to get a real receiver first
                # FIXME: What happens here is far from clear. Thus this part must be validated and clarified
                var resolved_receiver
                if mtype.need_anchor then
                        assert anchor != null
                        resolved_receiver = mtype.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, true)
                else
                        resolved_receiver = mtype
                end
                if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
                if resolved_receiver isa MParameterType then
                        assert resolved_receiver.mclass == anchor.mclass
                        resolved_receiver = anchor.arguments[resolved_receiver.rank]
                        if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
                end
                assert resolved_receiver isa MClassType # It is the only remaining type

                # Eh! The parameter is in the current class.
                # So we return the corresponding argument, no mater what!
                if resolved_receiver.mclass == self.mclass then
                        var res = resolved_receiver.arguments[self.rank]
                        #print "{class_name}: {self}/{mtype}/{anchor} -> direct {res}"
                        return res
                end

                if resolved_receiver.need_anchor then
                        assert anchor != null
                        resolved_receiver = resolved_receiver.resolve_for(anchor, null, mmodule, false)
                end
                # Now, we can get the bound
                var verbatim_bound = lookup_bound(mmodule, resolved_receiver)
                # The bound is exactly as declared in the "type" property, so we must resolve it again
                var res = verbatim_bound.resolve_for(mtype, anchor, mmodule, cleanup_virtual)

                #print "{class_name}: {self}/{mtype}/{anchor} -> indirect {res}"

                return res
        end

        redef fun can_resolve_for(mtype, anchor, mmodule)
        do
                if mtype.need_anchor then
                        assert anchor != null
                        mtype = mtype.anchor_to(mmodule, anchor)
                end
                return mtype.collect_mclassdefs(mmodule).has(mclass.intro)
        end
end

# A type that decorates another type.
#
# The point of this class is to provide a common implementation of sevices that just forward to the original type.
# Specific decorator are expected to redefine (or to extend) the default implementation as this suit them.
abstract class MProxyType
        super MType
        # The base type
        var mtype: MType

        redef fun model do return self.mtype.model
        redef fun need_anchor do return mtype.need_anchor
        redef fun as_nullable do return mtype.as_nullable
        redef fun as_notnull do return mtype.as_notnull
        redef fun as_notnullable do return mtype.as_notnullable
        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                var res = self.mtype.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
                return res
        end

        redef fun can_resolve_for(mtype, anchor, mmodule)
        do
                return self.mtype.can_resolve_for(mtype, anchor, mmodule)
        end

        redef fun lookup_fixed(mmodule, resolved_receiver)
        do
                var t = mtype.lookup_fixed(mmodule, resolved_receiver)
                return t
        end

        redef fun depth do return self.mtype.depth

        redef fun length do return self.mtype.length

        redef fun collect_mclassdefs(mmodule)
        do
                assert not self.need_anchor
                return self.mtype.collect_mclassdefs(mmodule)
        end

        redef fun collect_mclasses(mmodule)
        do
                assert not self.need_anchor
                return self.mtype.collect_mclasses(mmodule)
        end

        redef fun collect_mtypes(mmodule)
        do
                assert not self.need_anchor
                return self.mtype.collect_mtypes(mmodule)
        end
end

# A type prefixed with "nullable"
class MNullableType
        super MProxyType

        init
        do
                self.to_s = "nullable {mtype}"
        end

        redef var to_s: String is noinit

        redef var full_name is lazy do return "nullable {mtype.full_name}"

        redef var c_name is lazy do return "nullable__{mtype.c_name}"

        redef fun as_nullable do return self
        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                var res = super
                return res.as_nullable
        end

        # Efficiently returns `mtype.lookup_fixed(mmodule, resolved_receiver).as_nullable`
        redef fun lookup_fixed(mmodule, resolved_receiver)
        do
                var t = super
                if t == mtype then return self
                return t.as_nullable
        end
end

# A non-null version of a formal type.
#
# When a formal type in bounded to a nullable type, this is the type of the not null version of it.
class MNotNullType
        super MProxyType

        redef fun to_s do return "not null {mtype}"
        redef var full_name is lazy do return "not null {mtype.full_name}"
        redef var c_name is lazy do return "notnull__{mtype.c_name}"

        redef fun as_notnull do return self

        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                var res = super
                return res.as_notnull
        end

        # Efficiently returns `mtype.lookup_fixed(mmodule, resolved_receiver).as_notnull`
        redef fun lookup_fixed(mmodule, resolved_receiver)
        do
                var t = super
                if t == mtype then return self
                return t.as_notnull
        end
end

# The type of the only value null
#
# The is only one null type per model, see `MModel::null_type`.
class MNullType
        super MType
        redef var model: Model
        redef fun to_s do return "null"
        redef fun full_name do return "null"
        redef fun c_name do return "null"
        redef fun as_nullable do return self

        # Aborts on `null`
        redef fun as_notnull do abort # sorry...
        redef fun need_anchor do return false
        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual) do return self
        redef fun can_resolve_for(mtype, anchor, mmodule) do return true

        redef fun collect_mclassdefs(mmodule) do return new HashSet[MClassDef]

        redef fun collect_mclasses(mmodule) do return new HashSet[MClass]

        redef fun collect_mtypes(mmodule) do return new HashSet[MClassType]
end

# A signature of a method
class MSignature
        super MType

        # The each parameter (in order)
        var mparameters: Array[MParameter]

        # The return type (null for a procedure)
        var return_mtype: nullable MType

        redef fun depth
        do
                var dmax = 0
                var t = self.return_mtype
                if t != null then dmax = t.depth
                for p in mparameters do
                        var d = p.mtype.depth
                        if d > dmax then dmax = d
                end
                return dmax + 1
        end

        redef fun length
        do
                var res = 1
                var t = self.return_mtype
                if t != null then res += t.length
                for p in mparameters do
                        res += p.mtype.length
                end
                return res
        end

        # REQUIRE: 1 <= mparameters.count p -> p.is_vararg
        init
        do
                var vararg_rank = -1
                for i in [0..mparameters.length[ do
                        var parameter = mparameters[i]
                        if parameter.is_vararg then
                                assert vararg_rank == -1
                                vararg_rank = i
                        end
                end
                self.vararg_rank = vararg_rank
        end

        # The rank of the ellipsis (`...`) for vararg (starting from 0).
        # value is -1 if there is no vararg.
        # Example: for "(a: Int, b: Bool..., c: Char)" #-> vararg_rank=1
        var vararg_rank: Int is noinit

        # The number or parameters
        fun arity: Int do return mparameters.length

        redef fun to_s
        do
                var b = new FlatBuffer
                if not mparameters.is_empty then
                        b.append("(")
                        for i in [0..mparameters.length[ do
                                var mparameter = mparameters[i]
                                if i > 0 then b.append(", ")
                                b.append(mparameter.name)
                                b.append(": ")
                                b.append(mparameter.mtype.to_s)
                                if mparameter.is_vararg then
                                        b.append("...")
                                end
                        end
                        b.append(")")
                end
                var ret = self.return_mtype
                if ret != null then
                        b.append(": ")
                        b.append(ret.to_s)
                end
                return b.to_s
        end

        redef fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MSignature
        do
                var params = new Array[MParameter]
                for p in self.mparameters do
                        params.add(p.resolve_for(mtype, anchor, mmodule, cleanup_virtual))
                end
                var ret = self.return_mtype
                if ret != null then
                        ret = ret.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
                end
                var res = new MSignature(params, ret)
                return res
        end
end

# A parameter in a signature
class MParameter
        super MEntity

        # The name of the parameter
        redef var name: String

        # The static type of the parameter
        var mtype: MType

        # Is the parameter a vararg?
        var is_vararg: Bool

        redef fun to_s
        do
                if is_vararg then
                        return "{name}: {mtype}..."
                else
                        return "{name}: {mtype}"
                end
        end

        # Returns a new parameter with the `mtype` resolved.
        # See `MType::resolve_for` for details.
        fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MParameter
        do
                if not self.mtype.need_anchor then return self
                var newtype = self.mtype.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
                var res = new MParameter(self.name, newtype, self.is_vararg)
                return res
        end

        redef fun model do return mtype.model
end

# A service (global property) that generalize method, attribute, etc.
#
# `MProperty` are global to the model; it means that a `MProperty` is not bound
# to a specific `MModule` nor a specific `MClass`.
#
# A MProperty gather definitions (see `mpropdefs`) ; one for the introduction
# and the other in subclasses and in refinements.
#
# A `MProperty` is used to denotes services in polymorphic way (ie. independent
# of any dynamic type).
# For instance, a call site "x.foo" is associated to a `MProperty`.
abstract class MProperty
        super MEntity

        # The associated MPropDef subclass.
        # The two specialization hierarchy are symmetric.
        type MPROPDEF: MPropDef

        # The classdef that introduce the property
        # While a property is not bound to a specific module, or class,
        # the introducing mclassdef is used for naming and visibility
        var intro_mclassdef: MClassDef

        # The (short) name of the property
        redef var name: String

        # The canonical name of the property.
        #
        # It is the short-`name` prefixed by the short-name of the class and the full-name of the module.
        # Example: "my_project::my_module::MyClass::my_method"
        redef var full_name is lazy do
                return "{intro_mclassdef.mmodule.namespace_for(visibility)}::{intro_mclassdef.mclass.name}::{name}"
        end

        redef var c_name is lazy do
                # FIXME use `namespace_for`
                return "{intro_mclassdef.mmodule.c_name}__{intro_mclassdef.mclass.name.to_cmangle}__{name.to_cmangle}"
        end

        # The visibility of the property
        var visibility: MVisibility

        # Is the property usable as an initializer?
        var is_autoinit = false is writable

        init
        do
                intro_mclassdef.intro_mproperties.add(self)
                var model = intro_mclassdef.mmodule.model
                model.mproperties_by_name.add_one(name, self)
                model.mproperties.add(self)
        end

        # All definitions of the property.
        # The first is the introduction,
        # The other are redefinitions (in refinements and in subclasses)
        var mpropdefs = new Array[MPROPDEF]

        # The definition that introduces the property.
        #
        # Warning: such a definition may not exist in the early life of the object.
        # In this case, the method will abort.
        var intro: MPROPDEF is noinit

        redef fun model do return intro.model

        # Alias for `name`
        redef fun to_s do return name

        # Return the most specific property definitions defined or inherited by a type.
        # The selection knows that refinement is stronger than specialization;
        # however, in case of conflict more than one property are returned.
        # If mtype does not know mproperty then an empty array is returned.
        #
        # If you want the really most specific property, then look at `lookup_first_definition`
        #
        # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
        # ENSURE: `not mtype.has_mproperty(mmodule, self) == result.is_empty`
        fun lookup_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                assert not mtype.need_anchor
                mtype = mtype.as_notnullable

                var cache = self.lookup_definitions_cache[mmodule, mtype]
                if cache != null then return cache

                #print "select prop {mproperty} for {mtype} in {self}"
                # First, select all candidates
                var candidates = new Array[MPROPDEF]
                for mpropdef in self.mpropdefs do
                        # If the definition is not imported by the module, then skip
                        if not mmodule.in_importation <= mpropdef.mclassdef.mmodule then continue
                        # If the definition is not inherited by the type, then skip
                        if not mtype.is_subtype(mmodule, null, mpropdef.mclassdef.bound_mtype) then continue
                        # Else, we keep it
                        candidates.add(mpropdef)
                end
                # Fast track for only one candidate
                if candidates.length <= 1 then
                        self.lookup_definitions_cache[mmodule, mtype] = candidates
                        return candidates
                end

                # Second, filter the most specific ones
                return select_most_specific(mmodule, candidates)
        end

        private var lookup_definitions_cache = new HashMap2[MModule, MType, Array[MPROPDEF]]

        # Return the most specific property definitions inherited by a type.
        # The selection knows that refinement is stronger than specialization;
        # however, in case of conflict more than one property are returned.
        # If mtype does not know mproperty then an empty array is returned.
        #
        # If you want the really most specific property, then look at `lookup_next_definition`
        #
        # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
        # ENSURE: `not mtype.has_mproperty(mmodule, self) implies result.is_empty`
        fun lookup_super_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                assert not mtype.need_anchor
                mtype = mtype.as_notnullable

                # First, select all candidates
                var candidates = new Array[MPROPDEF]
                for mpropdef in self.mpropdefs do
                        # If the definition is not imported by the module, then skip
                        if not mmodule.in_importation <= mpropdef.mclassdef.mmodule then continue
                        # If the definition is not inherited by the type, then skip
                        if not mtype.is_subtype(mmodule, null, mpropdef.mclassdef.bound_mtype) then continue
                        # If the definition is defined by the type, then skip (we want the super, so e skip the current)
                        if mtype == mpropdef.mclassdef.bound_mtype and mmodule == mpropdef.mclassdef.mmodule then continue
                        # Else, we keep it
                        candidates.add(mpropdef)
                end
                # Fast track for only one candidate
                if candidates.length <= 1 then return candidates

                # Second, filter the most specific ones
                return select_most_specific(mmodule, candidates)
        end

        # Return an array containing olny the most specific property definitions
        # This is an helper function for `lookup_definitions` and `lookup_super_definitions`
        private fun select_most_specific(mmodule: MModule, candidates: Array[MPROPDEF]): Array[MPROPDEF]
        do
                var res = new Array[MPROPDEF]
                for pd1 in candidates do
                        var cd1 = pd1.mclassdef
                        var c1 = cd1.mclass
                        var keep = true
                        for pd2 in candidates do
                                if pd2 == pd1 then continue # do not compare with self!
                                var cd2 = pd2.mclassdef
                                var c2 = cd2.mclass
                                if c2.mclass_type == c1.mclass_type then
                                        if cd2.mmodule.in_importation < cd1.mmodule then
                                                # cd2 refines cd1; therefore we skip pd1
                                                keep = false
                                                break
                                        end
                                else if cd2.bound_mtype.is_subtype(mmodule, null, cd1.bound_mtype) and cd2.bound_mtype != cd1.bound_mtype then
                                        # cd2 < cd1; therefore we skip pd1
                                        keep = false
                                        break
                                end
                        end
                        if keep then
                                res.add(pd1)
                        end
                end
                if res.is_empty then
                        print "All lost! {candidates.join(", ")}"
                        # FIXME: should be abort!
                end
                return res
        end

        # Return the most specific definition in the linearization of `mtype`.
        #
        # If you want to know the next properties in the linearization,
        # look at `MPropDef::lookup_next_definition`.
        #
        # FIXME: the linearization is still unspecified
        #
        # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
        # REQUIRE: `mtype.has_mproperty(mmodule, self)`
        fun lookup_first_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                return lookup_all_definitions(mmodule, mtype).first
        end

        # Return all definitions in a linearization order
        # Most specific first, most general last
        #
        # REQUIRE: `not mtype.need_anchor` to simplify the API (no `anchor` parameter)
        # REQUIRE: `mtype.has_mproperty(mmodule, self)`
        fun lookup_all_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                mtype = mtype.as_notnullable

                var cache = self.lookup_all_definitions_cache[mmodule, mtype]
                if cache != null then return cache

                assert not mtype.need_anchor
                assert mtype.has_mproperty(mmodule, self)

                #print "select prop {mproperty} for {mtype} in {self}"
                # First, select all candidates
                var candidates = new Array[MPROPDEF]
                for mpropdef in self.mpropdefs do
                        # If the definition is not imported by the module, then skip
                        if not mmodule.in_importation <= mpropdef.mclassdef.mmodule then continue
                        # If the definition is not inherited by the type, then skip
                        if not mtype.is_subtype(mmodule, null, mpropdef.mclassdef.bound_mtype) then continue
                        # Else, we keep it
                        candidates.add(mpropdef)
                end
                # Fast track for only one candidate
                if candidates.length <= 1 then
                        self.lookup_all_definitions_cache[mmodule, mtype] = candidates
                        return candidates
                end

                mmodule.linearize_mpropdefs(candidates)
                candidates = candidates.reversed
                self.lookup_all_definitions_cache[mmodule, mtype] = candidates
                return candidates
        end

        private var lookup_all_definitions_cache = new HashMap2[MModule, MType, Array[MPROPDEF]]
end

# A global method
class MMethod
        super MProperty

        redef type MPROPDEF: MMethodDef

        # Is the property defined at the top_level of the module?
        # Currently such a property are stored in `Object`
        var is_toplevel: Bool = false is writable

        # Is the property a constructor?
        # Warning, this property can be inherited by subclasses with or without being a constructor
        # therefore, you should use `is_init_for` the verify if the property is a legal constructor for a given class
        var is_init: Bool = false is writable

        # The constructor is a (the) root init with empty signature but a set of initializers
        var is_root_init: Bool = false is writable

        # Is the property a 'new' constructor?
        var is_new: Bool = false is writable

        # Is the property a legal constructor for a given class?
        # As usual, visibility is not considered.
        # FIXME not implemented
        fun is_init_for(mclass: MClass): Bool
        do
                return self.is_init
        end
end

# A global attribute
class MAttribute
        super MProperty

        redef type MPROPDEF: MAttributeDef

end

# A global virtual type
class MVirtualTypeProp
        super MProperty

        redef type MPROPDEF: MVirtualTypeDef

        # The formal type associated to the virtual type property
        var mvirtualtype = new MVirtualType(self)
end

# A definition of a property (local property)
#
# Unlike `MProperty`, a `MPropDef` is a local definition that belong to a
# specific class definition (which belong to a specific module)
abstract class MPropDef
        super MEntity

        # The associated `MProperty` subclass.
        # the two specialization hierarchy are symmetric
        type MPROPERTY: MProperty

        # Self class
        type MPROPDEF: MPropDef

        # The class definition where the property definition is
        var mclassdef: MClassDef

        # The associated global property
        var mproperty: MPROPERTY

        # The origin of the definition
        var location: Location

        init
        do
                mclassdef.mpropdefs.add(self)
                mproperty.mpropdefs.add(self)
                if mproperty.intro_mclassdef == mclassdef then
                        assert not isset mproperty._intro
                        mproperty.intro = self
                end
                self.to_s = "{mclassdef}#{mproperty}"
        end

        # Actually the name of the `mproperty`
        redef fun name do return mproperty.name

        # The full-name of mpropdefs combine the information about the `classdef` and the `mproperty`.
        #
        # Therefore the combination of identifiers is awful,
        # the worst case being
        #
        #  * a property "p::m::A::x"
        #  * redefined in a refinement of a class "q::n::B"
        #  * in a module "r::o"
        #  * so "r::o#q::n::B#p::m::A::x"
        #
        # Fortunately, the full-name is simplified when entities are repeated.
        # For the previous case, the simplest form is "p#A#x".
        redef var full_name is lazy do
                var res = new FlatBuffer

                # The first part is the mclassdef. Worst case is "r::o#q::n::B"
                res.append mclassdef.full_name

                res.append "#"

                if mclassdef.mclass == mproperty.intro_mclassdef.mclass then
                        # intro are unambiguous in a class
                        res.append name
                else
                        # Just try to simplify each part
                        if mclassdef.mmodule.mproject != mproperty.intro_mclassdef.mmodule.mproject then
                                # precise "p::m" only if "p" != "r"
                                res.append mproperty.intro_mclassdef.mmodule.full_name
                                res.append "::"
                        else if mproperty.visibility <= private_visibility then
                                # Same project ("p"=="q"), but private visibility,
                                # does the module part ("::m") need to be displayed
                                if mclassdef.mmodule.namespace_for(mclassdef.mclass.visibility) != mproperty.intro_mclassdef.mmodule.mproject then
                                        res.append "::"
                                        res.append mproperty.intro_mclassdef.mmodule.name
                                        res.append "::"
                                end
                        end
                        if mclassdef.mclass != mproperty.intro_mclassdef.mclass then
                                # precise "B" only if not the same class than "A"
                                res.append mproperty.intro_mclassdef.name
                                res.append "::"
                        end
                        # Always use the property name "x"
                        res.append mproperty.name
                end
                return res.to_s
        end

        redef var c_name is lazy do
                var res = new FlatBuffer
                res.append mclassdef.c_name
                res.append "___"
                if mclassdef.mclass == mproperty.intro_mclassdef.mclass then
                        res.append name.to_cmangle
                else
                        if mclassdef.mmodule != mproperty.intro_mclassdef.mmodule then
                                res.append mproperty.intro_mclassdef.mmodule.c_name
                                res.append "__"
                        end
                        if mclassdef.mclass != mproperty.intro_mclassdef.mclass then
                                res.append mproperty.intro_mclassdef.name.to_cmangle
                                res.append "__"
                        end
                        res.append mproperty.name.to_cmangle
                end
                return res.to_s
        end

        redef fun model do return mclassdef.model

        # Internal name combining the module, the class and the property
        # Example: "mymodule#MyClass#mymethod"
        redef var to_s: String is noinit

        # Is self the definition that introduce the property?
        fun is_intro: Bool do return mproperty.intro == self

        # Return the next definition in linearization of `mtype`.
        #
        # This method is used to determine what method is called by a super.
        #
        # REQUIRE: `not mtype.need_anchor`
        fun lookup_next_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                assert not mtype.need_anchor

                var mpropdefs = self.mproperty.lookup_all_definitions(mmodule, mtype)
                var i = mpropdefs.iterator
                while i.is_ok and i.item != self do i.next
                assert has_property: i.is_ok
                i.next
                assert has_next_property: i.is_ok
                return i.item
        end
end

# A local definition of a method
class MMethodDef
        super MPropDef

        redef type MPROPERTY: MMethod
        redef type MPROPDEF: MMethodDef

        # The signature attached to the property definition
        var msignature: nullable MSignature = null is writable

        # The signature attached to the `new` call on a root-init
        # This is a concatenation of the signatures of the initializers
        #
        # REQUIRE `mproperty.is_root_init == (new_msignature != null)`
        var new_msignature: nullable MSignature = null is writable

        # List of initialisers to call in root-inits
        #
        # They could be setters or attributes
        #
        # REQUIRE `mproperty.is_root_init == (new_msignature != null)`
        var initializers = new Array[MProperty]

        # Is the method definition abstract?
        var is_abstract: Bool = false is writable

        # Is the method definition intern?
        var is_intern = false is writable

        # Is the method definition extern?
        var is_extern = false is writable

        # An optional constant value returned in functions.
        #
        # Only some specific primitife value are accepted by engines.
        # Is used when there is no better implementation available.
        #
        # Currently used only for the implementation of the `--define`
        # command-line option.
        # SEE: module `mixin`.
        var constant_value: nullable Object = null is writable
end

# A local definition of an attribute
class MAttributeDef
        super MPropDef

        redef type MPROPERTY: MAttribute
        redef type MPROPDEF: MAttributeDef

        # The static type of the attribute
        var static_mtype: nullable MType = null is writable
end

# A local definition of a virtual type
class MVirtualTypeDef
        super MPropDef

        redef type MPROPERTY: MVirtualTypeProp
        redef type MPROPDEF: MVirtualTypeDef

        # The bound of the virtual type
        var bound: nullable MType = null is writable

        # Is the bound fixed?
        var is_fixed = false is writable
end

# A kind of class.
#
#  * `abstract_kind`
#  * `concrete_kind`
#  * `interface_kind`
#  * `enum_kind`
#  * `extern_kind`
#
# Note this class is basically an enum.
# FIXME: use a real enum once user-defined enums are available
class MClassKind
        redef var to_s: String

        # Is a constructor required?
        var need_init: Bool

        # TODO: private init because enumeration.

        # Can a class of kind `self` specializes a class of kine `other`?
        fun can_specialize(other: MClassKind): Bool
        do
                if other == interface_kind then return true # everybody can specialize interfaces
                if self == interface_kind or self == enum_kind then
                        # no other case for interfaces
                        return false
                else if self == extern_kind then
                        # only compatible with themselves
                        return self == other
                else if other == enum_kind or other == extern_kind then
                        # abstract_kind and concrete_kind are incompatible
                        return false
                end
                # remain only abstract_kind and concrete_kind
                return true
        end
end

# The class kind `abstract`
fun abstract_kind: MClassKind do return once new MClassKind("abstract class", true)
# The class kind `concrete`
fun concrete_kind: MClassKind do return once new MClassKind("class", true)
# The class kind `interface`
fun interface_kind: MClassKind do return once new MClassKind("interface", false)
# The class kind `enum`
fun enum_kind: MClassKind do return once new MClassKind("enum", false)
# The class kind `extern`
fun extern_kind: MClassKind do return once new MClassKind("extern class", false)