From b4734ce5b92f00026351748932fb4158617f0da7 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 10 Aug 2018 21:27:34 +0200 Subject: Updated type provider to support java native types --- .../dslreasoner/viatra2logic/Viatra2Logic.xtend | 320 +++++++++++++++------ 1 file changed, 236 insertions(+), 84 deletions(-) (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend index 95ba9219..ce902353 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend @@ -4,20 +4,23 @@ 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.PrimitiveTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor +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.logiclanguage.Variable import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory import java.util.ArrayList import java.util.HashMap +import java.util.HashSet import java.util.LinkedList import java.util.List import java.util.Map import java.util.Set import org.eclipse.emf.ecore.EAttribute -import org.eclipse.emf.ecore.EClass import org.eclipse.emf.ecore.EClassifier import org.eclipse.emf.ecore.EEnum import org.eclipse.emf.ecore.EReference @@ -28,6 +31,9 @@ import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey 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.PBody import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall @@ -37,7 +43,9 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormaliz import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import org.eclipse.viatra.query.runtime.matchers.psystem.TypeJudgement +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey @Data class ViatraQuerySetDescriptor { val List> patterns @@ -45,6 +53,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.TypeJudgement val Map,EStructuralFeature> derivedFeatures } class Viatra2LogicTrace { + public val Map query2Disjunction = new HashMap public val Map query2Relation = new HashMap public val Map query2Annotation = new HashMap public val Map, Variable> parameter2Variable = new HashMap @@ -58,6 +67,8 @@ class Viatra2LogicConfiguration { class Viatra2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE + val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) + val Ecore2Logic ecore2Logic Constraint2Logic constraint2Logic @@ -72,18 +83,44 @@ class Viatra2Logic { Viatra2LogicConfiguration config) { val viatra2LogicTrace = new Viatra2LogicTrace - for(query: queries.patterns) { + val typeAlanysis = new HashMap + val pQueries = queries.patterns.map[it.internalQueryRepresentation] + + for(query: pQueries) { + val disjunction = normalizer.rewrite(query) + viatra2LogicTrace.query2Disjunction.put(query,disjunction) + } + + for(query: pQueries) { + val types = query.lookup(viatra2LogicTrace.query2Disjunction).bodies.toInvertedMap[ + TypeHelper::inferUnaryTypesFor(it.uniqueVariables,it.constraints,EMFQueryMetaContext.DEFAULT) + ] +// for(m : types.values) { +// for(n: m.entrySet) { +// val variable = n.key +// println(''' - «variable.name»''') +// for(type : n.value) { +// println('''«variable.name» - «type»''') +// } +// } +// +// } + + typeAlanysis.put(query,types) + } + + for(query: pQueries) { try { - this.transformQueryHeader(query,ecore2LogicTrace,viatra2LogicTrace,config) + this.transformQueryHeader(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) } catch(IllegalArgumentException e) { throw new IllegalArgumentException(''' Unable to translate query "«query.fullyQualifiedName»". Reason: «e.class.simpleName», «e.message»''',e) } } - for(query: queries.patterns) { + for(query: pQueries) { try { - this.transformQuerySpecification(query,ecore2LogicTrace,viatra2LogicTrace,config) + this.transformQuerySpecification(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) } catch (IllegalArgumentException e){ throw new IllegalArgumentException(''' Unable to translate query "«query.fullyQualifiedName»". @@ -95,31 +132,27 @@ class Viatra2Logic { }*/ transformQueryConstraints( - queries.validationPatterns, + queries.validationPatterns.map[internalQueryRepresentation], queries.derivedFeatures, ecore2LogicTrace,viatra2LogicTrace) return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) } - def protected transformQueryHeader(IQuerySpecification squery, + def protected transformQueryHeader( + PQuery pquery, + Map>> types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) { - val pquery = squery.internalQueryRepresentation - val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' + val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' val parameters = new ArrayList(pquery.parameters.size) for(vParam: pquery.parameters) { - //println(">" + vParam.declaredUnaryType) - val type = vParam.declaredUnaryType as BaseEMFTypeKey - val parameterType = transformTypeReference( - type, - ecore2LogicTrace - ) -// if(parameterType == null) { -// println(parameterType) -// } val parameterName = '''parameter «vParam.name»''' + val parameterType = getType(vParam,types,ecore2LogicTrace) + if(parameterType === null) { + throw new AssertionError('''null type for parameter «vParam.name»''') + } val lParam = createVar(parameterName,parameterType) viatra2LogicTrace.parameter2Variable.put(pquery->vParam,lParam) parameters+=lParam @@ -141,42 +174,37 @@ class Viatra2Logic { } def protected transformQuerySpecification( - IQuerySpecification squery, + PQuery pquery, + Map>> types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) { - val pquery = squery.internalQueryRepresentation - val disjunction = if(config.normalize) { - val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) - normalizer.rewrite(pquery) - } else { - pquery.disjunctBodies - } + val disjunction = pquery.lookup(viatra2LogicTrace.query2Disjunction) + val translatedBodies = new ArrayList(disjunction.bodies.size) for(body : disjunction.bodies) { - translatedBodies+=body.transformBody(ecore2LogicTrace,viatra2LogicTrace,config) + translatedBodies+=body.transformBody(types,ecore2LogicTrace,viatra2LogicTrace,config) } val relation = pquery.lookup(viatra2LogicTrace.query2Relation) relation.value = Or(translatedBodies) } def transformQueryConstraints( - Set> validationPatterns, + Iterable validationPatterns, Map,EStructuralFeature> derivedFeatures, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace) { - for(validationPattern : validationPatterns) { - val pquery = validationPattern.internalQueryRepresentation + for(pquery : validationPatterns) { + val targetRelation = pquery.lookup(viatra2LogicTrace.query2Relation) val constraint = Assertion('''errorpattern «pquery.fullyQualifiedName.replace('.',' ')»''', Forall[ - for(param: pquery.parameters) { - addVar(param.name,transformTypeReference( - param.declaredUnaryType as BaseEMFTypeKey, - ecore2LogicTrace)) + for(param: targetRelation.parameters) { + addVar('''p«targetRelation.parameters.indexOf(param)»''', + EcoreUtil::copy(param)) } - Not(pquery.lookup(viatra2LogicTrace.query2Relation).call(it.variables)) + Not(targetRelation.call(it.variables)) ] ) val annotation = createTransformedViatraWellformednessConstraint => [ @@ -205,6 +233,7 @@ class Viatra2Logic { } def transformBody(PBody body, + Map>> types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) @@ -220,10 +249,11 @@ class Viatra2Logic { val innerPositiveVariables = new LinkedList val innerNegativeVariables = new LinkedList for(innerVariable : body.uniqueVariables) { + if(!variable2Variable.containsKey(innerVariable)) { val name = '''variable «innerVariable.name.normalizeName»''' //println(body.pattern.fullyQualifiedName + "-") - val logicType = getType(innerVariable,body,ecore2LogicTrace) + val logicType = getType(innerVariable,types,ecore2LogicTrace) val logicVariable = createVar(name,logicType) if(innerVariable.isPositiveVariable) { innerPositiveVariables += logicVariable @@ -252,38 +282,47 @@ class Viatra2Logic { return allVariablesAreExisting } +// def toTypeJudgement(PVariable v, IInputKey key) { +// new TypeJudgement(key,new Tuple1) +// } def private normalizeName(String variableName) { return variableName.replaceAll("[\\W]|_", "") } - def TypeDescriptor getType(PVariable v, PBody body, TracedOutput ecore2LogicTrace) { - var Map> unaryTypeRestrictions = null; - if (v.isPositiveVariable) { - unaryTypeRestrictions = body.getAllUnaryTypeRestrictions(EMFQueryMetaContext.DEFAULT) - if (!unaryTypeRestrictions.containsKey(v)) { - throw new IllegalArgumentException('''No positive constraints on variable: «v.name»''') - } - val allTypes = v.lookup(unaryTypeRestrictions) - - val types = allTypes.filter[it.inputKey instanceof BaseEMFTypeKey].toSet - - if (types.size == 0) { - throw new AssertionError(''' - No EMF type for «v.name». - Non-EMF types: [«FOR t : allTypes.filter[!types.contains(it)].map[inputKey.prettyPrintableName] SEPARATOR ','»«t»«ENDFOR»]''') - } else if (types.size == 1) { - return (types.head.inputKey as BaseEMFTypeKey). - transformTypeReference(ecore2LogicTrace) - } else { -// println(''' -// Type Judgements of «v.name» -// «types.map[inputKey.prettyPrintableName]» -// ''') - return this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace, calculateCommonSubtype(types.map [ - (it.inputKey as BaseEMFTypeKey).emfKey as EClass - ], ecore2LogicTrace)) + /** + * Translates the type of a parameter variable in a pattern + */ + def TypeReference getType(PParameter v, Map>> types, TracedOutput ecore2LogicTrace) { + // If parameter type is specified then the specified type is used + if(v.declaredUnaryType !== null) { + return transformTypeReference(v.declaredUnaryType,ecore2LogicTrace) + } + // Otherwise, calculate the type based on the type of the variable in the bodies + else { + val bodies = types.keySet + val typesFromBodies = new ArrayList(bodies.size) + for(body : bodies) { + // collect the variable in the body + val exported = body.symbolicParameters.filter[it.patternParameter === v] + if(exported.size !== 1) { + throw new AssertionError('''Parameter «v.name» has no reference in body!''') + } + val variable = exported.head.parameterVariable + typesFromBodies+=variable.getType(types,ecore2LogicTrace) } + return typesFromBodies.calculateCommonSupertype + } + } + + /** + * Translates the type of a variable in a pattern body + */ + def TypeReference getType(PVariable v, Map>> types ,TracedOutput ecore2LogicTrace) { + if (v.isPositiveVariable) { + val keys = getTypesFromCollection(v,types) + val logicTypes = keys.map[transformTypeReference(it,ecore2LogicTrace)].filterNull + return logicTypes.calculateCommonSubtype } else { val onlyConstraint = v.referringConstraints.head as NegativePatternCall val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) @@ -295,42 +334,155 @@ class Viatra2Logic { } else return declaredUnaryType.transformTypeReference(ecore2LogicTrace) } - } - def calculateCommonSubtype(Iterable allsuperClasses,TracedOutput ecore2LogicTrace) { - val superClasses = allsuperClasses.filter[it!=EcorePackage.eINSTANCE.EObject] - val head = superClasses.head - if(superClasses.forall[it.isSuperTypeOf(head)]) return head - else { - val allClasses = this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace) - //println(allClasses.toList) - val commonSubclasses = allClasses.filter[sub | superClasses.forall[sup | sup.isSuperTypeOf(sub)]] - //println(commonSubclasses.toList) - val mostGenericSubclasses = commonSubclasses.filter[generic | ! commonSubclasses.exists[moreGeneric | moreGeneric!=generic && moreGeneric.isSuperTypeOf(generic)]] - //println(mostGenericSubclasses.toList) - if(mostGenericSubclasses.isEmpty) throw new AssertionError('''No common supertype: - «FOR s : superClasses SEPARATOR ", "»«s.name»«ENDFOR»''') - else return mostGenericSubclasses.head + def getTypesFromCollection(PVariable v, Map>> types) { + for(entry : types.entrySet) { + if(entry.key.uniqueVariables.contains(v)) { + return v.lookup(entry.value) + } + } + throw new IllegalArgumentException('''Variable «v.name» is not present in neither of the bodies!''') + } + + + def TypeReference calculateCommonSubtype(Iterable types) { + val primitiveTypeReferences = types.filter(PrimitiveTypeReference) + val complexTypeReferences = types.filter(ComplexTypeReference) + if(complexTypeReferences.isEmpty) { + 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 types) { + val primitiveTypeReferences = types.filter(PrimitiveTypeReference) + val complexTypeReferences = types.filter(ComplexTypeReference) + if(complexTypeReferences.isEmpty) { + 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 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) + } - def dispatch transformTypeReference(EDataTypeInSlotsKey k,TracedOutput ecore2LogicTrace) { + /** + * Transforms a Viatra type reference to a logic type. + */ + def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput ecore2LogicTrace) { val w = k.wrappedKey - if(w == EcorePackage.Literals.EINT) { + 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) { - this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w); + 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 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.superclass == java.lang.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!''') + } + return null + } + def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput 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 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 transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput ecore2LogicTrace) { - this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey) + def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput ecore2LogicTrace) { + println(k) + throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''') } def boolean isPositiveVariable(PVariable v) { -- cgit v1.2.3-54-g00ecf