From 539618ccaedfe05d5d62971c8fd0578f5ff3d040 Mon Sep 17 00:00:00 2001 From: Oszkar Semerath Date: Mon, 15 Jul 2019 17:31:00 +0200 Subject: parsing count, min, max, check and eval v1 --- .../viatra2logic/Constraint2Logic.xtend | 69 ++++ .../viatra2logic/ExpressionEvaluation2Logic.xtend | 132 +++++++ .../dslreasoner/viatra2logic/Viatra2Logic.xtend | 328 ++++------------- .../viatra2logic/Viatra2LogicTypeInferer.xtend | 392 +++++++++++++++++++++ .../viatra2logic/Viatra2LogicTypeResult.xtend | 47 +++ .../viatra2logic/XExpressionExtractor.xtend | 24 ++ 6 files changed, 727 insertions(+), 265 deletions(-) create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend index 3e8b3366..ffbca0af 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend @@ -30,10 +30,20 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint +import org.eclipse.viatra.query.runtime.matchers.aggregators.DoubleSumOperator +import org.eclipse.viatra.query.runtime.matchers.aggregators.IntegerSumOperator +import org.eclipse.viatra.query.runtime.matchers.aggregators.LongSumOperator +import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator +import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator.Extreme +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation class Constraint2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder val Ecore2Logic ecore2Logic + val ExpressionEvaluation2Logic expressionEvaliation2Logic = new ExpressionEvaluation2Logic + val expressionExtractor = new XExpressionExtractor new(Ecore2Logic ecore2Logic) { this.ecore2Logic = ecore2Logic @@ -269,6 +279,65 @@ class Constraint2Logic { } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') } + def dispatch Term transformConstraint(AggregatorConstraint constraint, + TracedOutput ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation) + val parameterSubstitution = new LinkedList + for(index : 0.. ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation) + val parameterSubstitution = new LinkedList + for(index : 0.. ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Map variable2Variable, + Viatra2LogicConfiguration config) + { + val outputVariable = constraint.outputVariable + val expression = expressionExtractor.extractExpression(constraint.evaluator) + return expressionEvaliation2Logic.transformEval(outputVariable,expression,variable2Variable) + } + def dispatch Term transformConstraint(PConstraint constraint, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend new file mode 100644 index 00000000..f474ded4 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -0,0 +1,132 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable +import org.eclipse.xtext.xbase.XBinaryOperation +import org.eclipse.xtext.xbase.XExpression +import org.eclipse.xtext.xbase.XFeatureCall +import org.eclipse.xtext.xbase.XMemberFeatureCall +import org.eclipse.xtext.xbase.XNumberLiteral +import org.eclipse.xtext.xbase.XUnaryOperation + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class ExpressionEvaluation2Logic { + val extension LogicProblemBuilder builder = new LogicProblemBuilder + + def Term transformCheck(XExpression expression, Map variable2Variable) { + return expression.transform(variable2Variable) + } + def Term transformEval(PVariable target, XExpression expression, Map variable2Variable) { + return target.lookup(variable2Variable) == expression.transform(variable2Variable) + } + + static val N_Base = "org.eclipse.xtext.xbase.lib." + + static val N_PLUS1 = "operator_plus" + static val N_MINUS1 = "operator_minus" + + static val N_MINUS2 = "operator_minus" + static val N_PLUS2 = "operator_plus" + static val N_POWER = "operator_power" + static val N_MULTIPLY = "operator_multiply" + static val N_DIVIDE = "operator_divide" + static val N_MODULO = "operator_modulo" + static val N_LESSTHAN = "operator_lessThan" + static val N_LESSEQUALSTHAN = "operator_lessEqualsThan" + static val N_GREATERTHAN = "operator_greaterThan" + static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan" + static val N_EQUALS = "operator_equals" + static val N_NOTEQUALS = "operator_notEquals" + static val N_EQUALS3 = "operator_tripleEquals" + static val N_NOTEQUALS3 = "operator_tripleNotEquals" + + + + protected def isN(String name, String s) { + val res = name.startsWith(N_Base) && name.endsWith(s) + //println('''[«res»] «name» ?= «N_Base»*«s»''') + return res + } + + static val N_POWER2 = "java.lang.Math.pow" + + def protected dispatch Term transform(XBinaryOperation e, Map variable2Variable) { + val left = e.leftOperand.transform(variable2Variable) + val right = e.rightOperand.transform(variable2Variable) + val feature = e.feature.qualifiedName + if(feature.isN(N_MINUS2)) { return Minus(left,right) } + else if(feature.isN(N_PLUS2)) { return Plus(left,right) } + else if(feature.isN(N_POWER)) { return Pow(left,right) } + else if(feature.isN(N_MULTIPLY)) { return Multiply(left,right) } + else if(feature.isN(N_DIVIDE)) { return Divide(left,right) } + else if(feature.isN(N_MODULO)) { return Modulo(left,right) } + else if(feature.isN(N_LESSTHAN)) { return LessThan(left,right) } + else if(feature.isN(N_LESSEQUALSTHAN)) { return LessOrEqual(left,right) } + else if(feature.isN(N_GREATERTHAN)) { return MoreThan(left,right) } + else if(feature.isN(N_GREATEREQUALTHAN)) { return MoreOrEqual(left,right) } + else if(feature.isN(N_EQUALS)) { return Equals(left,right) } + else if(feature.isN(N_NOTEQUALS)) { return Distinct(left,right) } + else if(feature.isN(N_EQUALS3)) { return Equals(left,right) } + else if(feature.isN(N_NOTEQUALS3)) { return Distinct(left,right) } + else { + println("-> " + e.feature+","+e.class) + println("-> " + e.leftOperand) + println("-> " + e.rightOperand) + println("-> " + e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''') + } + } + + def protected dispatch Term transform(XUnaryOperation e, Map variable2Variable) { + val operand = e.operand.transform(variable2Variable) + val feature = e.feature.qualifiedName + if(feature.isN(N_MINUS1)) { return Minus(0.asTerm,operand)} + else if(feature.isN(N_PLUS1)) { return operand} + else{ + println("-> " + e.feature+","+e.class) + println("-> " + e.operand) + println("-> " + e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''') + } + } + + def protected dispatch Term transform(XMemberFeatureCall e, Map variable2Variable) { + val transformedArguments = e.actualArguments.map[transform(variable2Variable)] + val feature = e.feature.qualifiedName + if(feature == N_POWER2) { + return Pow(transformedArguments.get(0),transformedArguments.get(1)) + }else { + println(e.feature+","+e.class) + println(e.actualArguments.join(", ")) + println(e.feature.qualifiedName) + throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''') + } + } + + def protected dispatch Term transform(XFeatureCall e, Map variable2Variable) { + val featureName = e.feature.qualifiedName + val entryWithName = variable2Variable.entrySet.filter[it.key.name == featureName].head + if(entryWithName !== null) { + return entryWithName.value.toTerm + } else { + throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') + } + } + + def protected dispatch Term transform(XNumberLiteral l, Map variable2Variable) { + val s = l.value + try{ return Integer.parseInt(s).asTerm } catch(NumberFormatException e){} + try{ return Short.parseShort(s).asTerm } catch(NumberFormatException e){} + try{ return Double.parseDouble(s).asTerm } catch(NumberFormatException e){} + try{ return Float.parseFloat(s).asTerm } catch(NumberFormatException e){} + throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''') + } + + def protected dispatch Term transform(XExpression e, Map variable2Variable) { + throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''') + } +} \ No newline at end of file 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 3b828170..0f97d3fe 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,48 +4,36 @@ 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.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.EClassifier -import org.eclipse.emf.ecore.EEnum import org.eclipse.emf.ecore.EReference import org.eclipse.emf.ecore.EStructuralFeature -import org.eclipse.emf.ecore.EcorePackage +import org.eclipse.emf.ecore.util.EcoreUtil import org.eclipse.viatra.query.runtime.api.IQuerySpecification 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.PConstraint 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.NegativePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer 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.queries.PDisjunction -import org.eclipse.emf.ecore.util.EcoreUtil -import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey @Data class ViatraQuerySetDescriptor { val List> patterns @@ -57,24 +45,24 @@ class Viatra2LogicTrace { public val Map query2Relation = new HashMap public val Map query2Annotation = new HashMap public val Map, Variable> parameter2Variable = new HashMap - //public val Map variable2Variable = new HashMap } class Viatra2LogicConfiguration { public var normalize = true - public var transitiveClosureDepth = 3 } class Viatra2Logic { val extension LogicProblemBuilder builder = new LogicProblemBuilder val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) + val Viatra2LogicTypeInferer typeInferer val Ecore2Logic ecore2Logic Constraint2Logic constraint2Logic new(Ecore2Logic ecore2Logic) { this.ecore2Logic = ecore2Logic - constraint2Logic = new Constraint2Logic(ecore2Logic) + this.typeInferer = new Viatra2LogicTypeInferer(ecore2Logic) + this.constraint2Logic = new Constraint2Logic(ecore2Logic) } def TracedOutput transformQueries( @@ -82,65 +70,55 @@ class Viatra2Logic { TracedOutput ecore2LogicTrace, Viatra2LogicConfiguration config) { + // Create trace val viatra2LogicTrace = new Viatra2LogicTrace - val typeAlanysis = new HashMap + + // Translation works on PQueries. QuerySpecification -> PQuery. val pQueries = queries.patterns.map[it.internalQueryRepresentation] - for(query: pQueries) { - val disjunction = normalizer.rewrite(query) + // If requested, the queries are normalized + 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) - } + // The types are calculated + val types = typeInferer.inferTypes(pQueries,ecore2LogicTrace,viatra2LogicTrace) + // First, the signature of the queries are translated, ... for(query: pQueries) { try { - this.transformQueryHeader(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) + this.transformQueryHeader(query,types,ecore2LogicTrace,viatra2LogicTrace,config) } catch(IllegalArgumentException e) { throw new IllegalArgumentException(''' Unable to translate query "«query.fullyQualifiedName»". Reason: «e.class.simpleName», «e.message»''',e) } } + + // ...then the bodies, ... for(query: pQueries) { try { - this.transformQuerySpecification(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) + this.transformQuerySpecification(query,types,ecore2LogicTrace,viatra2LogicTrace,config) } catch (IllegalArgumentException e){ throw new IllegalArgumentException(''' Unable to translate query "«query.fullyQualifiedName»". Reason: «e.class.simpleName», «e.message»''',e) } } - /*for(d : viatra2LogicTrace.query2Relation.values) { - checkDefinition(d) - }*/ + // ... and finally, the annotations. transformQueryConstraints( queries.validationPatterns.map[internalQueryRepresentation], queries.derivedFeatures, ecore2LogicTrace,viatra2LogicTrace) + return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) } def protected transformQueryHeader( PQuery pquery, - Map>> types, + Viatra2LogicTypeResult types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) @@ -149,7 +127,7 @@ class Viatra2Logic { val parameters = new ArrayList(pquery.parameters.size) for(vParam: pquery.parameters) { val parameterName = '''parameter «vParam.name»''' - val parameterType = getType(vParam,types,ecore2LogicTrace) + val parameterType = types.getType(pquery,vParam) if(parameterType === null) { throw new AssertionError('''null type for parameter «vParam.name» in pattern «pquery.fullyQualifiedName»''') } @@ -175,7 +153,7 @@ class Viatra2Logic { def protected transformQuerySpecification( PQuery pquery, - Map>> types, + Viatra2LogicTypeResult types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) @@ -233,7 +211,7 @@ class Viatra2Logic { } def transformBody(PBody body, - Map>> types, + Viatra2LogicTypeResult types, TracedOutput ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace, Viatra2LogicConfiguration config) @@ -248,19 +226,29 @@ class Viatra2Logic { // Inner Variables val innerPositiveVariables = new LinkedList val innerNegativeVariables = new LinkedList + val innerAggreatedVariables = new LinkedList + //println(body.uniqueVariables) for(innerVariable : body.uniqueVariables) { if(!variable2Variable.containsKey(innerVariable)) { - val name = '''variable «innerVariable.name.normalizeName»''' - //println(body.pattern.fullyQualifiedName + "-") - val logicType = getType(innerVariable,types,ecore2LogicTrace) - val logicVariable = createVar(name,logicType) - if(innerVariable.isPositiveVariable) { - innerPositiveVariables += logicVariable + if(innerVariable.aggregateOnly) { + // do not create variable + innerAggreatedVariables.add(innerVariable) + variable2Variable.put(innerVariable,null) } else { - innerNegativeVariables += logicVariable + val name = '''variable «innerVariable.name.normalizeName»''' + val logicType = types.getType(body,innerVariable) + if(logicType === null) { + throw new IllegalArgumentException('''Variable «innerVariable.name.normalizeName» has no type!''') + } + val logicVariable = createVar(name,logicType) + if(innerVariable.negativeOnly) { + innerNegativeVariables += logicVariable + } else { + innerPositiveVariables += logicVariable + } + variable2Variable.put(innerVariable,logicVariable) } - variable2Variable.put(innerVariable,logicVariable) } } @@ -282,226 +270,36 @@ class Viatra2Logic { return allVariablesAreExisting } -// def toTypeJudgement(PVariable v, IInputKey key) { -// new TypeJudgement(key,new Tuple1) -// } def private normalizeName(String variableName) { return variableName.replaceAll("[\\W]|_", "") } - - /** - * 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) { - val res = transformTypeReference(v.declaredUnaryType,ecore2LogicTrace) - if(res === null) { - throw new AssertionError(''' - Unable to translate declared type «v.declaredUnaryType». - ''') - } else { - return res - } - } - // 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) - val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable) - val declaredUnaryType = parameter.declaredUnaryType as BaseEMFTypeKey - if (declaredUnaryType === null) { - throw new UnsupportedOperationException( - '''parameter «parameter.name» in pattern «onlyConstraint.referredQuery.fullyQualifiedName» does not have type!''') - } else - return declaredUnaryType.transformTypeReference(ecore2LogicTrace) - } - } - - 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) - } - - /** - * 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 || 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 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 == java.lang.Enum){ - val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace) - for(enum : enums) { - if(c == enum.instanceClass) { - return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum)) - } + def isNegativeOnly(PVariable variable) { + if(variable.referringConstraints.size == 1) { + val PConstraint onlyConstraint = variable.referringConstraints.head + if(onlyConstraint instanceof NegativePatternCall) { + return true + } else { + return false } - 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 + return false } } - 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 TypeReference transformTypeReference(IInputKey k,TracedOutput ecore2LogicTrace) { - //println(k) - throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''') - } - def boolean isPositiveVariable(PVariable v) { - val constraints = v.referringConstraints - if(constraints.size == 1) { - val onlyConstraint = constraints.head - if(onlyConstraint instanceof NegativePatternCall) { + def isAggregateOnly(PVariable variable) { + if(variable.referringConstraints.size == 1) { + val PConstraint onlyConstraint = variable.referringConstraints.head + if(onlyConstraint instanceof AggregatorConstraint) { + return true + } else if(onlyConstraint instanceof PatternMatchCounter) { + return true + } else { return false } + } else { + return false } - return true } } \ 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 @@ +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 pQueries, TracedOutput 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 ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Set 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 ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Set 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 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 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 ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Set 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 ecore2LogicTrace, + Viatra2LogicTrace viatra2LogicTrace, + Set 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 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 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 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 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 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 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 TypeReference transformTypeReference(IInputKey k,TracedOutput 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/Viatra2LogicTypeResult.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend new file mode 100644 index 00000000..7ba90724 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend @@ -0,0 +1,47 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import java.util.Map +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.queries.PParameter +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtext.xbase.lib.Functions.Function0 +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import org.eclipse.emf.ecore.util.EcoreUtil +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference + +@Data class Viatra2LogicTypeResult{ + Map,Function0> typesInParameters + Map,Function0> typesInBodies; + + def addType(PBody body, PVariable variable, TypeReference typeConstructor) { + typesInBodies.put(body->variable,typeConstructor.createTypeConstructor) + } + def addType(PQuery query, PParameter variable, TypeReference typeConstructor) { + typesInParameters.put(query->variable,typeConstructor.createTypeConstructor) + } + def getType(PBody body, PVariable variable) { + return (body->variable).lookup(typesInBodies).apply + } + def getType(PQuery query, PParameter variable) { + return (query->variable).lookup(typesInParameters).apply + } + + def containsSolution(PBody body, PVariable variable) { + return typesInBodies.containsKey(body->variable) + } + def containsSolution(PParameter variable) { + return typesInParameters.containsKey(variable) + } + + def dispatch Function0 createTypeConstructor(ComplexTypeReference ref) { + return [LogiclanguageFactory.eINSTANCE.createComplexTypeReference=>[it.referred = ref.referred]] + } + def dispatch Function0 createTypeConstructor(PrimitiveTypeReference ref) { + return [EcoreUtil.copy(ref)] + } +} \ No newline at end of file diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend new file mode 100644 index 00000000..ea8d0b23 --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend @@ -0,0 +1,24 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic + +import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator +import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator +import org.eclipse.xtext.xbase.XExpression + +class XExpressionExtractor { + def dispatch XExpression extractExpression(XBaseEvaluator evaluator) { evaluator.expression } + def dispatch XExpression extractExpression(IExpressionEvaluator evaluator) { + val clazz = evaluator.class + if(clazz.name == "org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.VariableMappingExpressionEvaluatorWrapper") { + val field = clazz.declaredFields.filter[it.name == "wrapped"].head + if(field === null) { + throw new IllegalArgumentException('''Class «clazz.simpleName» has no field "wrapped"!''') + } else { + field.setAccessible(true); + val wrappedEvaluator = field.get(evaluator) as XBaseEvaluator + return wrappedEvaluator.extractExpression + } + } else { + throw new IllegalArgumentException('''Unsupported expression evaluation form: «clazz.simpleName»!''') + } + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf