From 4e988f21c68caed6d273d29f3b0b9829b720fdba Mon Sep 17 00:00:00 2001 From: Simon Wegendt Date: Tue, 4 Jun 2019 15:05:13 +0200 Subject: [PATCH] Revert size inference as part of type solver However sizes will still be encoded in the type specifier and type checked. See comment at #300. --- .../src/org/eclipse/mita/base/TypeDsl.xtext | 5 +- .../typesystem/BaseConstraintFactory.xtend | 49 +++++++------------ .../constraints/SubtypeConstraint.xtend | 13 ++--- .../typesystem/infra/MitaBaseResource.xtend | 4 ++ ...cerTypeVariableNamesForErrorMessages.xtend | 15 +++--- .../typesystem/infra/SubtypeChecker.xtend | 10 +--- .../typesystem/infra/TypeClassUnifier.xtend | 4 +- .../serialization/SerializationAdapter.xtend | 32 ++---------- .../serialization/ValueClasses.xtend | 8 --- .../solver/CoerciveSubtypeSolver.xtend | 47 +++--------------- .../types/TypeConstructorType.xtend | 3 ++ .../base/typesystem/types/TypeScheme.xtend | 16 ++++-- .../typesystem/ProgramConstraintFactory.xtend | 5 +- 13 files changed, 67 insertions(+), 144 deletions(-) diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/TypeDsl.xtext b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/TypeDsl.xtext index 9ecb3a64..e52a7f00 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/TypeDsl.xtext +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/TypeDsl.xtext @@ -98,12 +98,13 @@ TypeParameter returns TypeParameter: RawTypeParameter returns RawTypeParameter: {RawTypeParameter} // since Invariant is the first=default value of Variance this assigns invariance on no match - (variance=Variance)? + //(variance=Variance)? name=ID ; InstanceTypeParameter returns InstanceTypeParameter: {InstanceTypeParameter} - (variance=Variance)? + // since Invariant is the first=default value of Variance this assigns invariance on no match + //(variance=Variance)? name=ID 'is' ofType=[Type] ; diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/BaseConstraintFactory.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/BaseConstraintFactory.xtend index 7b4be1eb..fbcfbf43 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/BaseConstraintFactory.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/BaseConstraintFactory.xtend @@ -54,7 +54,6 @@ import org.eclipse.mita.base.types.Expression import org.eclipse.mita.base.types.GeneratedType import org.eclipse.mita.base.types.InstanceTypeParameter import org.eclipse.mita.base.types.NamedElement -import org.eclipse.mita.base.types.NaryTypeAddition import org.eclipse.mita.base.types.NativeType import org.eclipse.mita.base.types.NullTypeSpecifier import org.eclipse.mita.base.types.Operation @@ -63,6 +62,7 @@ import org.eclipse.mita.base.types.ParameterWithDefaultValue import org.eclipse.mita.base.types.PrimitiveType import org.eclipse.mita.base.types.RawTypeParameter import org.eclipse.mita.base.types.StructuralParameter +import org.eclipse.mita.base.types.StructuralType import org.eclipse.mita.base.types.StructureType import org.eclipse.mita.base.types.SumAlternative import org.eclipse.mita.base.types.SumType @@ -88,8 +88,6 @@ import org.eclipse.mita.base.typesystem.types.BaseKind import org.eclipse.mita.base.typesystem.types.BottomType import org.eclipse.mita.base.typesystem.types.FunctionType import org.eclipse.mita.base.typesystem.types.IntegerType -import org.eclipse.mita.base.typesystem.types.LiteralNumberType -import org.eclipse.mita.base.typesystem.types.NumericAddType import org.eclipse.mita.base.typesystem.types.NumericType import org.eclipse.mita.base.typesystem.types.ProdType import org.eclipse.mita.base.typesystem.types.Signedness @@ -110,8 +108,7 @@ import org.eclipse.xtext.scoping.IScopeProvider import static extension org.eclipse.mita.base.types.TypesUtil.ignoreCoercions import static extension org.eclipse.mita.base.util.BaseUtils.force -import static extension org.eclipse.mita.base.util.BaseUtils.zip -import org.eclipse.mita.base.types.StructuralType +import org.eclipse.mita.base.types.NaryTypeAddition class BaseConstraintFactory implements IConstraintFactory { @@ -621,7 +618,7 @@ class BaseConstraintFactory implements IConstraintFactory { system.addConstraint(new SubtypeConstraint(falseTV, commonTV, mkIssue.apply("", " (:: %s)", expr.falseCase))); return system.associate(commonTV); } - + protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, BinaryExpression expr) { if(expr.operator instanceof LogicalOperator) { val boolType = typeRegistry.getTypeModelObjectProxy(system, expr, StdlibTypeRegistry.boolTypeQID); @@ -664,6 +661,19 @@ class BaseConstraintFactory implements IConstraintFactory { val resultType = system.computeConstraintsForFunctionCall(expr, null, opQID.lastSegment, operands, operations); return system.associate(resultType, expr); } + + protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, NaryTypeAddition expr) { + // for now assume that operations on types are always T* -> T + val result = system.getTypeVariable(expr); + expr.values.forEach[ + system.addConstraint(new SubtypeConstraint(system.computeConstraints(it), result, new ValidationIssue(Severity.ERROR, '''«it» (:: %s) doesn't share a common type with the other members of this expression''', it, null, ""))) + ] + return result; + } + + protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, TypeReferenceLiteral expr) { + return system.associate(system.getTypeVariableProxy(expr, TypesPackage.eINSTANCE.typeReferenceLiteral_Type)) + } protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, Type type) { system.associate(system.translateTypeDeclaration(type), type); @@ -864,7 +874,7 @@ class BaseConstraintFactory implements IConstraintFactory { } protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, TypeExpressionSpecifier typeSpecifier) { - return system.associate(system.computeConstraintsForExpression(typeSpecifier.value), typeSpecifier); + return system.associate(system.computeConstraints(typeSpecifier.value), typeSpecifier); } protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, TypeReferenceSpecifier typeSpecifier) { @@ -887,7 +897,7 @@ class BaseConstraintFactory implements IConstraintFactory { // since type specifiers reference something we don't always know the variance here val typeArgs = typeArgTypes.map[it -> Variance.UNKNOWN].force; // compute constraints to validate t (argument count etc.) - val typeInstance = system.nestInType(null, new AtomicType(typeSpecifier.eGet(eRef, false) as EObject, typeName), typeArgs, type, typeName); + val typeInstance = system.nestInType(typeSpecifier, new AtomicType(typeSpecifier.eGet(eRef, false) as EObject, typeName), typeArgs, type, typeName); typeInstance; } @@ -1011,29 +1021,6 @@ class BaseConstraintFactory implements IConstraintFactory { println('BCF: computeConstraints called on null'); return null; } - - protected dispatch def computeConstraintsForExpression(ConstraintSystem system, NaryTypeAddition e) { - return system.associate(new NumericAddType(e, "typeAdd", e.values.map[system.computeConstraintsForLiteral(it) as AbstractType -> Variance.INVARIANT].force), e); - } - protected dispatch def computeConstraintsForExpression(ConstraintSystem system, PrimitiveValueExpression e) { - return system.associate(system.computeConstraintsForLiteral(e.value), e); - } - protected dispatch def computeConstraintsForLiteral(ConstraintSystem system, TypeReferenceLiteral e) { - return system.associate(system.resolveReferenceToSingleAndGetType(e, TypesPackage.eINSTANCE.typeReferenceLiteral_Type), e); - } - - protected dispatch def computeConstraintsForExpression(ConstraintSystem system, Expression e) { - throw new UnsupportedOperationException("BCF: unimplemented computeConstraintsForExpression for " + e.class.simpleName); - } - - protected dispatch def computeConstraintsForLiteral(ConstraintSystem system, IntLiteral literal) { - return system.associate(new LiteralNumberType(literal, literal.value, system.translateInteger(literal, literal.value)), literal); - } - - protected dispatch def computeConstraintsForLiteral(ConstraintSystem system, Literal literal) { - throw new UnsupportedOperationException("BCF: unimplemented computeConstraintsForLiteral for " + literal.class.simpleName); - } - protected def associate(ConstraintSystem system, AbstractType t) { return associate(system, t, t.origin); diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/constraints/SubtypeConstraint.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/constraints/SubtypeConstraint.xtend index 11423e97..01d94002 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/constraints/SubtypeConstraint.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/constraints/SubtypeConstraint.xtend @@ -23,11 +23,9 @@ import org.eclipse.mita.base.typesystem.types.AbstractType import org.eclipse.mita.base.typesystem.types.SumType import org.eclipse.mita.base.typesystem.types.TypeConstructorType import org.eclipse.mita.base.typesystem.types.TypeVariable +import org.eclipse.mita.base.typesystem.types.TypeVariableProxy import org.eclipse.xtend.lib.annotations.Accessors import org.eclipse.xtend.lib.annotations.EqualsHashCode -import org.eclipse.mita.base.typesystem.types.LiteralNumberType -import org.eclipse.mita.base.typesystem.types.TypeVariableProxy -import org.eclipse.mita.base.typesystem.types.LiteralTypeExpression /** * Corresponds to subtype relationship sub <: sup as defined in @@ -80,16 +78,11 @@ class SubtypeConstraint extends AbstractTypeConstraint { override isAtomic(ConstraintSystem system) { if(cachedIsAtomic == CachedBoolean.Uncached) { - cachedIsAtomic = CachedBoolean.from((subType.isAtomic && superType.isAtomic && !isLiteralTypeCheck) || (system.canHaveSuperTypes(subType) || system.hasSubtypes(superType)) && !(typesAreCommon(subType, superType))); + cachedIsAtomic = CachedBoolean.from((subType.isAtomic && superType.isAtomic) || (system.canHaveSuperTypes(subType) || system.hasSubtypes(superType)) && !(typesAreCommon(subType, superType))); } return cachedIsAtomic.get(); } - - def boolean isLiteralTypeCheck() { - (subType instanceof LiteralTypeExpression || superType instanceof LiteralTypeExpression) - && (!(subType instanceof TypeVariable) && !(superType instanceof TypeVariable)) - } - + dispatch def boolean typesAreCommon(AbstractType type, AbstractType type2) { return false } diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/MitaBaseResource.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/MitaBaseResource.xtend index 104b9d34..3081fc41 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/MitaBaseResource.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/MitaBaseResource.xtend @@ -20,6 +20,9 @@ import java.io.InputStream import java.util.ArrayList import java.util.Map import org.apache.log4j.Logger +import org.eclipse.core.runtime.IProgressMonitor +import org.eclipse.core.runtime.Status +import org.eclipse.core.runtime.jobs.Job import org.eclipse.emf.common.util.BasicEList import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.EReference @@ -174,6 +177,7 @@ class MitaBaseResource extends LazyLinkingResource { typeLinker.doActuallyClearReferences(model); typeLinker.linkModel(model, diagnosticsConsumer); typeDependentLinker.linkModel(model, diagnosticsConsumer); + collectAndSolveTypes(model); } diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/NicerTypeVariableNamesForErrorMessages.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/NicerTypeVariableNamesForErrorMessages.xtend index f47abc2c..ff7e9d09 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/NicerTypeVariableNamesForErrorMessages.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/NicerTypeVariableNamesForErrorMessages.xtend @@ -13,20 +13,17 @@ package org.eclipse.mita.base.typesystem.infra -import java.util.HashMap -import java.util.Map +import it.unimi.dsi.fastutil.ints.Int2ObjectOpenHashMap import java.util.Random import java.util.stream.Collectors import java.util.stream.IntStream import org.eclipse.core.runtime.Assert -import org.eclipse.xtext.xbase.lib.Functions.Function1 -import org.eclipse.mita.base.typesystem.types.AbstractType.NameModifier import org.eclipse.mita.base.typesystem.types.AbstractType.Either +import org.eclipse.mita.base.typesystem.types.AbstractType.NameModifier class NicerTypeVariableNamesForErrorMessages extends NameModifier { - - Map seenNames = new HashMap(); + Int2ObjectOpenHashMap seenNames = new Int2ObjectOpenHashMap(); var nextSuffix = 1; var state = getAlphabet("").iterator; @@ -46,10 +43,10 @@ class NicerTypeVariableNamesForErrorMessages extends NameModifier { } override apply(int varIdx) { - if(!seenNames.containsKey(Integer.valueOf(varIdx))) { - seenNames.put(Integer.valueOf(varIdx), nextName()); + if(!seenNames.containsKey(varIdx)) { + seenNames.put(varIdx, nextName()); } - return Either.right(seenNames.get(Integer.valueOf(varIdx))); + return Either.right(seenNames.get(varIdx)); } def static void main(String[] args) { diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/SubtypeChecker.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/SubtypeChecker.xtend index fce3c85b..cd09930c 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/SubtypeChecker.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/SubtypeChecker.xtend @@ -35,8 +35,6 @@ import org.eclipse.mita.base.typesystem.types.BottomType import org.eclipse.mita.base.typesystem.types.FloatingType import org.eclipse.mita.base.typesystem.types.FunctionType import org.eclipse.mita.base.typesystem.types.IntegerType -import org.eclipse.mita.base.typesystem.types.LiteralNumberType -import org.eclipse.mita.base.typesystem.types.NumericAddType import org.eclipse.mita.base.typesystem.types.ProdType import org.eclipse.mita.base.typesystem.types.Signedness import org.eclipse.mita.base.typesystem.types.SumType @@ -129,7 +127,7 @@ class SubtypeChecker { return realType; ]; ].force; - val ta_t = s.getOptionalType(typeResolveOrigin ?: t.origin).instantiate(s); + val ta_t = s.getOptionalType(typeResolveOrigin ?: t.origin).instantiate(s, t.origin); val ta = ta_t.key.head; val optionalType = ta_t.value return explicitSuperTypes.flatMap[s.doGetSuperTypes(it, typeResolveOrigin ?: it.origin)].flatMap[#[it, optionalType.replace(ta, it)]].toSet; @@ -195,11 +193,7 @@ class SubtypeChecker { protected def SubtypeCheckResult checkByteWidth(IntegerType sub, IntegerType top, int bSub, int bTop) { return (bSub <= bTop).subtypeMsgFromBoolean('''«top.name» is too small for «sub.name»'''); } - - dispatch def SubtypeCheckResult isSubtypeOf(ConstraintSystem s, EObject context, LiteralNumberType sub, LiteralNumberType top) { - return (sub.value <= top.value).subtypeMsgFromBoolean('''«top.name» is bigger than «sub.name»'''); - } - + // dispatch def SubtypeCheckResult isSubtypeOf(ConstraintSystem s, EObject context, NumericAddType sub, NumericAddType top) { // val subDecomp = sub.decompose(this, s, context); // val topDecomp = top.decompose(this, s, context); diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/TypeClassUnifier.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/TypeClassUnifier.xtend index 2ca6ff3f..64366f48 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/TypeClassUnifier.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/infra/TypeClassUnifier.xtend @@ -63,7 +63,7 @@ class TypeClassUnifier { } val instances = types.map[ if(it instanceof TypeScheme) { - it.instantiate(system).value; + it.instantiate(system, null).value; } ].force; // commonStructure: fst :: (a, b) -> c @@ -167,7 +167,7 @@ class TypeClassUnifier { def AbstractType unifyTypeClassInstancesStructure(ConstraintSystem system, Iterable _instances) { val instances = _instances.map[ if(it instanceof TypeScheme) { - it.instantiate(system).value; + it.instantiate(system, null).value; } else { it; diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/SerializationAdapter.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/SerializationAdapter.xtend index 48535909..729b0711 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/SerializationAdapter.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/SerializationAdapter.xtend @@ -37,6 +37,7 @@ import org.eclipse.emf.ecore.EStructuralFeature import org.eclipse.emf.ecore.EcoreFactory import org.eclipse.emf.ecore.impl.BasicEObjectImpl import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.mita.base.types.Variance import org.eclipse.mita.base.types.validation.IValidationIssueAcceptor.ValidationIssue import org.eclipse.mita.base.typesystem.constraints.AbstractTypeConstraint import org.eclipse.mita.base.typesystem.constraints.EqualityConstraint @@ -68,10 +69,7 @@ import org.eclipse.xtext.naming.QualifiedName import static extension org.eclipse.mita.base.util.BaseUtils.force import static extension org.eclipse.mita.base.util.BaseUtils.zip -import org.eclipse.mita.base.typesystem.types.LiteralNumberType import org.eclipse.mita.base.typesystem.types.DependentTypeVariable -import org.eclipse.mita.base.typesystem.types.NumericAddType -import org.eclipse.mita.base.types.Variance class SerializationAdapter { @@ -206,11 +204,7 @@ class SerializationAdapter { protected dispatch def AbstractType fromValueObject(SerializedIntegerType obj) { return new IntegerType(obj.origin.resolveEObject(), obj.widthInBytes, obj.signedness); } - - protected dispatch def AbstractType fromValueObject(SerializedLiteralNumberType obj) { - return new LiteralNumberType(obj.origin.resolveEObject(), obj.value, obj.typeOf.fromValueObject as AbstractType); - } - + protected dispatch def AbstractType fromValueObject(SerializedTypeHole obj) { return new TypeHole(obj.origin.resolveEObject(), obj.idx); } @@ -230,9 +224,6 @@ class SerializationAdapter { protected dispatch def AbstractType fromValueObject(SerializedProductType obj) { return new ProdType(obj.origin.resolveEObject(), obj.name, obj.typeArguments.fromSerializedTypeArguments()); } - protected dispatch def AbstractType fromValueObject(SerializedNumericAddType obj) { - return new NumericAddType(obj.origin.resolveEObject, obj.name, obj.typeArguments.fromSerializedTypeArguments()); - } protected dispatch def AbstractType fromValueObject(SerializedSumType obj) { return new SumType(obj.origin.resolveEObject(), obj.name, obj.typeArguments.fromSerializedTypeArguments()); @@ -311,15 +302,7 @@ class SerializationAdapter { } return new String(content, "ISO-8859-1"); } - - protected dispatch def Object toValueObject(LiteralNumberType lit) { - return new SerializedLiteralNumberType => [ - fill(it, lit); - it.value = lit.value; - it.typeOf = lit.typeOf.toValueObject as SerializedAbstractType; - ] - } - + protected dispatch def Object toValueObject(Object nul) { throw new NullPointerException; } @@ -494,6 +477,7 @@ class SerializationAdapter { ] } + protected dispatch def Object fill(SerializedCompoundType ctxt, TypeConstructorType obj) { _fill(ctxt as SerializedAbstractType, obj as AbstractType); ctxt.typeArguments = obj.typeArgumentsAndVariances.map[ it.key.toValueObject as SerializedAbstractType -> it.value ].toList @@ -518,13 +502,7 @@ class SerializationAdapter { fill(it, obj) ] } - - protected dispatch def Object toValueObject(NumericAddType obj) { - new SerializedNumericAddType => [ - fill(it, obj) - ] - } - + protected dispatch def Object toValueObject(TypeConstructorType obj) { new SerializedTypeConstructorType => [ fill(it, obj) diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/ValueClasses.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/ValueClasses.xtend index 16916739..ee64cf3e 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/ValueClasses.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/serialization/ValueClasses.xtend @@ -92,11 +92,6 @@ final class SerializedIntegerType extends SerializedNumericType { public Signedness signedness; } -final class SerializedLiteralNumberType extends SerializedAbstractBaseType { - public SerializedAbstractType typeOf; - public long value; -} - abstract class SerializedCompoundType extends SerializedAbstractType { public List> typeArguments = new ArrayList; } @@ -112,9 +107,6 @@ final class SerializedProductType extends SerializedCompoundType { final class SerializedSumType extends SerializedCompoundType { } -final class SerializedNumericAddType extends SerializedCompoundType { -} - final class SerializedTypeScheme extends SerializedAbstractType { public List vars; public SerializedAbstractType on; diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/solver/CoerciveSubtypeSolver.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/solver/CoerciveSubtypeSolver.xtend index 6ba2c89c..523327fc 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/solver/CoerciveSubtypeSolver.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/solver/CoerciveSubtypeSolver.xtend @@ -31,6 +31,7 @@ import org.eclipse.mita.base.expressions.util.ExpressionUtils import org.eclipse.mita.base.types.Operation import org.eclipse.mita.base.types.ParameterWithDefaultValue import org.eclipse.mita.base.types.validation.IValidationIssueAcceptor.ValidationIssue +import org.eclipse.mita.base.typesystem.BaseConstraintFactory import org.eclipse.mita.base.typesystem.StdlibTypeRegistry import org.eclipse.mita.base.typesystem.constraints.AbstractTypeConstraint import org.eclipse.mita.base.typesystem.constraints.EqualityConstraint @@ -42,6 +43,7 @@ import org.eclipse.mita.base.typesystem.infra.ConstraintGraph import org.eclipse.mita.base.typesystem.infra.ConstraintGraphProvider import org.eclipse.mita.base.typesystem.infra.Graph import org.eclipse.mita.base.typesystem.infra.MitaBaseResource +import org.eclipse.mita.base.typesystem.infra.NicerTypeVariableNamesForErrorMessages import org.eclipse.mita.base.typesystem.infra.SubtypeChecker import org.eclipse.mita.base.typesystem.infra.TypeClassUnifier import org.eclipse.mita.base.typesystem.types.AbstractBaseType @@ -51,6 +53,7 @@ import org.eclipse.mita.base.typesystem.types.BottomType import org.eclipse.mita.base.typesystem.types.FunctionType import org.eclipse.mita.base.typesystem.types.IntegerType import org.eclipse.mita.base.typesystem.types.ProdType +import org.eclipse.mita.base.typesystem.types.Signedness import org.eclipse.mita.base.typesystem.types.SumType import org.eclipse.mita.base.typesystem.types.TypeConstructorType import org.eclipse.mita.base.typesystem.types.TypeHole @@ -66,13 +69,6 @@ import org.eclipse.xtext.util.CancelIndicator import static extension org.eclipse.mita.base.util.BaseUtils.force import static extension org.eclipse.mita.base.util.BaseUtils.zip -import org.eclipse.mita.base.typesystem.BaseConstraintFactory -import org.eclipse.mita.base.typesystem.infra.NicerTypeVariableNamesForErrorMessages -import org.eclipse.mita.base.typesystem.types.Signedness -import org.eclipse.mita.base.typesystem.types.NumericType -import org.eclipse.mita.base.typesystem.types.LiteralTypeExpression -import org.eclipse.mita.base.typesystem.types.LiteralNumberType -import org.eclipse.mita.base.typesystem.types.NumericAddType /** * Solves coercive subtyping as described in @@ -144,7 +140,7 @@ class CoerciveSubtypeSolver implements IConstraintSolver { ] val msg = typeClass.mostSpecificGeneralization; val funTypeInstance = if(msg instanceof TypeScheme) { - msg.instantiate(currentSystem).value; + msg.instantiate(currentSystem, null).value; } if(funTypeInstance instanceof FunctionType) { val typeThatShouldBeInstance = tcc.typ; @@ -336,7 +332,7 @@ class CoerciveSubtypeSolver implements IConstraintSolver { protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, ExplicitInstanceConstraint constraint) { val ts = constraint.typeScheme; if(ts instanceof TypeScheme) { - val instance = ts.instantiate(system); + val instance = ts.instantiate(system, constraint.instance.origin); val instanceType = instance.value val resultSystem = system.plus( new EqualityConstraint(constraint.instance, instanceType, constraint.errorMessage) @@ -412,7 +408,7 @@ class CoerciveSubtypeSolver implements IConstraintSolver { val EObject fun = k_v.value; // typRaw might be a typeScheme (int32 -> b :: id: \T.T -> T) val typ_distance = if(typRaw instanceof TypeScheme) { - typRaw.instantiate(system).value -> Double.POSITIVE_INFINITY + typRaw.instantiate(system, constraint.typ.origin).value -> Double.POSITIVE_INFINITY } else { typRaw -> 0.0; } @@ -626,26 +622,7 @@ class CoerciveSubtypeSolver implements IConstraintSolver { val result = doSimplify(system, substitution, typeResolutionOrigin, constraint, sub, top); return result; } - - protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, NumericAddType sub, AbstractType top) { - sub.typeArguments.forEach[ - system.plus(new SubtypeConstraint(it, top, constraint._errorMessage)); - ] - - return SimplificationResult.success(system, Substitution.EMPTY); - } - - protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, LiteralNumberType sub, AbstractType top) { - return SimplificationResult.success(system.plus(new SubtypeConstraint(sub.typeOf, top, constraint._errorMessage)), Substitution.EMPTY); - } - - protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, LiteralNumberType sub, LiteralNumberType top) { - if(sub.value <= top.value) { - return SimplificationResult.success(system, Substitution.EMPTY); - } - return SimplificationResult.failure(constraint.errorMessage); - } - + protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, SumType sub, SumType top) { return system._doSimplify(substitution, typeResolutionOrigin, constraint, sub as TypeConstructorType, top as TypeConstructorType); } @@ -741,12 +718,7 @@ class CoerciveSubtypeSolver implements IConstraintSolver { return SimplificationResult.success(system, Substitution.EMPTY); } } - protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, TypeScheme sub, AbstractType top) { - val vars_instance = sub.instantiate(system) - val newSystem = system.plus(new SubtypeConstraint(vars_instance.value, top, constraint._errorMessage)); - return SimplificationResult.success(newSystem, Substitution.EMPTY); - } - + protected dispatch def SimplificationResult doSimplify(ConstraintSystem system, Substitution substitution, EObject typeResolutionOrigin, SubtypeConstraint constraint, Object sub, Object top) { SimplificationResult.failure(new ValidationIssue(Severity.ERROR, println('''INTERNAL ERROR: doSimplify.SubtypeConstraint not implemented for «sub.class.simpleName» and «top.class.simpleName»'''), "")) } @@ -817,9 +789,6 @@ class CoerciveSubtypeSolver implements IConstraintSolver { val supremum = subtypeChecker.getSupremum(system, predecessors, typeResolutionOrigin); val successors = graph.getBaseTypeSuccecessors(vIdx); val infimum = subtypeChecker.getInfimum(system, successors, typeResolutionOrigin); - if(predecessors.exists[it instanceof LiteralTypeExpression] || successors.exists[it instanceof LiteralTypeExpression]) { - print("") - } val supremumIsValid = supremum !== null && successors.forall[ t | subtypeChecker.isSubType(system, typeResolutionOrigin, supremum, t) ]; val infimumIsValid = infimum !== null && predecessors.forall[ t | subtypeChecker.isSubType(system, typeResolutionOrigin, t, infimum) ]; diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeConstructorType.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeConstructorType.xtend index 343902a1..a1302cca 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeConstructorType.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeConstructorType.xtend @@ -63,6 +63,9 @@ class TypeConstructorType extends AbstractType { throw new NullPointerException; } this._freeVars = getTypeArguments().flatMap[it.freeVars].force; + if(this.toString == "foo") { + print("") + } } new(EObject origin, AbstractType type, List> typeArguments) { diff --git a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeScheme.xtend b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeScheme.xtend index 29665e7f..f448fd8e 100644 --- a/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeScheme.xtend +++ b/bundles/org.eclipse.mita.base/src/org/eclipse/mita/base/typesystem/types/TypeScheme.xtend @@ -26,6 +26,7 @@ import static extension org.eclipse.mita.base.util.BaseUtils.force import org.eclipse.mita.base.typesystem.constraints.SubtypeConstraint import org.eclipse.mita.base.types.validation.IValidationIssueAcceptor.ValidationIssue import org.eclipse.mita.base.typesystem.constraints.JavaClassInstanceConstraint +import org.eclipse.mita.base.typesystem.infra.NicerTypeVariableNamesForErrorMessages @EqualsHashCode @Accessors @@ -37,6 +38,9 @@ class TypeScheme extends AbstractType { super(origin, on.name); this.vars = vars; this.on = on; + if(this.toString == "∀[f_366, f_367, f_368].__args(array, array) → array") { + print("") + } } override Tree quote() { @@ -68,13 +72,12 @@ class TypeScheme extends AbstractType { return on.freeVars.filter(TypeVariable).reject[vars.contains(it)]; } - def instantiate(ConstraintSystem system) { + def instantiate(ConstraintSystem system, EObject origin) { val newVars = new ArrayList(); val newOn = vars.fold(on, [term, boundVar | - val freeVar = system.newTypeVariable(null); + val freeVar = system.newTypeVariable(origin); if(boundVar instanceof DependentTypeVariable) { - system.addConstraint(new SubtypeConstraint(freeVar, boundVar.dependsOn, new ValidationIssue("%s is not a %s", null))) - system.addConstraint(new JavaClassInstanceConstraint(new ValidationIssue("%s is not instanceof %s", null), freeVar, LiteralTypeExpression)); + system.addConstraint(new SubtypeConstraint(freeVar, boundVar.dependsOn, new ValidationIssue("%s is not a %s", origin))) } newVars.add(freeVar); term.replace(boundVar, freeVar); @@ -95,7 +98,7 @@ class TypeScheme extends AbstractType { return this; } return new TypeScheme(origin, this.vars, - on.replace(sub.filter[vars.contains(it)]) + on.replace(sub.filter[!vars.contains(it)]) ); } else { return new TypeScheme(origin, this.vars, this.on.replace(sub)); @@ -111,6 +114,9 @@ class TypeScheme extends AbstractType { } override modifyNames(NameModifier converter) { + if(converter instanceof NicerTypeVariableNamesForErrorMessages) { + print(""); + } return new TypeScheme(origin, vars.map[modifyNames(converter) as TypeVariable].force, on.modifyNames(converter)); } diff --git a/bundles/org.eclipse.mita.program/src/org/eclipse/mita/program/typesystem/ProgramConstraintFactory.xtend b/bundles/org.eclipse.mita.program/src/org/eclipse/mita/program/typesystem/ProgramConstraintFactory.xtend index d25424bc..c3051971 100644 --- a/bundles/org.eclipse.mita.program/src/org/eclipse/mita/program/typesystem/ProgramConstraintFactory.xtend +++ b/bundles/org.eclipse.mita.program/src/org/eclipse/mita/program/typesystem/ProgramConstraintFactory.xtend @@ -29,6 +29,7 @@ import org.eclipse.mita.base.types.Operation import org.eclipse.mita.base.types.PresentTypeSpecifier import org.eclipse.mita.base.types.TypedElement import org.eclipse.mita.base.types.TypesPackage +import org.eclipse.mita.base.types.Variance import org.eclipse.mita.base.types.validation.IValidationIssueAcceptor.ValidationIssue import org.eclipse.mita.base.typesystem.StdlibTypeRegistry import org.eclipse.mita.base.typesystem.constraints.EqualityConstraint @@ -88,8 +89,6 @@ import org.eclipse.xtext.diagnostics.Severity import org.eclipse.xtext.naming.QualifiedName import static extension org.eclipse.mita.base.util.BaseUtils.force -import org.eclipse.mita.base.types.Variance -import org.eclipse.mita.base.typesystem.types.LiteralNumberType class ProgramConstraintFactory extends PlatformConstraintFactory { protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, Program program) { @@ -223,7 +222,7 @@ class ProgramConstraintFactory extends PlatformConstraintFactory { protected dispatch def TypeVariable computeConstraints(ConstraintSystem system, ArrayLiteral arrayLiteral) { val literalTypes = arrayLiteral.values.map[it -> system.computeConstraints(it)]; val innerType = system.newTypeVariable(null); - val sizeType = new LiteralNumberType(arrayLiteral, arrayLiteral.values.size, typeRegistry.getTypeModelObjectProxy(system, arrayLiteral, StdlibTypeRegistry.u32TypeQID)) + val sizeType = system.newTypeVariable(null); literalTypes.forEach[ system.addConstraint(new SubtypeConstraint(it.value, innerType, new ValidationIssue(Severity.ERROR, '''«it.key» (:: %s) doesn't share a common type with the other members of this array literal''', it.value.origin, null, ""))) ]