stdlib/strings: Moved Buffer to FlatBuffer, Buffer is now abstract.
[nit.git] / src / model / model.nit
index 69ca872..6102df5 100644 (file)
 #
 # It also provide an API to build and query models.
 #
-# All model classes starts with the M letter (MModule, MClass, etc.)
+# All model classes starts with the M letter (`MModule`, `MClass`, etc.)
 #
 # TODO: better doc
 #
-# TODO: liearization, closures, extern stuff
+# TODO: liearization, extern stuff
 # FIXME: better handling of the types
 module model
 
 import poset
 import location
-import model_base
+import mmodule
+private import more_collections
 
 redef class Model
        # All known classes
@@ -69,7 +70,7 @@ redef class Model
        # Collections of classes grouped by their short name
        private var mclasses_by_name: MultiHashMap[String, MClass] = new MultiHashMap[String, MClass]
 
-       # Return all class named `name'.
+       # Return all class named `name`.
        #
        # If such a class does not exist, null is returned
        # (instead of an empty array)
@@ -87,7 +88,7 @@ redef class Model
        # Collections of properties grouped by their short name
        private var mproperties_by_name: MultiHashMap[String, MProperty] = new MultiHashMap[String, MProperty]
 
-       # Return all properties named `name'.
+       # Return all properties named `name`.
        #
        # If such a property does not exist, null is returned
        # (instead of an empty array)
@@ -114,7 +115,7 @@ redef class MModule
        # (introduction and refinement)
        var mclassdefs: Array[MClassDef] = new Array[MClassDef]
 
-       # Does the current module has a given class `mclass'?
+       # 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
@@ -139,6 +140,7 @@ redef class MModule
                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
@@ -148,17 +150,140 @@ redef class MModule
                return res
        end
 
+       # Sort a given array of classes using the linerarization 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 linerarization 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 linerarization 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 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
+
+       # 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, 0, enum_kind, public_visibility)
+                               var cladef = new MClassDef(self, c.mclass_type, new Location(null, 0,0,0,0), new Array[String])
+                               return c
+                       end
+                       print("Fatal Error: no primitive class {name}")
+                       exit(1)
+               end
+               assert cla.length == 1 else print cla.join(", ")
+               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 AbstractSorter[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 AbstractSorter[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
+# `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.
-# However, because a MClass is global, it does not really have properties nor
+# single `MClass` object always denote the same class.
+# However, because a `MClass` is global, it does not really have properties nor
 # belong to a hierarchy since the property and the
 # hierarchy of a class depends of a module.
 class MClass
@@ -172,7 +297,7 @@ class MClass
        var name: String
 
        # The canonical name of the class
-       # Example: "owner::module::MyClass"
+       # Example: `"owner::module::MyClass"`
        fun full_name: String
        do
                return "{self.intro_mmodule.full_name}::{name}"
@@ -220,40 +345,49 @@ class MClass
        # All class definitions (introduction and refinements)
        var mclassdefs: Array[MClassDef] = new Array[MClassDef]
 
-       # Alias for `name'
+       # Alias for `name`
        redef fun to_s do return self.name
 
        # The definition that introduced the class
-       # Warning: the introduction is the first `MClassDef' object associated
+       # Warning: the introduction is the first `MClassDef` object associated
        # to self.  If self is just created without having any associated
        # definition, this method will abort
-       private fun intro: MClassDef
+       fun intro: MClassDef
        do
                assert has_a_first_definition: not mclassdefs.is_empty
                return mclassdefs.first
        end
 
+       # 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
+       # 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 mtype is Array[E].
-       # If you want `Array[Object]' the see `MClassDef::bound_mtype'
+       # 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'.
+       # To get other types based on a generic class, see `get_mtype`.
        #
-       # ENSURE: mclass_type.mclass == self
+       # ENSURE: `mclass_type.mclass == self`
        var mclass_type: MClassType
 
        # Return a generic type based on the class
-       # Is the class is not generic, then the result is `mclass_type'
+       # Is the class is not generic, then the result is `mclass_type`
        #
-       # REQUIRE: type_arguments.length == self.arity
+       # REQUIRE: `mtype_arguments.length == self.arity`
        fun get_mtype(mtype_arguments: Array[MType]): MClassType
        do
                assert mtype_arguments.length == self.arity
@@ -274,26 +408,26 @@ 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 `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 module
 class MClassDef
        # The module where the definition is
        var mmodule: MModule
 
-       # The associated MClass
+       # The associated `MClass`
        var mclass: MClass
 
        # The bounded type associated to the mclassdef
        #
-       # For a non-generic class, `bound_mtype' and `mclass.mclass_type'
+       # 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'
+       # If you want Array[E], then see `mclass.mclass_type`
        #
-       # ENSURE: bound_mtype.mclass = self.mclass
+       # ENSURE: `bound_mtype.mclass == self.mclass`
        var bound_mtype: MClassType
 
        # Name of each formal generic parameter (in order of declaration)
@@ -304,7 +438,7 @@ class MClassDef
 
        # Internal name combining the module and the class
        # Example: "mymodule#MyClass"
-       redef fun to_s do return "{mmodule}#{mclass}"
+       redef var to_s: String
 
        init(mmodule: MModule, bound_mtype: MClassType, location: Location, parameter_names: Array[String])
        do
@@ -316,21 +450,22 @@ class MClassDef
                mmodule.mclassdefs.add(self)
                mclass.mclassdefs.add(self)
                self.parameter_names = parameter_names
+               self.to_s = "{mmodule}#{mclass}"
        end
 
        # All declared super-types
        # FIXME: quite ugly but not better idea yet
        var supertypes: Array[MClassType] = new Array[MClassType]
 
-       # Register the super-types for the class (ie "super SomeType")
-       # This function can only invoked once by class
+       # 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 res = model.mclassdef_hierarchy.add_node(self)
-               self.in_hierarchy = res
                var mtype = self.bound_mtype
 
                for supertype in supertypes do
@@ -344,12 +479,29 @@ class MClassDef
                        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'
+       # The view of the class definition in `mclassdef_hierarchy`
        var in_hierarchy: nullable POSetElement[MClassDef] = null
 
        # Is the definition the one that introduced `mclass`?
@@ -364,12 +516,12 @@ end
 
 # A global static type
 #
-# MType are global to the model; it means that a MType is not bound to a
+# 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.
+# since a single `MType` object always denote the same type.
 #
-# However, because a MType is global, it does not really have properties
+# 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
@@ -381,67 +533,101 @@ end
 # 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.
+# 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)
-#
-# FIXME: Add a 'is_valid_anchor' to improve imputability.
-# Currently, anchors are used "as it" without check thus if the caller gives a
-# bad anchor, then the method will likely crash (abort) in a bad case
-#
-# FIXME: maybe allways add an anchor with a nullable type (as in is_subtype)
 abstract class MType
-       # Return true if `self' is an subtype of `sup'.
+
+       # The model of the type
+       fun model: Model is abstract
+
+       # 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 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 types
+
+               # First, resolve the formal types to a common version in the receiver
+               # The trick here is that fixed formal type will be associed to the bound
+               # And unfixed formal types will be associed to a canonical formal type.
                if sub isa MParameterType or sub isa MVirtualType then
                        assert anchor != null
-                       sub = sub.resolve_for(anchor, anchor, mmodule, false)
+                       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, anchor, mmodule, false)
+                       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.
 
-               if sup isa MParameterType or sup isa MVirtualType or sup isa MNullType then
+               # 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)
-               end
-               if sup isa MNullableType then
-                       if sub isa MNullType then
-                               return true
-                       else if sub isa MNullableType then
-                               return sub.mtype.is_subtype(mmodule, anchor, sup.mtype)
-                       else if sub isa MClassType then
-                               return sub.is_subtype(mmodule, anchor, sup.mtype)
-                       else
-                               abort
+
+                       # 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 sup isa MClassType # It is the only remaining type
-               if sub isa MNullableType or sub isa MNullType then
+               assert sub isa MClassType # It is the only remaining type
+
+               if sup isa MNullType then
+                       # `sup` accepts only null
                        return false
                end
 
-               assert sub isa MClassType # It is the only remaining type
+               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)
@@ -449,7 +635,6 @@ abstract class MType
                if not sup isa MGenericType then return true
                var sub2 = sub.supertype_to(mmodule, anchor, sup.mclass)
                assert sub2.mclass == sup.mclass
-               assert sub2 isa MGenericType
                for i in [0..sup.mclass.arity[ do
                        var sub_arg = sub2.arguments[i]
                        var sup_arg = sup.arguments[i]
@@ -471,34 +656,38 @@ abstract class MType
        # 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[C]
+       #       super G[B]
        #       redef type U: Y
        #     end
-       # Map[T,U]  anchor_to  H  #->  Map[C,Y]
+       # Map[T,U]  anchor_to  H  #->  Map[B,Y]
        #
        # Explanation of the example:
-       # In H, T is set to C, because "H super G[C]", and U is bound to Y,
+       # 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[C, Y]
+       # Map[B, Y]
        #
-       # ENSURE: not self.need_anchor implies return == self
-       # ENSURE: not return.need_anchor
+       # 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, anchor, mmodule, true)
+               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'.
+       # 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.
@@ -506,17 +695,24 @@ abstract class MType
        # In Nit, for each super-class of a type, there is a equivalent super-type.
        #
        # Example:
-       #     class G[T, U]
-       #     class H[V] super G[V, Bool]
+       #     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'
-       # ENSURE: return.mclass = mclass
-       fun supertype_to(mmodule: MModule, anchor: MClassType, super_mclass: MClass): MClassType
+       # 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 = self.anchor_to(mmodule, anchor)
+               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
@@ -527,51 +723,102 @@ abstract class MType
                abort
        end
 
-       # Replace formals generic types in self with resolved values in `mtype'
-       # If `cleanup_virtual' is true, then virtual types are also replaced
+       # 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.
+       # This function returns self if `need_anchor` is false.
        #
-       # Example:
-       #     class G[E]
-       #     class H[F] super G[F]
-       # Array[E]  resolve_for  H[Int]  #->  Array[Int]
+       # ## 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
+       #  * 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_type', we do not want a full resolution of
+       # Because, unlike `anchor_to`, we do not want a full resolution of
        # a type but only an adapted version of it.
        #
-       # Example:
-        #     class A[E]
-       #         foo(e:E):E
+       # ## 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`)
+       #
        # TODO: Explain the cleanup_virtual
        #
-       # FIXME: the parameter `cleanup_virtual' is just a bad idea, but having
+       # FIXME: the parameter `cleanup_virtual` is just a bad idea, but having
        # two function instead of one seems also to be a bad idea.
        #
-       # ENSURE: not self.need_anchor implies return == self
-       fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract
+       # 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
+
+       # 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
-       #
-       # FIXME: DO NOT WORK YET
        fun as_nullable: MType
        do
                var res = self.as_nullable_cache
@@ -583,6 +830,33 @@ abstract class MType
 
        private var as_nullable_cache: nullable MType = null
 
+
+       # The deph 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
@@ -590,26 +864,26 @@ abstract class MType
        #
        # This function is used mainly internally.
        #
-       # REQUIRE: not self.need_anchor
+       # 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
+       # 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
+       # 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
+       # REQUIRE: `not self.need_anchor`
        fun has_mproperty(mmodule: MModule, mproperty: MProperty): Bool
        do
                assert not self.need_anchor
@@ -619,18 +893,24 @@ end
 
 # A type based on a class.
 #
-# MClassType have properties (see `has_property').
+# `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
+
        private init(mclass: MClass)
        do
                self.mclass = mclass
        end
 
+       # The formal arguments of the type
+       # ENSURE: `result.length == self.mclass.arity`
+       var arguments: Array[MType] = new Array[MType]
+
        redef fun to_s do return mclass.to_s
 
        redef fun need_anchor do return false
@@ -640,36 +920,41 @@ class MClassType
                return super.as(MClassType)
        end
 
-       redef fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MClassType do return self
+       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
-               if not collect_mclassdefs_cache.has_key(mmodule) then
+               var cache = self.collect_mclassdefs_cache
+               if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
-               return collect_mclassdefs_cache[mmodule]
+               return cache[mmodule]
        end
 
        redef fun collect_mclasses(mmodule)
        do
                assert not self.need_anchor
-               if not collect_mclasses_cache.has_key(mmodule) then
+               var cache = self.collect_mclasses_cache
+               if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
-               return collect_mclasses_cache[mmodule]
+               return cache[mmodule]
        end
 
        redef fun collect_mtypes(mmodule)
        do
                assert not self.need_anchor
-               if not collect_mtypes_cache.has_key(mmodule) then
+               var cache = self.collect_mtypes_cache
+               if not cache.has_key(mmodule) then
                        self.collect_things(mmodule)
                end
-               return collect_mtypes_cache[mmodule]
+               return cache[mmodule]
        end
 
-       # common implementation for `collect_mclassdefs', `collect_mclasses', and `collect_mtypes'.
+       # common implementation for `collect_mclassdefs`, `collect_mclasses`, and `collect_mtypes`.
        private fun collect_things(mmodule: MModule)
        do
                var res = new HashSet[MClassDef]
@@ -723,30 +1008,55 @@ class MGenericType
                                break
                        end
                end
-       end
 
-       # The formal arguments of the type
-       # ENSURE: return.length == self.mclass.arity
-       var arguments: Array[MType]
+               self.to_s = "{mclass}[{arguments.join(", ")}]"
+       end
 
        # Recursively print the type of the arguments within brackets.
-       # Example: "Map[String,List[Int]]"
-       redef fun to_s
-       do
-               return "{mclass}[{arguments.join(",")}]"
-       end
+       # Example: `"Map[String, List[Int]]"`
+       redef var to_s: String
 
        redef var need_anchor: Bool
 
        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.
@@ -757,6 +1067,8 @@ class MVirtualType
        # 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
+
        # Lookup the bound for a given resolved_receiver
        # The result may be a other virtual type (or a parameter type)
        #
@@ -784,18 +1096,49 @@ class MVirtualType
 
        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_reciever = mtype.resolve_for(anchor, anchor, mmodule, true)
+               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, true)
+               var res = verbatim_bound.resolve_for(mtype, anchor, mmodule, cleanup_virtual)
                #print "{class_name}: {self}/{mtype}/{anchor} -> {self}/{resolved_reciever}/{anchor} -> {verbatim_bound}/{mtype}/{anchor} -> {res}"
-               return 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 reciever 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
+               # It the resolved type isa intern class, then there is no possible valid redefinition is any potentiel subclass. self is just fixed. so simply return the resolution
+               if res isa MClassType and res.mclass.kind == enum_kind then return res
+               # TODO: Add 'fixed' virtual type in the specification.
+               # 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
@@ -824,21 +1167,23 @@ 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'.
+# 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).
-# TODO: Add a 'name_for' to get better messages.
+# Therefore parameter only have an internal name (see `to_s` for details).
+# TODO: Add a `name_for` to get better messages.
 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?
+       # FIXME: is `position` a better name?
        var rank: Int
 
        # Internal name of the parameter type
@@ -859,7 +1204,6 @@ class MParameterType
                        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?
-                               assert t isa MGenericType
                                var res = t.arguments[self.rank]
                                return res
                        end
@@ -869,6 +1213,7 @@ class MParameterType
 
        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
@@ -879,25 +1224,33 @@ class MParameterType
                # 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 happend here is far from clear. Thus this part must be validated and clarified
-               var resolved_receiver = mtype.resolve_for(anchor.mclass.mclass_type, anchor, mmodule, true)
+               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.as(MGenericType).arguments[resolved_receiver.rank]
+                       resolved_receiver = anchor.arguments[resolved_receiver.rank]
                        if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
                end
-               assert resolved_receiver isa MClassType else print "{class_name}: {self}/{mtype}/{anchor}? {resolved_receiver}"
+               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
-                       assert resolved_receiver isa MGenericType
                        var res = resolved_receiver.arguments[self.rank]
                        #print "{class_name}: {self}/{mtype}/{anchor} -> direct {res}"
                        return res
                end
 
-               resolved_receiver = resolved_receiver.resolve_for(anchor, anchor, mmodule, false)
+               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
@@ -908,6 +1261,15 @@ class MParameterType
                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
+
        init(mclass: MClass, rank: Int)
        do
                self.mclass = mclass
@@ -916,19 +1278,21 @@ class MParameterType
 end
 
 # A type prefixed with "nullable"
-# FIXME Stub implementation
 class MNullableType
        super MType
 
        # The base type of the nullable type
        var mtype: MType
 
+       redef fun model do return self.mtype.model
+
        init(mtype: MType)
        do
                self.mtype = mtype
+               self.to_s = "nullable {mtype}"
        end
 
-       redef fun to_s do return "nullable {mtype}"
+       redef var to_s: String
 
        redef fun need_anchor do return mtype.need_anchor
        redef fun as_nullable do return self
@@ -938,6 +1302,15 @@ class MNullableType
                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
@@ -959,10 +1332,10 @@ end
 
 # The type of the only value null
 #
-# The is only one null type per model, see `MModel::null_type'.
+# The is only one null type per model, see `MModel::null_type`.
 class MNullType
        super MType
-       var model: Model
+       redef var model: Model
        protected init(model: Model)
        do
                self.model = model
@@ -971,6 +1344,7 @@ class MNullType
        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]
 
@@ -979,52 +1353,75 @@ class MNullType
        redef fun collect_mtypes(mmodule) do return new HashSet[MClassType]
 end
 
-# A signature of a method (or a closure)
+# A signature of a method
 class MSignature
        super MType
 
-       # The names of each parameter (in order)
-       var parameter_names: Array[String]
-
-       # The types of each parameter (in order)
-       var parameter_mtypes: Array[MType]
+       # The each parameter (in order)
+       var mparameters: Array[MParameter]
 
        # The return type (null for a procedure)
        var return_mtype: nullable MType
 
-       # All closures
-       var mclosures: Array[MClosureDecl] = new Array[MClosureDecl]
+       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
 
-       init(parameter_names: Array[String], parameter_mtypes: Array[MType], return_mtype: nullable MType, vararg_rank: Int)
+       redef fun length
        do
-               self.parameter_names = parameter_names
-               self.parameter_mtypes = parameter_mtypes
+               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(mparameters: Array[MParameter], return_mtype: nullable MType)
+       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.mparameters = mparameters
                self.return_mtype = return_mtype
                self.vararg_rank = vararg_rank
        end
 
-       # Is there closures in the signature?
-       fun with_mclosure: Bool do return not self.mclosures.is_empty
-
-       # The rank of the ellipsis (...) for vararg (starting from 0).
+       # 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
 
        # The number or parameters
-       fun arity: Int do return parameter_mtypes.length
+       fun arity: Int do return mparameters.length
 
        redef fun to_s
        do
-               var b = new Buffer
-               if not parameter_names.is_empty then
+               var b = new FlatBuffer
+               if not mparameters.is_empty then
                        b.append("(")
-                       for i in [0..parameter_names.length[ do
+                       for i in [0..mparameters.length[ do
+                               var mparameter = mparameters[i]
                                if i > 0 then b.append(", ")
-                               b.append(parameter_names[i])
+                               b.append(mparameter.name)
                                b.append(": ")
-                               b.append(parameter_mtypes[i].to_s)
-                               if i == self.vararg_rank then
+                               b.append(mparameter.mtype.to_s)
+                               if mparameter.is_vararg then
                                        b.append("...")
                                end
                        end
@@ -1038,45 +1435,52 @@ class MSignature
                return b.to_s
        end
 
-       redef fun resolve_for(mtype: MType, anchor: MClassType, mmodule: MModule, cleanup_virtual: Bool): MSignature
+       redef fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MSignature
        do
-               var params = new Array[MType]
-               for t in self.parameter_mtypes do
-                       params.add(t.resolve_for(mtype, anchor, mmodule, cleanup_virtual))
+               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(self.parameter_names, params, ret, self.vararg_rank)
+               var res = new MSignature(params, ret)
                return res
        end
 end
 
-# A closure declaration is a signature
-# FIXME Stub implementation
-class MClosureDecl
-       # Is the closure optionnal
-       var is_optional: Bool
-       # Has the closure to not continue
-       var is_break: Bool
-       # The name of the closure (exluding the !)
+# A parameter in a signature
+class MParameter
+       # The name of the parameter
        var name: String
-       # The signature of the closure
-       var msignature: MSignature
+
+       # The static type of the parameter
+       var mtype: MType
+
+       # Is the parameter a vararg?
+       var is_vararg: Bool
+
+       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
 end
 
 # A service (global property) that generalize method, attribute, etc.
 #
-# MProperty are global to the model; it means that a MProperty is not bound
+# `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
+# 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
+# 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.
+# For instance, a call site "x.foo" is associated to a `MProperty`.
 abstract class MProperty
        # The associated MPropDef subclass.
        # The two specialization hierarchy are symmetric.
@@ -1117,12 +1521,12 @@ abstract class MProperty
        var mpropdefs: Array[MPROPDEF] = new Array[MPROPDEF]
 
        # The definition that introduced the property
-       # Warning: the introduction is the first `MPropDef' object
+       # Warning: the introduction is the first `MPropDef` object
        # associated to self. If self is just created without having any
        # associated definition, this method will abort
        fun intro: MPROPDEF do return mpropdefs.first
 
-       # Alias for `name'
+       # Alias for `name`
        redef fun to_s do return name
 
        # Return the most specific property definitions defined or inherited by a type.
@@ -1130,7 +1534,7 @@ abstract class MProperty
        # 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_property`
+       # 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
@@ -1157,40 +1561,10 @@ abstract class MProperty
                end
 
                # Second, filter the most specific ones
-               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) 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
-               self.lookup_definitions_cache[mmodule, mtype] = res
-               return res
+               return select_most_specific(mmodule, candidates)
        end
 
-       private var lookup_definitions_cache: HashMap2[MModule, MType, Array[MPropDef]] = new HashMap2[MModule, MType, Array[MPropDef]]
+       private var lookup_definitions_cache: HashMap2[MModule, MType, Array[MPROPDEF]] = 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;
@@ -1199,14 +1573,14 @@ abstract class MProperty
        #
        # 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]
+       # FIXME: Move to `MPropDef`?
+       fun lookup_super_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                assert not mtype.need_anchor
                if mtype isa MNullableType then mtype = mtype.mtype
 
                # First, select all candidates
-               var candidates = new Array[MPropDef]
+               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
@@ -1221,7 +1595,14 @@ abstract class MProperty
                if candidates.length <= 1 then return candidates
 
                # Second, filter the most specific ones
-               var res = new Array[MPropDef]
+               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
@@ -1231,12 +1612,12 @@ abstract class MProperty
                                var cd2 = pd2.mclassdef
                                var c2 = cd2.mclass
                                if c2.mclass_type == c1.mclass_type then
-                                       if cd2.mmodule.in_importation <= cd1.mmodule 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) then
+                               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
@@ -1254,19 +1635,54 @@ abstract class MProperty
        end
 
        # Return the most specific definition in the linearization of `mtype`.
-       # If mtype does not know mproperty then null is returned.
        #
        # If you want to know the next properties in the linearization,
        # look at `MPropDef::lookup_next_definition`.
        #
-       # FIXME: NOT YET IMPLEMENTED
+       # FIXME: the linearisation is still unspecified
        #
-       # REQUIRE: not mtype.need_anchor
-       fun lookup_first_property(mmodule: MModule, mtype: MType): nullable MPROPDEF
+       # 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 linearisation order
+       # Most speficic first, most general last
+       fun lookup_all_definitions(mmodule: MModule, mtype: MType): Array[MPROPDEF]
        do
                assert not mtype.need_anchor
-               return null
+               if mtype isa MNullableType then mtype = mtype.mtype
+
+               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: HashMap2[MModule, MType, Array[MPROPDEF]] = new HashMap2[MModule, MType, Array[MPROPDEF]]
 end
 
 # A global method
@@ -1282,7 +1698,7 @@ class MMethod
 
        # 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
+       # therefore, you should use `is_init_for` the verify if the property is a legal constructor for a given class
        var is_init: Bool writable = false
 
        # The the property a 'new' contructor?
@@ -1326,11 +1742,11 @@ end
 
 # A definition of a property (local property)
 #
-# Unlike MProperty, a MPropDef is a local definition that belong to a
+# Unlike `MProperty`, a `MPropDef` is a local definition that belong to a
 # specific class definition (which belong to a specific module)
 abstract class MPropDef
 
-       # The associated MProperty subclass.
+       # The associated `MProperty` subclass.
        # the two specialization hierarchy are symmetric
        type MPROPERTY: MProperty
 
@@ -1353,30 +1769,32 @@ abstract class MPropDef
                self.location = location
                mclassdef.mpropdefs.add(self)
                mproperty.mpropdefs.add(self)
+               self.to_s = "{mclassdef}#{mproperty}"
        end
 
        # Internal name combining the module, the class and the property
        # Example: "mymodule#MyClass#mymethod"
-       redef fun to_s
-       do
-               return "{mclassdef}#{mproperty}"
-       end
+       redef var to_s: String
 
        # 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`.
-       # If there is no next method then null is returned.
        #
        # This method is used to determine what method is called by a super.
        #
-       # FIXME: NOT YET IMPLEMENTED
-       #
-       # REQUIRE: not mtype.need_anchor
-       fun lookup_next_definition(mmodule: MModule, mtype: MType): nullable MPROPDEF
+       # REQUIRE: `not mtype.need_anchor`
+       fun lookup_next_definition(mmodule: MModule, mtype: MType): MPROPDEF
        do
                assert not mtype.need_anchor
-               return null
+
+               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
 
@@ -1394,6 +1812,9 @@ class MMethodDef
 
        # The signature attached to the property definition
        var msignature: nullable MSignature writable = null
+
+       # The the method definition abstract?
+       var is_abstract: Bool writable = false
 end
 
 # A local definition of an attribute
@@ -1430,11 +1851,11 @@ end
 
 # A kind of class.
 #
-#  * abstract_kind
-#  * concrete_kind
-#  * interface_kind
-#  * enum_kind
-#  * extern_kind
+#  * `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