Merge: Subtype improvements

During the work with the covariance, some bugs with `is_subtype` where identified.

The PR tries to improve the code and fixes those bugs.
It also simplifies the code in the formal types and propose a new `lookup_fixed` method on `MType`.

Pull-Request: #926
Reviewed-by: Alexandre Terrasa <alexandre@moz-code.org>

diff --git a/src/model/model.nit b/src/model/model.nit
index c26e262..899f023 100644 (file)
--- a/src/model/model.nit
+++ b/src/model/model.nit
@@ -628,24 +628,18 @@ abstract class MType
        do
                var sub = self
                if sub == sup then return true
+
+               #print "1.is {sub} a {sup}? ===="
+
                if anchor == null then
                        assert not sub.need_anchor
                        assert not sup.need_anchor
                else
+                       # First, resolve the formal types to the simplest equivalent forms in the receiver
                        assert sub.can_resolve_for(anchor, null, mmodule)
+                       sub = sub.lookup_fixed(mmodule, anchor)
                        assert sup.can_resolve_for(anchor, null, mmodule)
-               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)
+                       sup = sup.lookup_fixed(mmodule, anchor)
                end
 
                # Does `sup` accept null or not?
@@ -669,15 +663,17 @@ abstract class MType
                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
+               while sub isa MParameterType or sub isa MVirtualType do
+                       #print "3.is {sub} a {sup}?"
+
+                       # A unfixed formal type can only accept itself
+                       if sub == sup then return true
+
                        assert anchor != null
-                       sub = sub.anchor_to(mmodule, anchor)
+                       sub = sub.lookup_bound(mmodule, anchor)
+
+                       #print "3.is {sub} a {sup}?"
 
                        # Manage the second layer of null/nullable
                        if sub isa MNullableType then
@@ -687,9 +683,15 @@ abstract class MType
                                return sup_accept_null
                        end
                end
+               #print "4.is {sub} a {sup}? <- no more resolution"
 
                assert sub isa MClassType # It is the only remaining type
 
+               # A unfixed formal type can only accept itself
+               if sup isa MParameterType or sup isa MVirtualType then
+                       return false
+               end
+
                if sup isa MNullType then
                        # `sup` accepts only null
                        return false
@@ -878,6 +880,28 @@ abstract class MType
        # ENSURE: `not self.need_anchor implies result == self`
        fun resolve_for(mtype: MType, anchor: nullable MClassType, mmodule: MModule, cleanup_virtual: Bool): MType is abstract
 
+       # Resolve formal type to its verbatim bound.
+       # If the type is not formal, just return self
+       #
+       # The result is returned exactly as declared in the "type" property (verbatim).
+       # So it could be another formal type.
+       #
+       # In case of conflict, the method aborts.
+       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType do return self
+
+       # Resolve the formal type to its simplest equivalent form.
+       #
+       # Formal types are either free or fixed.
+       # When it is fixed, it means that it is equivalent with a simpler type.
+       # When a formal type is free, it means that it is only equivalent with itself.
+       # This method return the most simple equivalent type of `self`.
+       #
+       # This method is mainly used for subtype test in order to sanely compare fixed.
+       #
+       # By default, return self.
+       # See the redefinitions for specific behavior in each kind of type.
+       fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType do return self
+
        # Can the type be resolved?
        #
        # In order to resolve open types, the formal types must make sence.
@@ -1168,86 +1192,85 @@ class MVirtualType
 
        # The property associated with the type.
        # Its the definitions of this property that determine the bound or the virtual type.
-       var mproperty: MProperty
+       var mproperty: MVirtualTypeProp
 
        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)
-       #
-       # The result is returned exactly as declared in the "type" property (verbatim).
-       #
-       # In case of conflict, the method aborts.
-       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       do
+               return lookup_single_definition(mmodule, resolved_receiver).bound.as(not null)
+       end
+
+       private fun lookup_single_definition(mmodule: MModule, resolved_receiver: MType): MVirtualTypeDef
        do
                assert not resolved_receiver.need_anchor
                var props = self.mproperty.lookup_definitions(mmodule, resolved_receiver)
                if props.is_empty then
                        abort
                else if props.length == 1 then
-                       return props.first.as(MVirtualTypeDef).bound.as(not null)
+                       return props.first
                end
                var types = new ArraySet[MType]
+               var res  = props.first
                for p in props do
-                       types.add(p.as(MVirtualTypeDef).bound.as(not null))
+                       types.add(p.bound.as(not null))
+                       if not res.is_fixed then res = p
                end
                if types.length == 1 then
-                       return types.first
+                       return res
                end
                abort
        end
 
-       # Is the virtual type fixed for a given resolved_receiver?
-       fun is_fixed(mmodule: MModule, resolved_receiver: MType): Bool
+       # A VT is fixed when:
+       # * the VT is (re-)defined with the annotation `is fixed`
+       # * the VT is (indirectly) bound to an enum class (see `enum_kind`) since there is no subtype possible
+       # * the receiver is an enum class since there is no subtype possible
+       redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
-               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
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
+
+               var prop = lookup_single_definition(mmodule, resolved_receiver)
+               var res = prop.bound.as(not null)
+
+               # Recursively lookup the fixed result
+               res = res.lookup_fixed(mmodule, resolved_receiver)
+
+               # 1. For a fixed VT, return the resolved bound
+               if prop.is_fixed then return res
+
+               # 2. For a enum boud, return the bound
+               if res isa MClassType and res.mclass.kind == enum_kind then return res
+
+               # 3. for a enum receiver return the bound
+               if resolved_receiver.mclass.kind == enum_kind then return res
+
+               return self
        end
 
        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
+               if not cleanup_virtual then return self
                assert can_resolve_for(mtype, anchor, mmodule)
                # self is a virtual type declared (or inherited) in mtype
                # The point of the function it to get the bound of the virtual type that make sense for mtype
                # But because mtype is maybe a virtual/formal type, we need to get a real receiver first
                #print "{class_name}: {self}/{mtype}/{anchor}?"
-               var resolved_reciever
+               var resolved_receiver
                if mtype.need_anchor then
                        assert anchor != null
-                       resolved_reciever = mtype.resolve_for(anchor, null, mmodule, true)
+                       resolved_receiver = mtype.resolve_for(anchor, null, mmodule, true)
                else
-                       resolved_reciever = mtype
+                       resolved_receiver = mtype
                end
                # Now, we can get the bound
-               var verbatim_bound = lookup_bound(mmodule, resolved_reciever)
+               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} -> {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
+               return res
        end
 
        redef fun can_resolve_for(mtype, anchor, mmodule)
@@ -1304,12 +1327,15 @@ class MParameterType
 
        redef fun to_s do return name
 
-       # Resolve the bound for a given resolved_receiver
-       # The result may be a other virtual type (or a parameter type)
-       fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
+       redef fun lookup_bound(mmodule: MModule, resolved_receiver: MType): MType
        do
                assert not resolved_receiver.need_anchor
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
                var goalclass = self.mclass
+               if resolved_receiver.mclass == goalclass then
+                       return resolved_receiver.arguments[self.rank]
+               end
                var supertypes = resolved_receiver.collect_mtypes(mmodule)
                for t in supertypes do
                        if t.mclass == goalclass then
@@ -1322,6 +1348,22 @@ class MParameterType
                abort
        end
 
+       # A PT is fixed when:
+       # * Its bound is a enum class (see `enum_kind`).
+       #   The PT is just useless, but it is still a case.
+       # * More usually, the `resolved_receiver` is a subclass of `self.mclass`,
+       #   so it is necessarily fixed in a `super` clause, either with a normal type
+       #   or with another PT.
+       #   See `resolve_for` for examples about related issues.
+       redef fun lookup_fixed(mmodule: MModule, resolved_receiver: MType): MType
+       do
+               assert not resolved_receiver.need_anchor
+               resolved_receiver = resolved_receiver.as_notnullable
+               assert resolved_receiver isa MClassType # It is the only remaining type
+               var res = self.resolve_for(resolved_receiver.mclass.mclass_type, resolved_receiver, mmodule, false)
+               return res
+       end
+
        redef fun resolve_for(mtype, anchor, mmodule, cleanup_virtual)
        do
                assert can_resolve_for(mtype, anchor, mmodule)
@@ -1354,7 +1396,7 @@ class MParameterType
                        resolved_receiver = anchor.arguments[resolved_receiver.rank]
                        if resolved_receiver isa MNullableType then resolved_receiver = resolved_receiver.mtype
                end
-               assert resolved_receiver isa MClassType
+               assert resolved_receiver isa MClassType # It is the only remaining type
 
                # Eh! The parameter is in the current class.
                # So we return the corresponding argument, no mater what!
@@ -1418,6 +1460,14 @@ class MNullableType
                return self.mtype.can_resolve_for(mtype, anchor, mmodule)
        end
 
+       # Efficiently returns `mtype.lookup_fixed(mmodule, resolved_receiver).as_nullable`
+       redef fun lookup_fixed(mmodule, resolved_receiver)
+       do
+               var t = mtype.lookup_fixed(mmodule, resolved_receiver)
+               if t == mtype then return self
+               return t.as_nullable
+       end
+
        redef fun depth do return self.mtype.depth
 
        redef fun length do return self.mtype.length

diff --git a/src/modelize/modelize_property.nit b/src/modelize/modelize_property.nit
index 757f85d..ea858c9 100644 (file)
--- a/src/modelize/modelize_property.nit
+++ b/src/modelize/modelize_property.nit
@@ -1138,6 +1138,11 @@ redef class ATypePropdef
                var mpropdef = new MVirtualTypeDef(mclassdef, mprop, self.location)
                self.mpropdef = mpropdef
                modelbuilder.mpropdef2npropdef[mpropdef] = self
+               if mpropdef.is_intro then
+                       modelbuilder.toolcontext.info("{mpropdef} introduces new type {mprop.full_name}", 4)
+               else
+                       modelbuilder.toolcontext.info("{mpropdef} redefines type {mprop.full_name}", 4)
+               end
                set_doc(mpropdef, modelbuilder)
 
                var atfixed = get_single_annotation("fixed", modelbuilder)

diff --git a/tests/base_formal_subtype.nit b/tests/base_formal_subtype.nit
new file mode 100644 (file)
index 0000000..9487b53
--- /dev/null
+++ b/tests/base_formal_subtype.nit
@@ -0,0 +1,164 @@
+# This file is part of NIT ( http://www.nitlanguage.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.
+
+import end
+
+interface Object end
+
+enum Bool end
+
+class A[E: Object]
+       var o: Object
+
+       var e: E
+
+       type VE: E
+       var ve: VE
+
+       type VVE: VE
+       var vve: VVE
+
+       type VGE: G[E]
+       var vge: VGE
+
+       type VVGE: VGE
+       var vvge: VVGE
+
+       type VGVE: G[VE]
+       var vgve: VGVE
+
+       type VGVVE: G[VVE]
+       var vgvve: VGVVE
+
+       fun foo
+       do
+               # In order to check type relations, this test looks for the warnings about useless cast
+               # The following should produce a warning
+               assert o isa Object
+
+               assert e isa E
+               assert e isa Object
+
+               assert ve isa VE
+               assert ve isa E
+               assert ve isa Object
+
+               assert vve isa VVE
+               assert vve isa VE
+               assert vve isa E
+               assert vve isa Object
+
+               assert vge isa VGE
+               assert vge isa G[E]
+               assert vge isa G[Object]
+               assert vge isa Object
+
+               assert vvge isa VVGE
+               assert vvge isa VGE
+               assert vvge isa G[E]
+               assert vvge isa G[Object]
+               assert vvge isa Object
+
+               assert vgve isa VGVE
+               assert vgve isa G[VE]
+               assert vgve isa G[E]
+               assert vgve isa G[Object]
+               assert vgve isa Object
+
+               assert vgvve isa VGVVE
+               assert vgvve isa G[VVE]
+               assert vgvve isa G[VE]
+               assert vgvve isa G[E]
+               assert vgvve isa G[Object]
+               assert vgvve isa Object
+
+               # The following should not
+               assert o isa VGVVE
+               assert o isa G[VVE]
+               assert o isa VVGE
+               assert o isa VGVE
+               assert o isa G[VE]
+               assert o isa VGE
+               assert o isa G[E]
+               assert o isa G[Object]
+               assert o isa VVE
+               assert o isa VE
+               assert o isa E
+
+               assert e isa VGVVE
+               assert e isa G[VVE]
+               assert e isa VVGE
+               assert e isa VGVE
+               assert e isa G[VE]
+               assert e isa VGE
+               assert e isa G[E]
+               assert e isa G[Object]
+               assert e isa VVE
+               assert e isa VE
+
+               assert ve isa VGVVE
+               assert ve isa G[VVE]
+               assert ve isa VVGE
+               assert ve isa VGVE
+               assert ve isa G[VE]
+               assert ve isa VGE
+               assert ve isa G[E]
+               assert ve isa G[Object]
+               assert ve isa VVE
+
+               assert vve isa VGVVE
+               assert vve isa G[VVE]
+               assert vve isa VVGE
+               assert vve isa VGVE
+               assert vve isa G[VE]
+               assert vve isa VGE
+               assert vve isa G[E]
+               assert vve isa G[Object]
+
+               assert vge isa VGVVE
+               assert vge isa G[VVE]
+               assert vge isa VVGE
+               assert vge isa VGVE
+               assert vge isa G[VE]
+               assert vge isa VVE
+               assert vge isa VE
+               assert vge isa E
+
+               assert vvge isa VGVVE
+               assert vvge isa G[VVE]
+               assert vvge isa VGVE
+               assert vvge isa G[VE]
+               assert vvge isa VVE
+               assert vvge isa VE
+               assert vvge isa E
+
+               assert vgve isa VGVVE
+               assert vgve isa G[VVE]
+               assert vgve isa VGE
+               assert vgve isa VVGE
+               assert vgve isa VVE
+               assert vgve isa VE
+               assert vgve isa E
+
+               assert vgvve isa VGE
+               assert vgvve isa VVGE
+               assert vgvve isa VGVE
+               assert vgvve isa VVE
+               assert vgvve isa VE
+               assert vgvve isa E
+       end
+end
+
+class G[E]
+end

diff --git a/tests/sav/base_formal_subtype.res b/tests/sav/base_formal_subtype.res
new file mode 100644 (file)
index 0000000..445a4fa
--- /dev/null
+++ b/tests/sav/base_formal_subtype.res
@@ -0,0 +1,30 @@
+base_formal_subtype.nit:48,10--21: Warning: Expression is already a Object.
+base_formal_subtype.nit:50,10--16: Warning: Expression is already a E.
+base_formal_subtype.nit:51,10--21: Warning: Expression is already a Object since it is a E.
+base_formal_subtype.nit:53,10--18: Warning: Expression is already a VE.
+base_formal_subtype.nit:54,10--17: Warning: Expression is already a E since it is a VE.
+base_formal_subtype.nit:55,10--22: Warning: Expression is already a Object since it is a VE.
+base_formal_subtype.nit:57,10--20: Warning: Expression is already a VVE.
+base_formal_subtype.nit:58,10--19: Warning: Expression is already a VE since it is a VVE.
+base_formal_subtype.nit:59,10--18: Warning: Expression is already a E since it is a VVE.
+base_formal_subtype.nit:60,10--23: Warning: Expression is already a Object since it is a VVE.
+base_formal_subtype.nit:62,10--20: Warning: Expression is already a VGE.
+base_formal_subtype.nit:63,10--20: Warning: Expression is already a G[E] since it is a VGE.
+base_formal_subtype.nit:64,10--25: Warning: Expression is already a G[Object] since it is a VGE.
+base_formal_subtype.nit:65,10--23: Warning: Expression is already a Object since it is a VGE.
+base_formal_subtype.nit:67,10--22: Warning: Expression is already a VVGE.
+base_formal_subtype.nit:68,10--21: Warning: Expression is already a VGE since it is a VVGE.
+base_formal_subtype.nit:69,10--21: Warning: Expression is already a G[E] since it is a VVGE.
+base_formal_subtype.nit:70,10--26: Warning: Expression is already a G[Object] since it is a VVGE.
+base_formal_subtype.nit:71,10--24: Warning: Expression is already a Object since it is a VVGE.
+base_formal_subtype.nit:73,10--22: Warning: Expression is already a VGVE.
+base_formal_subtype.nit:74,10--22: Warning: Expression is already a G[VE] since it is a VGVE.
+base_formal_subtype.nit:75,10--21: Warning: Expression is already a G[E] since it is a VGVE.
+base_formal_subtype.nit:76,10--26: Warning: Expression is already a G[Object] since it is a VGVE.
+base_formal_subtype.nit:77,10--24: Warning: Expression is already a Object since it is a VGVE.
+base_formal_subtype.nit:79,10--24: Warning: Expression is already a VGVVE.
+base_formal_subtype.nit:80,10--24: Warning: Expression is already a G[VVE] since it is a VGVVE.
+base_formal_subtype.nit:81,10--23: Warning: Expression is already a G[VE] since it is a VGVVE.
+base_formal_subtype.nit:82,10--22: Warning: Expression is already a G[E] since it is a VGVVE.
+base_formal_subtype.nit:83,10--27: Warning: Expression is already a G[Object] since it is a VGVVE.
+base_formal_subtype.nit:84,10--25: Warning: Expression is already a Object since it is a VGVVE.