model: generalize MType::lookup_bound

[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
                if mclasses_by_name.has_key(name) then
                        return mclasses_by_name[name]
                else
                        return null
                end
        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
                if not mproperties_by_name.has_key(name) then
                        return null
                else
                        return mproperties_by_name[name]
                end
        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
        fun object_type: MClassType
        do
                var res = self.object_type_cache
                if res != null then return res
                res = self.get_primitive_class("Object").mclass_type
                self.object_type_cache = res
                return res
        end

        private var object_type_cache: nullable MClassType

        # 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`
        fun bool_type: MClassType
        do
                var res = self.bool_type_cache
                if res != null then return res
                res = self.get_primitive_class("Bool").mclass_type
                self.bool_type_cache = res
                return res
        end

        private var bool_type_cache: nullable MClassType

        # 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" then
                                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))
                                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
        # Example: `"owner::module::MyClass"`
        fun full_name: String
        do
                return "{self.intro_mmodule.full_name}::{name}"
        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]

        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.add(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
                for t in self.get_mtype_cache do
                        if t.arguments == mtype_arguments then
                                return t
                        end
                end
                var res = new MGenericType(self, mtype_arguments)
                self.get_mtype_cache.add res
                return res
        end

        private var get_mtype_cache = new Array[MGenericType]
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

        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
                if anchor == null then
                        assert not sub.need_anchor
                        assert not sup.need_anchor
                else
                        assert sub.can_resolve_for(anchor, null, mmodule)
                        assert sup.can_resolve_for(anchor, null, mmodule)
                end

                # First, resolve the formal types to a common version in the receiver
                # The trick here is that fixed formal type will be associated to the bound
                # And unfixed formal types will be associated to a canonical formal type.
                if sub isa MParameterType or sub isa MVirtualType then
                        assert anchor != null
                        sub = sub.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, false)
                end
                if sup isa MParameterType or sup isa MVirtualType then
                        assert anchor != null
                        sup = sup.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, false)
                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 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
                if sub isa MNullableType then
                        if not sup_accept_null then return false
                        sub = sub.mtype
                else if sub isa MNullType then
                        return sup_accept_null
                end
                # Now the case of direct null and nullable is over.

                # A unfixed formal type can only accept itself
                if sup isa MParameterType or sup isa MVirtualType then
                        return sub == sup
                end

                # If `sub` is a formal type, then it is accepted if its bound is accepted
                if sub isa MParameterType or sub isa MVirtualType then
                        assert anchor != null
                        sub = sub.anchor_to(mmodule, anchor)

                        # Manage the second layer of null/nullable
                        if sub isa MNullableType then
                                if not sup_accept_null then return false
                                sub = sub.mtype
                        else if sub isa MNullType then
                                return sup_accept_null
                        end
                end

                assert sub isa MClassType # It is the only remaining type

                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:
        #     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
        #
        #     class A[E]
        #         fun foo(e:E) is abstract
        #     end
        #     class B[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(B[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]],B[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
        # 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
        #
        #  * 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

        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 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
                assert not self.need_anchor
                var cache = self.collect_mclasses_cache
                if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
                return cache[mmodule]
        end

        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

        # Recursively print the type of the arguments within brackets.
        # Example: `"Map[String, List[Int]]"`
        redef var to_s: String is noinit

        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 virtual formal type.
class MVirtualType
        super MType

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

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

        redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        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.as(MVirtualTypeDef).bound.as(not null)
                end
                var types = new ArraySet[MType]
                for p in props do
                        types.add(p.as(MVirtualTypeDef).bound.as(not null))
                end
                if types.length == 1 then
                        return types.first
                end
                abort
        end

        # Is the virtual type fixed for a given resolved_receiver?
        fun is_fixed(mmodule: MModule, resolved_receiver: MType): Bool
        do
                assert not resolved_receiver.need_anchor
                var props = self.mproperty.lookup_definitions(mmodule, resolved_receiver)
                if props.is_empty then
                        abort
                end
                for p in props do
                        if p.as(MVirtualTypeDef).is_fixed then return true
                end
                return false
        end

        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                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_reciever
                if mtype.need_anchor then
                        assert anchor != null
                        resolved_reciever = mtype.resolve_for(anchor, null, mmodule, true)
                else
                        resolved_reciever = mtype
                end
                # Now, we can get the bound
                var verbatim_bound = lookup_bound(mmodule, resolved_reciever)
                # 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} -> {self}/{resolved_receiver}/{anchor} -> {verbatim_bound}/{mtype}/{anchor} -> {res}"

                # What to return here? There is a bunch a special cases:
                # If 'cleanup_virtual' we must return the resolved type, since we cannot return self
                if cleanup_virtual then return res
                # If the receiver is a intern class, then the virtual type cannot be redefined since there is no possible subclass. self is just fixed. so simply return the resolution
                if resolved_reciever isa MNullableType then resolved_reciever = resolved_reciever.mtype
                if resolved_reciever.as(MClassType).mclass.kind == enum_kind then return res
                # If the resolved type isa MVirtualType, it means that self was bound to it, and cannot be unbound. self is just fixed. so return the resolution.
                if res isa MVirtualType then return res
                # If we are final, just return the resolution
                if is_fixed(mmodule, resolved_reciever) then return res
                # If the resolved type isa intern class, then there is no possible valid redefinition in any potential subclass. self is just fixed. so simply return the resolution
                if res isa MClassType and res.mclass.kind == enum_kind then return res
                # TODO: What if bound to a MParameterType?
                # Note that Nullable types can always be redefined by the non nullable version, so there is no specific case on it.

                # If anything apply, then `self' cannot be resolved, so return self
                return self
        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
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 MType

        # 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 fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
                var goalclass = self.mclass
                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

        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

                # 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 prefixed with "nullable"
class MNullableType
        super MType

        # The base type of the nullable type
        var mtype: MType

        redef fun model do return self.mtype.model

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

        redef var to_s: String is noinit

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

        redef fun can_resolve_for(mtype, anchor, mmodule)
        do
                return self.mtype.can_resolve_for(mtype, anchor, mmodule)
        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

# 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 as_nullable do return self
        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

        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
        # Example: "owner::my_module::MyClass::my_method"
        fun full_name: String
        do
                return "{self.intro_mclassdef.mmodule.full_name}::{self.intro_mclassdef.mclass.name}::{name}"
        end

        # The visibility of the property
        var visibility: MVisibility

        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`
        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`
        #
        # FIXME: Move to `MPropDef`?
        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`
        # REQUIRE: `mtype.has_mproperty(mmodule, self)`
        fun lookup_first_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                assert mtype.has_mproperty(mmodule, self)
                return lookup_all_definitions(mmodule, mtype).first
        end

        # Return all definitions in a linearization order
        # Most specific first, most general last
        fun lookup_all_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                assert not mtype.need_anchor
                mtype = mtype.as_notnullable

                var cache = self.lookup_all_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_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

        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)