1 files changed, 392 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend
new file mode 100644
index 00000000..b8a6b9c1
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend
@@ -0,0 +1,392 @@
+package hu.bme.mit.inf.dslreasoner.viatra2logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import java.util.HashMap
+import java.util.HashSet
+import java.util.List
+import java.util.Set
+import org.eclipse.emf.ecore.EEnum
+import org.eclipse.emf.ecore.EcorePackage
+import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
+import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
+import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
+import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
+import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
+import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
+import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
+import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
+import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
+import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternCallBasedDeferred
+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
+import org.eclipse.xtext.xbase.XExpression
+import org.eclipse.xtext.xbase.typesystem.IBatchTypeResolver
+import org.eclipse.xtext.xbase.typesystem.references.UnknownTypeReference
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import org.eclipse.xtext.xbase.typesystem.references.InnerTypeReference
+class Viatra2LogicTypeInferer{
+        val Ecore2Logic ecore2Logic
+        val extension LogicProblemBuilder builder = new LogicProblemBuilder
+        /**Typeresolver uses the same resolver as EMFPatternLanguageStandaloneSetup.*/
+        val IBatchTypeResolver typeResolver = 
+                (new EMFPatternLanguageStandaloneSetup).createInjector.getInstance(IBatchTypeResolver)
+        val expressionExtractor = new XExpressionExtractor
+        
+        new(Ecore2Logic ecore2Logic) {
+                this.ecore2Logic = ecore2Logic
+        }
+        
+        def Viatra2LogicTypeResult inferTypes(List<PQuery> pQueries, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace) {
+                val Viatra2LogicTypeResult result = new Viatra2LogicTypeResult(new HashMap,new HashMap);
+                for(query : pQueries) {
+                        for(body: query.lookup(viatra2LogicTrace.query2Disjunction).bodies) {
+                                for(variable : body.uniqueVariables) {
+                                        getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,emptySet)
+                                }
+                        }
+                        for(parameter: query.parameters) {
+                                getOrMakeTypeDecision(result,query,parameter,ecore2LogicTrace,viatra2LogicTrace,emptySet)
+                        }
+                }
+                return result
+        }
+        
+        private def TypeReference getOrMakeTypeDecision(
+                Viatra2LogicTypeResult result,
+                PVariable variable, PBody body,
+                TracedOutput<LogicProblem,  Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Set<? extends PParameter> checkedInDecisionMaking)
+        {
+                if(result.containsSolution(body,variable)) {
+                        return result.getType(body,variable)
+                } else {
+                        val inferredTypesByViatra = TypeHelper::inferUnaryTypesFor(body.uniqueVariables, body.constraints, EMFQueryMetaContext.DEFAULT)
+                        val constraintsForVariable = variable.lookup(inferredTypesByViatra)
+                        
+                        val typeConstraintsDerivedByTypeHelper = constraintsForVariable.map[transformTypeReference(ecore2LogicTrace)]
+                        val typesFromEval = variable.getTypesFromEval(typeResolver)
+                        val typesFromAggregatorResult = variable.getTypeFromPassivePatternCallConstraintResult(
+                                result,
+                                ecore2LogicTrace,
+                                viatra2LogicTrace,
+                                checkedInDecisionMaking)
+                                 
+                        val typesFromPositiveReasoning = (typeConstraintsDerivedByTypeHelper + typesFromEval + typesFromAggregatorResult).filterNull
+                        
+                        val types = if(!typesFromPositiveReasoning.empty) {
+                                typesFromPositiveReasoning
+                        } else {
+                                variable.getTypeFromPassivePatternCallConstraints(
+                                        result,
+                                        ecore2LogicTrace,
+                                        viatra2LogicTrace,
+                                        checkedInDecisionMaking)
+                        }
+                        
+                        val commonSubtype = this.calculateCommonSubtype(types)
+                        
+                        result.addType(body,variable,commonSubtype)
+                        return commonSubtype
+                }
+        }
+        private def TypeReference getOrMakeTypeDecision(
+                Viatra2LogicTypeResult result,
+                PQuery query,
+                PParameter parameter,
+                TracedOutput<LogicProblem,  Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Set<? extends PParameter> checkedInDecisionMaking)
+        {
+                if(checkedInDecisionMaking.contains(parameter)) {
+                        return null
+                }
+                if(result.containsSolution(parameter)) {
+                        return result.getType(query, parameter)
+                }
+                
+                var TypeReference typeReference;
+                
+                if(parameter.declaredUnaryType !== null) {
+                         val key = parameter.declaredUnaryType
+                         typeReference = key.transformTypeReference(ecore2LogicTrace)
+                } else {
+                        val bodies = query.lookup(viatra2LogicTrace.query2Disjunction).bodies
+                        val newChecked = new HashSet(checkedInDecisionMaking) => [add(parameter)]
+                        val Iterable<TypeReference> variableTypes = bodies.map[body|
+                                val symbolicParameter = body.symbolicParameters.filter[patternParameter === parameter].head
+                                val variable = symbolicParameter.parameterVariable
+                                getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,newChecked)
+                        ]
+                        typeReference = calculateCommonSupertype(variableTypes)
+                }
+                result.addType(query,parameter,typeReference)
+                return typeReference
+        }
+        
+        private def Iterable<? extends TypeReference> getTypesFromEval(PVariable v, IBatchTypeResolver typeResolver) {
+                val constraints = v.getReferringConstraintsOfType(
+                        typeof(ExpressionEvaluation)
+                ).filter[
+                        it.outputVariable === v
+                ]
+                val res = constraints.map[getTypeFromEval]
+                return res
+        }
+        
+        def TypeReference getTypeFromEval(ExpressionEvaluation evaluation) {
+                val XExpression expression = expressionExtractor.extractExpression(evaluation.evaluator)
+                val returnType = typeResolver.resolveTypes(expression).getReturnType(expression);
+                if(returnType === null || returnType instanceof UnknownTypeReference) {
+                        return null
+                } else {
+                        val javaIdentifier = returnType.wrapperTypeIfPrimitive.javaIdentifier
+                        if(javaIdentifier == Boolean.name) {
+                                return LogicBool
+                        } else if(javaIdentifier == Integer.name || javaIdentifier == Short.name) {
+                                return LogicInt
+                        } else if(javaIdentifier == Double.name || javaIdentifier == Float.name){
+                                return LogicReal
+                        } else if(javaIdentifier == String.name) {
+                                return LogicString
+                        } else {
+                                throw new UnsupportedOperationException('''Unsupported eval type: "«javaIdentifier»"!''')
+                        }
+                }
+        }
+        
+        private def getTypeFromPassivePatternCallConstraintResult(
+                PVariable v,
+                Viatra2LogicTypeResult result,
+                TracedOutput<LogicProblem,  Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Set<? extends PParameter> checkedInDecisionMaking
+        ) {
+                val referringConstraints = v.referringConstraints
+                
+                val referringCountMatcherTargeting = referringConstraints
+                        .filter(PatternMatchCounter)
+                        .filter[it.resultVariable === v]
+                        .map[builder.LogicInt]
+                val referringAggregatorConstraintsTargeting = referringConstraints
+                        .filter(AggregatorConstraint)
+                        .filter[it.resultVariable === v]
+                        .map[ // get the type of the referred column
+                                getOrMakeTypeDecision(
+                                        result,
+                                        it.referredQuery,
+                                        it.referredQuery.parameters.get(aggregatedColumn),
+                                        ecore2LogicTrace,
+                                        viatra2LogicTrace,
+                                        checkedInDecisionMaking)]
+                                        
+                return referringCountMatcherTargeting + referringAggregatorConstraintsTargeting
+        }
+        
+        private def getTypeFromPassivePatternCallConstraints(
+                PVariable v,
+                Viatra2LogicTypeResult result,
+                TracedOutput<LogicProblem,  Ecore2Logic_Trace> ecore2LogicTrace,
+                Viatra2LogicTrace viatra2LogicTrace,
+                Set<? extends PParameter> checkedInDecisionMaking
+        ) {
+                val referringConstraints = v.referringConstraints
+                if(referringConstraints.size === 1) {
+                        val onlyConstraint = referringConstraints.head
+                        
+                        if(onlyConstraint instanceof PatternCallBasedDeferred) {
+                                val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex)
+                                val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable)
+                                val res = getOrMakeTypeDecision(result, onlyConstraint.referredQuery, parameter, ecore2LogicTrace,viatra2LogicTrace,checkedInDecisionMaking)
+                                return #[res]
+                        } else {
+                                throw new IllegalArgumentException('''A non-PatternCallBasedDeferred type constraint is referring to the variable "«v.name»"!''')
+                        }
+                } else {
+                        throw new IllegalArgumentException('''Multiple («referringConstraints.size», «FOR c:referringConstraints SEPARATOR ", "»«c»«ENDFOR») constraints are referring to variable "«v.name»", but no type is inferred!''')
+                }
+        }
+        
+        def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) {
+                val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
+                val complexTypeReferences = types.filter(ComplexTypeReference)
+                if(complexTypeReferences.isEmpty) {
+                        // If there is an int type, ...
+                        if(primitiveTypeReferences.exists[it instanceof IntTypeReference]) {
+                                // ... and all types are either real or int, then return int!
+                                if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) {
+                                        return primitiveTypeReferences.filter(IntTypeReference).head
+                                }
+                                // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
+                                else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
+                        }
+                        // If there is no Real, then the types should be homogenious
+                        val head = primitiveTypeReferences.head
+                        if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
+                                throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
+                        }
+                        return head
+                } else if(primitiveTypeReferences.isEmpty) {
+                        val complexTypes = complexTypeReferences.map[it.referred].toSet
+                        if(complexTypes.size === 1) {
+                                return builder.toTypeReference(complexTypes.head)
+                        }
+                        // Collect possible subtypes
+                        val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet]
+                        val commonTypeSet = new HashSet(subtypeSets.head)
+                        val otherSets = subtypeSets.tail
+                        for(otherSet : otherSets) {
+                                commonTypeSet.retainAll(otherSet)
+                        }
+                        if(commonTypeSet.empty) {
+                                throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
+                        }
+                        
+                        
+                        return calculateCommonComplexSupertype(commonTypeSet)
+                        
+                } else {
+                        throw new IllegalArgumentException('''
+                        Inconsistent types, mixing primitive and complex types:
+                                «primitiveTypeReferences.map[eClass.name].toSet.toList»
+                                        and
+                                «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
+                        
+                }
+        }
+        
+        
+        def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) {
+                val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
+                val complexTypeReferences = types.filter(ComplexTypeReference)
+                if(complexTypeReferences.isEmpty) {
+                        // If there is a real type, ...
+                        if(primitiveTypeReferences.exists[it instanceof RealTypeReference]) {
+                                // ... and all types are either real or int, then return real!
+                                if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) {
+                                        return primitiveTypeReferences.filter(RealTypeReference).head
+                                }
+                                // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
+                                else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
+                        }
+                        // If there is no Real, then the types should be homogenious
+                        val head = primitiveTypeReferences.head
+                        if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
+                                throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
+                        }
+                        return head
+                } else if(primitiveTypeReferences.isEmpty) {
+                        val complexTypes = complexTypeReferences.map[it.referred].toSet
+                        return calculateCommonComplexSupertype(complexTypes)
+                        
+                } else {
+                        throw new IllegalArgumentException('''
+                        Inconsistent types, mixing primitive and complex types:
+                                «primitiveTypeReferences.map[eClass.name].toSet.toList»
+                                        and
+                                «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
+                        
+                }
+        }
+        def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) {
+                if(complexTypes.size === 1) {
+                        return builder.toTypeReference(complexTypes.head)
+                }
+                // Collect possible supertypes
+                val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet]
+                val commonTypeSet = new HashSet(supertypeSets.head)
+                val otherSets = supertypeSets.tail
+                for(otherSet : otherSets) {
+                        commonTypeSet.retainAll(otherSet)
+                }
+                if(commonTypeSet.empty) {
+                        throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
+                }
+                // Remove type that already have covered
+                val coveredTypes = commonTypeSet.map[it.supertypes].flatten
+                commonTypeSet.removeAll(coveredTypes)
+                return builder.toTypeReference(commonTypeSet.head)
+        }
+        
+        /**
+         * Transforms a Viatra type reference to a logic type.
+         */
+        def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val w = k.wrappedKey 
+                if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) {
+                        return builder.LogicInt
+                } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) {
+                        return builder.LogicReal
+                } else if(w == EcorePackage.Literals.EBOOLEAN) {
+                        return builder.LogicBool
+                } else if(w == EcorePackage.Literals.ESTRING) {
+                        return builder.LogicString
+                } else if(w instanceof EEnum) {
+                        val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w)
+                        return builder.toTypeReference(c);
+                } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''')
+        }
+        def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val c = k.wrapperInstanceClass
+                if(c == Integer || c == Long || c == Short) {
+                        return LogicInt
+                } else if(c == Float || c == Double) {
+                        return LogicReal
+                } else if(c == Boolean) {
+                        return LogicBool
+                } else if(c == String) {
+                        return LogicString
+                } else if(c.superclass == Enum){
+                        val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace)
+                        for(enum : enums) {
+                                if(c == enum.instanceClass) {
+                                        return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum))
+                                }
+                        }
+                        throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''')
+                } else {
+                        return null
+                }
+        }
+        def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val c = k.wrappedKey
+                                
+                if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
+                        return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
+                } else {
+                        return null
+                }
+        }
+        def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                val c = k.wrappedKey
+                
+                if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
+                        return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
+                } else {
+                        return null
+                }
+        }
+        
+        def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
+                throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''')
+        }
+}
+\ No newline at end of file

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend new file mode 100644 index 00000000..b8a6b9c1 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend
@@ -0,0 +1,392 @@
	1	package hu.bme.mit.inf.dslreasoner.viatra2logic
	2
	3	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
	4	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
	5	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
	6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
	11	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	12	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
	13	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	14	import java.util.HashMap
	15	import java.util.HashSet
	16	import java.util.List
	17	import java.util.Set
	18	import org.eclipse.emf.ecore.EEnum
	19	import org.eclipse.emf.ecore.EcorePackage
	20	import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
	21	import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
	22	import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
	23	import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
	24	import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
	25	import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
	26	import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
	27	import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
	28	import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
	29	import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
	30	import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
	31	import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
	32	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
	33	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
	34	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternCallBasedDeferred
	35	import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
	36	import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
	37	import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
	38	import org.eclipse.xtext.xbase.XExpression
	39	import org.eclipse.xtext.xbase.typesystem.IBatchTypeResolver
	40	import org.eclipse.xtext.xbase.typesystem.references.UnknownTypeReference
	41
	42	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
	43	import org.eclipse.xtext.xbase.typesystem.references.InnerTypeReference
	44
	45	class Viatra2LogicTypeInferer{
	46	val Ecore2Logic ecore2Logic
	47	val extension LogicProblemBuilder builder = new LogicProblemBuilder
	48	/*Typeresolver uses the same resolver as EMFPatternLanguageStandaloneSetup./
	49	val IBatchTypeResolver typeResolver =
	50	(new EMFPatternLanguageStandaloneSetup).createInjector.getInstance(IBatchTypeResolver)
	51	val expressionExtractor = new XExpressionExtractor
	52
	53	new(Ecore2Logic ecore2Logic) {
	54	this.ecore2Logic = ecore2Logic
	55	}
	56
	57	def Viatra2LogicTypeResult inferTypes(List<PQuery> pQueries, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace) {
	58	val Viatra2LogicTypeResult result = new Viatra2LogicTypeResult(new HashMap,new HashMap);
	59	for(query : pQueries) {
	60	for(body: query.lookup(viatra2LogicTrace.query2Disjunction).bodies) {
	61	for(variable : body.uniqueVariables) {
	62	getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,emptySet)
	63	}
	64	}
	65	for(parameter: query.parameters) {
	66	getOrMakeTypeDecision(result,query,parameter,ecore2LogicTrace,viatra2LogicTrace,emptySet)
	67	}
	68	}
	69	return result
	70	}
	71
	72	private def TypeReference getOrMakeTypeDecision(
	73	Viatra2LogicTypeResult result,
	74	PVariable variable, PBody body,
	75	TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
	76	Viatra2LogicTrace viatra2LogicTrace,
	77	Set<? extends PParameter> checkedInDecisionMaking)
	78	{
	79	if(result.containsSolution(body,variable)) {
	80	return result.getType(body,variable)
	81	} else {
	82	val inferredTypesByViatra = TypeHelper::inferUnaryTypesFor(body.uniqueVariables, body.constraints, EMFQueryMetaContext.DEFAULT)
	83	val constraintsForVariable = variable.lookup(inferredTypesByViatra)
	84
	85	val typeConstraintsDerivedByTypeHelper = constraintsForVariable.map[transformTypeReference(ecore2LogicTrace)]
	86	val typesFromEval = variable.getTypesFromEval(typeResolver)
	87	val typesFromAggregatorResult = variable.getTypeFromPassivePatternCallConstraintResult(
	88	result,
	89	ecore2LogicTrace,
	90	viatra2LogicTrace,
	91	checkedInDecisionMaking)
	92
	93	val typesFromPositiveReasoning = (typeConstraintsDerivedByTypeHelper + typesFromEval + typesFromAggregatorResult).filterNull
	94
	95	val types = if(!typesFromPositiveReasoning.empty) {
	96	typesFromPositiveReasoning
	97	} else {
	98	variable.getTypeFromPassivePatternCallConstraints(
	99	result,
	100	ecore2LogicTrace,
	101	viatra2LogicTrace,
	102	checkedInDecisionMaking)
	103	}
	104
	105	val commonSubtype = this.calculateCommonSubtype(types)
	106
	107	result.addType(body,variable,commonSubtype)
	108	return commonSubtype
	109	}
	110	}
	111
	112	private def TypeReference getOrMakeTypeDecision(
	113	Viatra2LogicTypeResult result,
	114	PQuery query,
	115	PParameter parameter,
	116	TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
	117	Viatra2LogicTrace viatra2LogicTrace,
	118	Set<? extends PParameter> checkedInDecisionMaking)
	119	{
	120	if(checkedInDecisionMaking.contains(parameter)) {
	121	return null
	122	}
	123	if(result.containsSolution(parameter)) {
	124	return result.getType(query, parameter)
	125	}
	126
	127	var TypeReference typeReference;
	128
	129	if(parameter.declaredUnaryType !== null) {
	130	val key = parameter.declaredUnaryType
	131	typeReference = key.transformTypeReference(ecore2LogicTrace)
	132	} else {
	133	val bodies = query.lookup(viatra2LogicTrace.query2Disjunction).bodies
	134	val newChecked = new HashSet(checkedInDecisionMaking) => [add(parameter)]
	135	val Iterable<TypeReference> variableTypes = bodies.map[body\|
	136	val symbolicParameter = body.symbolicParameters.filter[patternParameter === parameter].head
	137	val variable = symbolicParameter.parameterVariable
	138	getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,newChecked)
	139	]
	140	typeReference = calculateCommonSupertype(variableTypes)
	141	}
	142	result.addType(query,parameter,typeReference)
	143	return typeReference
	144	}
	145
	146	private def Iterable<? extends TypeReference> getTypesFromEval(PVariable v, IBatchTypeResolver typeResolver) {
	147	val constraints = v.getReferringConstraintsOfType(
	148	typeof(ExpressionEvaluation)
	149	).filter[
	150	it.outputVariable === v
	151	]
	152	val res = constraints.map[getTypeFromEval]
	153	return res
	154	}
	155
	156	def TypeReference getTypeFromEval(ExpressionEvaluation evaluation) {
	157	val XExpression expression = expressionExtractor.extractExpression(evaluation.evaluator)
	158	val returnType = typeResolver.resolveTypes(expression).getReturnType(expression);
	159	if(returnType === null \|\| returnType instanceof UnknownTypeReference) {
	160	return null
	161	} else {
	162	val javaIdentifier = returnType.wrapperTypeIfPrimitive.javaIdentifier
	163	if(javaIdentifier == Boolean.name) {
	164	return LogicBool
	165	} else if(javaIdentifier == Integer.name \|\| javaIdentifier == Short.name) {
	166	return LogicInt
	167	} else if(javaIdentifier == Double.name \|\| javaIdentifier == Float.name){
	168	return LogicReal
	169	} else if(javaIdentifier == String.name) {
	170	return LogicString
	171	} else {
	172	throw new UnsupportedOperationException('''Unsupported eval type: "«javaIdentifier»"!''')
	173	}
	174	}
	175	}
	176
	177	private def getTypeFromPassivePatternCallConstraintResult(
	178	PVariable v,
	179	Viatra2LogicTypeResult result,
	180	TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
	181	Viatra2LogicTrace viatra2LogicTrace,
	182	Set<? extends PParameter> checkedInDecisionMaking
	183	) {
	184	val referringConstraints = v.referringConstraints
	185
	186	val referringCountMatcherTargeting = referringConstraints
	187	.filter(PatternMatchCounter)
	188	.filter[it.resultVariable === v]
	189	.map[builder.LogicInt]
	190	val referringAggregatorConstraintsTargeting = referringConstraints
	191	.filter(AggregatorConstraint)
	192	.filter[it.resultVariable === v]
	193	.map[ // get the type of the referred column
	194	getOrMakeTypeDecision(
	195	result,
	196	it.referredQuery,
	197	it.referredQuery.parameters.get(aggregatedColumn),
	198	ecore2LogicTrace,
	199	viatra2LogicTrace,
	200	checkedInDecisionMaking)]
	201
	202	return referringCountMatcherTargeting + referringAggregatorConstraintsTargeting
	203	}
	204
	205	private def getTypeFromPassivePatternCallConstraints(
	206	PVariable v,
	207	Viatra2LogicTypeResult result,
	208	TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
	209	Viatra2LogicTrace viatra2LogicTrace,
	210	Set<? extends PParameter> checkedInDecisionMaking
	211	) {
	212	val referringConstraints = v.referringConstraints
	213	if(referringConstraints.size === 1) {
	214	val onlyConstraint = referringConstraints.head
	215
	216	if(onlyConstraint instanceof PatternCallBasedDeferred) {
	217	val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex)
	218	val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable)
	219	val res = getOrMakeTypeDecision(result, onlyConstraint.referredQuery, parameter, ecore2LogicTrace,viatra2LogicTrace,checkedInDecisionMaking)
	220	return #[res]
	221	} else {
	222	throw new IllegalArgumentException('''A non-PatternCallBasedDeferred type constraint is referring to the variable "«v.name»"!''')
	223	}
	224	} else {
	225	throw new IllegalArgumentException('''Multiple («referringConstraints.size», «FOR c:referringConstraints SEPARATOR ", "»«c»«ENDFOR») constraints are referring to variable "«v.name»", but no type is inferred!''')
	226	}
	227	}
	228
	229	def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) {
	230	val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
	231	val complexTypeReferences = types.filter(ComplexTypeReference)
	232	if(complexTypeReferences.isEmpty) {
	233	// If there is an int type, ...
	234	if(primitiveTypeReferences.exists[it instanceof IntTypeReference]) {
	235	// ... and all types are either real or int, then return int!
	236	if(primitiveTypeReferences.forall[it instanceof RealTypeReference \|\| it instanceof IntTypeReference]) {
	237	return primitiveTypeReferences.filter(IntTypeReference).head
	238	}
	239	// Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
	240	else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
	241	}
	242	// If there is no Real, then the types should be homogenious
	243	val head = primitiveTypeReferences.head
	244	if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
	245	throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
	246	}
	247	return head
	248	} else if(primitiveTypeReferences.isEmpty) {
	249	val complexTypes = complexTypeReferences.map[it.referred].toSet
	250	if(complexTypes.size === 1) {
	251	return builder.toTypeReference(complexTypes.head)
	252	}
	253	// Collect possible subtypes
	254	val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet]
	255	val commonTypeSet = new HashSet(subtypeSets.head)
	256	val otherSets = subtypeSets.tail
	257	for(otherSet : otherSets) {
	258	commonTypeSet.retainAll(otherSet)
	259	}
	260	if(commonTypeSet.empty) {
	261	throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
	262	}
	263
	264
	265	return calculateCommonComplexSupertype(commonTypeSet)
	266
	267	} else {
	268	throw new IllegalArgumentException('''
	269	Inconsistent types, mixing primitive and complex types:
	270	«primitiveTypeReferences.map[eClass.name].toSet.toList»
	271	and
	272	«complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
	273
	274	}
	275	}
	276
	277
	278	def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) {
	279	val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
	280	val complexTypeReferences = types.filter(ComplexTypeReference)
	281	if(complexTypeReferences.isEmpty) {
	282	// If there is a real type, ...
	283	if(primitiveTypeReferences.exists[it instanceof RealTypeReference]) {
	284	// ... and all types are either real or int, then return real!
	285	if(primitiveTypeReferences.forall[it instanceof RealTypeReference \|\| it instanceof IntTypeReference]) {
	286	return primitiveTypeReferences.filter(RealTypeReference).head
	287	}
	288	// Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
	289	else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
	290	}
	291	// If there is no Real, then the types should be homogenious
	292	val head = primitiveTypeReferences.head
	293	if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
	294	throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
	295	}
	296	return head
	297	} else if(primitiveTypeReferences.isEmpty) {
	298	val complexTypes = complexTypeReferences.map[it.referred].toSet
	299	return calculateCommonComplexSupertype(complexTypes)
	300
	301	} else {
	302	throw new IllegalArgumentException('''
	303	Inconsistent types, mixing primitive and complex types:
	304	«primitiveTypeReferences.map[eClass.name].toSet.toList»
	305	and
	306	«complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
	307
	308	}
	309	}
	310	def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) {
	311	if(complexTypes.size === 1) {
	312	return builder.toTypeReference(complexTypes.head)
	313	}
	314	// Collect possible supertypes
	315	val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet]
	316	val commonTypeSet = new HashSet(supertypeSets.head)
	317	val otherSets = supertypeSets.tail
	318	for(otherSet : otherSets) {
	319	commonTypeSet.retainAll(otherSet)
	320	}
	321	if(commonTypeSet.empty) {
	322	throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
	323	}
	324	// Remove type that already have covered
	325	val coveredTypes = commonTypeSet.map[it.supertypes].flatten
	326	commonTypeSet.removeAll(coveredTypes)
	327	return builder.toTypeReference(commonTypeSet.head)
	328	}
	329
	330	/**
	331	* Transforms a Viatra type reference to a logic type.
	332	*/
	333	def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
	334	val w = k.wrappedKey
	335	if(w == EcorePackage.Literals.EINT \|\| w == EcorePackage.Literals.ESHORT \|\| w == EcorePackage.Literals.ELONG) {
	336	return builder.LogicInt
	337	} else if(w == EcorePackage.Literals.EDOUBLE \|\| w == EcorePackage.Literals.EFLOAT) {
	338	return builder.LogicReal
	339	} else if(w == EcorePackage.Literals.EBOOLEAN) {
	340	return builder.LogicBool
	341	} else if(w == EcorePackage.Literals.ESTRING) {
	342	return builder.LogicString
	343	} else if(w instanceof EEnum) {
	344	val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w)
	345	return builder.toTypeReference(c);
	346	} else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''')
	347	}
	348	def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
	349	val c = k.wrapperInstanceClass
	350	if(c == Integer \|\| c == Long \|\| c == Short) {
	351	return LogicInt
	352	} else if(c == Float \|\| c == Double) {
	353	return LogicReal
	354	} else if(c == Boolean) {
	355	return LogicBool
	356	} else if(c == String) {
	357	return LogicString
	358	} else if(c.superclass == Enum){
	359	val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace)
	360	for(enum : enums) {
	361	if(c == enum.instanceClass) {
	362	return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum))
	363	}
	364	}
	365	throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''')
	366	} else {
	367	return null
	368	}
	369	}
	370	def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
	371	val c = k.wrappedKey
	372
	373	if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
	374	return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
	375	} else {
	376	return null
	377	}
	378	}
	379	def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
	380	val c = k.wrappedKey
	381
	382	if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
	383	return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
	384	} else {
	385	return null
	386	}
	387	}
	388
	389	def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
	390	throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''')
	391	}
	392	} \ No newline at end of file